Workshop on Formal Meta-Theory

Theme

The topic of the workshop is the representation, manipulation, and reasoning about programming languages, formal proofs, and deductive systems in general. Such systems generally contain binding constructs and therefore require sophisticated techniques for contextual and generic reasoning.

Contributed Talks

• Andrew Cave, Fair Reactive Programming

  Functional Reactive Programming (FRP) models reactive systems with events and signals, which have previously been observed to correspond to the “eventually” and “always” modalities of linear temporal logic (LTL). In this talk, I illustrate a constructive variant of LTL with least fixed point and greatest fixed point operators in the spirit of the modal mu-calculus, and illustrate its proofs-as-programs interpretation in the realm of reactive programs. Previous work emphasized the propositions-as-types part of the correspondence between LTL and FRP; here we additionally develop the proofs-as-programs part. I illustrate that this type system can express liveness properties such as the fairness of schedulers and the eventual delivery of results.

  Joint work with F. Ferreira, B. Pientka, and P. Panangaden

• Kaustuv Chaudhuri, Fixpoints and Equality in the Calculus of Structures

  The calculus of structures is a proof system that represents all proof steps as rewrite rules that can apply in any formula context. It has some benefits over the sequent calculus in representing proofs, as it allows more freedom in the order of the rewrite steps. It is also a newer formalism than the sequent calculus and has not been applied to as many tasks. In this talk, I will show how to extend the calculus of structures to support fixpoints and equality while retaining its incremental and local nature. If time permits, I will sketch how to add nominal quantification as well. Most of this stuff is work in progress.

• Matteo Cimini, A Congruence Format for Nominal SOS

  Structural Operational Semantics (SOS) is one of the most natural ways for providing programming languages with a formal semantics. Results on the meta-theory of SOS typically state that if the syntax that is employed in writing a semantic specification conforms to some syntactic template then certain property is guaranteed to hold for the specified language. These syntactic templates are called rule formats. In this talk, we focus on Nominal SOS, a formalization of SOS with explicit syntax and primitives for the specification of languages with binders. We offer a rule format for Nominal SOS that guarantees that bisimilarity is a congruence. We show the applicability of the format to π-calculus and (a modified) λ-calculus, and we recover congruence for two classic equivalences, Sangiorgi’s open bisimilarity and Abramsky’s applicative bisimilarity.

• Francisco Ferreira, Compiling Contextual Objects Bringing Higher-Order Abstract Syntax to Programmers

  Binders in data-structures representing code or proofs can be represented in a variety of ways, from low-level first-order representations such as de Bruijn indices to higher-order abstract syntax (HOAS), with nominal logic somewhere in-between. HOAS is arguably the cleanest and highest-level representation but comes with significant problems in expressiveness and efficiency. In this talk, I will describe a scheme to solve the remaining efficiency concern by showing how to compile Beluga pattern matching down to lower-level primitives. It does so by compiling Beluga’s binders into an intermediate first-order representation that abstracts over the eventual low-level representation, and by adapting ML-style pattern compilation to the more general case of Beluga’s patterns.

  Based on the PLPV’13 paper

• Brigitte Pientka, Reasoning with Higher-Order Abstract Syntax and Contexts: A Comparative Study

  A variety of logical frameworks support the use of higher-order abstract syntax (HOAS) in representing formal systems given via axioms and inference rules and reasoning about them. In such frameworks, object-level binding is encoded directly using meta-level binding. Although these systems seem superficially the same, they differ in a variety of ways. In this talk, we concentrate on how systems handle a context of assumption. In particular, we compare two proof styles, the generalized context approach and the context relation approach.

  Based on joint work with Amy Felty and Alberto Momigliano

• Matthias Puech, Gasp: an OCaml library for manipulating LF objects

  We present a compact OCaml library, Gasp, that helps writing term- and proof-manipulating programs. It can be used to write certificate-issuing applications, like LCF-like interactive theorem provers, certifying compilers or type checkers. These certificates, expressed in the LF logical framework, are verified dynamically as they are produced and consumed. In particular, we introduce the environment-free style for computing on open objects, supported by function inverses. After presenting its interface and use, we will discuss its implementation, notably the underlying representation of LF objects and typed evaluation algorithm. Finally, we will show that by changing the base representation from LF to Contextual LF, we can leverage function inverses to make certificate-issuing programs incremental, in particular type checkers.

  Joint work with Y. Régis-Gianas

• Olivier Savary-Bélanger, Certified Code Transformations in Beluga

  Certified compilation is desirable, but its cost in general programming environments, in term of development time and complexity, has so far limited its use. In this project, we explore program transformations’ certification enforced through more precise types. We implemented a type preserving compilation pipeline composed of CPS, closure-conversion and hoisting over the simply typed lambda calculus. In this talk, we will present an overview of the motivation of programming safe code transformation in Beluga, and of different challenges encountered during the development.

  Joint work with M. Boespflug, B. Pientka, and S. Monnier

• Lutz Straßburger, Cut Elimination in Nested Sequents for Intuitionistic Modal Logics

  We present cut-free deductive systems without labels for the intuitionistic variants of the modal logics obtained by extending IK with a subset of the axioms d, t, b, 4, and 5. For this, we use the formalism of nested sequents, which allows us to give a uniform cut elimination argument for all 15 logic in the intuitionistic S5 cube.

  Based on the FoSSaCS 2013 paper

• David Thibodeau, Programming and Reasoning about Coinduction using Copatterns

  Programs with infinite-like behaviour such as operating systems and input/output devices can be mathematically modelled with coinduction, the dual notion of induction. While the latter is well understood and programming languages and proof systems offer extensive support to represent inductive objects, current representations of coinduction in such systems have been proven to be unsatisfactory, either because their lack of elegance makes them difficult to use and reason about, or because they break desirable properties.

  This talk presents a calculus exploiting the duality between induction and coinduction to obtain a symmetric language mixing both finite and infinite data and whose operational semantics is based on copattern matching. This last device allows us to synthesize data by expressing what are the observations that we can make on the coinductive object. Starting from a simply typed setting, we then present how these ideas can extend to Beluga’s dependent types.

  Joint work with A. Abel, B. Pientka, and A. Setzer published at POPL’13

Participants

Schedule

March 5, Tuesday

March 6, Wednesday

Support and Organization

This workshop will be hosted by the Laboratoire d’Informatique (LIX) and by INRIA Saclay. Funding is provided by the INRIA Associated Team RAPT and by the CPCFQ.