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.
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? | Matteo Manighetti. Expressiveness of extensions of MALL with fixpoints and induction. |
11:00 - 11:30. | Abhishek De and Alexis Saurin. Proof nets for non-wellfounded proofs. | |
11:30 - 12:00. | Ozan Kahramanogullari. Deep inference for proof search. | Roberto Maieli and Vito Michele Abrusci. Contractile Proof Nets for Multiplicative Cyclic Linear Logic. |
12:00 - 12:30. | Adam Lassiter and Willem Heijltjes. 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. Revantha Ramanayake. Structural proof theory: shedding structure. | 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, Favio E. Miranda-Perea and Pilar Selene Linares-Arévalo. Two deductive systems for the constructive logic S4, a formal verification. | Pierre Clairambault and Andrzej Murawski. On the expressivity of linear recursion schemes. |
15:30 - 16:00. | COFFEE BREAK | |
16:00 - 16:30. | Lutz Strassburger. What are combinatorial proofs? | |
16:30 - 17:00. | Willem Heijltjes and Michelangelo Mecozzi. Expansion tree proofs with unification. | Business meeting. |
17:00 - 17:30. | Peter Schuster, Giulio Fellin and Daniel Wessel. 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 and Giulio Manzonetto. 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 and Alessio Guglielmi. A Subatomic Proof System for Binary Decision Trees. | Claudia Faggian and 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. | Beniamino Accattoli, Ugo Dal Lago and 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. Serenella Cerrito. Deciding ATL* satisfiability by tableaux. | 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. | Zeinab Galal. A Quantitative Semantics of Differential Linear Logic with Setoids. |
15:30 - 16:00. | COFFEE BREAK | Lê Thành Dung Nguyen. Transductions in affine logic. |
16:00 - 16:30. | David Sherratt and Willem Heijltjes. The Spinal Atomic Lambda Calculus. | |
16:30 - 17:00. | Paulo Guilherme Santos and Reinhard Kahle. 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. |
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.