Questions tagged [program-extraction]
Normally a proof assistant is used to complete a proof. As a side effect source code may be generated.
4
questions
0
votes
3
answers
130
views
How do I extract efficient string code in Coq to OCaml?
I have a Gallina (Coq) program that I am extracting to OCaml. The program is a (symbolic) interpreter for a small programming language, and I defined functions to stringify the states so I can print ...
- 212
11
votes
1
answer
592
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,171
14
votes
4
answers
305
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 ...
- 891
17
votes
1
answer
199
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 ...
- 539