Selected Papers of the 1st International Conference on Formal Structures and Deduction (FSCD 2016)

Editors: Delia Kesner and Brigitte Pientka

1. Focusing in Orthologic

Laurent, Olivier.
We propose new sequent calculus systems for orthologic (also known as minimal quantum logic) which satisfy the cut elimination property. The first one is a simple system relying on the involutive status of negation. The second one incorporates the notion of focusing (coming from linear logic) to […]

2. Complexity Hierarchies and Higher-order Cons-free Term Rewriting

Kop, Cynthia ; Simonsen, Jakob Grue.
Constructor rewriting systems are said to be cons-free if, roughly, constructor terms in the right-hand sides of rules are subterms of the left-hand sides; the computational intuition is that rules cannot build new data structures. In programming language research, cons-free languages have been used […]

3. The Algebraic Intersection Type Unification Problem

Dudenhefner, Andrej ; Martens, Moritz ; Rehof, Jakob.
The algebraic intersection type unification problem is an important component in proof search related to several natural decision problems in intersection type systems. It is unknown and remains open whether the algebraic intersection type unification problem is decidable. We give the first […]

4. The Independence of Markov's Principle in Type Theory

Coquand, Thierry ; Mannaa, Bassel.
In this paper, we show that Markov's principle is not derivable in dependent type theory with natural numbers and one universe. One way to prove this would be to remark that Markov's principle does not hold in a sheaf model of type theory over Cantor space, since Markov's principle does not hold for […]

5. Environmental Bisimulations for Delimited-Control Operators with Dynamic Prompt Generation

Aristizábal, Andrés ; Biernacki, Dariusz ; Lenglet, Sergueï ; Polesiuk, Piotr.
We present sound and complete environmental bisimilarities for a variant of Dybvig et al.'s calculus of multi-prompted delimited-control operators with dynamic prompt generation. The reasoning principles that we obtain generalize and advance the existing techniques for establishing program […]

6. Formal Languages, Formally and Coinductively

Traytel, Dmitriy.
Traditionally, formal languages are defined as sets of words. More recently, the alternative coalgebraic or coinductive representation as infinite tries, i.e., prefix trees branching over the alphabet, has been used to obtain compact and elegant proofs of classic results in language theory. In this […]

7. Normalisation by Evaluation for Type Theory, in Type Theory

Altenkirch, Thorsten ; Kaposi, Ambrus.
We develop normalisation by evaluation (NBE) for dependent types based on presheaf categories. Our construction is formulated in the metalanguage of type theory using quotient inductive types. We use a typed presentation hence there are no preterms or realizers in our construction, and every […]