Aug 20
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.
Jul 26
A 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.
Jul 25
There is a 12 month postdoc position available at LIX, Ecole Polytechnique, within the Parsifal team. The deadline for applications is August 24, 2012.
Jul 03
The following papers by Parsifal team members have been accepted to Computer Science Logic (CSL) to be held at Fontainebleau, France in September 2012.
Jul 02
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.
Jun 06
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
Jun 04
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.
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″
May 25
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.
May 15
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).
