Abstracts

Collected Abstracts (PDF)

 

Tuesday, November 5

09:30–10:30
Alessio Guglielmi University of Bath
Proof Composition Mechanisms and Their Geometric Interpretation
10:30–10:45
Break
10:45–11:15
Richard McKinley
Higher-order sequent proofs, higher-order nets
11:15–11:45
Willem Heijltjes and Robin Houston
The proof equivalence problem for multiplicative linear logic is PSPACE-complete
11:45–12:15
Roman Kuznets
Craig Interpolation, Proof-Theoretically via Nested Sequents
12:15–13:45
Lunch at LIX
13:45–14:45
Alex Simpson University of Edinburgh
Sequent Calculus for Stochastic Games
14:45–15:00
Break
15:00–15:30
Sorin Stratulat
Reductive-free cyclic induction reasoning
15:30–16:00
Richard Moot
First-order linear logic as a general framework for logic-based computational linguistics
16:00–16:30
Thomas Studer
Towards syntactic cut-elimination for temporal logics
16:30–16:45
Break
16:45–17:45
James Brotherston University College London
Cyclic Abduction of Inductive Safety & Termination Preconditions
17:45–18:15
Roberto Maieli
Construction of Bipolar Focussing Proof Structures

Wednesday, November 6

09:30–10:30
Sara Negri University of Helsinki
Extending the scope of labelled sequent calculi: the case of classical counterfactuals
10:30–10:45
Break
10:45–11:15
Roy Dyckhoff
Automating LPO Reasoning about Termination
11:15–11:45
Anupam Das
Some ideas on bounded arithmetics for systems of monotone proofs
11:45–12:15
George Metcalfe
Proof Theory for Lattice-Ordered Groups
12:15–13:45
Lunch at LIX
13:45–14:45
Dominic Hughes Stanford University
First-order proofs without syntax
14:45–15:00
Break
15:00–15:30
Stefan Hetzl and Daniel Weller
Expansion Trees with Cut
15:30–16:00
Matthias Baaz
Interpolation in finitely-valued first-order logics
16:00–16:30
Sebastian Eberhard and Stefan Hetzl
Guessing induction formulas for proofs of universal statements
16:30–16:45
Break
16:45–17:45
Agata Ciabattoni Vienna University of Technology
Power and Limits of Structural Rules
17:45–18:15
Nicolas Guenot
Linear Session Types for Solos

Thursday, November 7

09:30–10:30
Claudio Sacerdoti Coen University of Bologna
Curry-Howard for a lightweight interactive theorem prover
10:30–10:45
Break
10:45–11:15
Iliano Cervesato and Jorge Luis Sacchini
Meta-Reasoning in the Concurrent Logical Framework CLF
11:15–11:45
Amy Felty, Alberto Momigliano and Brigitte Pientka
Toward a Theory of Contexts of Assumptions in Logical Frameworks
11:45–12:15
Fabien Renaud, Dale Miller and Zakaria Chihani
A Semantics for Proof Evidence
12:15–13:45
Lunch at LIX
13:45–14:45
Herman Geuvers Radboud University Nijmegen
Pure Type Systems revisited
14:45–15:00
Break
15:00–15:30
Danko Ilik
Type isomorphisms in presence of strong sums: axiomatizability, practical decidability and subtyping
15:30–16:00
Noam Zeilberger
Proofs in monoidal closed bifibrations
16:00–16:30
José Espírito Santo, Ralph Matthes, Koji Nakazawa and Luís Pinto
A classical theory of values and computations
16:30–16:45
Break
16:45–17:45
Cezary Kaliszyk University of Innsbruck
Automation in Interactive Proof

Friday, November 8 (PSATTT)

09:30–10:30
Chad E. Brown Independent Researcher
Distributed Mathematics
10:30–11:00
Enrico Tassi
Modelling canonical reasoning via unification hints (Do mathematicians learn prolog at kindergarden?)
11:00–11:30
Coffee break
11:30–12:00
Ralph Matthes
A Coinductive Approach to Proof Search
12:00–12:30
Damien Pous
Untyping Typed Algebraic Structures and Colouring Cyclic Linear Logic Proof Nets
12:30–13:00
Sorin Stratulat
Certifying formula-based induction reasoning
13:00–14:30
Lunch break
14:30–15:30
David Delahaye CNAM
Automating Deduction Modulo
15:30–16:00
Coffee break
16:00–16:30
Claire Dross
Defining new theories in SMT solvers using first-order axioms with triggers
16:30–17:00
Damien Rouhling
Delayed instantiation of existential variables in presence of a theory
17:00–17:30
Arnaud Spiwack
Implementing an interactive proof system