Skip to Main content Skip to Navigation
Conference papers

Hereditary Substitutions for Simple Types, Formalized

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.
Document type :
Conference papers
Complete list of metadata

Cited literature [14 references]  Display  Hide  Download

https://hal.inria.fr/inria-00520606
Contributor : Chantal Keller <>
Submitted on : Tuesday, March 20, 2012 - 11:36:59 AM
Last modification on : Thursday, March 5, 2020 - 6:22:53 PM
Long-term archiving on: : Monday, November 26, 2012 - 11:35:18 AM

File

msfp10.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00520606, version 1

Collections

Citation

Chantal Keller, Thorsten Altenkirch. Hereditary Substitutions for Simple Types, Formalized. MSFP - Third Workshop on Mathematically Structured Functional Programming - 2010, Sep 2010, Baltimore, United States. ⟨inria-00520606⟩

Share

Metrics

Record views

513

Files downloads

627