A Denotational Engineering of Programming Languages

TL;DR

This paper explores the design of programming languages using denotational models and introduces sound program-constructors that ensure correctness by construction, demonstrated through an example language Lingua.

Contribution

It presents a systematic approach to language design with denotational semantics and develops sound program-constructors that embed correctness specifications.

Findings

Denotational models consist of syntax and denotation algebras with a homomorphism as semantics.

Programs contain their total-correctness specifications, enabling correctness-by-construction.

The approach is illustrated with the example language Lingua.

Abstract

The book is devoted to two research areas: (1) Designing programming languages along with their denotational models. A denotational model of a language consists of two many-sorted algebras - an algebra of syntax and an algebra of denotations - and a (unique) homomorphism from syntax to denotations called the semantics of the language. (2) Designing sound program-constructors for languages with denotational models. In our approach programs syntactically contain their total-correctness specifications. A program is said to be correct if it is correct wrt its specification. A program-constructor is sound if given correct component-programs yields a correct resulting program. Both methods are illustrated on an example-language Lingua.