SD'19 is the fifth in a series of workshops aiming to gather various communities of structural proof theorists. The main interest is in new algebraic and geometric results in proof theory which expand our abilities to manipulate proofs, help to reduce bureaucracy in deductive systems, and ultimately lead to new methods for proof search and new kinds of proof certificates.
There have been four previous editions of Structures and Deduction, the last of which occurred in 2017. We are in the process of creating a permanent online presence for matters relating to the Structures and Deduction workshop series.
Themes of the workshop include but are not limited to:
As well as theoretical work in the form of regular papers, we encourage submission of implementations, tools and system descriptions.
SD will take place in the U-Tower in Dortmund. All talks will be in Room 1 on the first floor. TLLA will take place in Room 2 on the first floor, except for the the joint invited talks each morning which take place in Room 1.
Saturday 29 June. | SD | TLLA |
---|---|---|
09:00 - 09:30. | Invited talk. Delia Kesner. Reasoning about languages with control operators. | |
09:30 - 10:00. | ||
10:00 - 10:30. | COFFEE BREAK | |
10:30 - 11:00. | Invited talk. Ross Horne. Can we Prove Privacy Properties using the Calculus of Structures? | Abhishek De. Proof nets for non-wellfounded proofs. |
11:00 - 11:30. | Zeinab Galal. A Quantitative Semantics of Differential Linear Logic with Setoids. | |
11:30 - 12:00. | Ozan Kahramanogullari. Deep inference for proof search. | |
12:00 - 12:30. | Adam Lassiter. Additive to Classical Proof Search. | |
12:30 - 13:00. | LUNCH BREAK | |
13:00 - 13:30. | ||
13:30 - 14:00. | ||
14:00 - 14:30. | Invited talk. Serenella Cerrito. Deciding ATL* satisfiability by tableaux. | Invited talk. Paul Blain Levy. Call-by-push-value and linear logic. |
14:30 - 15:00. | ||
15:00 - 15:30. | Lourdes Del Carmen González Huesca. Two deductive systems for the constructive logic S4, a formal verification. | Pierre Clairambault. On the expressivity of linear recursion schemes. |
15:30 - 16:00. | COFFEE BREAK | |
16:00 - 16:30. | Lutz Straßburger. What are combinatorial proofs? | |
16:30 - 17:00. | Michelangelo Mecozzi. Expansion tree proofs with unification. | Business meeting. |
17:00 - 17:30. | Peter Schuster. The Jacobson Radical of a Propositional Theory. |
Sunday 30 June. | SD | TLLA |
---|---|---|
09:00 - 09:30. | Invited talk. Thomas Seiller. Semantics and complexity lower bounds. | |
09:30 - 10:00. | ||
10:00 - 10:30. | COFFEE BREAK | |
10:30 - 11:00. | Invited talk. Andrea Aler Tubella. A story of multiplicatives and additives. | Davide Barbarossa. About the Power of Taylor Expansion. |
11:00 - 11:30. | Luc Pellissier. What is the Taylor expansion a natural transformation of? | |
11:30 - 12:00. | Chris Barrett. A Subatomic Proof System for Binary Decision Trees. | Giulio Guerrieri. Standardization via Linear Logic for Call-by-Name, Call-by-Value and Choice Effects. |
12:00 - 12:30. | Tim Waring. A graph theoretic extension of Boolean logic. | Gabriele Vanoni. The Geometry of Abstract Machines. |
12:30 - 13:00. | LUNCH BREAK | |
13:00 - 13:30. | ||
13:30 - 14:00. | ||
14:00 - 14:30. | Invited talk. Revantha Ramanayake. Structural proof theory: shedding structure. | Invited talk. Raphaëlle Crubillé. Stable Semantics of Probabilistic Higher-Order Programs. |
14:30 - 15:00. | ||
15:00 - 15:30. | Stepan Kuznetsov. Complexity of Reasoning in Residuated Kleene Algebras. | Lê Thành Dung Nguyen. Transductions in affine logic. |
15:30 - 16:00. | COFFEE BREAK | |
16:00 - 16:30. | David Sherratt. The Spinal Atomic Lambda Calculus. | |
16:30 - 17:00. | Paulo Guilherme Santos. Kreisel's Conjecture and Reflexion Principles: Two Restricted Versions of the Conjecture. | |
17:00 - 17:30. | Mirjana Ilic. On sequent calculi proofs in relevant logics. |
In traditional cut-elimination procedures in Gentzen theory, we eliminate cut instances from proofs by moving upwards instances of the mix rule: this rule conflates one instance of cut and several instances of contraction. In the absence of contraction, the procedure leaves the size of the proofs essentially the same, whereas if contraction is present the size of the proofs can grow exponentially or more. In other words, there are two mechanisms that have different effects on complexity: while cut elimination per se would keep proofs in the same complexity class (modulo polynomials), the presence of contraction makes for a jump to a higher complexity class.
In this talk we present a generalised modular normalisation procedure that allows us to separate cut and contraction and normalise on each of them separately and in a natural way. Furthermore, by taking advantage of the regularity of inference rules in deep inference, we are able to provide a classification for rules based on their behaviour and impact on normalisation and to provide some insight into the role that the shape of a rule plays in cut-elimination.
This talk is centered on ATL*, the most expressive logic of the family of alternating-time temporal logics, that can be seen as a multi-agent version of CTL*. It will start with a short introduction highlighting the links between sequent calculi and tableaux calculi to decide the validity/satisfiability problem for modal propositional logics, temporal logics being a particular case of modal logics.
The core of the presentation will be the description of a tableau calculus for ATL* that is the foundation of TATL, a running theorem prover for ATL* (obviously subsuming CTL and CTL*): https://atila.ibisc.univ-evry.fr/tableau_ATL_star/. A sketch of ongoing work aiming to extend the present functionalities of TATL, by allowing it to synthesize minimal models of satisfiable formulae will conclude the talk.
The results presented are based on joint works by Serenella Cerrito, AmÃ©lie David and Valentin Goranko.
In the calculus of structures, we can soundly model processes in calculi, such as the pi-calculus, directly as logical formulae. In order to retain soundness of logical embeddings of processes involving private names, we must extend existing proof systems with a pair of de Morgan dual nominal quantifiers. In this talk, we explain the need for these new quantifiers and discuss their properties. We also examine evidence surrounding the question of whether the resulting logic can be used to prove privacy properties of cryptographic protocols. We explain why the latter question also leverages logical systems between classical and intuitionistic logic.
One of the most surprising examples of the proofs-as-programs paradigm is the correspondence between the Peirce Law in classical logic and the call-cc control operator in functional programming, first noticed by Griffin in 1990, and then extended by Parigot in 1992, which has introduced the lambda-mu calculus as an isomorphic term language of classical natural deduction logic.
This talk provides some tools to reason about dynamic properties of the lambda-mu calculus.
In the first part of the talk, we discuss how to identify programs with control operators having exactly the same reduction semantics. This is achieved by introducing a relation which is a strong bisimulation defined over a revised presentation of Parigot's lambda-mu calculus. We show that our relation is conservative with respect to Laurent's original sigma-equivalence for lambda-mu terms (which is not a strong bisimulation), still being able to characterize structural equivalence in Polarized Proof-Nets.
In the second part of the talk, we show how to exactly measure time and space in the lambda-mu calculus. Our approach is based on typing systems equipped with non-idempotent intersection and union types, which are able to provide information about the number of evaluation steps to normal form and the size of this normal forms. These quantitative informations are measured separately, simply because the size of the result can be exponentially bigger than the number of steps. We develop our study for three well-known evaluation strategies: head, leftmost and maximal evaluation, pertaining to head, weak and strong normalization, respectively.
Since at least the late 1960s, structural proof theory has witnessed numerous proof formalisms used to construct analytic/cut-free proof calculi for the vast number of non-classical logics lacking an analytic/cut-free sequent calculus. In most cases, these 'exotic' proof formalisms extend Gentzenâ€™s sequent calculus by enriching the sequent with additional structure. Some familiar examples are hypersequent calculi (sequences of sequents) and nested sequent calculi (trees of sequents). The primary result takes the same form: C is an analytic/cut-free calculus (in proof formalism F) for logic L. Typically, as F incorporates more structure, the harder it is to use C to obtain useful results about L. Despite this, and despite the glut of exotic proof formalisms, the logical content and meaning of the analyticity result in an exotic proof formalism does not appear to have been formally investigated.
As a concrete starting point for such an investigation, I will discuss some recent work investigating the logical content of the analyticity result in cut-free hypersequent calculi for substructural, intermediate and modal logics. We shed the additional structure of the hypersequent in a controlled manner to obtain a sequent calculus, accepting, in return, systematic relaxations of the analyticity property.
I have been investigating for some time the question of proving separation and/or lower bounds results using techniques and results from specific models of linear logic I introduced under the name "Interaction Graphs". Related to game semantics and Girard’s geometry of interaction models, the latter propose a mathematical model of programs and the dynamics of their execution founded upon the proofs-as-programs correspondance.
After sketching the main lines of this work and the questions arising from it, I will focus on a recent result obtained in collaboration with Luc Pellissier. Based on the mathematics at work in Interaction Graphs, we provide an abstract account of three lower bounds results from the literature which were not known to be related. Moreover, this abstraction allows us to refine the most involved of those results — due to Mulmuley (1999) —, improving the state-of-the-art on the P vs NC question.
We do not intend to have published proceedings, as we encourage people to present work in progress, or material that is already submitted. If there is a strong demand among the participants we may organise a special issue of an open access journal for full papers.
All questions about submissions should be addressed to sd19@easychair.org, or directly to one of the co-chairs.