Towards Extraction of Continuity Moduli in Coq

Saarland University Computer Science

Yannick Forster, Dominik Kirst, Florian Steinberg

We report on a work-in-progress extraction of continuity information for Coq functionals on Baire space. The extraction is implemented as a MetaCoq plugin and generates a certified modulus function, given a term in the System T fragment of Coq. In fact, the extraction first reifies Coq definitions into a syntactic representation of System T and subsequently employs a constructive and informative continuity theorem for System T following Escardó.


Coq Formalisation (Coq version 8.9.1 with MetaCoq installed)