Program = demonstrate ? Curry-Howard correspondence today

Documents and media

Download program

pdf (366.45 KB)

Program

Lecture

10:00 - 11:00

A door must be opened or closed ! Classical logic, continuations, control operators

Xavier Leroy

05 Dec 2018

Program = demonstrate ? Curry-Howard correspondence today

Amphithéâtre Guillaume Budé, Site Marcelin Berthelot

Computer-aided mathematics

Assia Mahboubi

05 Dec 2018

Program = demonstrate ? Curry-Howard correspondence today

Amphithéâtre Guillaume Budé, Site Marcelin Berthelot

Can we change the world ? Imperative programming, monadic effects, algebraic effects

Xavier Leroy

12 Dec 2018

Program = demonstrate ? Curry-Howard correspondence today

Amphithéâtre Guillaume Budé, Site Marcelin Berthelot

Programming with Coq : recursion and dependent filtering

Matthieu Sozeau

12 Dec 2018

Program = demonstrate ? Curry-Howard correspondence today

Amphithéâtre Guillaume Budé, Site Marcelin Berthelot

Free theorems : parametricity

Xavier Leroy

19 Dec 2018

Program = demonstrate ? Curry-Howard correspondence today

Amphithéâtre Guillaume Budé, Site Marcelin Berthelot

Can you duplicate an object ? Linearity and resource control

Guillaume Munch-Maccagnoni

19 Dec 2018

Program = demonstrate ? Curry-Howard correspondence today

Amphithéâtre Guillaume Budé, Site Marcelin Berthelot

Forcing, a program transformation like any other ?

Xavier Leroy

09 Jan 2019

Program = demonstrate ? Curry-Howard correspondence today

Amphithéâtre Guillaume Budé, Site Marcelin Berthelot

Step by step : step-indexing techniques

Xavier Leroy

09 Jan 2019

Program = demonstrate ? Curry-Howard correspondence today

Amphithéâtre Guillaume Budé, Site Marcelin Berthelot

Happy Sisyphus : infinite types, coinduction demonstrations, and reactive programming

Xavier Leroy

16 Jan 2019

Program = demonstrate ? Curry-Howard correspondence today

Amphithéâtre Guillaume Budé, Site Marcelin Berthelot

Realisability and forcing

Alexandre Miquel

16 Jan 2019

Program = demonstrate ? Curry-Howard correspondence today

Amphithéâtre Guillaume Budé, Site Marcelin Berthelot

What is equality From Leibniz to the homotopic theory of types

Xavier Leroy

23 Jan 2019

Program = demonstrate ? Curry-Howard correspondence today

Amphithéâtre Guillaume Budé, Site Marcelin Berthelot

Semantics of probabilistic functional programs in the light of linear logic

Christine Tasson

23 Jan 2019

Program = demonstrate ? Curry-Howard correspondence today

Amphithéâtre Guillaume Budé, Site Marcelin Berthelot

From construction calculus to the theory of univalent types

Thierry Coquand

30 Jan 2019

Program = demonstrate ? Curry-Howard correspondence today

Amphithéâtre Guillaume Budé, Site Marcelin Berthelot

Conclusion, discussion and answers to the year's questions

Xavier Leroy

30 Jan 2019

Program = demonstrate ? Curry-Howard correspondence today

Amphithéâtre Guillaume Budé, Site Marcelin Berthelot

30 Jan 2019

11:30 - 12:30

Program = demonstrate ? Curry-Howard correspondence today

Documents and media

Program

Paths to discovery : the Curry-Howard correspondence, 1930-1970

Polymorphism on all levels ! From the F system to calculating constructions

Weapons of mass construction : inductive types and inductive predicates

Dependent types : a whole program !

A door must be opened or closed ! Classical logic, continuations, control operators

Computer-aided mathematics

Can we change the world ? Imperative programming, monadic effects, algebraic effects

Programming with Coq : recursion and dependent filtering

Free theorems : parametricity

Can you duplicate an object ? Linearity and resource control

Forcing, a program transformation like any other ?

Step by step : step-indexing techniques

Happy Sisyphus : infinite types, coinduction demonstrations, and reactive programming

Realisability and forcing

What is equality From Leibniz to the homotopic theory of types

Semantics of probabilistic functional programs in the light of linear logic

From construction calculus to the theory of univalent types

Conclusion, discussion and answers to the year's questions

See also