ProofCert: Broad Spectrum Proof Certificates
This web page will be migrating
ProofCert is the name of
an ERC Advanced
Grant awarded to Dale
Miller for the five years 2012-2016.
The following is taken from the proposal's abstract.
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
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.
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
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 (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
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 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
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
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,
- 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,
- 1 Dec 2015: Huge Steele begins a one year postdoc position on the
- 2 Nov 2015: Zak Chihani defended his PhD today. His thesis title
is “Certification of First-order proofs in classical and
- 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
- Nov 2014: Sonia Marin (PhD student) and Giselle Reis and Marco
Volpe (PostDocs) have joined Parsifal to work on the ProofCert
- Oct 2014: Rob Blanco (PhD student) and Taus Brock-Nannestad
(PostDoc) have joined Parsifal to work on the ProofCert
- 31 July 2014: Siddhartha Prasad completed a two month internship
in the team. His work on equality certificates
- 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
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.
- Jun 2013: Fabien Renaud present the
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
during the CADE 24 meeting.
- Mar 2013: The
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
(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
- 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
- On 18 November 2011, Miller presented ProofCert to
Council of INRIA
- European Research
release on 2011 Advanced Investigator Grants, 24 January
- INRIA has announced this