Henning – Page 2 – TYPES 2021

Pierre-Marie Pédrot

Gallinette Team, Inria Rennes-Bretagne-Atlantique

All your base categories are belong to us: A syntactic model of presheaves in type theory

Presheaves are a staple categorical structure, which naturally arises in a wide variety of situations. In the realm of logic, they are often used as a model factory. Indeed, presheaves over some base category will result in a topos, whose contents can be fine-tuned by carefully picking the base category. As computer scientists, though, we have learnt that there are even better logical systems than toposes: dependent type theories! Through the Curry-Howard mirror, they are also full-blown functional programming languages that actually compute.

This begs the following question: is it possible to build the type-theoretic equivalent of presheaves, while retaining the good computational properties of our dependent programming languages? We will see that strikingly enough, presheaves can already be presented as computational objects to some extent, except for the annoying fact…

Author: Henning

Working Groups

Computation and Intersection Types

The syntactic tale of the oracle and the trees A model of continuity in a dependent setting

Novel rules of β-conversion in partial type theory

A Gradual Intersection Typed Calculus

Intersection Types for a Computational λ-Calculus with Global State

New Type Theories

Using Two-Level Type Theory for Staged Compilation

Type theories without contexts

Syntax for two-level type theory

Native Type Theory

Functorial Adapters

Lunch

Inductive Types

Simulating large eliminations in Cedille

Quotient inductive-inductive types in the setoid model

Eliminating Infinitary Induction-induction

Recursion

Type-Theoretic Constructions of the Final Coalgebra of the Finite Powerset Functor

Size-Based Termination for Non-Positive Types

M-Types and Bisimulation

Constructive Notions of Ordinals in Homotopy Type Theory

All your base categories are belong to us

All your base categories are belong to us: A syntactic model of presheaves in type theory

Genuine pairs and the trouble with triples in homotopy type theory

On the constructive content of infinitary classical theories

Break