"modern" haskell implementation of the algorithm described in the paper of the same name.
You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
Rachel Samuelsson cb00846b94 include application test 7 months ago
Algo.hs include application test 7 months ago
README.md initial commit 7 months ago


An algorithm for type-checking dependent types

A “modern” implementation of algorithm described in Thierry Coquand’s paper. This employs some monad nicities compared to the haskell implementation in the paper (and isn’t a pdf).

This isn’t meant to be “better”, it might even be more confusing to you. I wrote this to get more of a feel for checking dependent types.