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.

STRONG NORMALIZATION and CONFLUENCE

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

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

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

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

LOGICS and PROOF THEORY

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

Focusing in Orthologic
14:30
Olivier Laurent

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

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

CATEGORY THEORY and ALGEBRA

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

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

Category Theory in Coq 8.5
17:30
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.

TECNHIQUES

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

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

Reversible Term Rewriting
11:30
Naoki Nishida, Adrian Palacios and German Vidal

Formal Languages, Formally and Coinductively
12:00
Dmitriy Traytel

SEMANTICS and MODELS

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

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

Classical extraction in continuation models
15:00
Valentin Blot

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

UNIFICATION

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

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

Nominal Narrowing
17:30
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.

REWRITING

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

Normalisation by Random Descent
11:00
Vincent van Oostrom and Yoshihito Toyama

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

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

TYPE THEORY

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

The Independence of Markov’s Principle in Type Theory
14:30
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.

PROOF NETS and GRAPHS

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

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

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

Complexity of Term Graph Rewriting
12:00
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

AOB