Séminaires du LAMA

Séminaires hebdomadaires (Salle TLR, voir Comment venir).

Autres séminaires :

Prochains séminaires du LAMA :

EDPs²Jeudi 17 novembre 2022 à 14h JERAA (Lyon),
Journéee EDP Rhone Alpes Auvergne 17-18 Novembre

GéométrieJeudi 06 octobre 2022 à 14h, En salle TLR et sur Zoom : https://cnrs.zoom.us/j/97788860132?pwd=ZmNSeUwvWnByeUhzOUJXMlFtZDhSUT09 Stéphane Druel (Institut Camille Jordan, Lyon),
À venir

Résumé : (Masquer les résumés)
À venir

LIMDJeudi 29 septembre 2022 à 10h Yannick Zakowski (ENS Lyon),
Monadic Definitional Interpreters as Formal Semantic Models of Computations

Résumé : (Masquer les résumés)
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.

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

Résumé : (Masquer les résumés)
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)