Mon 8 Jan 2018 11:30 - 12:00 at Museum A - Verifying Programs and Systems Chair(s): Natarajan Shankar

The completeness proofs for Propositional Dynamic Logic (PDL) in the literature are non-constructive and usually presented in an informal manner. We obtain a formal and constructive completeness proof for Converse PDL by recasting a completeness proof by Kozen and Parikh into our constructive setting. We base our proof on a Pratt-style decision method for satisfiability constructing finite models for satisfiable formulas and pruning refutations for unsatisfiable formulas. Completeness of Segerberg's axiomatization of PDL is then obtained by translating pruning refutations to derivations in the Hilbert system. We first treat PDL without converse and then extend the proofs to Converse PDL. All results are formalized in Coq/Ssreflect.

Mon 8 Jan

Displayed time zone: Tijuana, Baja California change

10:30 - 12:00
Verifying Programs and SystemsCPP at Museum A
Chair(s): Natarajan Shankar SRI International, USA
10:30
30m
Talk
Total Haskell is Reasonable Coq
CPP
Antal Spector-Zabusky , Joachim Breitner University of Pennsylvania, Christine Rizkallah University of Pennsylvania, USA, Stephanie Weirich University of Pennsylvania, USA
DOI
11:00
30m
Talk
A Formal Proof in Coq of a Control Function for the Inverted Pendulum
CPP
Damien Rouhling University of Côte d'Azur, France
DOI
11:30
30m
Talk
Completeness and Decidability of Converse PDL in the Constructive Type Theory of Coq
CPP
Christian Doczkal CNRS, France, Joachim Bard Saarland University, Germany
DOI