Questions tagged [program-extraction]

Normally a proof assistant is used to complete a proof. As a side effect source code may be generated.

Filter by
Sorted by
Tagged with
10 votes
1 answer
484 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 ...
user avatar
  • 1,662
14 votes
4 answers
262 views

Algorithms obtained through constructive formalization

Formal proofs in proof systems that avoid the law of the excluded middle and certain other principles can be automatically converted into algorithms. What useful new algorithms have been produced by ...
user avatar
15 votes
1 answer
151 views

WLOG reasoning and Proof Assistants

The possibility of using proof assistants in combinatorics has been mentioned here and in more detail here. I'm interested in automating that part of some discrete problems which reduces the search ...
user avatar
  • 509