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

Start a hangout

Dale Miller

Works at INRIA & LIX/Ecole Polytechnique

Attended Carnegie Mellon University

Lives in Orsay, France

226 followers|192,075 views

AboutPostsPhotos+1's

One or two postdoctoral positions are available from Inria-Saclay within the LIX laboratory of Ecole Polytechnique. These positions are

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.

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.

1

1

Add a comment...

A new tutorial on how to use the Abella interactive theorem prover is available from the Journal of Formalized Reasoning.

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

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

4

1

Add a comment...

@Maclomaclee looks a bit like Fig 7 in bit.ly/1qYfz6A · 27 minutes ago. You must listen to BBC R4 Soul Music, on La Bohème bbc.in/1wbjhhR (and see bit.ly/1wbjeCu ). 35 minutes ago · @Maclomaclee CL are just another way of expressing P values, so suffer from the same problems ...

1

Add a comment...

The call-for-papers for the 42nd International Colloquium on Automata, Languages, and Programming (ICALP 2015) is now on line. The meeting will take place in Kyoto, Japan during 6-10 July 2015.

1

Add a comment...

The Tour de France has just moved through Orsay.

2 photos

3

Add a comment...

The ACM Special Interest Group on Logic and Computation (SIGLOG) is now open for membership.

The ACM Special Interest Group on Logic and Computation (SIGLOG) is a community organization dedicated to the advancement of logic and computation, and formal methods in Computer Science, broadly defined. SIGLOG aims to serve a broad range of interests. The flagship conference will be the ...

6

6

Add a comment...

The Vienna Summer of Logic should be the largest event in the history of logic. The call for volunteers to help with this meeting is now open. In 1983, I volunteered for a meeting on the lambda-calculus and functional programming and I was able to meet Church, Curry, and Rosser among others giants of the field. I'm sure that this summer's meeting will offer young attendees similar opportunities.

3

Add a comment...

In his circles

411 people

I gave a CS Department Colloquium on "Communicating and trusting formal proofs" at ETH Zurich on 20 April. You can find the slides and audio of this talk as a video on their multimedia portal.

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.

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.

Multimedia Portal, Podcast Portal

2

3

Add a comment...

Cory Doctorow on why privacy is about more than concealing crime—and why backdoors are inevitably available to everyone, not just people you trust.

1

Add a comment...

Tom Ball, Ras Bodik, +Greg Morrisett, and I are organizing a new kind of programming languages conference. We already have several excellent conferences, but they are focused on incremental bits of novelty. We want to create a new kind of venue that complements these: to present and discuss big-picture questions and long-running programs; to view progress along the long arc of a research effort. The conference is May 3-6, 2015 in lovely Asilomar (on the Pacific Coast), CA, USA.

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.

If this sounds interesting,

1

2

Add a comment...

It's time to register for the Vienna Summer of Logic, July 9-24, 2014.

http://vsl2014.logic.at

http://vsl2014.logic.at

1

1

Add a comment...

I am looking for two PhD students and two post doc to start in Fall 2014.

1

4

Add a comment...

People

In his circles

411 people

Work

Occupation

Director of Research

Employment

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

Places

Currently

Orsay, France

Previously

Annville, Pennsylvania, USA - Nervi, Genoa, Italy - Edinburgh, Scotland - Boalsburg, PA, USA - Pittsburgh, PA, USA - Philadelphia. PA, USA

Links

YouTube

Other profiles

Contributor to

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

Story

Introduction

Raised in Annville, Pennsylvania. Undergraduate studies at Lebanon Valley College. Graduate studies at Carnegie Mellon University. Fourteen years on the faculty of the University of Pennsylvania and five years on the faculty of Penn State. Since 2002, Director of Research at INRIA Saclay & LIX/Ecole Polytechnique, outside Paris, France.

Education

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

Basic Information

Gender

Male

Dale Miller's +1's are the things they like, agree with, or want to recommend.

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 |