Category: Talks

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. …

Continue reading

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 …

Continue reading

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 …

Continue reading

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 …

Continue reading

Beniamino Accatoli speaks at Rocquencourt

I N R I A – Rocquencourt Amphi Turing du bātiment 1 Lundi 7 mai, 10h30 Beniamino Accatoli LIX Abella formalization of lambda-calculus residual theory Abella is a new proof assistant developed by Andrew Gacek and based on work of Gacek, Miller and Nadathur. Its main feature is a primitive handling of binders via higher order abstract …

Continue reading

Talk by Maribel Fernandez, 26 April

Nominal Completion for Rewrite Systems with Binders Talk by Maribel Fernandez. Joint work with Albert Rubio. Venue: Salle de reunion, 10h30 Thursday 26 April 2012 Nominal rewriting generalises first-order rewriting by providing support for the specification of binding operators, using the nominal approach. In this talk, I will present a new ordering that can be used to …

Continue reading

Two talks for Friday, 4 May 2012

We will have two talks on Friday, 4 May 2012.  Pierre-Louis Curien will speak at 11h and Chuck Liang will speak at 14h30.  Both talks will be in the Salle de Reunion of LIX. System L syntax for sequent calculus Pierre-Louis Curien We recall two related syntaxes for focalised logic (linear and classical), derived from Curien-Herbelin’s …

Continue reading

Celebration of the career of Peter Andrews

On 4 April 2012, there was a reception for Peter Andrews on the ocassion of his retirement from the Mathematics Department at Carnegie Mellon University. Dale Miller offered some personal words and some scientific talks were presented the following day.

Chuck Liang speaks at GdT Théorie des types et réalisabilité

Two talks will be given at the GdT Théorie des types et réalisabilité in the salle orange au 5e étage, 23 avenue d’Italie. Mercredi 21 mars, 14h and 15h15, salle orange 1 (double séance) Chuck Liang  An Intuitionistic Logic for Sequential Control We introduce the propositional logic ICL for “Intuitionistic Control Logic”, which adds to intuitionistic logic …

Continue reading

Guenot and Miller speak at ChoCola, Lyon

Nicolas Guenot and Dale Miller spoke at the ChoCola meeting, ENS Lyon on 15 March 2012.  The program is available.