Galois Tech Talk (1 of 3 next week!): Formalizing Haskell 98 in the K Semantic Framework

  • Date Thursday, January 1, 1970  Time
  • Speaker
  • Location

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.)

Formalizing Haskell 98 in the K Semantic Framework

David Lazar

Tuesday, 10 January 2012, 10:30am


Galois Inc.

421 SW 6th Ave. Suite 300,

Portland, OR, USA

(3rd floor of the Commonwealth building)


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.

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.