Conference Programme

FSCD Business Meeting

22 June 2016 09:00-10:00
Compositional Compiler Verification for a Multi-Language World

Verified compilers are typically proved correct under severe restrictions on what the compiler's output may be linked with, from no linking at all to linking only with code compiled from the same source language. Such assumptions contradict the reality of how we use these compilers since most software systems today are comprised of components written in different languages compiled by different compilers to a common target, as well as low-level libraries that may be handwritten in the target language. The key challenge in verifying compilers for today's world of multi-language software is how to formally state a compiler correctness theorem that is compositional along two dimensions. First, the theorem must guarantee correct compilation of components while allowing compiled code to be composed (linked) with target-language components of arbitrary provenance, including those compiled from other languages. Second, the theorem must support verification of multi-pass compilers by composing correctness proofs for individual passes.  In this talk, I will describe a methodology for verifying compositional compiler correctness for a higher-order typed language and discuss the challenges that lie ahead. I will argue that compositional compiler correctness is, in essence, a language interoperability problem: for viable solutions in the long term, we need "economical" means of specifying interoperability between high-level and low-level components, and between more precisely and less precisely typed code.


22 June 2016 10:30-12:30
Strong normalization for the parameter-free polymorphic lambda calculus based on the Omega-rule
Ryota Akiyoshi and Kazushige Terui

Strongly Normalising Cyclic Data Computation by Iteration Categories of Second-Order Algebraic Theory
Makoto Hamana

Ground Confluence Prover based on Rewriting Induction
Takahito Aoto and Yoshihito Toyama

Certifying Confluence of Almost Orthogonal CTRSs via Exact Tree Automata Completion
Christian Sternagel and Thomas Sternagel


22 June 2016 14:00-16:00
Structural Interactions and Absorption of Structural Rules in BI Sequent Calculus
Ryuta Arisaka

Focusing in Orthologic
Olivier Laurent

Modular Focused Proof Systems for Intuitionistic Modal Logics
Kaustuv Chaudhuri, Sonia Marin and Lutz Strassburger

Minimal Paradefinite Logics for Reasoning with Incompleteness and Inconsistency
Ofer Arieli and Arnon Avron


22 June 2016 16:30-18:00
Homological Computations for Term Rewriting Systems
Philippe Malbos and Samuel Mimram

Globular: a proof assistant for higher rewriting
Krzysztof Bar, Aleks Kissinger and Jamie Vicary

Category Theory in Coq 8.5
Amin Timany and Bart Jacobs

FSCD Business Meeting

23 June 2016 09:00-10:00
Verified Analysis of Functional Data Structures

This talk reports on some recent work on the analysis of both functional correctness and amortized complexity of a number of classical data structures in a functional setting. First we will present an approach to the automatic verification of search tree algorithms. The key idea here is to base the verification on the list resulting from the inorder traversal of a search tree. The functional correctness of a number of classical search trees (e.g. AVL trees, red-black trees and splay trees) could be verified automatically in this manner (including the search tree invariant but excluding further structural invariants). Then we will present a framework for the interactive verification of the amortized complexity of functional data structures and show how it can be applied to a number of classical heap and search tree algorithms.


23 June 2016 10:30-12:30
Environmental bisimulations for delimited-control operators with dynamic prompt generation
Andrés Aristizábal, Dariusz Biernacki, Sergueï Lenglet and Piotr Polesiuk

Synthesis of Functional Programs with Help of First-order Intuitionistic Logic
Marcin Benke, Aleksy Schubert and Daria Walukiewicz-Chrząszcz

Reversible Term Rewriting
Naoki Nishida, Adrian Palacios and German Vidal

Formal Languages, Formally and Coinductively
Dmitriy Traytel


23 June 2016 14:00-16:00
Weighted Relational Models for Mobile Names
James Laird

New Results on Morris's Observational Theory: the benefits of separating the inseparable
Flavien Breuvart, Giulio Manzonetto, Andrew Polonsky and Domenico Ruoppolo

Classical extraction in continuation models
Valentin Blot

On Undefined and Meaningless in Lambda Definability
Fer-Jan de Vries


23 June 2016 16:30-18:00
The Intersection Type Unification Problem
Andrej Dudenhefner, Jakob Rehof and Moritz Martens

Functions-as-constructors Higher-order Unification
Tomer Libal and Dale Miller

Nominal Narrowing
Daniele Nantes-Sobrinho, Mauricio Ayala-Rincon and Maribel Fernández

FSCD Business Meeting

24 June 2016 09:00-10:00
Coalgebras and Higher-Order Computation: a GoI Approach

Girard's geometry of interaction (GoI) can be seen as a compositional compilation method from functional programs to sequential machines, where tokens move around and express interactions between (parts of) programs. Intrigued by the combination of abstract theory and concrete dynamics in GoI, our line of work (withNaohiko Hoshino, Koko Muroya and Toshiki Kataoka) has aimed at exploiting, in GoI, results from the theory of coalgebra---a categorical abstraction of state-based transition systems that has found its use principally in concurrency theory. Such reinforced connection between higher-order computation and state-based dynamics is made possible thanks to an elegant categorical axiomatization of GoI by Abramsky, Haghverdi and Scott, where traced monoidal categories are identified to be essential in modeling interaction. In the talk I shall lay out these basic ideas, together with some of our results on: GoI semantics for a quantum programming language; and extension of GoI with algebraic effects.


24 June 2016 10:30-12:30
Non-omega-overlapping TRSs are UN
Stefan Kahrs and Connor Smith

Normalisation by Random Descent
Vincent van Oostrom and Yoshihito Toyama

Automating the First-Order Theory of Rewriting for Left-Linear Right-Ground TRSs
Franziska Rapp and Aart Middeldorp

Complexity Hierarchies and Higher-Order Cons-Free Rewriting
Cynthia Kop and Jakob Grue Simonsen


24 June 2016 14:00-15:00
Normalisation by Evaluation for Dependent Types
Thorsten Altenkirch and Ambrus Kaposi

The Independence of Markov’s Principle in Type Theory
Thierry Coquand and Bassel Mannaa

FSCD Business Meeting

25 June 2016 09:00-10:00
Teaching Foundations of Computation and Deduction through Literate Programming and Proving

The talk will describe experiments in teaching fundamental informatics notions around mathematical structures for formal concepts, and effective algorithms to manipulate them. The major themes of lambda-calculus and type theory served as guides for the effective implementation of functional programming languages and higher-order proof assistants, appropriate for reflecting the theoretical material into effective tools to represent constructively the concepts and formally certify the proofs of their properties. Progressively, a literate programming and proving style replaced informal mathematics in the presentation of the material as executable course notes. The talk will evoke the various stages of (in)completion of the corresponding set of notes along the years, and tell how their elaboration proved to be essential to the discovery of fundamental results.


25 June 2016 10:30-12:30
Computing connected proof(-structure)s from their Taylor expansion
Giulio Guerrieri, Luc Pellissier and Lorenzo Tortora De Falco

Interaction Automata and the ia2d Interpreter
Stéphane Gimenez and David Obwaller

Proving Correctness of Graph Rewriting Systems using C2PDL
Jon Hael Brenas, Rachid Echahed and Martin Strecker

Complexity of Term Graph Rewriting
Martin Avanzini and Georg Moser

FSCD Business Meeting

25 June 2016 14:00-16:00
Welcome by Steering Committee
  • Chair: Luke Ong

Report of FSCD 2016
  • PC Co­Chairs: Delia Kesner and Brigitte Pientka

Report of FSCD 2016 Conference and Workshop
  • Chair: Sandra Alves

Progress reports on FSCD 2017, 3­6 September, Oxford (co­locating with ICFP 2017)
  • PC Chair: Dale Miller
  • Conference Chair: Sam Staton

FSCD 2018 ­ member conference of FLoC 2018, 6­19 July, Oxford 
  • Brief progress report: Luke Ong

Election of FSCD SC members
  • Luke Ong