We found a match
Your institution may have access to this item. Find your institution then sign in to continue.
- Title
Modules over relative monads for syntax and semantics.
- Authors
AHRENS, BENEDIKT
- 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.
- Subjects
MODULES (Algebra); MONADS (Mathematics); MATHEMATICS theorems; SEMANTICS; SYNTAX in programming languages; SUBSTITUTION (Logic)
- Publication
Mathematical Structures in Computer Science, 2016, Vol 26, Issue 1, p3
- ISSN
0960-1295
- Publication type
Article
- DOI
10.1017/S0960129514000103