Extended natural semantics
- 1 April 1993
- journal article
- research article
- Published by Cambridge University Press (CUP) in Journal of Functional Programming
- Vol. 3 (2) , 123-152
- https://doi.org/10.1017/s0956796800000666
Abstract
We extend the definition of natural semantics to include simply typed λ-terms, instead of first-order terms, for representing programs, and to include inference rules for the introduction and discharge of hypotheses and eigenvariables. This extension, which we call extended natural semantics, affords a higher-level notion of abstract syntax for representing programs and suitable mechanisms for manipulating this syntax. We present several examples of semantic specifications for a simple functional programming language and demonstrate how we achieve simple and elegant manipulations of bound variables in functional programs. All the examples have been implemented and tested in λProlog, a higher-order logic programming language that supports all of the features of extended natural semantics.Keywords
This publication has 16 references indexed in Scilit:
- Natural semantics and some of its meta-theory in ElfPublished by Springer Nature ,2005
- Compiler verification in LFPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- Uniform proofs as a foundation for logic programmingAnnals of Pure and Applied Logic, 1991
- Encoding a dependent-type λ-calculus in a logic programming languagePublished by Springer Nature ,1990
- The foundation of a generic theorem proverJournal of Automated Reasoning, 1989
- Deriving mixed evaluation from standard evaluation for a simple functional languagePublished by Springer Nature ,1989
- Centaur: the systemPublished by Association for Computing Machinery (ACM) ,1988
- What is a model of the lambda calculus?Information and Control, 1982
- Call-by-name, call-by-value and the λ-calculusTheoretical Computer Science, 1975
- A unification algorithm for typed