A Denotational Engineering of Programming Languages
Blikle Andrzej

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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
