Author's posts

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

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.

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.

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.

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)

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.

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

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.

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

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.