University of Illinois Urbana-Champaign

Haskel syntax and static semantics written in K-framework

Morrell, Bradley

This item is only available for download by members of the University of Illinois community. Students, faculty, and staff at the U of I may log in with your NetID and password to view the item. If you are trying to access an Illinois-restricted dissertation or thesis, you can request a copy through your library's Inter-Library Loan office or purchase a copy directly from ProQuest.

Permalink

https://hdl.handle.net/2142/105410

Description

Title
Haskel syntax and static semantics written in K-framework
Author(s)
Morrell, Bradley
Contributor(s)
Gunter, Elsa
Issue Date
2018-12
Keyword(s)
  • Haskell
  • Type-System
Abstract
This thesis introduces a static semantics for Haskell by utilizing the K-framework. This implementation includes support for the module system of Haskell but not for type classes. Many layers have to be implemented in K before type inference can be performed. The first part of the implementation is the entire context-free syntax of Haskell in K. Since all the syntax is included, any program written in Haskell extended syntax can be parsed into an abstract syntax tree. However, this includes only the Haskell extended syntax, not syntactic short-cuts such as treating tabs as syntactic sugar for grouping constructs such as curly braces. Programs that include multiple modules can be parsed, but the multiple modules must be written in a single file. This is unlike how the Glasgow Haskell Compiler allows for module imports, where each module must be kept in a separate file. The multiple modules are then made as nodes in a directed acyclic graph. A directed edge in the graph represents a module importing another module. This graph is used for importing the user-defined types from one module into another module. Context-sensitive checks and type inference are then performed on modules. The static semantics specifies that, at each node in the graph, assuming all child modules are already checked and inferred, the user-defined types of each of the child modules are imported into the module at the given node. All rules of the Haskell type system must take mutual recursion into account. There is repeated layering of inferences in Haskell. Due to being written in K, the semantics introduced here is mathematically precise and executable. Since the semantics is executable, the semantics can be tested against test sets to validate the correctness of the semantics. The executability of the semantics was utilized to test both positive inferences and exceptional inferences. This is part of a larger project to give a formal semantics to Haskell.
Type of Resource
text
Language
en
Permalink
http://hdl.handle.net/2142/105410

Owning Collections

Senior Theses - Electrical and Computer Engineering PRIMARY
The best of ECE undergraduate research