Modules over relative monads for syntax and semantics

Research output: Contribution to journalArticle

Colleges, School and Institutes

External organisations

  • Laboratoire J. A. Dieudonné, Université Nice Sophia Antipolis, France

Abstract

We give an algebraic characterization of the syntax and semantics of a class of untyped functional programming languages.

To this end, we introduce a notion of 2-signature: such a signature specifies not only the terms of a language, but also reduction rules on those terms. To any 2-signature (S, A) we associate a category of ‘models’. We then prove that this category has an initial object, which integrates the terms freely generated by S, and which is equipped with reductions according to the rules given in A. We call this initial object the programming language generated by (S, A). Models of a 2-signature are built from relative monads and modules over such monads. Through the use of monads, the models – and in particular, the initial model – come equipped with a substitution operation that is compatible with reduction in a suitable sense.

The initiality theorem is formalized in the proof assistant Coq, yielding a machinery which, when fed with a 2-signature, provides the associated programming language with reduction relation and certified substitution.

Details

Original languageEnglish
Pages (from-to)3-37
Number of pages35
JournalMathematical Structures in Computer Science
Volume26
Issue number1
Early online date5 Dec 2014
Publication statusPublished - 1 Jan 2016