## Profile

## Stream

### Dale Miller

Shared publicly -Abstract: In the mist of feeling insecure with our electronic communications, we can take solace in the advice that we can "trust the math" behind cryptography. Faced with concerns over the safety of fly-by-wire planes and self-driving cars, we should be able to find solace in the fact that some parts of our safety critical systems have been proved formally correct: that is, we should be able to "trust the proof". The way formal proofs are built today, however, makes trusting them difficult. While proof assistants are used to build formal proofs, those proofs are often locked to that assistant. Formal proofs produced by one proof assistant cannot usually be checked and trusted by another proof assistant nor by a future version of itself. Thus, one of the components of the scientific method that ensures trust---reproducibility---is missing from proof checking.

The field of proof theory, as initiated by Gentzen in the 1930's, has identified a great deal of structure in formal proofs. Given recent developments in this topic, it is now possible to apply what we know about proofs in theory to what we would like to have for proofs in practice. To that end, I will present the Foundational Proof Certificates framework for defining the semantics of proof evidence. Since such definitions are executable, it is possible to build proof checkers that can check a wide range of formal proofs. In this scheme, the logic engine that executes such definitions is the only thing that needs to be trusted. Since such a logic engine is based on well-known computational logic topics, anyone can write a logic engine in their choice of programming language and hardware in order for them to build a checker they can trust. I will also overview some of the consequences of defining proofs in this manner: provers can become networked far more richly than they are currently and both libraries and marketplaces of proofs are enabled in a technology independent fashion.

### Dale Miller

Shared publicly -### Dale Miller

Shared publicly -### Dale Miller

Shared publicly -### Dale Miller

Shared publicly -### Dale Miller

Shared publicly -supported by the ERC Advanced Grant ProofCert and are part of a long-term effort to build trustable proof checkers for a wide variety of proof structures.

### Dale Miller

Shared publicly -``Abella: A System for Reasoning about Relational Specifications'' by David Baelde, Kaustuv Chaudhuri, Andrew Gacek, Dale iller, Gopalan Nadathur, Alwen Tiu, and Yuting Wang

This prover reasons directly with inductively and co-inductively defined relations (instead of functions). Particularly novel features of Abella include its support for lambda-tree syntax, the nabla-quantifier, and the two-level logic approach to reasoning with logic specifications.

### Dale Miller

Shared publicly -### Dale Miller

Shared publicly -If this sounds interesting,

*please*: don't just +1 it,

**reshare**it. Why? To keep costs down and retain ownership of the conference with the community, we are independent, not affiliated with any organizations. That means

**you**are the

*only*PR channel we have. So please do us a favor. Thanks.

### Dale Miller

Shared publicly -http://vsl2014.logic.at

### Dale Miller

Shared publicly -- INRIA & LIX/Ecole PolytechniqueDirector of Research, present
- University of Pennsylvania, Penn State, INRIA, Ecole Polytechnique

- My publications and talk (current)
- Book: Programming in Higher-Order Logic (current)

- Carnegie Mellon UniversityMathematics, 1978 - 1983
- Lebanon Valley CollegeMathematics, 1974 - 1978

Polarity in Type Theory existentialtype.wordpress.com There has recently arisen some misguided claims about a supposed opposition between functional and object-oriented programming. The claims a |

Abella abella.cs.umn.edu Description. Abella is an interactive theorem prover based on lambda-tree syntax. This means that Abella is well-suited for reasoning about |

Gopalan Nadathur www.cs.umn.edu Contents. Research Interests and Activities; My Research Papers; Some Recent Talks; Teyjus--A Lambda Prolog Implementation; Conference Progr |

Bedwyr slimmer.gforge.inria.fr Bedwyr: A proof search approach to model checking. Overview. Bedwyr is a generalization of logic programming that allows model checking dire |

λProlog - Wikipedia, the free encyclopedia en.wikipedia.org λProlog. From Wikipedia, the free encyclopedia. Jump to: navigation, search. λProlog, also written lambda Prolog, is a logic programming lan |

Bienvenue dans l'igloo de mrpingouin! www.lix.polytechnique.fr David Baelde. I'm a computer science researcher. I'm generally interested in the foundations of logics and programming. I work mostl |

ProofCert » Parsifal team.inria.fr ProofCert: Broad Spectrum Proof Certificates. ProofCert is the name of an ERC Advanced Grant awarded to Dale Miller for the five years 2012- |

Parsifal » team.inria.fr Preuves Automatiques et Raisonnement sur des SpécIFicAtions Logiques. Parsifal has been a team within LIX since September 2003 and an INRIA |

CPP 2012 cpp12.kuis.kyoto-u.ac.jp The CPP and APLAS meetings will share two keynote speakers. We are delighted that. Xavier Leroy, INRIA and; Greg Morrisett, Harvard Universi |

NASA -
Opportunity's Selfie www.nasa.gov NASA's Mars Rover Opportunity catches its own late-afternoon shadow in this dramatically lit view eastward across Endeavour Crater on Mars. |

A CS Professor's blog: Harvard: a model for French universities? teachingintrotocs.blogspot.com Yesterday's issue of Le Monde newspaper had a full page article on everything that is admirable about Harvard, the "best university |

Papers and Talks of Dale Miller www.lix.polytechnique.fr A Proof-Theoretic Approach to the Static Analysis of Logic Programs by Dale Miller. In Reasoning in Simple Type Theory: Festschrift in honou |

Pisa Summer Workshop on Proof Theory www.helsinki.fi [Arno]. Pisa Summer Workshop on Proof Theory. Pisa, Italy, 12-15 June 2012. Organizers: Department of Philosophy, University of Pisa; Depart |

Andrew Gacek www.cs.umn.edu I'm the one in the middle :-). Andrew Gacek. Department of Computer Science and Engineering. Institute of Technology. University of Minn |

Home Page | CPP 2011 formes.asia First International Conference on. Certified Programs and Proofs. (CPP 2011). December 7–9, 2011, Taiwan. http://formes.asia/cpp. (co-locate |

Catuscia Palamidessi's home page www.lix.polytechnique.fr INRIA Saclay and LIX LIX, École Polytechnique, Rue de Saclay, 91128 Palaiseau Cedex, FRANCE Office: +33 (0)1 69 33 41 17 Assistant: +33 (0)1 |

λProlog Home Page www.lix.polytechnique.fr λProlog. Programming with higher-order logic. λProlog is a logic programming language based on an intuitionistic fragment of Church's Si |