We’re now well past the autumn season, but paper leaves are still stacking up in Gallium. Here are a few drafts we’ve produced in these last few months. You may be interested in having a look, and of course we warmly welcome feedback.

Type Soundness and Race Freedom for Mezzo

Thibaut Balabonski, François Pottier and Jonathan Protzenko describe the mechanized formalization effort that went alongside the design and implementation of Mezzo. Of course, the corresponding Coq development is also available.

Draft: http://gallium.inria.fr/~fpottier/publis/bpp-mezzo.pdf
Coq formalization: http://gallium.inria.fr/~fpottier/mezzo/mezzo-coq.tar.gz

The programming language Mezzo is equipped with a rich type system that controls aliasing and access to mutable memory. We present a modular formalization of Mezzo’s core type system, in the form of a concurrent λ-calculus, which we extend with references and locks. We prove that well-typed programs do not go wrong and are data-race free. Our definitions and proofs are machine-checked.

System F with Coercion Constraints

Julien Cretin and Didier Rémy have a research report on this considerable generalization of their previous work on coercion abstraction. This work is also part of Julien’s PhD thesis, which he expertly presented last Friday, and is also entirely formalized in Coq.

Research Report: http://hal.inria.fr/hal-00934408
Coq formalization: https://github.com/ia0/fcc
Coqdoc documentation: http://phd.ia0.fr/coq/Index.html#Index_v

We present a second-order lambda-calculus with coercion constraints that generalizes a previous extension of System F with parametric coercion abstractions by allowing multiple but simultaneous type and coercion abstractions, as well as recursive coercions and equi-recursive types. This allows to present in a uniform way several type system features that had previously been studied separately: type containment, bounded and instance-bounded polymorphism, which are already encodable with parametric coercion abstraction, and ML-style subtyping constraints. Our framework allows for a clear separation of language constructs with and without computational content. We also distinguish coherent coercions that are fully erasable from potentially incoherent coercions that suspend the evaluation – and enable the encoding of GADTs.

Technically, type coercions that witness subtyping relations between types are replaced by a more expressive notion of typing coercions that witness subsumption relations between typings, e.g. pairs composed of a typing environment and a type. Our calculus is equipped with a strong notion of reduction that allows reduction under abstractions-but we also introduce a form of weak reduction as reduction cannot proceed under incoherent type abstractions. Type soundness is proved by adapting the step-indexed semantics technique to strong reduction strategies, moving indices inside terms so as to control the reduction steps internally.

Multi-focusing on extensional rewriting with sums

This work is a byproduct of my (Gabriel Scherer) foray into the proof search literature, wondering which types have unique inhabitants. Some of what I’ve been trying to sketch up turned out to be rather close to “multi-focusing”, a promising approach to canonicity of syntactic proof calculi, so I decided to spend some time working on that notion.

http://gallium.inria.fr/~scherer/drafts/multifoc-long.pdf

We propose a logical justification for the rewriting-based equivalence procedure for simply-typed lambda-terms with sums of Lindley. It relies on maximally multi-focused proofs, a notion of canonical derivations introduced for linear logic. Lindley’s rewriting closely corresponds to rewriting, a technical device used in the meta-theory of maximal multi-focus.

(You might be thinking that this entry stands out for not having a mechanized formalization. I agree. Working in Gallium can be pressuring at times.)