Rencontre, 15 mai 2025

Programme

10:30 – 12:00

Daniel Gratzer (Aarhus University)

Invited talk: Modal dependent type theory and synthetic category theory

In this talk, we discuss the process of extending Martin-Löf dependent type theory with one or more modalities: special unary type constructors distinguished by their relatively poor behavior. We introduce a proposed class of modalities—weak dependent right adjoints—which proven flexible enough to accommodate many interesting examples (guarded recursion, internalized parametricity, cohesion, etc.) but still rigid enough to admit a calculus with good syntactic properties. We show then how these weak dependent right adjoints may be assembled into a general framework for modal type theory (MTT). Finally, time permitting, we highlight a recent application of MTT to Riehl and Shulman's theory of synthetic ∞-categories.

This talk contains joint work with Alex Kavvos, Andreas Nuyts, Lars Birkedal, Jonathan Weinberger, and Ulrik Buchholtz.

13:45 – 14:45

Elies Harington (LIX and LIPN)

Invited talk: ∞-categorical models of linear logic : higher polynomials, higher species

The notion of categorical model of linear logic is now well studied and established around the notion of linear-non-linear adjunction, which encompasses the previous notions of Seely categories, Lafont categories and linear categories. These categorical structures have counterparts in the realm of ∞-categories, which can thus be thought of as "weak", or "homotopical" models of linear logic. In this talk, we give a tour of categorical semantics of linear logic, and show examples of ∞-categorical models generalizing polynomial functors, generalized species, and models from linear algebra.

15:15 – 16:15

Hiroshi Unno (Research Institute of Electrical Communication, Tohoku University)

Invited talk: Refinement Types and Higher-Order Model Checking for Algebraic Effects and Handlers

Algebraic effects and handlers provide a modular way to structure programs with computational effects and are increasingly adopted in practical programming languages such as OCaml. Their expressivity and utility stem from the capability to manipulate delimited continuations. However, delimited continuations also introduce complex control flows, making program verification more challenging.

In this talk, we present two complementary approaches to verifying programs with algebraic effects and handlers. Both approaches are based on Answer Type Modification (ATM), which enables type systems to precisely track what effects occur and in what order during program execution, reflecting this information as modifications to the answer types of delimited continuations. However, they use ATM in different ways.

The first approach introduces a novel dependent refinement type system for algebraic effects and handlers. This system incorporates a mechanism called Answer Refinement Modification (ARM), which can be seen as a specialization of ATM that applies modifications to the refinement predicates of answer refinement types. We automate refinement type checking and inference for the system by reducing them to solving Constrained Horn Clauses (CHCs) and integrating with existing CHC solvers, and have implemented this approach in RCaml, a refinement type-based verifier for OCaml.

The second approach extends higher-order model checking (HOMC) to programs with algebraic effects and handlers. While HOMC achieves decidability for pure higher-order programs with finite data domains, simply adding algebraic effects and handlers makes model checking undecidable due to the potential for an unbounded number of active handlers. To address this, we propose restricting programs using ATM, thereby bounding the number of active handlers. Under this restriction, the model checking problem becomes decidable again while still supporting a wide range of practical effects. To enable reuse of existing HOMC tools for pure programs, we present a CPS transformation that reduces the model checking of programs with algebraic effects and handlers to that of pure programs. We have implemented this approach in EffCaml, a transformation-based verifier for OCaml, which incorporates a type inference algorithm for our type system with ATM, the CPS transformation, and integration with HOMC tools.