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.
-
Notifications
You must be signed in to change notification settings - Fork 2
Coq formalization of System Fcc (coercion framework)
ia0/fcc
About
Coq formalization of System Fcc (coercion framework)