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
Category: Publications
Apr 02
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.
Mar 31
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. …
Aug 30
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.
Jul 21
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-β …
Jul 15
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.
Mar 25
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.
Mar 24
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.
Jan 10
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.
Oct 08
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 http://dx.doi.org/10.1016/j.apal.2012.09.005 and http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/pil-final.pdf .
- 1
- 2
