no. 13
Informal proofs formally checked by machine
Annales scientifiques de l'Université de Clermont. Mathématiques, Tome 60 (1976) no. 13, pp. 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},
     pages = {31--53},
     publisher = {UER de Sciences exactes et naturelles de l'Universit\'e de Clermont},
     volume = {60},
     number = {13},
     year = {1976},
     mrnumber = {468369},
     zbl = {0352.68110},
     language = {en},
     url = {http://www.numdam.org/item/ASCFM_1976__60_13_31_0/}
}
TY  - JOUR
AU  - Aiello, Luigia
AU  - Aiello, Mario
AU  - Attardi, Giuseppe
AU  - Prini, Gianfranco
TI  - Informal proofs formally checked by machine
JO  - Annales scientifiques de l'Université de Clermont. Mathématiques
PY  - 1976
SP  - 31
EP  - 53
VL  - 60
IS  - 13
PB  - UER de Sciences exactes et naturelles de l'Université de Clermont
UR  - http://www.numdam.org/item/ASCFM_1976__60_13_31_0/
LA  - en
ID  - ASCFM_1976__60_13_31_0
ER  - 
%0 Journal Article
%A Aiello, Luigia
%A Aiello, Mario
%A Attardi, Giuseppe
%A Prini, Gianfranco
%T Informal proofs formally checked by machine
%J Annales scientifiques de l'Université de Clermont. Mathématiques
%D 1976
%P 31-53
%V 60
%N 13
%I UER de Sciences exactes et naturelles de l'Université de Clermont
%U http://www.numdam.org/item/ASCFM_1976__60_13_31_0/
%G en
%F 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, Tome 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 | Zbl

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 | Zbl

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

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.