2 ms·
Not necessarily. Isabelle/HOL, an prover not based on CH but on the LCF-architecture, can also do program extraction, see e.g. Program extraction in Isabelle:
by mafribe 9y ago
Not necessarily. Isabelle/HOL, an prover not based on CH but on the LCF-architecture, can also do program extraction, see e.g. Program extraction in Isabelle:
https://wwwbroy.in.tum.de/~berghofe/papers/TYPES2002_slides.pdf https://wwwbroy.in.tum.de/~berghofe/papers/TYPES2002_slides....