10:00 to 11:00
Lecture

Modalities and models of type theory

Thierry Coquand
Dependent type theory and mathematical formalization
10:00 to 11:00
    Mireille-Delmas-Marty Amphitheater, Marcelin-Berthelot Site
    Open to all, subject to availability
    -

    Lecture outline:

    • exact modalities left;
    • application to the construction of new type-theoretic models;
    • unprovability of Church's thesis and countable choice;
    • Quillen model structure and constructive model of the notion of homotopy types.

    Documents and media

    Speaker(s)

    Thierry Coquand

    Professor of Computer Science, University of Gothenburg, Sweden

    Events

    Type theory, from Russell to de Bruijn
    Thierry Coquand

    Lecture
    10:00 to 11:00

    Natural deduction and models
    Thierry Coquand

    Lecture
    10:00 to 11:00

    Universe, paradoxes and standardization
    Thierry Coquand

    Lecture
    10:00 to 11:00

    Type theory and set theory
    Thierry Coquand

    Lecture
    10:00 to 11:30

    The mystery of equality; the notion of type as a generalization of the notion of …
    Thierry Coquand

    Lecture
    10:00 to 11:00

    Type theory models and the principle of univalence
    Thierry Coquand

    Lecture
    10:00 to 11:00

    Eilenberg-MacLane spaces and cohomology
    Thierry Coquand

    Lecture
    10:00 to 11:00

    Modalities and models of type theory
    Thierry Coquand

    Lecture
    10:00 to 11:00

    See also

    Thierry Coquand, chair Computer Sciences and Digital Technologies
    Dependent type theory and mathematical formalization