BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Bedrock: A Software Development Ecosystem Inside a Proof Assistant
   - Adam Chlipala\, MIT
DTSTART:20141215T100000Z
DTEND:20141215T110000Z
UID:TALK56590@talks.cam.ac.uk
CONTACT:Microsoft Research Cambridge Talks Admins
DESCRIPTION:The benefits of formal correctness proofs for software are cle
 ar intuitively\, but the high human costs of proof construction have gener
 ally been viewed as prohibitive. The speaker believes that pervasive verif
 ication 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 achiev
 e the virtue of correct programs\; formal methods also suggest new program
 ming approaches that better support abstraction and modularity than do coa
 rser-grained specification styles like normal static types.\n\nThis talk o
 verviews 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 v
 erified 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 acr
 oss source languages). A few different programming styles have been connec
 ted 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 spec
 ifications that are refined automatically into assembly code with correctn
 ess proofs.\n\nThe talk will present Bedrock's shared foundation and sketc
 h the pieces that go into refining declarative specifications into closed 
 assembly programs\, covering joint work with Thomas Braibant\, Santiago Cu
 ellar\, Benjamin Delaware\, Jason Gross\, Gregory Malecha\, Clément Pit--
 Claudel\, and Peng Wang\n
LOCATION:Auditorium\, Microsoft Research Ltd\, 21 Station Road\, Cambridge
 \, CB1 2FB
END:VEVENT
END:VCALENDAR