Typing and computational properties of lambda expressions
作者： Daniel Leivant
DOI: 10.1016/0304-3975(86)90109-X
关键词:
摘要: Abstract We use a perception of second-order typing in the λ-Calculus, as conveying semantic properties expressions models over λ-expressions, to exhibit natural and uniform proofs theorems Girard (1971/1972) Coppo, Dezani Veneri (1981) about relations between computational λ-expressions (solvability, normalizability, strong normalizability), some generalizations these theorems.
elsevier.com
sci-hub.se 参考文章(30)
William W. Tait, A realizability interpretation of the theory of species Lecture Notes in Mathematics. pp. 240- 251 ,(1975) , 10.1007/BFB0064875
Sören Stenlund, Combinators, λ-Terms and Proof Theory ,(2011)
Per Martin-Löf, Hauptsatz for the Theory of Species Proceedings of the Second Scandinavian Logic Symposium. ,vol. 63, pp. 217- 233 ,(1971) , 10.1016/S0049-237X(08)70848-6
Mario Coppo, An Extended Polymorphic Type System for Applicative Languages mathematical foundations of computer science. ,vol. 88, pp. 194- 204 ,(1980) , 10.1007/BFB0022505
Kim B. Bruce, Albert R. Meyer, The semantics of second order polymorphic lambda calculus. international symposium on semantics of data types. pp. 131- 156 ,(1984) , 10.1007/3-540-13346-1_6
Dag Prawitz, Ideas and Results in Proof Theory Proceedings of the Second Scandinavian Logic Symposium. ,vol. 63, pp. 235- 307 ,(1971) , 10.1016/S0049-237X(08)70849-8
John C. Reynolds, Towards a theory of type structure Programming Symposium, Proceedings Colloque sur la Programmation. pp. 408- 423 ,(1974) , 10.1007/3-540-06859-7_148
N. G. de Bruijn, The mathematical language AUTOMATH, its usage, and some of its extensions Studies in logic and the foundations of mathematics. ,vol. 133, pp. 73- 100 ,(1970) , 10.1007/BFB0060623
Daniel Leivant, The complexity of parameter passing in polymorphic procedures Proceedings of the thirteenth annual ACM symposium on Theory of computing - STOC '81. pp. 38- 45 ,(1981) , 10.1145/800076.802455
Henk Barendregt, Mario Coppo, Mariangiola Dezani-Ciancaglini, A FILTER LAMBDA MODEL AND THE COMPLETENESS OF TYPE ASSIGNMENT Journal of Symbolic Logic. ,vol. 48, pp. 931- 940 ,(1983) , 10.2307/2273659