BEGIN:VCALENDAR PRODID;X-RICAL-TZSOURCE=TZINFO:-//Calagator//EN CALSCALE:GREGORIAN X-WR-CALNAME:Calagator METHOD:PUBLISH VERSION:2.0 BEGIN:VTIMEZONE TZID;X-RICAL-TZSOURCE=TZINFO:America/Los_Angeles BEGIN:DAYLIGHT DTSTART:20110313T020000 RDATE:20110313T020000 TZOFFSETFROM:-0800 TZOFFSETTO:-0700 TZNAME:PDT END:DAYLIGHT END:VTIMEZONE BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20110714T200247Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20110719T113000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20110719T103000 DTSTAMP;VALUE=DATE-TIME:20110714T200247Z LAST-MODIFIED;VALUE=DATE-TIME:20110714T200247Z UID:http://calagator.org/events/1250460825 DESCRIPTION:Presented by Adam Foltzer. \;\n \;\nInterpreters 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 impossibl e to write interpreters for non-terminating languages. The standard alte rnative is to inductively define operational semantics\, but this can yi eld proofs that are difficult to automate\, particularly in the presence of changing language features. \;\n \;\nThis talk presents a comb ined approach\, where an interpreter is used in combination with operati onal semantics to prove type preservation of a small functional language . To demonstrate the scalability of the Coq development\, let expression s and a pair types will be added and preservation will be proved again w ith only one extra line of proof script. \;\n \;\nThis technique a nd development are adapted from Greg Morrisett's lectures at the 2011 Or egon Programming Languages Summer School\, and are available at his web site.\n\nTags: galois\, tech talk\, theorem proving\, coq\n\nImported fr om: http://calagator.org/events/1250460825 URL:http://corp.galois.com/blog/2011/7/14/tech-talk-combining-denotationa l-and-operational-semantics-f.html SUMMARY:Galois tech talk: Combining Denotational and Operational Semantic s for Scalable Proof Development LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:1 END:VEVENT END:VCALENDAR