Author's posts
Aug 20
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. …
Jul 26
A web site for “Programming with Higher-Order Logic”
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 02
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 …
Jun 06
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 …
Jun 04
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 …
May 25
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 …
May 15
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).
May 15
Stefan Hetzl joins the team for 3 months
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.
May 05
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 …
