Workshop Program

10:30-12:30

Session 2: Proofs and automation aa

(chair: Femke van Raamsdonk)

10:30	Cynthia Kop Cutting a proof into bite-sized chunks (Incrementally proving termination in higher-order term rewriting)
11:30	Johanna Schwartzentruber and Brigitte Pientka Semi-Automation of Meta-Theoretic Proofs in Beluga
12:00	Niccolò Veltri and Cheng-Syuan Wan Substructural Logics with Additives (LSFA contributed talk)

12:30-14:00

14:00-15:30

Section 3: Refinement Types

(chair: Alberto Ciaffaglione)

14:00	Niki Vazou (joint with LSFA) Refinement Types from Light to Deep Verification
15:00	Antoine Gaulin and Brigitte Pientka Readable proofs with refinement types

15:30-16:00

16:00-17:30

Session 4: Verification and interpretation

(chair: Carlos Olarte)

16:00	James Oswald and Brandon Rozek Parallel Verification of Natural Deduction Proof Graphs
16:30	Félix Castro An interpretation (by parametricity) of E-HA^ω inside HA^ω
17:00	Artur Graczyk, Marialena Hadjikostiand and Andrei Popescu A Framework for the Verification of Collision Freeness for Collaborative Robots

17:30-18:30

Business Meeting

(chair: Elaine Pimentel)