Course:CPSC312-2017-Haskell-Proof-Checker

Haskell - Proof Assistant

Authors: Addison Sasko , Reed Mullanix

What is the problem?

This project aims to write a simple proof-of-concept proof assistant in Haskell. A proof assistant is something used to verify that a mathematical proof is free of certain classes of errors.

What is the something extra?

This project will require implementing a stronger type system then currently exists in Haskell (probably, maybe?). It will also require a decent background in type theory, as well as an understanding of parsing and interpreter design (CPSC 311).

What did we learn from doing this?

We learned that haskell is an excellent tool for creating a programming language. The source can be found here