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.
We have several new arrivals in Parsifal. Postdocs Taus Brock-Nannestad (from 1 Oct) Giselle Reis (from 1 Nov) Marco Volpe (from 1 Nov) Ph.D. students Roberto Blanco (supervised by Dale Miller) Sonia Marin (supervised by Dale Miller and Lutz Straßburger) Research engineer Tomer Libal (starting 1 Jan, 2015)
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. …
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-β …