|
 REFERENCES
Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.
| |
1
|
BLEDSOE, W W. Splitting and reduction heursltlCS in automatic theorem proving Art~f. lntel. 2, 1 (1971), 55-77.
|
| |
2
|
BheDSOE, W W , BoY~:R, R S., ~ND HENNE~a~N, W H Computer proofs of limit theorems. Artzf Iniel. 8 (1972), 27--60
|
| |
3
|
BaoTz, D Provmgtheorems by mathematical reduction Ph.D Th, Comput Sci Dep, Stunford U , Stanford, Cahf , 1973
|
| |
4
|
BURSTALb, R. M Proving properties of programs by structural induction Comput J. 12 (1969), 41-48
|
| |
5
|
COOPER, D Programs for mechanical program verification. In Machine Intelhgence 6, B Meltzer and D Michle, Eds , Edinburgh U. Press, Edinburgh, 1971, pp 43-59.
|
| |
6
|
DARLINGTON, J , AND BURSTALL, }~. M A system which automatically improves programs. Proc Internat Joint Conf on Art~f. Intell., 1973, pp 479-485
|
| |
7
|
DEUTSCH, L. P An interactive program verifier Ph.D Th, Comput. Scl. Dep., U of Callforma, Berkeley, Cahf, 1973.
|
| |
8
|
ELSPAS, B The semiautomatic generation of inductive assertions for program correctness proofs Rep No 55, Seminar, Des Instltuts fur Theorle der Automaten und Schaltnetzwerke, Gesellschaft fur Mathematlk und Datenverarbeitung, Bonn, Aug 21, 1972
|
| |
9
|
ELSPAS, B , LZVITT, K N , AND WALDINGER, R.J. An interactive system for the verification of computer programs Final rep, Project 1891, Stanford Res Inst, Menlo Park, Calif, 1973
|
| |
10
|
FLOYD, R W Assigning meamng to programs Proceedings of a Symposmm m Apphed Mathematics, Vol 19 Mathematical Aspects of Computer Science, J. T Schwartz, Ed , Amer Math Soc , Providence, R. t, 1967, pp. 19-32.
|
| |
11
|
GERH.~.RT, S Verification of APL programs Ph D Th, Carnegm-Mellon U., Pittsburgh, Pa, 1972
|
| |
12
|
|
| |
13
|
|
| |
14
|
KATZ, S M, AND MANNA, Z A heuristic approach to program verification Proc. Internat Joint Conf on Artlf Intell, 1973, pp. 500-512
|
| |
15
|
|
 |
16
|
Zohar Manna , Stephen Ness , Jean Vuillemin, Inductive methods for proving properties of programs, Proceedings of ACM conference on Proving assertions about programs, p.27-50, January 06-07, 1972, Las Cruces, New Mexico, United States
|
| |
17
|
MCCARTHY, J A basis for a mathematical theory of computation In Computer Programming and Formal Systems, P. Braffort and D Hlrschberg, Eds., North-Holland, Amsterdam, 1963, p p 33-7O
|
| |
18
|
|
| |
19
|
McCARTHY, J., AND PAINTER, J A Correctness of a compiler for arithmetic expressions. Proceedings of a Symposium in Applied Mathematics, Vol 19 Mathematical Aspects of Computer Science, Schwartz, J T, Ed , Amer Math Soc , Prowdence, R I , 1967, pp 33-41.
|
| |
20
|
|
| |
21
|
MI1~NER, R., hND WEY~R~UCH, R Proving compiler correctness in a mechanized logic In Machine Intelligence 7, B Meltzer and D. Mlchm, Eds., Edinburgh U. Press, Edinburgh, 1972, pp. 51-70.
|
| |
22
|
MOOR~, J S. Computational logic' Structure sharing and proof of program properties Ph D. Th, Dep. of Computational Logic, School of Artif Intel., U. of Edinburgh, Edinburgh, 1973.
|
| |
23
|
NAUR, P Proof of algorithms by general snapshots BIT 6 (1966), 310-316
|
| |
24
|
PANE, D. Flxpomt induction and proofs of program properties In Machine Intelhgence 5, B Meltzer and D Mlchm, Eds , Edinburgh U. Press, Edinburgh, 1969, pp 59-78
|
| |
25
|
SCOTT, D. Outline of a Mathematical Theory of Computation Tech Monograph PRG-2, Programming Res Group, Oxford U Computing Lab, Nov. 1970
|
| |
26
|
TOPOR, R, AND BURSTALL, R M. Private communication (1973).
|
| |
27
|
|
CITED BY 70
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
P. Asirelli , P. Degano , G. Levi , A. Martèlli , U. Montanari , G. Pacini , F. Sirovich , F. Turini, A flexible environment for program development based on a symbolic interpreter, Proceedings of the 4th international conference on Software engineering, p.251-263, September 17-19, 1979, Munich, Germany
|
|
|
|
|
|
|
|
|
M. Gordon , R. Milner , L. Morris , M. Newey , C. Wadsworth, A Metalanguage for interactive proof in LCF, Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.119-130, January 23-25, 1978, Tucson, Arizona
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
David a. Greve , Matt Kaufmann , Panagiotis Manolios , J. strother Moore , Sandip Ray , JosÉ luis Ruiz-reina , Rob Sumners , Daron Vroon , Matthew Wilding, Efficient execution in an automated reasoning environment, Journal of Functional Programming, v.18 n.1, p.15-46, January 2008
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Adobe Acrobat
QuickTime
Windows Media Player
Real Player
Pdf
G.1