Séminaire, 17 octobre 2019
The meeting will take place in amphi B, ENS de Lyon, Monod site (3rd floor).
On this meeting, ChoCoLa is glad to be a partner of the LHC and Scalp working groups of the GDR IM of the CNRS, and is sorry for the multiple acronyms.
Here is the announcement for the LHC meeting, and here for the SCALP meeting.
Moreover, the PhD defense of Aurore Alcolei will take place at 5:00pm after the meeting.
Nota: For this meeting, we are only able to offer the lunch. Registration should be done via this form.
Please write to chocola-gestion@ens-lyon.fr if you have difficulties funding your trip, and would like to attend.
Programme
- 10:00 – 11:00
-
Danel Ahman (University of Ljubljana (Slovénie))
In languages with algebraic effects (resp. monads), the usual way of modelling interactions with the external world is to define a dedicated effect (resp. monad) and then treat it specially in the compiler, such as the RandomInt effect in the Eff language and the IO monad in Haskell. This however has various drawbacks. For instance, such languages often lack enforcement mechanisms to ensure that a program does not write to an already closed file. And what is even worse, in languages with algebraic effects, where all effects can be handled, it is very easy to accidentally cause one's program not to even reach file closing, by discarding a continuation somewhere in the handler.
In this talk, I will present our ongoing work on using comodels of algebraic effects as a programming abstraction for (i) modelling the external world and interactions with it, (ii) ensuring the linearity of these interactions, and (iii) controlling which capabilities of the external world different parts of programs have access to. Regarding (ii), the novel aspect of our work is that we do not ensure linearity of these interactions by the means of a linear type system, but instead we leave the external world implicit and interact with it through a combination of algebraic operations and (under the hood) a linear state-passing translation analogous to that of Møgelberg and Staton. Regarding (i) and (ii), we do not limit the programmer to a single external world, but instead allow them to modularly build their own intermediate external worlds. In addition, in the talk I will also discuss two natural ways how a comodel (i.e., the external world) can communicate information back to the program being run using this comodel.
(This is joint work with Andrej Bauer)
- 11:30 – 12:30
-
Eric Finster (Gallinette, INRIA)Invited talk: An opetopic syntax for higher monoidal closed categories
At the core of the modern understanding of the Curry-Howard correspondence between proofs and programs is the connection between, on the one hand, the syntax of logic and type theory, and on the other, certain mathematical structures, often taking the form of structured categories and related objects. In one of its most well-known incarnations, for example, we can see the simply typed lambda calculus as a syntactic notation for morphisms in a cartesian closed category. Equivalently, free cartesian closed categories can be constructed directly from syntax in a way which gives them a well-understood computational interpretation.
With the recent advances in understanding the homotopical nature of dependent type theory, as well as the parallel development of tractable models of higher categories, it is natural to wonder if this classical correspondence between syntax, semantics and computation can be extended in a direct way to higher structures. That is, can we find some kind of natural syntactic description of higher structured categories? In this talk I will explain one possibility for such a description of monoidal closed higher categories using a graphical syntax based on opetopes.
- 14:00 – 15:00
-
Dan Ghica (University of Birmingham)Invited talk: The next 700 abstract machines
We propose a new core calculus for programming languages with effects, interpreted using a hypergraph-rewriting abstract machine inspired by the Geometry of Interaction. The intrinsic calculus syntax and semantics only deals with the basic structural aspects of programming languages: variable binding, name binding, and thunking. Everything else, including function abstraction and application, must be provided as extrinsic operations with associated rewrite rules. The graph representation yields natural concepts of locality and robustness for equational properties and reduction rules, which enable a novel flexible and powerful reasoning methodology about (type-free) languages with effects. We illustrate and motivate the technique with challenging examples from the literature.
Paper: https://arxiv.org/abs/1907.01257
(Joint work with Koko Muroya and Todd Waugh Ambridge.)
- 15:30 – 16:30
-
Valeria Vignudelli (École Normale Supérieure de Lyon)
We study trace-based equivalences for labelled transition systems combining nondeterministic and probabilistic choices. We do so via a coalgebraic construction known as the generalized powerset construction, which consists in first determinizing a system and then recovering trace equivalence as bisimilarity on the determinized system. The generalized powerset construction allows us to apply these two steps, inspired by the standard powerset construction for nondeterministic automata, to a variety of systems, such as labelled transition systems with different computational effects captured by monads (e.g., systems with probabilistic choices). We show how trace semantics for labelled transition systems combining nondeterministic and probabilistic choices can be recovered by instantiating the generalized powerset construction, and we characterise and compare the resulting semantics to known definitions of trace equivalences appearing in the literatures. Most of our results are based on the exciting interplay between monads and their presentations via algebraic theories.
This talk is based on joint work with Filippo Bonchi and Ana Sokolova, available at https://arxiv.org/abs/1808.00923
