Le séminaire de l’équipe LIMD est sous la responsabilité de Sebastien Tavenas.
Options : Voir par date décroissante. Masquer les résumés.
Autres années : 2005, 2006, 2007, 2008, 2009, 2010, 2011, 2012, 2013, 2014, 2015, 2016, 2017, 2018, 2019, 2021, 2022, toutes ensemble.

Année 2020

Jeudi 16 janvier 2020 à 10h Chaitanya Leena Subramaniam (IRIF),
Dependent type theories as ``cellular'' Lawvere theories

Résumé : (Masquer les résumés)
(Joint work with P. LeFanu Lumsdaine.)
Lawvere theories and (coloured) operads provide particularly nice representations for suitable algebraic theories with a given set of sorts, as monoids in certain categories of collections.
We extend this to dependent type theories: For an inverse category C, we show how suitable “C-sorted type theories” may be viewed (1) as monoids in a category of collections, and (2) as generalised Lawvere theories in the sense of Berger–Melliès–Weber. Moreover, (essentially) every dependent type theory arises in this way.
Inverse categories are known from homotopy theory, where they (or their opposite categories) provide a good notion of a category of ``cells''. Examples are the category of semi-simplices, the category of globes, the category of opetopes, etc.

Jeudi 30 janvier 2020 à 10h Luc Pellissier (Inria et LIX),
TBA

Résumé : (Masquer les résumés)
TBA

Jeudi 06 février 2020 à 10h, ENS Lyon Variés (Variées),
Séminaire Chocola

Jeudi 13 février 2020 à 10h Davide Barbarossa (LIPN (Paris 13)),
Taylor Subsumes Scott, Berry, Kahn and Plotkin

Résumé : (Masquer les résumés)
The speculative ambition of replacing the old theory of program approximation based on syntactic continuity with the theory of resource consumption based on Taylor expansion and originating from the differential λ-calculus is nowadays at hand. Using this resource sensitive theory, we provide simple proofs of important results in λ-calculus that are usually demonstrated by exploiting Scott’s continuity, Berry’s stability or Kahn and Plotkin’s sequentiality theory. A paradigmatic example is given by the Perpendicular Lines Lemma for the Böhm tree semantics, which is proved here simply by induction, but relying on the main properties of resource approximants: strong normalization, confluence and linearity.

Jeudi 12 mars 2020 à 10h, ENS Lyon Variés (Variées),
Séminaire Chocola

Jeudi 02 avril 2020 à 10h, ENS Lyon Variés (Variées),
Séminaire Chocola

Jeudi 14 mai 2020 à 10h, ENS Lyon Variés (Variées),
Séminaire Chocola

Le séminaire de l’équipe LIMD est sous la responsabilité de Sebastien Tavenas.
Options : Voir par date décroissante. Masquer les résumés.
Autres années : 2005, 2006, 2007, 2008, 2009, 2010, 2011, 2012, 2013, 2014, 2015, 2016, 2017, 2018, 2019, 2021, 2022, toutes ensemble.