A natural deduction treatment of operational semantics

Abstract

We show how Natural Deduction extended with a replacement operator can provide a framework for defining programming languages, a framework which is more expressive than the usual Operational Semantics presentation in that it allows 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.