Logogram strony

Myśliciel A.Rodin

Narodziny gwiazdy

Rozmiar tekstu

The book

A Denotational Engineering of Programming Languages, preprint version dated 2019 09 30 Download
DOI  10.13140/RG.2.2.27499.39201/3

Keywords: Set-theoretic denotational semantics, many-sorted algebras, three-valued predicate calculus, a denotational model of types, abstract syntax, concrete syntax, total correctness with clean termination, sound program-construction rules.

The book is so far the major contribution to the project and 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. The algebra of denotation is defined in the first step, and syntax is derived from it later. This way guarantees the existence of a denotational semantics for the derived syntax. Mathematically it is a homomorphism from syntax to denotations.
  2. Designing sound program-constructors for languages with denotational models. In my 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 it yields a correct resulting program.

Both methods are illustrated on an example of a virtual language Lingua. The first aspect of the book has been summarised in a paper desctibed on the site On the development of a denotational model.