About some extensions of type theory
Supervisor: Hugo Herbelin (INRIA – IRIF)
Location: IRIF lab, University Paris Diderot
Designed by Martin-Löf’s in the 70s, Intensional Type Theory is a
formalism which is at the same time a logic and a programming
language. It is the basis of several proof assistants such as Agda,
Coq, Lean, Matita, the three latter implementing an impredicative
version of it called the Calculus of Inductive Constructions (CIC).
Type theory is at the core of a multiple correspondence “type =
formula = space = object”, and “program = proof = continuous map =
morphism” which is the subject of numerous research.
The objective of the internship is to study some variations and
extensions of type theory which will be picked out of one of the
following:
-
Designing a call-by-value form of type theory
- Type theory with explicit subtyping (universes à la Tarski),
with application to the validity of unrestricted η in the
Calculus of Inductive Constructions (see [A])
- Type theory with destructing let (with application to the
support of a generalized notion of context in the Calculus of
Inductive Constructions (see [S] for the study of simple let binders
in type theory)
- Presenting type theory in sequent calculus (see [H,M])
- Studying the standard notions of realizability in type
theory (see [BPT,JLPST])
Bibliography
-
[A] Ali Assaf, A framework for defining
computational higher-order logics, PhD thesis, 2015.
- [BPT] Simon Boulier, Pierre-Marie Pédrot, Nicolas Tabareau, The
The next 700 syntactical models of type theory, CPP, 2017.
- [H] Hugo Herbelin Intuitionistic dependent type theory in
sequent calculus, unpublished, 2008.
- [M] Étienne Miquey, A classical sequent calculus with
dependent types, ESOP, 2017.
- [JLPST] Guilhem Jaber, Gabriel Lewertowski, Pierre-Marie
Pédrot, Matthieu Sozeau, Nicolas Tabareau, The Definitional Side of
the Forcing , LICS, 2016.
- [HoTT] The HoTT Book
on Homotopy type theory, 2013.
- [NG] Rob Nederpelt, Herman Geuvers, Type Theory and Formal
Proof: An Introduction, 2014.
- [S] Paola Severi, Pure Type Systems with definitions, LFCS,
1994.
This document was translated from LATEX by
HEVEA.