A dependently typed system for the Hash programming language
What is the difference between math and programming? This project is an implementation of a dependent type system for an imperative programming language called Hash. Beyond standard programming language features, it supports pattern matching, compile time execution and even theorem proving through indexed inductive types, making it a suitable site for doing math. The dissertation discusses the design and implementation of this system written in Rust, explores examples, and considers some fundamental paradigm shifts that arise when types themselves are subject to computation.
Keywords
Compilers, Language Theory, Language Design, Type Systems, Functional Programming, Dependent Type Systems, Proof Systems
Staff
[Christopher Brown]{cmb21}