Dale's posts

Post has shared content

Public

Morning people are in for a treat this week: http://bit.ly/1S90qRY

Post has attachment

Public

Congratulations to Mario, Kostas, Annabelle, Carroll, Catuscia, and Geoffrey! "Their work is a stellar example of scholarship and it provides fascinating insights into security defenses from an information-flow perspective..."

Post has attachment

Public

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.

Post has attachment

Public

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.

Post has attachment

Public

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.

Post has attachment

Post has attachment

Public

Post has attachment

Public

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.

Post has shared content

Public

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,

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. Post has attachment

Public

The Tour de France has just moved through Orsay.

2014-07-27

2 Photos - View album

Wait while more posts are being loaded