A Logic for Correct Program Development. - Joseph L. Bates (1979)

Writing Programs that Construct Proofs. - Robert L. Constable; Todd B. Knoblock; Joseph L. Bates (J. Autom. Reason., 1985)

Proofs as Programs. - Joseph L. Bates; Robert L. Constable (ACM Trans. Program. Lang. Syst., 1985)