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
4 votes
2 answers
172 views

Which proof assistants implement Church's rule?

Church's rule (CR) is one of the hallmarks of constructive mathematics, and is an admissible rule in a wide variety of constructive theories (you might consider CR to be a requirement for constructive ...
0 votes
3 answers
158 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 ...
11 votes
1 answer
605 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 ...
14 votes
4 answers
314 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 ...
17 votes
1 answer
203 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 ...