Collected Abstracts (PDF)

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

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

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

14:45–15:00

Break

15:00–15:30

15:30–16:00

Matthias Baaz

Interpolation in finitely-valued first-order logics

16:00–16:30

16:30–16:45

Break

16:45–17:45

17:45–18:15

Nicolas Guenot

Linear Session Types for Solos

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

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

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

09:30–10:30

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

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