Formalization of

"A Type-Theoretic Framework for Software Component Synthesis"

by Jan Bessai. Available via DOI 10.17877/DE290R-20320

Requires Coq 8.8.0-8.9.1 and mathcomp-1.8.0.

Compile by running

make

in this directory.

See extracted/README.md for instructions on extracted code.