In this work, we study reduction monads, which are essentially the same as monads relative to the free functor from sets into graphs. Reduction monads abstract two aspects of the lambda calculus: on the one hand, in the monadic viewpoint, it is an object equipped with a well-behaved substitution; on the other hand, in the graphical viewpoint, it is an oriented graph whose vertices are terms and whose edges witness the reductions between two terms.
We study presentations of reduction monads. To this end, we propose a notion of reduction signature. As usual, such a signature plays the rôle of a virtual presentation, and specifies arities for generating operations—possibly subject to equations—together with arities for generating reduction rules. For each such signature, we define a category of models. Any model is, in particular, a reduction monad, and, in the spirit of Initial Semantics, we define the reduction monad presented (or specified) by the given reduction signature to be, if it exists, the initial object of this category of models.
Our main result identifies a class of reduction signatures which specify a reduction monad in the above sense. In particular, the lambda calculus is naturally specified by such a signature.
Fri 24 JanDisplayed time zone: Saskatchewan, Central America change
15:35 - 16:40
|Taylor Subsumes Scott, Berry, Kahn and PlotkinDistinguished Paper|
Research PapersLink to publication DOI Media Attached File Attached
|Reduction Monads and Their Signatures|
Benedikt Ahrens University of Birmingham, United Kingdom, André Hirschowitz Université Côte d'Azur, Ambroise Lafont Inria, France, Marco Maggesi Università di FirenzeLink to publication DOI Media Attached
|Coq Coq Correct! Verification of Type Checking and Erasure for Coq, in Coq|
Matthieu Sozeau Inria, Simon Boulier Inria, Yannick Forster Saarland University, Nicolas Tabareau Inria, Theo Winterhalter Inria — LS2NLink to publication DOI Media Attached File Attached