TYPES 2023: 29TH INTERNATIONAL CONFERENCE ON TYPES FOR PROOFS AND PROGRAMS
PROGRAM

Days: Monday, June 12th Tuesday, June 13th Wednesday, June 14th Thursday, June 15th

Monday, June 12th

View this program: with abstractssession overviewtalk overview

09:00-10:00 Session 2: Invited Talk. Verified Extraction from Coq to OCaml. Yannick Forster (Inria Nantes, France)

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.

10:00-11:00 Session 3: Proof assistants and proof technology
10:00
Decidable Type-Checking for Bidirectional Martin-Löf Type Theory (abstract)
10:20
Building an elaborator using extensible constraints (abstract)
10:40
From Lost to the River: Embracing Sort Proliferation (abstract)
11:00-11:30Coffee Break
11:30-12:30 Session 4: Foundations of type theory and constructive mathematics
11:30
Lax-Idempotent 2-Monads, Degrees of Relatedness, and Multilevel Type Theory (abstract)
11:50
Conservativity of Type Theory over Higher-order Arithmetic (abstract)
12:10
Enriched Categories in Univalent Foundations (abstract)
12:30-13:30 Session 5: Links between type theory and functional programming
12:30
Normal Form Bisimulations by Value (abstract)
12:50
Consequences of the modal unification of the functional calling paradigms (abstract)
13:10
Modal Types for Asynchronous FRP (abstract)
13:30-15:00Lunch Break
15:00-16:20 Session 6: Meta-theoretic studies of type systems
Chair:
15:00
A Logical Framework for Computational Type Theories (abstract)
15:20
Revisiting Containers in Cubical Agda (abstract)
15:40
Engineering logical relations for MLTT in Coq (abstract)
16:00
A Lock Calculus for Multimode Type Theory (abstract)
16:20-16:50Coffee Break
16:50-18:10 Session 7: Foundations of type theory and constructive mathematics
16:50
On epimorphisms and acyclic types in univalent type theory (abstract)
17:10
The ordinals in set theory and type theory are the same (abstract)
17:30
Diller-Nahm Bar Recursion (abstract)
17:50
Markov’s Principles in Constructive Type Theory (abstract)
Tuesday, June 13th

View this program: with abstractssession overviewtalk overview

09:00-10:00 Session 8: Invited Talk. The differentiation monad. Marie Kerjean (CNRS, France)

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.

10:00-11:00 Session 9: Formalizing mathematics using type theory
10:00
Classification of Covering Spaces and Canonical Change of Basepoint (abstract)
10:20
Choreographic Programming in Coq (abstract)
10:40
Dynamic Type Theory (abstract)
11:00-11:30Coffee Break
11:30-12:30 Session 10: Foundations of type theory and constructive mathematics
11:30
Towards an Interpretation of Inaccessible Sets in Martin-Löf Type Theory with One Mahlo Universe (abstract)
11:50
Categories as Semicategories with Identities (abstract)
12:10
New Observations on the Constructive Content of First-Order Completeness Theorems (abstract)
12:30-13:30 Session 11: Automation in computer-assisted reasoning
12:30
Embedding Differential Temporal Dynamic Logic in PVS (abstract)
12:50
A record expansion translation for Coq (abstract)
13:10
A graphical interface for diagrammatic proofs in proof assistants (abstract)
13:30-15:00Lunch Break
15:00-16:20 Session 12: Applications of type theory
15:00
Profinite lambda-terms and parametricity. (abstract)
15:20
Finite Combinatory Logic extended by a Boolean Query Language for Composition Synthesis (abstract)
15:40
A Formalization of Python's Execution Machinery (abstract)
16:00
Games and Strategies using Coinductive Types (abstract)
16:20-16:50Coffee Break
16:50-18:10 Session 13: Formalizing mathematics using type theory
16:50
Formalized non-wellfounded syntax through monoidal categories (abstract)
17:10
Categorical Logic in Lean (abstract)
17:30
Rezk Completion of Structured Categories (abstract)
17:50
Towards quotient inductive-inductive-recursive types (abstract)
Wednesday, June 14th

View this program: with abstractssession overviewtalk overview

09:00-10:00 Session 15: Invited Talk. Intersection and Simple types. Simona Ronchi Della Rocca (Università di Torino, Italy)

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.

10:00-11:00 Session 16: Foundations of type theory and constructive mathematics
10:00
Self-contained rules for classical and intuitionistic quantifiers (abstract)
10:20
Terms as Types: Calculations in the lambda-Calculus (abstract)
10:40
Monadic Realizability for Intuitionistic Higher-Order Logic (abstract)
11:00-11:30Coffee Break
11:30-12:30 Session 17: Links between type theory and functional programming
11:30
Operations On Syntax Should Not Inspect The Scope (abstract)
11:50
Partiality Wrecks GADTs' Functoriality (abstract)
12:10
Monadic Intersection Types (abstract)
12:30-13:30 Session 18: Meta-theoretic studies of type systems
12:30
The Rewster: The Coq Proof Assistant with Rewrite Rules (abstract)
12:50
On the Metatheory of Subtype Universes (abstract)
13:10
Nominal techniques as an Agda library (abstract)
13:30-15:00Lunch Break
15:00-16:20 Session 19: Applications of type theory
15:00
Program logics for ledgers (abstract)
15:20
Formalization of Blockchain Oracles in Coq (abstract)
15:40
A simple model of smart contracts in Agda (abstract)
16:00
Rank-polymorphic arrays within dependently-typed langauges (abstract)
16:20-16:50Coffee Break
Thursday, June 15th

View this program: with abstractssession overviewtalk overview

09:00-10:00 Session 20: Invited Talk. On Isomorphism Invariance and Isomorphism Reflection in Type Theory. Andrej Bauer (University of Ljubljana, Slovenia)

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

10:00-11:00 Session 21: Proof assistants and proof technology
10:00
Manifest Termination (abstract)
10:20
Extending cAERN to spaces of subsets (abstract)
10:40
Efficient Evaluation for Cubical Type Theories (abstract)
11:00-11:30Coffee Break
11:30-12:30 Session 22: Dependently typed programming
11:30
Categorical models of subtyping (abstract)
11:50
LayeredTypes - Combining dependent and independent type systems (abstract)
12:10
Towards dependent combinator calculus (abstract)
12:30-13:30 Session 23: Foundations of type theory and constructive mathematics
12:30
Higher coherence equations of semi-simplicial types as n-cubes of proofs (abstract)
12:50
Coinductive control of inductive data types (abstract)
13:10
Read the mode and stay positive (abstract)
13:30-15:00Lunch Break
15:00-16:20 Session 24: Links between type theory and functional programming
15:00
Types and Semantics of Extensible Data Types (abstract)
15:20
Extensional Equality Preservation in Intensional MLTT (abstract)
15:40
Composable partial functions in Coq, totally for free (abstract)
16:00
Towards a Translation from Liquid Haskell to Coq (abstract)