@inproceedings{kellerA10,
hal_id = {inria-00520606},
url = {http://hal.inria.fr/inria-00520606},
title = {{Hereditary Substitutions for Simple Types, Formalized}},
author = {Keller, Chantal and Altenkirch, Thorsten},
abstract = {{We analyze a normalization function for the simply typed lambda-calculus based on hereditary substitutions, a technique developed by Pfenning et al. The normalizer is implemented in Agda, a total language where all programs terminate. It requires no termination proof since it is structurally recursive which is recognized by Agda's termination checker. Using Agda as an interactive theorem prover we establish that our normalization function precisely identifies beta-eta-equivalent terms and hence can be used to decide beta-eta-equality. An interesting feature of this approach is that it is clear from the construction that beta-\eta-equality is primitive recursive.}},
keywords = {Hereditary substitutions Type Theory normalizer decidability of beta-eta-equality},
language = {Anglais},
affiliation = {Laboratoire d'informatique de l'{\'e}cole polytechnique - LIX , TYPICAL - INRIA Saclay - Ile de France , {\'E}cole normale sup{\'e}rieure de Lyon - ENS LYON , Functional Programming Laboratory},
booktitle = {{MSFP - Third Workshop on Mathematically Structured Functional Programming - 2010}},
publisher = {ACM Press},
address = {Baltimore, {\'E}tats-Unis},
editor = {Capretta, V. and Chapman, J. },
audience = {internationale },
year = {2010},
pdf = {http://hal.inria.fr/inria-00520606/PDF/msfp10.pdf},
}