Axiomatic Constructor Classes in Isabelle/HOLCF

We have definitionally extended Isabelle/HOLCF to support axiomatic Haskell-style constructor classes. We have subsequently defined the functor and monad classes, together with their laws, and implemented state and resumption monad transformers as generic constructor class instances. This is a step towards our goal of giving modular denotational semantics for concurrent lazy functional programming languages, such as GHC Haskell.

• Type: Conference
• Year: 2005
• Where: TPHOL
• Authors: Brian Huffman, John Matthews, Peter White
• Keywords: Artificial Intelligence, Axiomatic Haskell-style Constructor, Constructor Class Instances, Resumption Monad Transformers, TPHOL 2005