Fully abstract models of the lazy lambda calculus
- 1 January 1988
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- p. 368-376
- https://doi.org/10.1109/sfcs.1988.21953
Abstract
Much of what is known about the model theory and proof theory of the lambda -calculus is sensible in nature, i.e. only head normal forms are semantically meaningful. However, most functional languages are lazy, i.e. programs are evaluated in normal order to weak head normal forms. The author develops a theory of lazy or strongly sensible lambda -calculus that corresponds to practice. A general method for constructing fully abstract models for a class of lazy languages is illustrated. A formal system called lambda beta C ( lambda beta -calculus with convergence testing C) is introduced, and its properties are investigated.Keywords
This publication has 12 references indexed in Scilit:
- Can LCF be topped? Flat lattice models of typed lambda calculusPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- Categories of partial mapsInformation and Computation, 1988
- Fully abstract submodels of typed lambda calculiJournal of Computer and System Sciences, 1986
- Set-theoretical models of λ-calculus: theories, expansions, isomorphismsAnnals of Pure and Applied Logic, 1983
- What is a model of the lambda calculus?Information and Control, 1982
- Identity and existence in intuitionistic logicPublished by Springer Nature ,1979
- LCF considered as a programming languageTheoretical Computer Science, 1977
- Fully abstract models of typed λ-calculiTheoretical Computer Science, 1977
- A lazy evaluatorPublished by Association for Computing Machinery (ACM) ,1976
- Call-by-name, call-by-value and the λ-calculusTheoretical Computer Science, 1975