All Questions
Tagged with foundations coq
1
question
11
votes
1
answer
614
views
What is the role of impredicativity in program extraction?
Is impredicativity useful for program extraction in Coq? For example is there some kind of realizability argument that depends on impredicativity?
Of course it doesn't seem to be necessary for program ...
- 2,300