2011/07/31 by Benedikt Ahrens, BENEDIKT AHRENS · 1 citation
Computer Science · #Abstract syntax #Class (philosophy) #Logic, programming, and type systems #Model-Driven Software Engineering Techniques #Object (grammar) #Operational semantics #Proof assistant #Reduction (mathematics) #Semantics (computer science) #Signature (topology) #Syntax #cs.LO #cs.PL #semigroups and automata theory
paper · pdf · doi:10.1017/s0960129514000103
published as Math. Struct. Comp. Sci. 26 (2016) 3-37 · v2: - Abstract and Introduction completely rewritten - Addition of examples and remarks in Secs. 1 and 2 - Sec 3 now describes the implementation in proof assistant Coq of the main theorem v3: - final version for publication in MSCS
arxiv created 2013/11/19 · openalex publication_date 2014/12/05 · openalex created_date 2016/06/24 · arxiv updated 2019/02/20 · openalex updated_date 2026/08/05
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.