Seminars of LAMA

Four regular seminars take place at LAMA, in the seminar room, first floor of the building Le Chablais, (see How to come ?).

Weekly seminars:

Others seminars

Next seminars:

EDPs²Thursday 17th November 2022 at 14h JERAA (Lyon),
Journéee EDP Rhone Alpes Auvergne 17-18 Novembre

GéométrieThursday 6th October 2022 at 14h Stéphane Druel (Institut Camille Jordan, Lyon),
À venir

Abstract: (Hide abstracts)
À venir

LIMDThursday 29th September 2022 at 10h Yannick Zakowski (ENS Lyon),
Monadic Definitional Interpreters as Formal Semantic Models of Computations

Abstract: (Hide abstracts)
Monadic interpreters have been used for a long time as a mean to embed arbitrary computations in purely functional contexts. At its core, the idea is elementary: the object language of interest is implemented as an executable interpreter in the host language, and monads are simply the abstraction used to embed features such as side effects, failure, non-determinism. By building these interpreters on top of the free monad, the approach has offered a comfortable design point notably enabling an extensible syntax, reusable modular components, structural compositional definitions, as well as algebraic reasoning. The approach has percolated beyond its programming roots: it is also used as a way to formalize the semantics of computational systems, programming languages notably, in proof assistants based on dependently typed theories. In such assistants, the host language is even more restricted: programs are all pure, but also provably terminating. Divergent programs can nonetheless be embedded using for instance the Capretta monad: intuitively, a lazy, infinite (coinductive) tree models the dynamic of the computation. Interaction trees are a specific implementation, in the Coq proof assistant, of a set of tools realizing this tradition. They provide a coinductive implementation of the iterative free monad, equipped with a set of combinators, allowing notably for general recursion. Each iterator comes with its equational theory established with respect to a notion of weak bisimulation --- i.e. termination sensitive, but ignoring the amount of fuel consumed --- and practical support for equational reasoning. Further effects are implemented into richer monads via a general notion of interpretation, allowing one to introduce the missing algebras required for proper semantic reasoning. Beyond program equivalence, support for arbitrary heterogeneous relational reasoning is provided, typically allowing one to prove a compilation pass correct. Introduced in 2020, the project has spawned realistic applications --- they are used to model LLVM IR's semantics notably ---, as well as extensions to reduce the necessary boilerplate, or to offer proper support for non-determinism. In this talk, I will attempt to paint an illustrative overview of the core ideas and contributions constitutive of this line of work.

LAMAMonday 24th October 2022 at 09h45 J Blu M Pierre L Véron (Univ Savoie Mont-Blanc),
Journée en l'hommage de Pierre Baras

Abstract: (Hide abstracts)
La journée en l'honneur de Pierre aura lieu le lundi 24 octobre de 9h45 à 16h Programme provisoire 10h - 10h45 : hommages de Ph. Galez, Ph. Briand, P. Orro, G. Angénieux, N. Kardos (amphi Nivolet) 11h - 11h45 : exposé de J. Blum (amphi Nivolet) 12h - 14h : buffet au bâtiment EVE 14h - 14h45 : exposé de Michel Pierre (salle TLR) 15h - 15h45 : exposé de Laurent Véron (salle TLR)