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

In the scope of the MetaCoq project, which aims at placing Coq's typetheory on a well-defined and fully formal foundation, I am working withother members of the MetaCoq team on a re-implementation andverification of all aspects of Coq's extraction process to OCaml. Thenew extraction process is based on a formal semantics of Coq asprovided by MetaCoq and a formal semantics of the intermediate languageof the OCaml compiler derived from the Malfunction project.

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

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.

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.

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