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…

Ulrik Buchholtz

Department of Mathematics, Technische Universität Darmstadt

What is an unordered pair of groups, or of categories, or of types? In homotopy type theory, the naive answer is a pair of a two-element type K and a function from K to whatever we’re taking pairs of. This definition has the downside that the type of unordered pairs in a set is no longer a set. For example, the unordered pairs in the unit type is the infinite dimensional real projective space.

I’ll explain how to define genuine unordered pairs using ideas from equivariant homotopy theory and prove that the genuine unordered pairs in a set is still a set. Then I’ll define genuine unordered triples and relate my troubles with them. Finally, I’ll explain why genuine multisets of arbitrary cardinality are really difficult.

Chair: Nicolai Kraus

Sara Negri

Department of Mathematics, University of Genoa

Chair: Hugo Herbelin

Notable parts of algebra and geometry can be formalized as coherent theories over first-order logic. Albeit wide, the class of coherent theories misses certain axioms in algebra such as the axioms of torsion abelian groups, Archimedean ordered fields, or the notion of transitive closure used in the theory of connected graphs and in the modelling of epistemic social notions such as common knowledge. All those examples can however be axiomatized by means of geometric axioms, a generalization of coherent axioms that includes infinitary disjunctions. We give a constructive proof of cut elimination for infinitary classical and intuitionistic sequent calculi for geometric theories. We then exploit their uniformity to obtain, purely by methods of structural proof theory, Glivenko-style conservativity results leading to the infinitary generalization of the first-order Barr theorem as a special case.

(Includes joint work with Giulio Fellin and Eugenio Orlandelli)

Stephanie Balzer

School of Computer Science, Carnegie Mellon University

In this talk I introduce the audience to linear session types through the lens of noninterference. Session types, as the types of message-passing concurrency, naturally capture what information is learned by the exchange of messages, facilitating the development of a flow-sensitive information flow control (IFC) type system guaranteeing noninterference. Noninterference ensures that an observer (adversary) cannot infer any secrets from made observations. I will explain the key ideas underlying the development of the IFC type system as well as the construction of the logical relation conceived to prove noninterference. The type system is based on intuitionistic linear logic and enriched with possible worlds to impose invariants on run-time configurations of processes, leading to a stratification in line with the security lattice. The logical relation generalizes existing developments for session-typed languages to open configuration to allow for a more subtle statement of program equivalence.

…