Modules over relative monads for syntax and semantics

DOI10.1017/S0960129514000103zbMATH Open1361.68034arXiv1107.5252MaRDI QIDQ5741555FDOQ5741555

Authors: Benedikt Ahrens 

Publication date: 28 July 2016

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

Abstract: We give an algebraic characterization of the syntax and semantics of a class of languages with variable binding. 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$ we associate a category of "models" of $S$. This category has an initial object, which integrates the terms freely generated by $S$, and which is equipped with reductions according to the inequations given in $S$. We call this initial object the language generated by $S$. 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.

Full work available at URL: https://arxiv.org/abs/1107.5252

Recommendations

• Modules over monads and initial semantics
• Modules over monads and operational semantics (expanded version)
• scientific article; zbMATH DE number 1086712
• Modules over Monads and Linearity
• scientific article; zbMATH DE number 2086588
• Modular specification of monads through higher-order presentations
• Relative monads formalised
• Monads, partial evaluations, and rewriting
• Modules over monads and their algebras

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Cites Work

• Title not available (Why is that?)
• Nominal logic, a first order theory of names and binding
• Monads need not be endofunctors
• Equational Systems and Free Constructions (Extended Abstract)
• Modules over Monads and Linearity

Cited In (15)

• Extended initiality for typed abstract syntax
• From signatures to monads in \textsf{UniMath}
• Initial semantics for reduction rules
• Modules over Monads and Linearity
• Initial semantics for strengthened signatures
• High-level signatures and initial semantics
• Initiality for typed syntax and semantics
• Title not available (Why is that?)
• C-system of a module over a \(Jf\)-relative monad
• Modules over monads and initial semantics
• Distributive laws for relative monads
• The formal theory of relative monads
• Title not available (Why is that?)
• Initiality for typed syntax and semantics
• Title not available (Why is that?)

Uses Software

• Coq

This page was built for publication: Modules over relative monads for syntax and semantics

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5741555)