|
Change #31859
2015-01-15
10:14:26
|
create
Calagator::Event
1250467646
Galois tech talk: Combining Denotational and Operational Semantics for Scalable Proof Development
Roll back
| description |
nil |
→ |
Presented by Adam Foltzer.
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. |
| end_time |
nil |
→ |
2015-01-15 11:30:00 -0800 |
| id |
nil |
→ |
1250467646 |
| start_time |
nil |
→ |
2015-01-15 10:30:00 -0800 |
| title |
nil |
→ |
Galois tech talk: Combining Denotational and Operational Semantics for Scalable Proof Development |
| url |
nil |
→ |
http://corp.galois.com/blog/2011/7/14/tech-talk-combining-denotational-and-operational-semantics-f.html |
| venue_id |
nil |
→ |
202390439 |
|