 | Home | Last modified: August 10, 2021 |
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 OCaml source code for the FORK type-checker, as well as the FORK code for the encoding of references. It also contains a Coq proof that the encoding is semantics-preserving.
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.