Operational semantics in a natural deduction setting
from Representing Formal Systems
Published online by Cambridge University Press: 04 August 2010
Summary
Abstract
We show how Natural Deduction extended with two replacement operators can provide a framework for defining programming languages, a framework which is more expressive than the usual Operational Semantics presentation in that it permits hypothetical premises. This allows us to do without an explicit environment and store. Instead we use the hypothetical premises to make assumptions about the values of variables. We define the extended Natural Deduction logic using the Edinburgh Logical Framework.
Introduction
The Edinburgh Logical Framework (ELF) provides a formalism for defining Natural Deduction style logics. Natural Deduction is rather more powerful than the notation which is commonly used to define programming languages in “inference-style” Operational Semantics, following Plotkin and others, for example Kahn. So one may ask
“Can a Natural Deduction style be used with advantage to define programming languages?”.
We show here that, with a slight extension, it can, and hence that the ELF can be used as a formal meta-language for defining programming languages. However ELF employs the “judgements as types” paradigm and takes the form of a typed lambda calculus with dependent types. We do not need all this power here, and in this paper we present a slight extension of Natural Deduction as a semantic notation for programming language definition. This extension can itself be defined in ELF.
The inspiration for using a meta-logic for Natural Deduction proofs comes from Martin-Löf.
- Type
- Chapter
- Information
- Logical Frameworks , pp. 185 - 214Publisher: Cambridge University PressPrint publication year: 1991
- 7
- Cited by