10:00 to 11:00
Lecture

Universe, paradoxes and standardization

Thierry Coquand
Dependent type theory and mathematical formalization
10:00 to 11:00
    Salle 5, Site Marcelin Berthelot
    Open to all, subject to availability
    -

    Lecture outline :

    • girard's paradox with one type of all types ;
    • difference with Russell's paradox ;
    • universe as reflection principle ;
    • algebraic proof of canonicity with the Artin gluing technique and normalization proof ;
    • application to proof verification.

    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