Séminaires du LAMA
Séminaires hebdomadaires (Salle TLR, voir Comment venir).
- Séminaire de l’équipe EDPs2.
- Séminaire de l’équipe de géométrie, habituellement le jeudi à 14h.
- Séminaire de l’équipe LIMD, habituellement le jeudi à 10h15 et commun avec l'équipe Plume (ENS Lyon).
Autres séminaires :
- Séminaire du laboratoire
- Séminaire des doctorants
- Séminaire CMI : il accueille un chercheur qui vient présenter sa recherche aux étudiants suivants le Cursus Master Ingénieur (CMI).
- séminaires des laboratoires de la fédération de recherche en Mathématiques (MARA) :
Prochains séminaires du LAMA :
EDPs²Jeudi 17 novembre 2022 à 14h
GéométrieJeudi 06 octobre 2022 à 14h, En salle TLR et sur Zoom : https://cnrs.zoom.us/j/97788860132?pwd=ZmNSeUwvWnByeUhzOUJXMlFtZDhSUT09
Résumé : (Masquer les résumés)
À venir
LIMDJeudi 29 septembre 2022 à 10h
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
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)