Informal proofs formally checked by machine
Annales scientifiques de l'Université de Clermont. Mathématiques, Volume 60 (1976) no. 13, p. 31-53
@article{ASCFM_1976__60_13_31_0,
     author = {Aiello, Luigia and Aiello, Mario and Attardi, Giuseppe and Prini, Gianfranco},
     title = {Informal proofs formally checked by machine},
     journal = {Annales scientifiques de l'Universit\'e de Clermont. Math\'ematiques},
     publisher = {UER de Sciences exactes et naturelles de l'Universit\'e de Clermont},
     volume = {60},
     number = {13},
     year = {1976},
     pages = {31-53},
     zbl = {0352.68110},
     mrnumber = {468369},
     language = {en},
     url = {http://www.numdam.org/item/ASCFM_1976__60_13_31_0}
}
Aiello, Luigia; Aiello, Mario; Attardi, Giuseppe; Prini, Gianfranco. Informal proofs formally checked by machine. Annales scientifiques de l'Université de Clermont. Mathématiques, Volume 60 (1976) no. 13, pp. 31-53. http://www.numdam.org/item/ASCFM_1976__60_13_31_0/

1 - J.A. Robinson - A machine oriented logic based on the resolution principle- Journal of the ACM - Vol.12 - 1965. | MR 170494 | Zbl 0139.12303

2 - R. Ehrenfeucht, M. Rabin - There is no perfect proof procedure- Unpublished paper - Underground Jerusalem 1972.

3 - R. Milner - Logic for computable functions: description of a machine implementation- Artificial Intelligence Memo No 169 - Stanford University - 1972.

4 - R. Weyhrauch, A. Thomas - FOL: a proof checker for first order logic- Artificial Intelligence Memo No 235 - Stanford University - 1974.

5 - L. Aiello, M. Aiello, R. Weyhrauch - The semantics of PASCAL in LCF- Artificial Intelligence Memo No 221 - Stanford University - 1974.

6 - M. Aiello, R. Weyhrauch - Checking proofs in the metamathematics of first order logic- Artificial Intelligence Memo No 222 - Stanford University 1974 - Also in Proc. of the Fourth International Joint Conference on Artificial Intelligence - Tbilisi - 1975.

7 - C. Montangero, G. Pacini, F. Turini - MAGMA-LISP: a «machine language» for artificial intelligence - Proceedings of the Fourth International Joint Conference on Artificial Intelligence - Tbilisi - 1975.

8 - D. Scott - An alternative approach to CUCH, IS WIM, OWHY- Unpublished paper- Underground Princeton - 1969.

9 - R. Milner- Models of LCF - Artificial Intelligence Memo No 186 - Stanford University 1973.

10 - A. Church - The calculi of λ-conversion - Annals of Mathematical Studies No 6- Princeton- 1941. | JFM 67.0041.01 | Zbl 0026.24205

11 - D. Scott - Continuous lattices - Technical Monograph PRG-7 - Oxford University - 1971. | MR 404073

12 - R. Milner, L. Morris, M. Newey - A logic for computable functions with reflexive and polymorphic types - Proceedings of the International Symposium of Proving and Improving Programs - Arc et Senans - 1975.

13 - M. Newey- Formal semantics of LISP with applications to program correctness - Thesis- Artificial Intelligence Memo No 257 - Stanford University - 1975.