Galois is pleased to host the following tech talk. These talks are open to the interested public. Please join us!
title:Combining Denotational and Operational Semantics for Scalable Proof Development
speakers:Adam Foltzer
time:Tuesday, 19 July 2011, 10:30am
location:
Galois Inc.
421 SW 6th Ave. Suite 300,
Portland, OR, USA
(3rd floor of the Commonwealth building)
abstract:Interpreters offer a convenient and intuitive way for programmers to reason about language behavior through denotational semantics. However in a setting like Coq, where all recursive functions must provably terminate, it is impossible to write interpreters for non-terminating languages. The standard alternative is to inductively define operational semantics, but this can yield proofs that are difficult to automate, particularly in the presence of changing language features.
This talk presents a combined approach, where an interpreter is used in combination with operational semantics to prove type preservation of a small functional language. To demonstrate the scalability of the Coq development, let expressions and a pair types will be added and preservation will be proved again with only one extra line of proof script.
This technique and development are adapted from Greg Morrisett’s lectures at the 2011 Oregon Programming Languages Summer School, and are available at his web site.
bio: Adam Foltzer is an Intern at Galois, Inc. and a Master’s student at Indiana University studying programming languages.