10:00 - 11:00am
Lecture

Type theory, from Russell to de Bruijn

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

    Lecture outline :

    • russell type theory ;
    • church's λ-calculus notation for functions ;
    • simple type theory and the HOL system ;
    • introduction to dependent types, AUTOMATH system ;
    • uniform treatment of mathematical objects and proofs ;
    • proof checking as type checking.

    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 - 11:00am

    Natural deduction and models
    Thierry Coquand

    Lecture
    10:00 - 11:00am

    Universe, paradoxes and standardization
    Thierry Coquand

    Lecture
    10:00 - 11:00am

    Type theory and set theory
    Thierry Coquand

    Lecture
    10:00 - 11:30am

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

    Lecture
    10:00 - 11:00am

    Type theory models and the principle of univalence
    Thierry Coquand

    Lecture
    10:00 - 11:00am

    Eilenberg-MacLane spaces and cohomology
    Thierry Coquand

    Lecture
    10:00 - 11:00am

    Modalities and models of type theory
    Thierry Coquand

    Lecture
    10:00 - 11:00am

    See also

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