Write a Blog >>

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 Jan
Times are displayed in time zone: (GMT-06:00) Saskatchewan, Central America change

15:35 - 16:40: Research Papers - Semantics & Type Theory at Ile de France II (IDF II)
Chair(s): Arthur Azevedo de AmorimCarnegie Mellon University, USA
POPL-2020-Research-Papers15:35 - 15:56
Davide BarbarossaUniversité Paris 13, Giulio ManzonettoUniversité Paris 13
Link to publication DOI Media Attached File Attached
POPL-2020-Research-Papers15:56 - 16:18
Benedikt AhrensUniversity of Birmingham, United Kingdom, André HirschowitzUniversité Côte d'Azur, Ambroise LafontInria, France, Marco MaggesiUniversità di Firenze
Link to publication DOI Media Attached
POPL-2020-Research-Papers16:18 - 16:40
Matthieu SozeauInria, Simon BoulierInria, Yannick ForsterSaarland University, Nicolas TabareauInria, Théo WinterhalterInria — LS2N
Link to publication DOI Media Attached File Attached