Section: New Results

Effects in proof theory and programming

Participants : Hugo Herbelin, Gabriel Lewertowski, Étienne Miquey, Alexis Saurin, Matthieu Sozeau.

A classical sequent calculus with dependent types

Dependent types are a key feature of type systems, typically used in the context of both richly-typed programming languages and proof assistants. Control operators, which are connected with classical logic along the proof-as-program correspondence, are known to misbehave in the presence of dependent types [11], unless dependencies are restricted to values. As a step in his work to develop a sequent-calculus version of Hugo Herbelin's $dP{A}_{\omega }$ system [13], Étienne Miquey proposed a sequent calculus with classical logic and dependent types. His calculus—named dL—is an extension of the $\mu \tilde{\mu }$-calculus with a syntactical restriction of dependent types to the fragment of negative-elimination free proofs. The corresponding type system includes a list of explicit dependencies, which maintains type safety. He showed that a continuation-passing style translation can be derived by adding delimited continuations, and how a chain of dependencies can be related to a manipulation of the return type of this continuations. This work has been accepted for publication at ESOP 2017 [39].

Logical foundations of call-by-need evaluation

Alexis Saurin, in collaboration with Pierre-Marie Pédrot, extended their reconstruction of call-by-need based on linear head reduction with control. They showed how linear head reduction could be adapted to the $\lambda \mu$-calculus. This classical linear head reduction lifts the usual properties of the intuitionistic one (with respect to $\sigma$-equivalence) to the $\lambda \mu$-calculus (and its $\sigma$-equivalence already formulated by Olivier Laurent in his PhD thesis). Moreover, they showed that substitution sequences of the $\lambda \mu$-calculus' linear head reduction are in correspondence with the classical Krivine abstract machine substitution sequences, validating the known fact that the KAM implements linear head reduction. This work has been published at ESOP'16 [29]. They plan to lift to the $\lambda \mu$-calculus their three-step transformation from linear head reduction to call-by-need, and to study the correspondence with Ariola, Herbelin and Saurin's classical call-by-need.

Call-by-name forcing for Dependent Type Theory

Guilhem Jaber, Gabriel Lewertowski, Pierre-Marie Pédrot, Matthieu Sozeau, and Nicolas Tabareau studied a variant of the forcing translation for dependent type theory, moving from the call-by-value variant to a call-by-name version which naturally preserves definitional equalities, avoiding the coherence pitfalls of the former one. This new version was inspired by Pierre-Marie Pédrot's former decomposition of forcing in call-by-push-value. It allows to show various metatheoretical results in a succint fashion, notably for the independence of axioms. Work is ongoing to produce more positive results including abstracting reasoning on step-indexing using this technique. This work was presented at LICS 2016 [28].

Classical realizability and implicative algebras

Étienne Miquey has been working with Alexandre Miquel in Montevideo on the topic of implicative algebras. Implicative algebras are an algebraization of the structure needed to develop a realizability model. In particular, they give rise to the usual ordered combinatory algebras and thus to the triposes used to model classical realizability. An implicative algebra is given by an implicative structure (which consists of a complete semi-lattice with a binary operation $\to$) together with a separator containing the element interpreted as true in the structure. Étienne Miquey has been working on a formalization of implicative algebras theory in Coq. Following the work of Guillaume Munch-Maccagnoni on focalization and classical realizability, he also worked on alternative presentations within structures based on other connectives, (negation, “par”, tensor), rather than $\to$. Such connectives correspond to the decomposition of the arrow according to the strategy of evaluation (call-by-name/call-by-value). The aim of this work is to obtain a classification of the possible algebraic structures to interpret classical realizability, in order to prove that different strategies of evaluation actually provide us with equivalent models.