Dale MILLER

Author's posts

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

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.

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

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 …

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

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

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.

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