ESSLLI 2012 course on Bedwyr and Abella

David Baelde (in collaboration with Gopalan Nadathur and Alwen Tui) taught an ESSLLI 2012 Introductory Course in the Logic and Computation track titled “Specification and Prototyping Using Higher Order Logic”.   His lectures involved using many of the ideas and systems that involve the Parsifal team:  the Teyjus implementation of λProlog and the Bedwyr and Abella systems.  Course information is available as are his lecture notes.


A web site for “Programming with Higher-Order Logic”

new web site associated to the book (by Miller & Nadathur) is now available.  You can find there links to all the code used in the book (so you can cut-and-paste into your editor) as well as the list of errata.

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.

TWIP: This Week In Parsifal

This week we have two visitors to the team in addition to Elaine Pimentel who has been here for some weeks already.  They are Vivek Nigam (former team member, now a postdoc in Munich) and Giselle Reis (phd student in Vienna). Also, Stefan Hetzl is starting this week a 3 month post doc position within Parsifal as well.

Several talks are planned this week as part of a workshop on specifying and reasoning about logic and proof systems.  These are posted on the team’s calendar (it takes a few seconds to load) or the usual Google Calendar.

Note: some other visitors will be here also next week for a different informal workshop on Abella, Bedwyr, and related systems.

Workshop on Abella and Bedwyr

Workshop on Abella and Bedwyr
Dates:  10-12 July 2012 (Tue/Wed/Thu)
Location: LIX (still in the old, familiar location)
All talks will take place in the Prefa (the extension to Aisle 0) except the last talk (Thursday at 14h) which will be held in the “bocal” (near the mailroom of LIX).

10 July, Tue

14h00 Lucca Hirschi (LRI and intern at ITU).  recent research with David Baelde on fixed points
15h00 Quentin Heath.  Recent enhancements to Bedwyr

11 July, Wed
10h30 Yuting Wang (intern from UMinn).   Recent work on the Abella system
14h00 Alberto Momigliano (Milan). Howe’s method in Abella
15h00 Beniamino Accattoli.  Proof pearl in Abella

12 July, Thu
10h30 Kaustuv Chaudhuri.   Recent work on Abella
14h00 Gopalan Nadathur (UMinn). Combining Deduction Modulo and Logics of Fixed-Point Definitions


Elaine Pimentel visits for 6 weeks

Elaine Pimentel starts her 6 week visit to LIX today.

Moving of LIX to the new building planned for August

The following was sent by email by Nozha Boujemaa, Directrice, Centre Inria Saclay Ile-de-France.

Digiteo-Palaiseau est baptisé “Bâtiment Alan Turing”. Ce déménagement se terminera le jeudi 7 juin.

La période du déménagement du LIX est estimée pour courant Aout.

Les agents du Parc Club devront annoncer dès lundi, dans leurs signatures, le changement d’adresse vers la nouvelle:

INRIA Saclay Ile-de-France
Bâtiment Alan Turing
1 rue Honoré d’Estienne d’Orves
Campus de l’École Polytechnique
91120 Palaiseau

Pour tous les autres agents qui ne sont pas sur le site: indiquer cette adresse pour toute correspondance postale avec notre CRI.

Attention, cette rue étant nouvelle, elle n’est pas encore reconnue par les GPS.  Les Coordonnées GPS sont : +48° 42′ 52.11″, +2° 12′ 20.78″

Willem Heijltjes speaks at LIX


Rescheduled for 6 June 2012 at 11h (bocal, LIX)

Proof nets and semi-star-autonomous categories

Willem Heijltjes, postdoc in Parsifal

Girard’s original proof nets are a canonical graphical presentation of proof in multiplicative linear logic without units. In capturing their categorical semantics, there is the problem of dealing with proof nets that have a single conclusion. These would normally be captured by morphisms out of the monoidal unit 1; however, for MLL /with/ units, proof nets are not canonical for the semantics of star-autonomous categories. We address this issue via a set-valued functor called the /virtual unit/, that takes the place of hom(1,-). Then proof nets are canonical for a notion of semi-star-autonomous category incorporating this functor. This is joint work with Lutz Strassburger.

Yuting Wang joins as an intern for the summer

Yuting Wang, currently a PhD student with Gopalan Nadathur at the University of Minnesota, will be joining the Parsifal team for an internship during this summer.  His positions formally starts today and ends 15 August 2012.  He will be working on the team’s INRIA Associated Team (Equipe Associée) RAPT (Recent Advances in Proof Theory).