| Home | Phone: +33 1 39 63 52 64 | Last modified: January 12, 2010 |
The FORK calculus is a version of system F-Omega with (certain) Recursive Kinds. This calculus is sufficiently expressive to permit a type-safe encoding of general references. Both the calculus and this encoding are described in this paper.
This archive contains the Objective Caml source code for the FORK type-checker, as well as the FORK code for the encoding of references.
This archive contains the Coq source code for a formalization of a type system by Hiroshi Nakano which the definition of FORK builds upon. The formalization contains a proof of subject reduction, a construction of the realizability model that allows proving that a well-typed term admits a head normal form, as well as a novel algorithm for deciding whether two types are in the subtyping relation. It is currently in a somewhat rough state. It is made available as a complement to the FORK paper.