Category: Publications

Two papers accepted at PxTP 2015

The following papers authored by members of Parsifal were accepted to the fourth workshop on Proof eXchange for Theorem Proving: A framework for proof certificates in finite state exploration by Quentin Heath and Dale Miller Importing SMT and Connection proofs as expansion trees by Giselle Reis

Two papers accepted at LICS 2015

The following papers authored by members of the Parsifal team were accepted to the 30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2015): Beniamino Accattoli and Claudio Sacerdoti Coen, On the Usefulness of Constructors. Matthias Baaz, Alexander Leitsch, and Giselle Reis, A note on the complexity of classical and intuitionistic proofs.

Four papers accepted to CSL-LICS 2014

The following four papers authored by Parsifal team members have been accepted to CSL-LICS 2014: Anupam Das. Pigeonhole and related combinatorial principles in deep inference and monotone systems Danko Ilik. Axioms and Decidability for Type Isomorphism in Presence of Sums Nicolas Guenot and Lutz Strassburger. Symmetric Normalisation for Intuitionistic Logic Kaustuv Chaudhuri and Nicolas Guenot. …

Continue reading

Accepted paper at CPP 2013

A paper by Alwen Tiu and Dale Miller titled Extracting Proofs from Tabled Proof Search has been accepted by the CPP 2013 conference and will be presented in Melbourne, Australia  in December 2013.

Abella 2.0.0 released

After over a year of development, Abella 2.0.0 has been released! The new release removes all the arbitrary restrictions on the specification logic, which is now fully higher-order. As a result, this version of Abella allows backchaining in specification contexts, and therefore also supports inductive specifications of dynamic extensions of programs. This example characterizing equivalence-upto-β …

Continue reading

Accepted paper at LFMTP 2013

A paper by Mahfuza Farooque, Stéphane Graham-Lengrand, and Assia Mahboubi titled A bisimulation between DPLL(T) and a proof-search strategy for the focused sequent calculus has been accepted to LFMTP 2013 and will be presented at the workshop in Boston during September 2013.

Paper accepted to LICS 2013

The submission to LICS 2013 titled Unifying Classical and Intuitionistic Logics for Computational Control by Chuck Liang and Dale Miller was accepted.  The final draft of this paper is due 26 April.  If you have any comments on the earlier draft, please get them to one of the authors by then.

Paper accepted to CADE 2013

The submission to CADE 2013 titled Foundational proof certificates in first-order logic by Zakaria Chihani, Dale Miller, and Fabien Renaud was accepted.  The final draft of this paper is due 1 April.  If you have any comments on the earlier draft, please get them to one of the authors by then.  

Paper on Nested Sequents for Intuitionistic Modal Logics

Lutz Straßburger’s paper “Cut Elimination in Nested Sequent Systems for Intuitionistic Modal Logics” has been accepted to FoSSaCS 2013 to be held in Rome during 16–24 March as part of ETAPS.

New paper on Combining Intuitionistic and Classical Logics

The following paper has recently been accepted and published by the Annals of Pure and Applied Logic. Kripke Semantics and Proof Systems for Combining Intuitionistic Logic and Classical Logic, by Chuck Liang and Dale Miller. Available online from and .