concl.tex

\chapter{Conclusion}

The Haskell 2010 report gives a semi-formal outline of the Haskell type system. It also describes it as a Hindley Milner polymorphic type system. However, the original Hindley Milner polymorphic type system is based on a simpler ML system. Haskell, on the other hand, being a modern real world language, is much more complex and requires parsing, preprocessing, modules, expressions, declarations, and other elements. On top of this, Haskell includes mutually recursive functions which need to be inferred. One such inference rule which allows for mutual recursion is presented in this paper. Ultimately, defining a formal syntax and semantics in K allows one to not only automatically convert the formal semantics into proofs in an automatic theorem prover, but also execute example programs using the formal semantics. This allows a formal semantics to be validated by passing the test suite provided for compilers. Defining yet another real word language in K allows the K-framework to become more popular as another community can learn about it and utilize it. The more that real world languages are defined in K, the more potential K has to become a popular language in industry.