Research on "Formal Methods in Computing"

Rank 2 Intersection Types for (a subset of) Caml

This page demonstrates a prototype implementation of a rank 2 intersection type system for higher order functional languages. The current version of the prototype (released in October 2003, developed by Emiliano Leporati - thanks to Sebastien Carlier for pointing out some bugs in an earlier version of the prototype):

• Implements the type system described in [ Damiani, 2003 ].
• Is based on an earlier prototype (carried on as part of the Master Thesis [ Leporati, 2000 ]) for a preliminary version of the type system (presented in [ Damiani, 2000 ]).
• Is written in O'Caml .
• Accepts as input a subset of (O')Caml itself - the language considered by the implementation is richer than the one considered in the report [ Damiani, 2003 ] (in particular it includes top-level definitions and datatype declarations).

Type a program in the form below and press the button.

• Parsing is not particularly smart. For instance, all the infix operators have the same precedence. To avoid problems, it is better to use a lot of parentheses.

Here you can find a description of the accepted SYNTAX and some EXAMPLES that you can copy and paste.