Rencontre, 14 mars 2019
Les exposés auront lieu en Amphi B, site Monod de l'ENS de Lyon (46 allée d'Italie), 3è étage.
Programme
- 10:30 – 12:00
-
Filip Sieczkowski (University of Wrocław)
Programming with algebraic effects and handlers is a fairly novel technique of representing computational effects. Rooted in the theoretical work of Plotkin and Power, from which the key notion of algebraicity of the effects stems, this framework offers a more modular way of effectful programming — in particular, a modular way of composing effectful programs.
The distinction between algebraic effects and other models of effectful computation is its separation between "interface" and "implementation": algebraic operations, such as raising an exception or reading/writing a cell of mutable state are treated as mere syntax or pieces of a specification, on their own devoid of interpretation. What Plotkin and Pretnar's insight adds to this view is the notion of a handler — a construct which provides an interpretation for the operation, within its scope. In connection with expressive type-and-effect systems, these constructs allow programmers almost unprecedented freedom to define and manage their own computational effects.
In this talk I would like to discuss some of the choices that one faces while designing a calculus that allows programming with algebraic effects, and show how one of the most important aspects that one needs to pay attention to is parametricity. To this end we develop a model calculus of algebraic effects and handlers with a polymorphic type-and-effect system that allows for both universal and existential quantification over effects (thus providing a somewhat limited model for modules in a setting with algebraic effects and handlers), and a step-indexed relational interpretation of this calculus. We can then use the relational interpretation to show some interesting properties of the calculus, in particular to show contextual equivalence and refinement results.
- 14:00 – 15:00
-
Ambroise Lafont (IMT Atlantique)
In their work on second-order equational logic, Fiore and Hur have studied presentations of simply typed languages by generating binding constructions and equations among them. To each pair consisting of a binding signature and a set of equations, they associate a category of `models', and they give a monadicity result which implies that this category has an initial object, which is the language presented by the pair.
In the present work, we propose, for the untyped setting, a variant of their approach where monads and modules over them are the central notions. More precisely, we study, for monads over sets, presentations by generating (`higher-order') operations and equations among them. We consider a notion of 2-signature which allows to specify a monad with a family of binding operations subject to a family of equations, as is the case for the paradigmatic example of the lambda calculus, specified by its two standard constructions (application and abstraction) subject to $\beta$- and $\eta$-equalities. Such a 2-signature is hence a pair (Σ,E) of a binding signature Σ and a family E of equations for Σ. This notion of 2-signature has been introduced earlier by Ahrens in a slightly different context.
We associate, to each 2-signature (Σ,E), a category of 'models of (Σ,E); and we say that a 2-signature is 'effective' if this category has an initial object; the monad underlying this (essentially unique) object is the 'monad specified by the 2-signature'. Not every 2-signature is effective; we identify a class of 2-signatures, which we call 'algebraic', that are effective.
Importantly, our 2-signatures together with their models enjoy 'modularity': when we glue (algebraic) 2-signatures together, their initial models are glued accordingly.
We provide a computer formalization for our main results.
- 15:30 – 16:30
-
Étienne Miquey (Gallinette, INRIA)
In 2012, Herbelin developed a calculus (dPA^ω) in which constructive proofs for the axioms of countable and dependent choices can be derived via the memoization of choice functions However, the property of normalization (and therefore the one of soundness) was only conjectured. The difficulty for the proof of normalization is due to the simultaneous presence of dependent dependent types (for the constructive part of the choice), of control operators (for classical logic), of coinductive objects (to encode functions of type ℕ→A into streams (a₀,a₁,…)) and of lazy evaluation with sharing (for these coinductive objects). Building on previous works, we introduce a variant of dPA^ω presented as a sequent calculus. On the one hand, we take advantage of a variant of Krivine classical realizability we developed to prove the normalization of classical call-by-need. On the other hand, we benefit of dL[tp], a classical sequent calculus with dependent types in which type safety is ensured using delimited continuations together with a syntactic restriction. By combining the techniques developed in these papers, we manage to define a realizability interpretation à la Krivine of our calculus that allows us to prove normalization and soundness. This talk will go over the whole process, starting from Herbelin’s calculus dPA^ω until our introduction of its sequent calculus counterpart dLPA^ω.
