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
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.
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. …
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.
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-β …
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.
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.
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.
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.
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 http://dx.doi.org/10.1016/j.apal.2012.09.005 and http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/pil-final.pdf .