Skip to Main content Skip to Navigation
New interface
Conference papers

Normalization by realizability also evaluates

Abstract : For those of us that generally live in the world of syntax, semantic proof methods such as realizability or logical relations / parametricity sometimes feel like magic. Why do they work? At which point in the proof is "the real work" done? Bernardy and Lasson express realizability and parametricity models as syntactic model -- but the abstraction/adequacy theorems are still explained as meta-level proofs. Hoping to better understand the proof technique, we look at those theorems as programs themselves. How does a normalization proof using realizability actually computes those normal forms? This detective work is an early stage and we propose a first attempt in a simple setting. Instead of arbitrary Pure Type Systems, we use the minimal negative propositional logic (arrows only). Instead of starting from the simply-typed lambda-calculus, we work on sequent-style terms in a simple subset of the Curien-Herbelin L calculus.
Complete list of metadata

Cited literature [12 references]  Display  Hide  Download
Contributor : David Baelde Connect in order to contact the contributor
Submitted on : Wednesday, December 31, 2014 - 3:44:25 PM
Last modification on : Thursday, February 3, 2022 - 11:18:20 AM
Long-term archiving on: : Wednesday, April 1, 2015 - 10:26:26 AM


Files produced by the author(s)


  • HAL Id : hal-01099138, version 1



Pierre-Évariste Dagand, Gabriel Scherer. Normalization by realizability also evaluates. Vingt-sixièmes Journées Francophones des Langages Applicatifs (JFLA 2015), Jan 2015, Le Val d'Ajol, France. ⟨hal-01099138⟩



Record views


Files downloads