Bedrock: A Software Development Ecosystem Inside a Proof Assistant

Add to your list(s) Download to your calendar using vCal

• Adam Chlipala, MIT
• Monday 15 December 2014, 10:00-11:00
• Auditorium, Microsoft Research Ltd, 21 Station Road, Cambridge, CB1 2FB.

If you have a question about this talk, please contact Microsoft Research Cambridge Talks Admins.

This event may be recorded and made available internally or externally via http://research.microsoft.com. Microsoft will own the copyright of any recordings made. If you do not wish to have your image/voice recorded please consider this before attending

The benefits of formal correctness proofs for software are clear intuitively, but the high human costs of proof construction have generally been viewed as prohibitive. The speaker believes that pervasive verification of deep theorems about software will never be common until formal methods are integrated within the software development process. To support that integration, we need to rethink the familiar programming toolchains. The new world needn’t be all about doing prodigious extra work to achieve the virtue of correct programs; formal methods also suggest new programming approaches that better support abstraction and modularity than do coarser-grained specification styles like normal static types.

This talk overviews Bedrock, a framework for certified programming inside of the Coq proof assistant. Bedrock programs are implemented, specified, verified, and compiled inside of Coq. A single program may be divided into modules with formal interfaces, written in different programming languages and verified with different proof styles. The common foundation is an assembly language with an operational semantics (serving as the trusted code base) and a semantic module system (orchestrating linking of code and proofs across source languages). A few different programming styles have been connected to the shared foundation, including a C-like language with an “array of bytes” memory model, higher-level more C++-like languages with “array of abstract data types” memory models, a domain-specific language for XML processing, standard Coq functional programs, and even declarative specifications that are refined automatically into assembly code with correctness proofs.

The talk will present Bedrock’s shared foundation and sketch the pieces that go into refining declarative specifications into closed assembly programs, covering joint work with Thomas Braibant, Santiago Cuellar, Benjamin Delaware, Jason Gross, Gregory Malecha, Clément Pit—Claudel, and Peng Wang

This talk is part of the Microsoft Research Cambridge, public talks series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Auditorium, Microsoft Research Ltd, 21 Station Road, Cambridge, CB1 2FB
• Cambridge Centre for Data-Driven Discovery (C2D3)
• Cambridge talks
• Chris Davis' list
• Guy Emerson's list
• Interested Talks
• Microsoft Research Cambridge, public talks
• Optics for the Cloud
• PMRFPS's
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• ndk22's list
• ob366-ai4er
• personal list
• rp587

Note that ex-directory lists are not shown.