ProofCert: Broad Spectrum Proof Certificates
NOTE: This website has moved here.
ProofCert is the name of an ERC Advanced Grant awarded to Dale Miller for the five years 2012-2016. This 2.2 million euro grant will finance several PhD students and PostDocs as well as fund visiting collaborators.
The following is taken from the proposal’s abstract.
The ProofCert proposal aims at building a foundation that will allow a broad spectrum of formal methods—ranging from automatic model checkers to interactive theorem provers—to work together to establish formal properties of computer systems. This project starts with a wonderful gift to us from decades of work by logicians and proof theorist: their efforts on logic and proof has given us a universally accepted means of communicating proofs between people and computer systems. Logic can be used to state desirable security and correctness properties of software and hardware systems and proofs are uncontroversial evidence that statements are, in fact, true. The current state-of-the-art of formal methods used in academics and industry shows, however, that the notion of logic and proof is severely fractured: there is little or no communication between any two such systems. Thus any efforts on computer system correctness is needlessly repeated many times in the many different systems: sometimes this work is even redone when a given prover is upgraded. In ProofCert, we will build on the bedrock of decades of research into logic and proof theory the notion of proof certificates. Such certificates will allow for a complete reshaping of the way that formal methods are employed.
A technical description is available. A few papers describing high-level aspects of the ProofCert project are listed below.
- A semantic framework for proof evidence by Zakaria Chihani, Dale Miller, and Fabien Renaud. To appear in the Journal of Automated Reasoning. Draft dated 9 February 2016.
- The foundational proof certificate approach has been expanded to treat proofs in various modal logics. This extension is described in the following two papers.
- A focused framework for emulating modal proof systems by Sonia Marin, Dale Miller, and Marco Volpe. To appear in AiML 2016. Draft dated 12 June 2016.
- Focused labeled proof systems for modal logic by Dale Miller and Marco Volpe. The Proceedings of LPAR-20. November 2015. Springer LNCS 9450. The conference version and an extended version (with appendices) are available.
- Proof certificates for model checking and inductive reasoning have been explored in the following two papers.
- A framework for proof certificates in finite state exploration by Quentin Heath and Dale Miller. In the proceedings of PxTP 2015 (doi).Draft dated 25 June 2015.
- Proof Outlines as Proof Certificates: a system description by Roberto Blanco and Dale Miller. In the Proceedings of the First International Workshop on Focusing (WoF 2015). EPTCS volume 197. A draft dated Draft dated 1 November 2015.
- Foundational Proof Certificates by Dale Miller. In the proceedings of All about Proofs, Proofs for All (APPA), edited by D. Delahaye and B. Woltzenlogel Paleo, pp. 150-163. Version dated 1 December 2014: pdf.
- Communicating and trusting proofs: The case for foundational proof certificates by Dale Miller. Proceedings of the 14th Congress of Logic, Methodology and Philosophy of Science in Nancy, France, 19-26 July 2011. Edited by P. Schroeder-Heister, W. Hodges, G. Heinzmann, and P. E. Bour, pp. 323-342. Published by College Publications, 2014. Draft dated 13 March 2014: pdf.
Notes (in reverse chronological order)
- 9-10 November 2016: Several members of the Parsifal team spoke at the Linear Logic 2016 meeting in Lyon. Miller gave an invited lecture titled “A proof theory for model checking”. Chaudhuri speak on “The Expressivity of Some Fragments of Subexponential Logic” and Marin spoke on “Comparing BOX and ! via polarities”.
- May 2016:Ameni Chtourou starts a summer internship within the team. She is supervised by Beniamino Accattoli.
- 25 June 2016: Miller gave an invited talk at Linearity 2016 Porto, Portugal
- 15 June 2016: Miller gave an invited talk at a research seminar titled Interactions between logic, computer science and linguistics: history and philosophy, Lille, France.
- 4 June 2016: Miller gave an invited talk at CIPPMI: Workshop on Proofs, justifications and certificates. Toulouse, France.
- 25 May 2016: Miller gave an invited talk at TYPES 2016: 22nd International Conference on Types for Proofs and Programs. Novi Sad, Serbia.
- 1 Dec 2015: Huge Steele begins a one year postdoc position on the ProofCert team.
- 2 Nov 2015: Zak Chihani defended his PhD today. His thesis title is “Certification of First-order proofs in classical and intuitionistic logics”.
- 1 Nov 2015: Matthias Puech and Noam Zeilberger joined the team as postdocs and Leonardo Lima, an undergraduate from Brazil (advised by Vivek Nigam), joined the team for a 5 month internship.
- Jan 2015: Tomer Libal has joined the ProofCert project as an engineer.
- Nov 2014: Sonia Marin (PhD student) and Giselle Reis and Marco Volpe (PostDocs) have joined Parsifal to work on the ProofCert project.
- Oct 2014: Rob Blanco (PhD student) and Taus Brock-Nannestad (PostDoc) have joined Parsifal to work on the ProofCert project.
- 31 July 2014: Siddhartha Prasad completed a two month internship in the team. His work on equality certificates is available.
- July 2014: Miller gave two invited talks on ProofCert related topics at workshops during the Vienna Summer of Logic: one at APPA and one at LATD.
- Nov 2013: Fabien Renaud gave a talk at the LIX Colloquium 2013 titled “A Semantics for Proof Evidence“.
- Sep 2013: Dale Miller gave an invited talk at LFMTP 2013: Logical Frameworks and Meta-Languages: Theory and Practice. His slide are available.
- Jun 2013: Fabien Renaud present the paper Checking foundational proof certificates for first-order logic (extended abstract) by Zakaria Chihani, Dale Miller, and Fabien Renaud at PxTP 2014: Proof Exchange for Theorem Proving, 9-10 June 2013, Lake Placid, USA.
- Jun 2013: Zak Chihani present these slides during the CADE 24 meeting.
- Mar 2013: The paper Foundational proof certificates in first-order logic, by Z. Chihani, D. Miller, and F. Renaud was accepted to CADE 24. The λProlog implementation of the proof checking framework reported in that paper is available (22 Jan 2013). Both the paper and the implementation will be revised prior to 1 April 2013.
- Nov 2012: NSF and the ERC will soon lunch a new program to encourage NSF CAREER awardees and NSF postdoctoral Fellows to conduct research visits within ERC funded projects. Read more.
- Sep 2012: The interns have completed their projects. This month Zak Chihani will start his PhD and Fabien Renaud starts his postdoc, both funded by ProofCert.
- Feb 2012: Two internships are proposed for Spring 2012. These can lead to a PhD supported by this grant.
- Feb 2012: ProofCert has one open PostDoc position.
- On 18 November 2011, Miller presented ProofCert to the Scientific Council of INRIA with these slides.
- European Research Council press release on 2011 Advanced Investigator Grants, 24 January 2012.
- INRIA has announced this award: French and English.
