Many type systems for programming languages include a notion of subtyping. Subtyping is often defined syntactically by a formal system, but this gets increasingly complex when union, intersection, and negation types are introduced.

In the semantic subtyping approach, instead, types are interpreted as sets and subtyping is defined in terms of set containment. Then, an algorithm is derived from the definition. While the algorithm is complex, the interpretation of types serves as a fairly simple specification. This approach also ensures that union and intersection on types behave as the corresponding operations on sets.

I will give an introduction to this approach and show how to define subtyping semantically for types including arrows, union, intersection, and negation, following [Frisch et al., 2008]. Then, we will look at ongoing work on adapting this approach (originally studied for call-by-value languages) to lazy semantics.

[Frisch et al., 2008] A. Frisch, G. Castagna, and V. Benzaken, Semantic subtyping, JACM, 2008.

Distributed protocols such as Paxos play an important role in many computer systems. Therefore, a bug in a distributed protocol may have tremendous effects. Accordingly, a lot of effort has been invested in verifying such protocols. However, checking invariants of such protocols is undecidable and hard in practice, as it requires reasoning about an unbounded number of nodes and messages. Moreover, protocol actions and invariants involve higher-order concepts such as set cardinalities, arithmetic, and complex quantification.

This paper makes a step towards automatic verification of such protocols. We aim at a technique that can verify correct protocols and identify bugs in incorrect protocols. To this end, we develop a methodology for deductive verification based on effectively propositional logic (EPR)—a decidable fragment of first-order logic (also known as the Bernays-Sch\“onfinkel-Ramsey class). In addition to decidability, EPR also enjoys the finite model property, allowing to display violations as finite structures which are intuitive for users. Our methodology involves modeling protocols using general (uninterpreted) first-order logic, and then systematically transforming the model to obtain a model and an inductive invariant that are decidable to check. The steps of the transformations are also mechanically checked, ensuring the soundness of the method. We have used our methodology to verify the safety of Paxos, and several of its variants, including Multi-Paxos, Vertical Paxos, Fast Paxos and Flexible Paxos. To the best of our knowledge, this work is the first to verify these protocols using a decidable logic, and the first formal verification of Vertical Paxos and Fast Paxos.

This is joint work with O. Padon, M. Sagiv, and S. Shoham.

Elizalde (2011) a caractérisé les permutations qu'on obtient en ordonnant des éléments consécutifs dans une trajectoire d'une $\beta$-transformation, avec une base $\beta$ positive. Le cas d'une base $\beta$ entière correspond au full shift sur $\beta$ lettres, qui a été étudié par Amigó, Elizalde et Kennel (2008). Nous considérons les bases négatives. Travail en commun avec Émilie Charlier.

We discuss the problem of equality in type theory. We present an approach to defining higher equality structures in type theory. As an application, we study the lambda calculus from the multi-dimensional point of view. Taking equality between lambda terms (1-cells) to be beta conversion modulo permutation of redexes, we discover that the induced higher structure is a homotopy 1-type. That is, whenever there exists a higher cell between two β-conversions, the space of such cells is contractible. The key property of the lambda calculus responsible for this is Lévy’s projection calculus (AKA calculus of residuals). We conclude that the result holds for any theory which admits a presentation with such a calculus. For example, all (weakly) orthogonal TRSs describe homotopy 1-types.

We investigate monads of partiality in Martin-Löf type theory, following Moggi’s general monad-based method for modelling effectful computations. These monads are often called lifting monads and appear in category theory with different but related definitions. In this talk, we unveil the relation between containers and lifting monads. We show that the lifting monads usually employed in type theory can be specified in terms of containers. Moreover, we give a precise characterization of containers whose interpretations carry a lifting monad structure. We show that these conditions are tightly connected with Rosolini’s notion of dominance. We provide several examples, putting particular emphasis on Capretta’s delay monad and its quotiented variant, the non-termination monad.