→
Seminar

Program = demonstrate ? Curry-Howard correspondence today

→
    from to
    See also:

    Documents and media

    Program

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

    -
    Lecture
    Program = demonstrate ? Curry-Howard correspondence today
    Amphithéâtre Guillaume Budé, Site Marcelin Berthelot
    -

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

    -
    Lecture
    Program = demonstrate ? Curry-Howard correspondence today
    Amphithéâtre Guillaume Budé, Site Marcelin Berthelot
    -

    Weapons of mass construction : inductive types and inductive predicates
    Xavier Leroy

    -
    Lecture
    Program = demonstrate ? Curry-Howard correspondence today
    Amphithéâtre Guillaume Budé, Site Marcelin Berthelot
    -

    Dependent types : a whole program !
    Pierre-Évariste Dagand

    -
    Seminar
    Program = demonstrate ? Curry-Howard correspondence today
    Amphithéâtre Guillaume Budé, Site Marcelin Berthelot
    -

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

    -
    Lecture
    Program = demonstrate ? Curry-Howard correspondence today
    Amphithéâtre Guillaume Budé, Site Marcelin Berthelot
    -

    Computer-aided mathematics
    Assia Mahboubi

    -
    Seminar
    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

    -
    Lecture
    Program = demonstrate ? Curry-Howard correspondence today
    Amphithéâtre Guillaume Budé, Site Marcelin Berthelot
    -

    Programming with Coq : recursion and dependent filtering
    Matthieu Sozeau

    -
    Seminar
    Program = demonstrate ? Curry-Howard correspondence today
    Amphithéâtre Guillaume Budé, Site Marcelin Berthelot
    -

    Free theorems : parametricity
    Xavier Leroy

    -
    Lecture
    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

    -
    Seminar
    Program = demonstrate ? Curry-Howard correspondence today
    Amphithéâtre Guillaume Budé, Site Marcelin Berthelot
    -

    Forcing, a program transformation like any other ?
    Xavier Leroy

    -
    Lecture
    Program = demonstrate ? Curry-Howard correspondence today
    Amphithéâtre Guillaume Budé, Site Marcelin Berthelot
    -

    Step by step : step-indexing techniques
    Xavier Leroy

    -
    Lecture
    Program = demonstrate ? Curry-Howard correspondence today
    Amphithéâtre Guillaume Budé, Site Marcelin Berthelot
    -

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

    -
    Lecture
    Program = demonstrate ? Curry-Howard correspondence today
    Amphithéâtre Guillaume Budé, Site Marcelin Berthelot
    -

    Realisability and forcing
    Alexandre Miquel

    -
    Seminar
    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

    -
    Lecture
    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

    -
    Seminar
    Program = demonstrate ? Curry-Howard correspondence today
    Amphithéâtre Guillaume Budé, Site Marcelin Berthelot
    -

    From construction calculus to the theory of univalent types
    Thierry Coquand

    -
    Seminar
    Program = demonstrate ? Curry-Howard correspondence today
    Amphithéâtre Guillaume Budé, Site Marcelin Berthelot
    -

    Conclusion, discussion and answers to the year's questions
    Xavier Leroy

    -
    Lecture
    Program = demonstrate ? Curry-Howard correspondence today
    Amphithéâtre Guillaume Budé, Site Marcelin Berthelot
    -

    See also

    Lecture related to the seminar: Program = demonstrate ? Curry-Howard correspondence today
    Xavier Leroy, chair Software Science