programming language engineers

Abstract: Mechanisation of a mathematical definition (also referred to as formalisation) has many benefits. Here, we focus on mechanising denotational semantic definitions of programming languages by embedding them in the Agda language. The Agda type-checker detects and reports any issues with the wellformedness and type correctness of the embedded definitions. To minimise the effort required, and to facilitate correlation of the original definition with its Agda embedding, mechanisation should not involve significant reformulation or extension. Here, we show how to embed conventional Scott-Strachey denotational definitions in Agda with almost no changes to $λ$-notation or domain equations. Agda notation for definitions of types and functions corresponds closely to the conventional meta-notation of denotational semantics. We have developed a collection of Agda modules with postulated types for commonly used domain constructors and their associated operations. We illustrate our approach with mechanisations of three denotational definitions: a model of the untyped $λ$-calculus, Plotkin's denotational semantics of PCF, and a semantics of a sublanguage of Scheme. In previous work, similar mechanisations in Agda have revealed several unsuspected wellformedness issues in published denotational definitions. Some of the postulated properties of our definitions are inconsistent with a classical set-theoretic interpretation of Agda. We conjecture that they would be consistent with an interpretation of Agda in a higher-order intuititionistic logic, such as that used by Simpson in his work on synthetic domain theory. After recalling previous work on mechanising domain theory, we consider the possibility of mechanising synthetic domain theory in Agda.

Abstract: Among the different ways of approaching the semantics of process calculi, true-concurrency models stand out for their ability to highlight subtle interplays between events. At their heart lie three crucial relations: concurrency, causality and conflict. This paper shows that reversibility, when endowed with a notion of independence, provides a rich tooling to study and characterise these true-concurrency relations. First, we prove that systems admitting pre-reversibility (i.e., that can be extended with an independence relation satisfying some basic axioms) have a unique notion of independence, events, concurrency, causality and conflict. We then analyse the relationship between independence and the true-concurrency relations, establishing novel independence-based characterisations of causality and conflict. Our second series of contributions revolves around two concrete process calculi and two syntactic notions defined on their transition labels, namely independence and dependence; we prove that they partition connected transitions and characterise elegantly concurrency on adjacent transitions. This part of our development was machine-checked using the proof assistant Beluga. Last, we study how the key mechanism commonly used in reversible process algebra can be used as a proxy to retrieve causality and core independence on past events. We conclude by discussing how our results extend beyond reversible systems.