Type checker

[Jay McCarthy]

Here's a simple verified and extracted type checker in Coq.

https://github.com/jeapostrophe/exp/blob/master/coq/STAE.v

The theorem is "ty_dec":

https://github.com/jeapostrophe/exp/blob/master/coq/STAE.v#L170

The extraction is here:

https://github.com/jeapostrophe/exp/blob/master/coq/STAE.ml#L95

--
Jay McCarthy <j...@cs.byu.edu>
Assistant Professor / Brigham Young University
http://faculty.cs.byu.edu/~jay

"The glory of God is Intelligence" - D&C 93