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

  • Date  Time 12:00 AM
  • 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.)

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.