The Gallinette team is organizing a workshop on Dependent Type Theory on Wednesday, December 14th, 2022.

This workshop will take place the day after Loïc Pujet’s PhD defense in the math seminar room of Laboratoire Jean Leray.

(the math building is reachable from building 11 of LS2N)

Registration

Registration is free but mandatory.

Click here to register.

Online Participation

It will be possible to attend online via zoom (no need to register above). Please follow the instructions below.

Topic: Workshop on Type Theory in Nantes
Time: Dec 14, 2022 09:00 AM Paris

Join Zoom Meeting
https://univ-nantes-fr.zoom.us/j/83229163551?pwd=NkFQai93VXM1SUVaaVpFcCs4MmtaUT09

Meeting ID: 832 2916 3551
Passcode: 503560

Program

• 9:00-9:30am Welcome breakfast
• 9:30-10:30am : Favonia "An Order-Theoretic Analysis of Universe Polymorphism"
• 10:30-11:00am : Coffee Break
• 11:00am-12:00pm : Paige North "Directed homotopy type theory"
• 12:00-2pm Lunch Break
• 2:00-3:00pm : Jon Sterling " Controlling unfolding in type theory"
• 3:00-3:30pm : Open Discussion / Break
• 3:30-4:30pm : Loïc Pujet "Merging Martin Löf's identity type and setoid equality"

Detailed Progam

Favonia

"An Order-Theoretic Analysis of Universe Polymorphism"

Abstract We present a novel formulation of universe polymorphism in dependent type theory in terms of monads on the category of strict partial orders, and a novel algebraic structure, displacement algebras, on top of which one can implement a generalized form of McBride's “crude but effective stratification” scheme for lightweight universe polymorphism. We give some examples of exotic but consistent universe hierarchies, and prove that every universe hierarchy in our sense can be embedded in a displacement algebra and hence implemented via our generalization of McBride's scheme. Many of our technical results are mechanized in Agda, and we have an OCaml library for universe levels based on displacement algebras, for use in proof assistant implementations.

Paige North

"Directed homotopy type theory"

Abstract TBA

Jon Sterling

"Controlling unfolding in type theory":

Abstract We present a novel mechanism for controlling the unfolding of definitions in dependent type theory. Traditionally, proof assistants let users specify whether each definition can or cannot be unfolded in the remainder of a development; unfolding definitions is often necessary in order to reason about them, but an excess of unfolding can result in brittle proofs and intractably large proof goals. In our system, definitions are by default not unfolded, but users can selectively unfold them in a local manner. We justify our mechanism by means of elaboration to a core type theory with extension types, a connective first introduced in the context of homotopy type theory. We prove a normalization theorem for our core calculus and have implemented our system in the cooltt proof assistant, providing both theoretical and practical evidence for it.

Joint work with Daniel Gratzer, Carlo Angiuli, Thierry Coquand, and Lars Birkedal.

Loïc Pujet

"Merging Martin Löf's identity type and setoid equality"

Abstract TBA