Author's posts

Chuck Liang and Gopalan Nadathur visit Parsifal in May

Prof. Chuck Liang (Hofstra) and Prof. Gopalan Nadathur (Univ. Minnesota) are visiting Parsifal during May and June. Chuck will be here until 15 June and Gopalan until 31 May.

Olivier Savary-Bélanger begins his summer internship

Olivier Savary-Bélanger joins us for a three month internship starting May 13. He will be working on automating various aspects of context relations in Abella, as part of the RAPT project.

Nicolas Guenot successfully defends his Ph.D.

Nicolas Guenot (new web page) defended his Ph.D. on 10 April at LIX under the supervision of Lutz Straßburger. He will continue to a postdoctoral position at Demtech at the IT University, Copenhagen.

Small Workshop on Formal Meta-Theory, 5-6 March

Parsifal will organize a workshop on formal meta-theory during 5-6 March to coincide with the visit of Prof. Brigitte Pientka from McGill during that week. We will also welcome some additional visitors from McGill: Andrew Cave, Francisco Ferreira, Olivier Savary-Bélanger, and David Thibodeau.

Paper on Nested Sequents for Intuitionistic Modal Logics

Lutz Straßburger’s paper “Cut Elimination in Nested Sequent Systems for Intuitionistic Modal Logics” has been accepted to FoSSaCS 2013 to be held in Rome during 16–24 March as part of ETAPS.

Parsifal organizes the Collegium Logicum 2012 Workshop, 15-16 November

The Collegium Logicum 2012 workshop on the theme of Structural Proof Theory is being organized at LIX during 15–16 November. There will be invited talks by Alex Simpson and Paulo Oliva, and a number of contributed talks by participants from France and Austria. The program is now available.

A new web-site for Abella

The Abella interactive theorem prover now has a new web-site: http://abella-prover.org. Relatedly, the canonical GitHub repository for Abella has been changed to: http://github.com/abella-prover/abella. Kaustuv Chaudhuri (Parsifal) and Yuting Wang (Univ. Minnesota) join Andrew Gacek (Rockwell Collins) as maintainers of Abella. A cumulative new release of Abella is planned during the remaining months of 2012. A …

Continue reading

RAPT/Promis Workshop in McGill University, Canada

Several members of Parsifal will participate in the Promis workshop in McGill University in Canada during 17–18 October, funded in part by the Equipe Associée RAPT. Abstracts of the talks are already available, and slides will be posted as they become available.

New 12 mo. postdoc position

There is a 12 month postdoc position available at LIX, Ecole Polytechnique, within the Parsifal team. The deadline for applications is August 24, 2012.

Papers accepted to CSL 2012

The following papers by Parsifal team members have been accepted to Computer Science Logic (CSL) to be held at Fontainebleau, France in September 2012. Stefan Hetzl and Lutz Straßburger, “Herbrand-Confluence for Cut Elimination in Classical First Order Logic“ Kaustuv Chaudhuri, Stefan Hetzl, and Dale Miller, “A Systematic Approach to Canonicity in the Classical Sequent Calculus“