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

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.

Mar 14

## Taus Brock-Nannestad talks at Parsifal Seminar

Taus Brock-Nannestad(Parsifal, Inria) Title:Forcing Saturation in the Inverse MethodAbstract: 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 achieve. 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.

Jan 05

## Two new members to the team

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

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)

Jun 12

## Chuck Liang visits during May and June

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

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

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.