Dieses Dokuwiki verwendet ein von Anymorphic Webdesign erstelltes Thema.

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

lectures [2014/05/21 22:11]
mellies
lectures [2014/06/20 09:06] (current)
mellies
Line 23: Line 23:
 |17h00-18h00|Timothy Gowers| Fully automatic problem solving with human-style output | |17h00-18h00|Timothy Gowers| Fully automatic problem solving with human-style output |
 ^Tuesday 27 May||| ^Tuesday 27 May|||
-|16h30-17h30|Bruno Vallette| Théorie de la déformation des algèbres de Batalin—Vilkovisky |+|14h00-15h00|Bruno Vallette| Théorie de la déformation des algèbres de Batalin—Vilkovisky |
 ^Wednesday 28 May||| ^Wednesday 28 May|||
-|16h30-17h30|Bruno Vallette| Théorie de la déformation des algèbres de Batalin—Vilkovisky |+|14h00-15h00|Bruno Vallette| Théorie de la déformation des algèbres de Batalin—Vilkovisky |
 ^Monday 16 June||| ^Monday 16 June|||
-|11h00-12h30|Olivier Serre|+|11h00-12h30|Olivier Serre| Tree Automata, Logic and Verification of (Higher-Order-) Functional Programs [[http://​www.pps.univ-paris-diderot.fr/​~mellies/​IHP-Serre-Mini-Course-Part1.pdf|slides of the first lecture]]|
 ^Wednesday 18 June||| ^Wednesday 18 June|||
-|11h00-12h30|Olivier Serre|+|10h30-12h00|Olivier Serre| Tree Automata, Logic and Verification of (Higher-Order-) Functional Programs [[http://​www.pps.univ-paris-diderot.fr/​~mellies/​IHP-Serre-Mini-Course-Part2.pdf|slides of the second lecture]] ​|
 ^Thursday 19 June||| ^Thursday 19 June|||
-|10h30-12h00|Marc Pouzet| +|10h30-12h00|Marc Pouzet| ​Synchronous Languages and their extension to mix discrete and continuous time [[http://​www.pps.univ-paris-diderot.fr/​~mellies/​IHP-Pouzet-Mini-Course-Part1A.pdf|slides of the first lecture part A]][[http://​www.pps.univ-paris-diderot.fr/​~mellies/​IHP-Pouzet-Mini-Course-Part1B.pdf|slides of the first lecture part B]]|
-|14h00-15h00|Martin Hyland|+
 ^Friday 20 June||| ^Friday 20 June|||
-|10h30-12h|Marc Pouzet|+|10h30-12h|Marc Pouzet| Synchronous Languages and their extension to mix discrete and continuous time| 
 +|14h00-15h00|Thomas Streicher| A Model of Control Operators in Coherence Spaces giving rise to a New Model of Classical Set Theory ​|
 ===== Abstracts ===== ===== Abstracts =====
  
Line 66: Line 66:
 //The practice and theory of Mezzo// //The practice and theory of Mezzo//
 > The programming language Mezzo is a member of the ML family, from whom it inherits algebraic data types, first-class functions, and automatic memory management. It is equipped with a rich type system that controls aliasing and access to mutable memory. This static discipline rules out certain programming mistakes, guarantees data race freedom, and opens up some new possibilities,​ such as gradual initialization and type(state) changes. In the first lecture, I will present Mezzo via a series of examples. In the second lecture, I would like to present the meta-theory of Mezzo. It is organized in a modular manner and has been machine-checked in Coq. > The programming language Mezzo is a member of the ML family, from whom it inherits algebraic data types, first-class functions, and automatic memory management. It is equipped with a rich type system that controls aliasing and access to mutable memory. This static discipline rules out certain programming mistakes, guarantees data race freedom, and opens up some new possibilities,​ such as gradual initialization and type(state) changes. In the first lecture, I will present Mezzo via a series of examples. In the second lecture, I would like to present the meta-theory of Mezzo. It is organized in a modular manner and has been machine-checked in Coq.
 +
 +**Olivier Serre**\\
 +//Tree Automata, Logic and Verification of (Higher-Order-) Functional Programs//
 +
 +>The first goal of these two lectures is to introduce the audience with tree automata and their connections with model checking of various logic (with a special focus on monadic second order logic). In particular we will explain why these two formalisms are equi-expressive when describing sets of trees. ​
 +
 +>In a second part we will explain how a higher-order recursion scheme (a kind of term rewriting system) can be used to model the behaviour of a higher-order functional program by generating (assuming some restriction on the program) its syntax tree. 
 +
 +>Finally we will combine these two concepts, automata/​logic and higher-order recursion schemes, and argue that they can successfully be used to solve important questions related to verification of programs, in particular the model-checking problem (both local and global) as well as the synthesis problem.
 +
 +> Note: the slides of the two lectures are available [[http://​www.pps.univ-paris-diderot.fr/​~mellies/​IHP-Serre-Mini-Course-Part1.pdf|here]] and [[http://​www.pps.univ-paris-diderot.fr/​~mellies/​IHP-Serre-Mini-Course-Part2.pdf|here]].
  
 **Bruno Vallette (Université Nice Sophia Antipolis)**\\ **Bruno Vallette (Université Nice Sophia Antipolis)**\\
Line 74: Line 85:
  
 > Au final, cette théorie permettra de résoudre plusieurs conjectures : celle de Lian—Zuckerman sur les algèbres vertex et celles de Kontsevich sur l’action du groupe de Givental, par exemple. ​ > Au final, cette théorie permettra de résoudre plusieurs conjectures : celle de Lian—Zuckerman sur les algèbres vertex et celles de Kontsevich sur l’action du groupe de Givental, par exemple. ​
- 
lectures.1400703090.txt.gz · Last modified: 2014/05/21 22:11 by mellies
Dieses Dokuwiki verwendet ein von Anymorphic Webdesign erstelltes Thema.
www.chimeric.de Valid CSS Driven by DokuWiki do yourself a favour and use a real browser - get firefox!! Recent changes RSS feed Valid XHTML 1.0