TYPES 2023
29th International Conference on Types for Proofs and Programs


Andrej Bauer (University of Ljubljana, Slovenia)

On Isomorphism Invariance and Isomorphism Reflection in Type Theory

Isomorphism Invariance, also called the Principle of Isomorphism and the Principle of Structuralism, is the idea that isomorphic mathematical objects share the same structure and relevant properties, or that whatever can reasonably be done with an object can also be done with an isomorphic copy

Isomorphism Invariance: “If A ≅ B and Φ(A) then Φ(B).”

Without any limitation on Φ, we may take Φ(X) to be A = X and obtain:

Isomorphism Reflection: “If A ≅ B then A = B.”

Conversely, Isomorphism Reflection implies Isomorphism Invariance by Leibniz's Identity of Indiscernibles.

Depending on how we interpret ≅ and =, these principles might be plainly false, uninspiringly true, or a foundational tenet:

  1. In set theory, if ≅ is existence of a bijection, the principles are false.
  2. In set theory, if ≅ is isomorphism of sets qua ∈-structures, both principles are true because Isomorphism Reflection is just the Extensionality axiom.
  3. In type theory, if = is propositional equality and ≅ is equivalence of types, Isomorphism Reflection is (a consequence of) the Univalence axiom.

While Isomorphism Invariance is widely used in informal practice, with ≅ understood as existence of structure-preserving isomorphism, Isomorphism Reflection seems quite unreasonable because it implies bizarre statements, e.g., that there is just one set of size one. Any formal justification of the former must therefore address the tension with the latter principle.

In this talk I will review what is known about the formal treatment of the principles, recall the cardinal model of type theory by Théo Winterhalter and myself which shows that Isomorphism reflection is consistent when = is taken as judgemental equality, and discuss the possibility of having other models validating judgemental Isomorphism reflection that might be compatible with non-classical reasoning principles. I shall also touch on the possibility of a restricted form of Isomorphism reflection that would provide a satisfactory formal definition of “canonical isomorphism”.

Simona Ronchi della Rocca (Università di Torino, Italy)

Title: Intersection and Simple types

When, in the seventies of the last century, Coppo and Dezani designed intersection types, their main motivation was to extend the typability power of simple types, adding them an intersection connective, enjoying associativity, commutativity and idempotency, so denoting set formation. In fact, the simple types system can be seen as a restriction of the intersection type system where all sets are singletons. Quite early intersection types turned out to be useful in characterizing qualitative properties of λ-calculus, like solvability and strong normalization, and in describing models of λ-calculus in various settings. A variant of intersection types, where the intersection is no more idempotent, has been recently used to explore quantitative properties of programming language, like the length of the normalisation procedure. It is natural to ask if there is a quantitative version of the simple type system, or more precisely a decidable restriction of non-idempotent intersection system with the same typability power of simple types. Since the lack of idempotency, now the intersection corresponds to multiset formation, so (extending the previous reasoning) the natural answer is to restrict the multiset formation to copies of the same type. But this answer is false, the so obtained system is decidable, but it has less typability power than simple types. We prove that the desired system is obtained by restricting the multiset formation to equivalent types, where the equivalence is an extension of the identity, modulo the cardinality of multisets.

Marie Kerjean (LIPN, CNRS, Université Sorbonne Paris Nord, France)

Title: The differentiation monad

In this talk, we will see how a twist in the continuation monad allows us to express the quantitative semantics of programs. I will explain how this new monad comes from the search for a fourth missing rule in Differential Linear Logic, an extension of Linear Logic allowing for the linearization of proofs. Finally, we will dive into concrete interpretations of this monad and put forward the link with graded monads.

Yannick Foster (Inria Nantes, France)

Title: Verified Extraction from Coq to OCaml

A central claim to fame of the Coq proof assistant is extraction to languages like OCaml, centrally used in landmark projects such as CompCert. Extraction was initially conceived and implemented by Pierre Letouzey, and is still guiding design decisions of Coq's type theory. While the core extraction algorithm is verified on paper, central features like optimisations --of which there are 10 the user can enable-- only have empirical correctness guarantees.

In the scope of the MetaCoq project, which aims at placing Coq's type theory on a well-defined and fully formal foundation, I am working with other members of the MetaCoq team on a re-implementation and verification of all aspects of Coq's extraction process to OCaml. The new extraction process is based on a formal semantics of Coq as provided by MetaCoq and a formal semantics of the intermediate language of the OCaml compiler derived from the Malfunction project.

In my talk, I plan on discussing the current state of this verification, its goals, possible extensions, and design decisions along the way, a discussion of the trusted computing and theory bases (and in particular ideas for reducing them), arising problems with Coq and the surrounding infrastructure, and the impact on other projects. I will conclude with thoughts on how other proof assistants can learn and benefit from the lessons we have learned.