coq

Fi+

Coq formalization and implementation of the Fi+ calculus

NeColus

Coq formalization of a coherent calculus with records and disjoint intersection types that supports nested composition