A Mathematical Approach to Language Design

Abstract

A framework for validating surface properties of programming language constructs, composed of proof rules (akin to those of Hoare) and supporting hypotheses, is constructed using the mathematical semantics of Scott and Strachey. The following approach to language design is then considered: the constructs of a language should have surface properties which 1) need few hypotheses other than assumed surface properties; and 2) have proofs consisting, as far as possible, of trivial fixpoint and structural inductions.