/f-multi-sub-fcc

Coq formalization of F{≤} ~> System Fcc (coercion framework)

Primary LanguageCoq

Coq formalization of System Fcc

System Fcc is a kernel type system designed following a unified approach with coercions.

It is documented in my PhD: http://phd.ia0.fr/

The development is done with the 8.4pl2 version of Coq.