|
(via comp.lang.functional)
This web application provides a friendly tool for experimenting with System I. System I allows inferring principal typings for pure terms of the lambda-calculus with intersection types for arbitrary finite ranks. It is particularly interesting because it can infer types for terms that cannot be typed in other commonly studied systems, as well as the fact that due to the principal typing property, type inference is compositional.
More information about this project is available.
More on prinicipal typing.
Posted to theory by Ehud Lamm on 6/9/02; 8:05:19 AM
|
System I Experimentation Tool
