10:00 to 11:00
Lecture

Type theory, from Russell to de Bruijn

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 :

    • 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

    Lecture
    10:00 to 11:00
    Thierry Coquand

    Type theory, from Russell to de Bruijn
    Lecture
    10:00 to 11:00
    Thierry Coquand

    Natural deduction and models
    Lecture
    10:00 to 11:00
    Thierry Coquand

    Universe, paradoxes and standardization
    Lecture
    10:00 to 11:30
    Thierry Coquand

    Type theory and set theory
    Lecture
    10:00 to 11:00
    Thierry Coquand

    The mystery of equality; the notion of type as a generalization of the notion of …
    Lecture
    10:00 to 11:00
    Thierry Coquand

    Type theory models and the principle of univalence
    Lecture
    10:00 to 11:00
    Thierry Coquand

    Eilenberg-MacLane spaces and cohomology
    Lecture
    10:00 to 11:00
    Thierry Coquand

    Modalities and models of type theory

    See also

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