Hacker News new | past | comments | ask | show | jobs | submit login

Why not just learn Coq or Agda yourself? There are also sorts of introductions for simple type systems that I'm sure you can build off of.

I have no idea how to implement fresh unification variable generation (my type system is a superset of Damas-Milner, kind of like how the calculus of constructions is a superset of System F-omega) in Coq or Agda. Everywhere I've seen it implemented, it involves mutable state. So, “in principle”, I could fake it using something like the state monad, and plumbing around the collection of unification variables generated so far, but in practice reasoning about this seems like a pain.

You could take a look at Coquand (2002) “A formalised proof of the soundness and completeness of a simply typed lambda-calculus with explicit substitutions”.


Drop in to #dependent on Freenode IRC, and let’s chat.

Guidelines | FAQ | Support | API | Security | Lists | Bookmarklet | Legal | Apply to YC | Contact