Normalization by evaluation for typed lambda calculus with coproducts
- 13 November 2002
- conference paper
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- No. 10436871,p. 303-310
- https://doi.org/10.1109/lics.2001.932506
Abstract
Solves the decision problem for the simply typed lambda calculus with a strong binary sum, or, equivalently, the word problem for free Cartesian closed categories with binary co-products. Our method is based on the semantic technique known as "normalization by evaluation", and involves inverting the interpretation of the syntax in a suitable sheaf model and, from this, extracting an appropriate unique normal form. There is no rewriting theory involved and the proof is completely constructive, allowing program extraction from the proof.Keywords
This publication has 10 references indexed in Scilit:
- Reduction-free normalisation for a polymorphic systemPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Normalization by Evaluation for the Computational Lambda-CalculusLecture Notes in Computer Science, 2001
- Lambda Definability with Sums via Grothendieck Logical RelationsLecture Notes in Computer Science, 1999
- Domains and Lambda-CalculiPublished by Cambridge University Press (CUP) ,1998
- Proof Theory at Work: Program Development in the Minlog SystemPublished by Springer Science and Business Media LLC ,1998
- Intuitionistic model constructions and normalization proofsMathematical Structures in Computer Science, 1997
- Type-directed partial evaluationPublished by Association for Computing Machinery (ACM) ,1996
- The virtues of eta-expansionJournal of Functional Programming, 1995
- Isomorphisms of Types: from λ-calculus to information retrieval and language designPublished by Springer Science and Business Media LLC ,1995
- Sheaves in Geometry and LogicUniversitext, 1994