Modules over relative monads for syntax and semantics

DOI10.1017/S0960129514000103MaRDI QIDQ5741555zbMATH OpenFDO

Authors Benedikt Ahrens

Publication date 28 July 2016

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

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

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

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.

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

Cites work

• scientific article; zbMATH DE number 1216133 (Why is no real title available?)
• Equational Systems and Free Constructions (Extended Abstract)
• Modules over Monads and Linearity
• Monads need not be endofunctors
• Nominal logic, a first order theory of names and binding

Cited in

(15)

• scientific article; zbMATH DE number 7559272 (Why is no real title available?)
• 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
• scientific article; zbMATH DE number 7577567 (Why is no real title available?)
• 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
• scientific article; zbMATH DE number 7379288 (Why is no real title available?)
• Initiality for typed syntax and semantics

Describes a project that uses

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)