The book

Utworzono: poniedziałek, 29 kwiecień 2019 15:12

Poprawiono: poniedziałek, 25 marzec 2024 12:08

Odsłony: 9096

A Denotational Engineering of Programming Languages

Preprint version (improved and modified) by March 25^th, 2024 Download
Preprint version by 2019 09 30 has been registered as 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 main 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 this semantics 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 described on the site On the development of a denotational model.