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. …
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 …
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 …
Elaine Pimentel starts her 6 week visit to LIX today.
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 …
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 …
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).
Stefan Hetzl, currently at the Vienna University of Technology, will be joining the Parsifal team for a three month postdoc during the dates 01/07/2012 and 30/09/2012. He will be working with (at least) Chaudhuri and Miller on the general problem of canonicity in classical sequent calculus.
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 …