Galois is pleased to host the following tech talk.
These talks are open to the interested public–please join us!
(There is no need to pre-register for the talk.)
title:
Formalizing Haskell 98 in the K Semantic Framework
speaker:
David Lazar
time:
Tuesday, 10 January 2012, 10:30am
location:
Galois Inc.
421 SW 6th Ave. Suite 300,
Portland, OR, USA
(3rd floor of the Commonwealth building)
abstract:
Formal semantics is notoriously hard. The K semantic framework is a system that makes the task of formally defining programming languages easy and practical. The primary goals of the K framework are modularity, expressivity, and executability. Adding a new language feature to a K definition does not require you to revisit and modify existing semantic rules. The K framework is able to concisely capture the semantics of non-determinism and concurrency. Each K definition automatically yields an interpreter for the language so that the definition can be tested for correctness. These features made it possible to develop a complete formal semantics of the C language in K.
The first half of the talk will be an overview of the K semantic framework. We’ll discuss the merits of the framework using the K definition of a complex toy language as a guiding example. The second half of the talk will focus on a work-in-progress formalization of Haskell 98 in K. We’ll look at the challenges of formalizing Haskell and the applications of this work.
bio:
David Lazar is an undergraduate studying computer science at the University of Illinois at Urbana-Champaign. He is one of several developers of the K framework. This summer, he worked on formalizing Haskell in K as a Google Summer of Code student.