Proofs as Programs.

Joseph L. Bates Robert L. Constable

Published in: ACM Trans. Program. Lang. Syst. (1985)

Keyphrases

computer programs
theorem proving
programming environment
automatic programming
prolog programs
data sets
theorem prover
intermediate level
formal proofs
computer vision
data structure
probabilistic model
fixpoint
natural deduction
provably correct
formal proof