Registration
This shows you the differences between two versions of the page.
|
lectures [2014/05/25 16:36] mellies |
lectures [2014/06/20 09:06] (current) mellies |
||
|---|---|---|---|
| Line 27: | Line 27: | ||
| |14h00-15h00|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| | + | |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 67: | 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 75: | 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. | ||
| - | |||