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

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 ...
Christopher King's user avatar
0 votes
3 answers

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 ...
Pietro Braione's user avatar
11 votes
1 answer

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 ...
Couchy's user avatar
  • 2,211
14 votes
4 answers

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 ...
Will Sawin's user avatar
17 votes
1 answer

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 ...
hardmath's user avatar
  • 539