|
 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
|
ACZEL, P. The type theoretic interpretation of constructive set theory. In Logic Colloquium '77. A. MacIntyre, L. Pacholaki, and J. Paris (Eds.). Elsevier North-Holland, New York, 1978, pp. 55-66.
|
| |
2
|
|
| |
3
|
BATES, J., ANO CONSTABLE, R.L. Definition of Micro-PRL. Tech. Rep. TR 82-492, Dept. of Computer Science, Cornell Univ., Ithaca, N.Y., Oct. 1981.
|
| |
4
|
BEESON, M. Formalizing constructive mathematics: Why and how? In Constructive Mathematics, F. Richman (Ed.). Lecture Notes in Computer Science. Springer-Verlag, New York, 1981, pp. 146-190.
|
| |
5
|
BISHOP, E. Foundations of Constructive Analysis. McGraw Hill, New York, 1967.
|
| |
6
|
BOYER, R.S., AND MOORE, J.S. A Computational Logic. Academic Press, New York, 1979.
|
| |
7
|
|
| |
8
|
CONSTABLE, R.L., AND O'DONNELL, M.J. A Programming Logic. Winthrop, Cambridge, Mass., 1978.
|
| |
9
|
CONSTABLE, R.L. Programs and types. In Proceedings 21st Annual Symposium on Foundations of Computer Science, IEEE, New York, 1980, pp. 118-128.
|
| |
10
|
|
| |
11
|
|
| |
12
|
CONSTABLE, R.L. Intensional analysis of functions and types. Tech. Rep. CSR-118-82, Dept. of Computer Science Internal Report, University of Edinburgh, Edinburgh, Scotland, June, 1982.
|
| |
13
|
CONSTABLE, R.L. Programs as proofs. Inf. Process Lett. 16, 3 (Apr. 1983), 105-112.
|
| |
14
|
DEBRUIJN, N.G. A Survey of the project AUTOMATH. In Essays on Combinatory Logic, Lambda Calculus and Formalism, J.P. Seldin and J.R. Hindley (Eds.). Academic Press, New York, 1980, 589-606.
|
| |
15
|
FEFERMAN, S. Constructive theories of functions and classes. In Logic Colloquium '78. Elsevier North-Holland, New York, 1979, pp. 159-224.
|
| |
16
|
GORDON, M., MILNER, R., AND WADSWORTH, C. Edinburgh LCF: A Mechanized Logic o{ Computation. Lecture Notes in Computer Science, vol. 78, Springer-Verlag, New York, 1979.
|
| |
17
|
HILBERT, D., AND ACKERMANN, W. Mathematical Logic, Robert E. Luce (Trans.), 2nd ed. Chelsea, New York, 1950.
|
| |
18
|
HOARE, C.A.R. Recursive data structures, int. J. Comput. Inf. Sci. 4, 2 (June 1975), 105-132.
|
| |
19
|
|
| |
20
|
JUTTING, L.S. Checking Landau's "Grundlagen' in the AUTOMATH system. Doctoral dissertation, Eindhoven Univ., Math. Centre Tracts 83, Math. Centre, Amsterdam, 1979.
|
| |
21
|
|
| |
22
|
MARTIN-LOF, P. About models for intuitionistic type theories and the notion of definitional equality. In Proceedings the 3d Scandinavian Logic Symposium, S. Kanger (Ed.). Elsevier North- Holland, New York, 1975, pp. 81-109.
|
| |
23
|
MART{N-LOF, P. An intuitionistic theory of types: Predicative part. In Logic Colloquium, H.E. Rose and J.C. Shepherdson (Eds.). Elsevier North-Holland, New York, 1975, pp. 73-118.
|
| |
24
|
MARTiN-LOF, P. Constructive mathematics and computer programming. 6th International Congress for Logic, Method and Philosophy o{ Science (Hannover, Aug.), 1979.
|
| |
25
|
PRAWITZ, D. Natural Deduction. Almqvist and Wiksell, Stockholm, 1965.
|
| |
26
|
SCOTT, D. Constructive Validity. In Symposium on Automatic Demonstration. Lecture Notes in Mathematics, vol. 125. Springer-Verlag, New York, 1970, 237-275.
|
| |
27
|
SCOTT, D. Data types as lattices. SIAM J. Comput. 5, 3 (Sept. 1976) 552-587
|
| |
28
|
STENLUNO, S. Combinators, Lambda-terrns, and Proo{-Theory. D. Reidel, Dordrecht, The Netherlands, 1972.
|
| |
29
|
|
 |
30
|
|
| |
31
|
|
| |
32
|
WHITEHEAD, A.N., AND RUSSELL, B. Principia Mathematica, vol. 1. Cambridge University Press, New York, 1925.
|
|
Adobe Acrobat
QuickTime
Windows Media Player
Real Player
Pdf
F.3