Realizability and parametricity in Pure Type Systems
type: Distribution
access URL: https://theses.hal.science/tel-00770669
format: HTML
issued: 2026-05-15T13:13:13.387183
modified: 2026-05-15T13:13:13.298662

test_moissonnage_selune
type: Agent

Realizability and parametricity in Pure Type Systems
type: Dataset
contact point: Organization
  fn: CCSD
keyword: infoinfo-ohcomputer-science-csother-csoh
keyword: systemes-de-types-purs
keyword: isomorphisme-de-curry-howard
keyword: infoeu-reposemanticsdoctoralthesis
keyword: curry-howard-isomoprhism
keyword: theorie-des-types
keyword: dependant-type
keyword: assistants-de-preuve
keyword: type-theory
keyword: realisabilite
keyword: proof-assistants
keyword: lambda-calcul
keyword: types-dependants
keyword: realizability
keyword: calculus-of-constructions
keyword: calcul-des-constructions
keyword: parametricite
keyword: logical-relation
keyword: parametricity
keyword: relation-logique
keyword: coq
keyword: pure-type-systems
keyword: lambda-calculus
keyword: theses
landing page: https://theses.hal.science/tel-00770669
description: This thesis focuses on the adaptation of realizability and parametricity to dependent types in the framework of Pure Type Systems. We describe a systematic method to build a logic from a programming language, both described as pure type systems. This logic provides formulas to express properties of programs and offers a formal framework that allows us to develop a theory of realizability in which realizers of formulas are exactly programs of the starting programming language. In our framework, the standard representation theorems of Gödel's system T and Girard's system F may be seen as two instances of a more general theorem. Then, we explain how the so-called « logical relations » of parametricity theory may be expressed in terms of realizability, which shows that the generated logic provides an adequate framework for developping a general theory of parametricity. Finally, we show how this parametricity theory can be adapted to the underlying type system of the proof assistant Coq and we give an original example of application of parametricity theory to the formalization of mathematics.
identifier: NNT: 2012ENSL0764
issued: 2026-05-15T13:13:13.377275
language: fr
modified: 2026-05-15T13:13:13.377286