Horace Blanc joins the team for an M2 internship

Horace Blanc is doing his MPRI M2 internship at Parsifal under the supervision of Beniamino Accattoli. He will be working on Lambda to Pi.

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.

Taus Brock-Nannestad talks at Parsifal Seminar

Taus Brock-Nannestad (Parsifal, Inria)

Title: Forcing Saturation in the Inverse Method

The Inverse Method is a marvellous method of proof search in classical
and non-classical logics. Among its nice features is the fact that any
sequent produced during proof search is indeed a valid theorem.
Unfortunately this feature is a double-edged sword. To disprove a
sequent using the inverse method requires finding all consequences of
the given assumptions, and checking that the goal sequent is not
contained therein. Naturally, this requires that this set of
consequences is finite. For all but the most trivial first-order
theories, there will be an infinite set of distinct consequences of the
assumptions, and hence this desired saturation becomes impossible to

In my talk, I will describe a way of forcing the inverse method to
saturate, by performing the proof search with an over-approximation of
the given assumptions. This is sound for the purposes of disproving
sequents, and can be iteratively refined if an attempt at a disproof
yields an unsound proof instead.

The method has been implemented by myself and Kaustuv Chaudhuri in the
form of the Mætning theorem prover.

Two new members to the team

Today is the first day for both Beniamino Accattoli (CR) and Tomer Libal (Engineer). Welcome onboard!

New arrivals

We have several new arrivals in Parsifal.


Ph.D. students

  • Roberto Blanco (supervised by Dale Miller)
  • Sonia Marin (supervised by Dale Miller and Lutz Straßburger)

Research engineer

Chuck Liang visits during May and June

Chuck Liang (Professor, Hofstra University) visits the team during 26 May – 20 June 2014.


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. Equality and Fixpoints in the Calculus of Structures

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.