Category: Publications

Accepted papers for CPP 2012

The list of accepted papers for CPP 2012 can be found here.  The team will have two papers at this conference. Kaustuv Chaudhuri. Compact Proof Certificates for Linear Logic. Beniamino Accattoli. Proof pearl: Abella formalization of lambda calculus cube property.

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.

Papers accepted to CSL 2012

The following papers by Parsifal team members have been accepted to Computer Science Logic (CSL) to be held at Fontainebleau, France in September 2012. Stefan Hetzl and Lutz Straßburger, “Herbrand-Confluence for Cut Elimination in Classical First Order Logic“ Kaustuv Chaudhuri, Stefan Hetzl, and Dale Miller, “A Systematic Approach to Canonicity in the Classical Sequent Calculus“

CFP: CPP 2012 – 2nd International Conference on Certified Programs and Proofs

The Second International Conference on Certified Programs and Proofs (CPP 2012) will be held in Kyoto, Japan during December 13-15, 2012.  It will be co-located with APLAS 2012. CPP is a new international forum on theoretical and practical topics in all areas, including computer science, mathematics and education, that consider certification as a essential paradigm for their …

Continue reading

Book to be published by Cambridge University Press

The book Programming with higher-order logic by Dale Miller and Gopalan Nadathur will be published by Cambridge University Press by the end of May 2012.  It is available for pre-ordering on Amazon.com and Amazon.fr.  The table of contents is available.

Paper accepted to QAPL 2012

The following paper was accepted to QAPL 2012: A non-local method for robustness analysis of floating point programs by Ivan Gazeau, Dale Miller, and Catuscia Palamidessi. Draft dated 3 Feb 2012 (HAL).