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:08]
mellies
lectures [2014/06/20 09:06] (current)
mellies
Line 22: Line 22:
 ^Monday 26 May||| ^Monday 26 May|||
 |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|||
 +|14h00-15h00|Bruno Vallette| Théorie de la déformation des algèbres de Batalin—Vilkovisky |
 ^Wednesday 28 May||| ^Wednesday 28 May|||
-|17h00-18h00|Bruno Vallette| +|14h00-15h00|Bruno Vallette| ​Théorie de la déformation des algèbres de Batalin—Vilkovisky ​|
-^Friday 30 May||| +
-|17h00-18h00|Bruno Vallette|+
 ^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 67: Line 67:
 > 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.
  
-**Bruno Vallette (Université Nice Sophia Antipolis)**// +**Olivier Serre**\\ 
-//Théorie de la déformation des algèbres de Batalin—Vilkovisky//+//Tree Automata, Logic and Verification of (Higher-Order-) Functional Programs//
  
->La notion d’algèbre de Batalin—Vilkovisky est assez élémentaire : algèbre commutative munie d’un opérateur différentiel d’ordre 2 et de carré nul. Elle apparait aujourd’hui en algèbre ​(algèbres vertex), géométrie (variétés de Frobenius), topologie (topologie des cordes) et physique mathématique (renormalisation). +>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
  
->Le but de ces exposés sera d’établir la théorie de la déformation des algèbres de Batalin—Vilkovisky ​(BV). Pour cela, nous aurons besoin de plusieurs outils, que nous rappellerons : une opérade qui code la catégorie de algèbres BV, une bonne résolution de cette opérade ​(la résolution de Koszul et le modèle minimal), et enfin, une algèbre de Lie qui code les déformations de structures d’algèbres BV+>In a second part we will explain how a higher-order recursion scheme ​(a kind of term rewriting systemcan be used to model the behaviour of a higher-order functional program by generating ​(assuming some restriction on the programits syntax tree
  
->Au finalcette théorie permettra de résoudre plusieurs conjectures ​celle de Lian—Zuckerman sur les algèbres ​vertex ​et celles ​de Kontsevich sur laction du groupe ​de Giventalpar exemple+>Finally we will combine these two conceptsautomata/​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. 
 + 
 +> Notethe 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)**\\ 
 +//​Théorie ​de la déformation des algèbres ​de Batalin—Vilkovisky//​ 
 +> La notion d’algèbre de Batalin—Vilkovisky est assez élémentaire : algèbre commutative munie d’un opérateur différentiel d’ordre 2 et de carré nul. Elle apparait aujourdhui en algèbre (algèbres vertex), géométrie (variétés ​de Frobenius)topologie (topologie des cordes) et physique mathématique (renormalisation)
  
 +> Le but de ces exposés sera d’établir la théorie de la déformation des algèbres de Batalin—Vilkovisky (BV). Pour cela, nous aurons besoin de plusieurs outils, que nous rappellerons : une opérade qui code la catégorie de algèbres BV, une bonne résolution de cette opérade (la résolution de Koszul et le modèle minimal), et enfin, une algèbre de Lie qui code les déformations de structures d’algèbres BV. 
  
 +> 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.1400702933.txt.gz · Last modified: 2014/05/21 22:08 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