Author's posts
Mar 16
New offices
Some team members have moved to new offices. Here is the full list of changes: From To B. Accattoli 2058 2063 R. Blanco 2054 2058 K. Chaudhuri 2059 2051 U. Gerard 2050 2057 Q. Heath 2054 2059 S. Marin 2057 2052 M. Puech 2062 2057 G. Reis 2057 2052 N. Zeilberger 2062 2051
Aug 10
Abella online tutorial
A tutorial for Abella was recently presented at CADE 25 in Berlin by K. Chaudhuri and Gopalan Nadathur. The slides (PDF) are available online. All the demonstration examples in the tutorial can be viewed and executed online using the new experimental Abella in the Browser plugin.
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.
Apr 02
Ulysse Gérard joins the team for an M2 internship
Ulysse Gérard will be doing his MPRI M2 internship at Parsifal under the supervision of Dale Miller. He will be working on proof theory for term representations.
Nov 03
New arrivals
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)
May 16
Yuting Wang and Mary Southern start their internships
This summer, Parsifal is hosting two interns from the University of Minnesota: Yuting Wang and Mary Southern. They will be working on the theory and implementation of Abella.
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. …
Mar 07
Discussion of Descriptive Complexity Theory in relation to Proof Theory (RGFP)
The next round of the Reading Group on Fixed Points (RGFP) will be on Thursday, March 27. We will discuss some results from descriptive complexity theory and their relation to structural proof theory. Of particular interest is the open question of defining a logic for PTIME.
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-β …
Jun 24
Elaine Pimentel and Carlos Olarte visiting until 16 July
Prof. Elaine Pimentel (UFMG) and Prof. Carlos Olarte (Univ. Javeriana, Cali) are visiting Parsifal and Comète in June and July.
