i wish there were a strictly typed LISP using a hindley-milner type system
i guess the closest is the toy language used in The Little Typer
even though the pi calculus is decidedly not hindley-milner
Follow
the calculus of inductive constructions would be an acceptable alternative i guess
