PRL Seminars

Type inference for Nuprl is undecideable, even for small subsets like the analogue of F2 in Nuprl. This leads to the need of development of heuristics, which will facilliate direct embedding of ML programs into Nuprl.

In this talk, I will give an overview of the type inference algorithm I developed. The algorithm works for the subset of Nuprl,which consists of lambda expressions+universes+dependent function types, although the ideas are readily expandable to all of Nuprl.