Formal Executable Semantics of Haskell

by David Lazar for Portland State University

The K semantic framework was developed to address the shortcomings of previous semantic frameworks which were non-modular, non-executable, and non-concurrent. This summer I will formalize the dynamic semantics of Haskell 98 in the K semantic framework. The framework will yield an interpreter for Haskell 98 which allows the semantics to be tested. The semantics will be modular so it can easily be extended to Haskell 2010 and to include other language extensions.