These seminars are common with the Plume team (ENS Lyon) and are held in the seminar room, second floor of the building Le Chablais, on the Bourget-du-lac (Savoy) site or at ENS Lyon.

## Next seminar:

**Thursday 12th March 2020 at 10h
**
Variés
(Variées),
*Séminaire Chocola*

The seminar of the team LIMD is under the responsibility of
Sebastien Tavenas.

**Settings:**
See with
increasing date
.
Hide abstracts

Other years: 2005, 2006, 2007, 2008, 2009, 2010, 2011, 2012, 2013, 2014, 2015, 2016, 2017, 2018, 2019,
all years together.

# Year 2020

**Thursday 14th May 2020 at 10h
**
Variés
(Variées),
*Séminaire Chocola*

**Thursday 2nd April 2020 at 10h
**
Variés
(Variées),
*Séminaire Chocola*

**Thursday 12th March 2020 at 10h
**
Variés
(Variées),
*Séminaire Chocola*

**Thursday 13th February 2020 at 10h
**
Davide Barbarossa
(LIPN (Paris 13)),
*Taylor Subsumes Scott, Berry, Kahn and Plotkin*

Abstract:(Hide abstracts)

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.

**Thursday 6th February 2020 at 10h
**
Variés
(Variées),
*Séminaire Chocola*

**Thursday 30th January 2020 at 10h
**
Luc Pellissier
(Inria et LIX),
*TBA*

Abstract:(Hide abstracts)

TBA

**Thursday 16th January 2020 at 10h
**
Chaitanya Leena Subramaniam
(IRIF),
*Dependent type theories as ``cellular'' Lawvere theories*

Abstract:(Hide abstracts)

(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.

The seminar of the team LIMD is under the responsibility of
Sebastien Tavenas.

**Settings:**
See with
increasing date
.
Hide abstracts

Other years: 2005, 2006, 2007, 2008, 2009, 2010, 2011, 2012, 2013, 2014, 2015, 2016, 2017, 2018, 2019,
all years together.