rachel/an-algorithm-for-checking-dependent-types
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
"modern" haskell implementation of the algorithm described in the paper of the same name.
2 Commits 1 Branch 0 Tags 29 KiB
Haskell 100%
master
Go to file
depsterr cb00846b94 include application test
2022-05-12 19:01:19 +02:00
Algo.hs include application test 2022-05-12 19:01:19 +02:00
README.md initial commit 2022-05-12 18:52:25 +02:00

README.md

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.