« Galois is Hiring! | Main | Tech talk: Parallel K-induction based Model Checking »

Tech talk: Combining Denotational and Operational Semantics for Scalable Proof Development

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


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.

Reader Comments (3)

Did you record this tech talk, and if so, will you post the video online? Thanks!
July 17, 2011 | Unregistered CommenterErik Helin
@ErikSeeing as the talk has yet to happen, having a recording of it already would be one remarkable feat.
July 18, 2011 | Unregistered CommenterThomas M. DuBuisson

So, now that it's been a while since the talk, will it be online?

August 9, 2011 | Unregistered CommenterUlrik

PostPost a New Comment

Enter your information below to add a new comment.

My response is on my own website »
Author Email (optional):
Author URL (optional):
Some HTML allowed: <a href="" title=""> <abbr title=""> <acronym title=""> <b> <blockquote cite=""> <code> <em> <i> <strike> <strong>