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 metadatas

Cited literature [12 references]  Display  Hide  Download

https://hal.inria.fr/hal-01099138
Contributor : David Baelde <>
Submitted on : Wednesday, December 31, 2014 - 3:44:25 PM
Last modification on : Tuesday, November 20, 2018 - 11:06:03 PM
Long-term archiving on : Wednesday, April 1, 2015 - 10:26:26 AM

File

jfla15_submission_31.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01099138, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

238

Files downloads

190