Venue: Grace Hopper room, Alan Turing Building, LIX, Ecole Polytechnique (Directions)
[Jump to Program]
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 mucalculus, and illustrate its proofsasprograms interpretation in the realm of reactive programs. Previous work emphasized the propositionsastypes part of the correspondence between LTL and FRP; here we additionally develop the proofsasprograms 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 metatheory 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 HigherOrder Abstract Syntax to Programmers
Binders in datastructures representing code or proofs can be represented in a variety of ways, from lowlevel firstorder representations such as de Bruijn indices to higherorder abstract syntax (HOAS), with nominal logic somewhere inbetween. HOAS is arguably the cleanest and highestlevel 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 lowerlevel primitives. It does so by compiling Beluga’s binders into an intermediate firstorder representation that abstracts over the eventual lowlevel representation, and by adapting MLstyle pattern compilation to the more general case of Beluga’s patterns.
Based on the PLPV’13 paper

Brigitte Pientka, Reasoning with HigherOrder Abstract Syntax and Contexts: A Comparative Study
A variety of logical frameworks support the use of higherorder abstract syntax (HOAS) in representing formal systems given via axioms and inference rules and reasoning about them. In such frameworks, objectlevel binding is encoded directly using metalevel 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 proofmanipulating programs. It can be used to write certificateissuing applications, like LCFlike 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 environmentfree 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 certificateissuing programs incremental, in particular type checkers.
Joint work with Y. RégisGianas

Olivier SavaryBé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, closureconversion 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 cutfree 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 infinitelike 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
Andrew Cave Francisco Ferreira Brigitte Pientka Olivier SavaryBélanger David Thibodeau 
David Baelde Kaustuv Chaudhuri Zakaria Chihani Matteo Cimini Lutz Straßburger 
PierreEvariste Dagand Matthias Puech 
Schedule
March 5, Tuesday
10:0011:00  Brigitte Pientka, Reasoning with HigherOrder Abstract Syntax and Contexts: A Comparative Study 
11:0012:00  Andrew Cave, Fair Reactive Programming 
12:0014:00  Lunch 
14:0015:00  David Thibodeau, Programming and Reasoning about Coinduction using Copatterns 
15:0016:00  Kaustuv Chaudhuri, Fixpoints and Equality in the Calculus of Structures 
16:0016:30  Lutz Straßburger, Cut Elimination in Nested Sequents for Intuitionistic Modal Logics 
March 6, Wednesday
10:0011:00  Matteo Cimini, A Congruence Format for Nominal SOS 
11:0012:00  Francisco Ferreira, Compiling Contextual Objects Bringing HigherOrder Abstract Syntax to Programmers 
12:0014:00  Lunch 
14:0015:00  Matthias Puech, Gasp: an OCaml library for manipulating LF objects 
15:0016:00  Olivier SavaryBélanger, Certified Code Transformations in Beluga 
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.