乐胖代购免代理版

{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T01:56:17Z","timestamp":1725414977381},"reference-count":592,"publisher":"Elsevier","isbn-type":[{"value":"9780444516206","type":"print"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1016\/s1874-5857(09)70018-4","type":"book-chapter","created":{"date-parts":[[2009,7,1]],"date-time":"2009-07-01T08:16:54Z","timestamp":1246436214000},"page":"723-817","source":"Crossref","is-referenced-by-count":14,"title":["Lambda-Calculus and Combinators in the 20th Century"],"prefix":"10.1016","author":[{"given":"Felice","family":"Cardone","sequence":"first","affiliation":[]},{"given":"J. Roger","family":"Hindley","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/S1874-5857(09)70018-4_bb0010","doi-asserted-by":"crossref","first-page":"375","DOI":"10.1017\/S0956796800000186","article-title":"Explicit substitutions","volume":"1","author":"Abadi","year":"1991","journal-title":"Journal of Functional Programming"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0015","doi-asserted-by":"crossref","first-page":"9","DOI":"10.1016\/0304-3975(93)90082-5","article-title":"Formal parametric polymorphism","volume":"121","author":"Abadi","year":"1993","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0020","doi-asserted-by":"crossref","first-page":"222","DOI":"10.1017\/S0022481200051914","article-title":"An abstraction algorithm for combinatory logic","volume":"41","author":"Abdali","year":"1976","journal-title":"Journal of Symbolic Logic"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0025","doi-asserted-by":"crossref","first-page":"543","DOI":"10.2307\/2275407","article-title":"Games and full completeness for multiplicative linear logic","volume":"59","author":"Abramsky","year":"1994","journal-title":"Journal of Symbolic Logic"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0030","first-page":"1","article-title":"Domain theory","volume":"volume 3","author":"Abramsky","year":"1994"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0035","series-title":"Computational Logic","first-page":"1","article-title":"Game semantics","author":"Abramsky","year":"1998"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0040","first-page":"1","article-title":"Full abstraction for PCF (extended abstract)","author":"Abramsky","year":"1994"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0045","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0168-0072(91)90065-T","article-title":"Domain theory in logical form","volume":"51","author":"Abramsky","year":"1991","journal-title":"Annals of Pure and Applied Logic"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0050","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1016\/0304-3975(94)00103-0","article-title":"Proofs as processes","volume":"135","author":"Abramsky","year":"1994","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0055","series-title":"Foundations of Secure Computation","first-page":"167","article-title":"Process realizability","author":"Abramsky","year":"2000"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0060","first-page":"67","article-title":"Consistency of the unrestricted abstraction principle using an intensional equivalence operator","author":"Aczel","year":"1980"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0065","first-page":"31","article-title":"Frege structures and the notions of proposition, truth and set","author":"Aczel","year":"1980"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0070","series-title":"Non-Well-Founded Sets","author":"Aczel","year":"1988"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0075","first-page":"1","article-title":"Die syntaktische Konnexit\u00e4t","volume":"1","author":"Ajdukiewicz","year":"1935","journal-title":"Studia Philosophica"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0080","series-title":"Domains and Lambda-Calculi, volume 46 of Cambridge Tracts in Theoretical Computer Science","author":"Amadio","year":"1998"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0085","series-title":"Proceedings First Annual IEEE Symposium on Logic In Computer Science","first-page":"122","article-title":"The finitary projection model for second order lambda calculus and solutions to higher order domain equations","author":"Amadio","year":"1986"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0090","doi-asserted-by":"crossref","first-page":"129","DOI":"10.2307\/421020","article-title":"Alonzo Church\u2019s contributions to philosophy and intensional logic","volume":"4","author":"Anderson","year":"1998","journal-title":"Bulletin of Symbolic Logic"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0095","series-title":"A Transfinite Type Theory with Type Variables","author":"Andrews","year":"1965"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0100","doi-asserted-by":"crossref","first-page":"414","DOI":"10.2307\/2269949","article-title":"Resolution in type theory","volume":"36","author":"Andrews","year":"1971","journal-title":"Journal of Symbolic Logic,"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0105","series-title":"Foundations of Computing","article-title":"Categories, Types and Structures. An Introduction to Category Theory for the Working Computer Scientist","author":"Asperti","year":"1991"},{"issue":"1-2","key":"10.1016\/S1874-5857(09)70018-4_bb0110","doi-asserted-by":"crossref","first-page":"3","DOI":"10.3233\/FI-1995-22121","article-title":"Linear logic, comonads and optimal reductions","volume":"22","author":"Asperti","year":"1995","journal-title":"Fundamenta Informaticae,"},{"issue":"8","key":"10.1016\/S1874-5857(09)70018-4_bb0115","doi-asserted-by":"crossref","first-page":"613","DOI":"10.1145\/359576.359579","article-title":"Can programming be liberated from the von Neumann style?","volume":"21","author":"Backus","year":"1978","journal-title":"Communications of the ACM,"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0120","doi-asserted-by":"crossref","first-page":"47","DOI":"10.2307\/410452","article-title":"A quasi-arithmetical notation for syntactic description","volume":"29","author":"Bar-Hillel","year":"1953","journal-title":"Language"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0125","first-page":"19","article-title":"Decision procedures for structure in natural languages","volume":"2","author":"Bar-Hillel","year":"1959","journal-title":"Logique et analyse"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0130","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1016\/S0019-9958(83)80033-3","article-title":"Semantics for classical AUTOMATH and related systems","volume":"59","author":"Barendregt","year":"1983","journal-title":"Information and Control"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0135","doi-asserted-by":"crossref","first-page":"377","DOI":"10.1016\/S1385-7258(76)80001-7","article-title":"Representability in lambda algebras","volume":"79","author":"Barendregt","year":"1976","journal-title":"Koninkl. Nederlands Akad. van Wetensch. Proc. Ser. A"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0140","doi-asserted-by":"crossref","first-page":"931","DOI":"10.2307\/2273659","article-title":"A filter lambda model and the completeness of type assignment","volume":"48","author":"Barendregt","year":"1983","journal-title":"Journal of Symbolic Logic"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0145","doi-asserted-by":"crossref","first-page":"769","DOI":"10.2307\/2275096","article-title":"Systems of illative combinatory logic complete for first order propositional and predicate calculus","volume":"58","author":"Barendregt","year":"1993","journal-title":"Journal of Symbolic Logic"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0150","series-title":"Some extensional term models for combinatory logics and \u22cb-calculi","author":"Barendregt","year":"1971"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0155","doi-asserted-by":"crossref","first-page":"441","DOI":"10.2307\/2273041","article-title":"A characterization of terms of the \u22cb-I-calculus having a normal form","volume":"38","author":"Barendregt","year":"1973","journal-title":"Journal of Symbolic Logic"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0160","doi-asserted-by":"crossref","first-page":"225","DOI":"10.1016\/0304-3975(76)90025-6","article-title":"A global representation of the recursive functions in the \u22cb-calculus","volume":"3","author":"Barendregt","year":"1976","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0165","series-title":"Handbook of Mathematical Logic","first-page":"1091","article-title":"The type-free lambda calculus","author":"Barendregt","year":"1977"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0170","series-title":"The Lambda Calculus, its Syntax and Semantics","author":"Barendregt","year":"1981"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0175","doi-asserted-by":"crossref","first-page":"59","DOI":"10.1016\/0304-3975(93)90083-6","article-title":"Constructive proofs of the range property in lambda calculus","volume":"121","author":"Barendregt","year":"1993","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0180","series-title":"Kreiseliana, about and around Georg Kreisel","first-page":"3","article-title":"Kreisel, lambda calculus, a windmill and a castle","author":"Barendregt","year":"1996"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0185","doi-asserted-by":"crossref","first-page":"181","DOI":"10.2307\/421013","article-title":"The impact of the lambda calculus in logic and computer science","volume":"3","author":"Barendregt","year":"1997","journal-title":"Bulletin of Symbolic Logic"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0190","article-title":"*-autonomous Categories","volume":"volume 752","author":"Barr","year":"1979"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0195","doi-asserted-by":"crossref","first-page":"159","DOI":"10.1017\/S0960129500001274","article-title":"*-autonomous categories and linear logic","volume":"1","author":"Barr","year":"1991","journal-title":"Mathematical Structures in Computer Science,"},{"issue":"1","key":"10.1016\/S1874-5857(09)70018-4_bb0200","doi-asserted-by":"crossref","first-page":"113","DOI":"10.1145\/2363.2528","article-title":"Proofs as programs","volume":"7","author":"Bates","year":"1985","journal-title":"ACM Transactions on programming Languages and Systems"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0205","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1016\/j.tcs.2003.11.012","article-title":"Equilogical spaces","volume":"315","author":"Bauer","year":"2004","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0210","series-title":"Type-assignment in the Lambda-calculus","author":"Ben-Yelles","year":"1979"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0215","doi-asserted-by":"crossref","first-page":"10","DOI":"10.2307\/2273784","article-title":"Fibered categories and the foundations of naive category theory","volume":"50","author":"B\u00e9nabou","year":"1985","journal-title":"Journal of Symbolic Logic"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0220","doi-asserted-by":"crossref","first-page":"699","DOI":"10.1017\/S0956796800001945","article-title":"\u22cb\ud710, a calculus of explicit substitutions which preserves strong normalisation","volume":"6","author":"Benaissa","year":"1996","journal-title":"Journal of Functional Programming"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0225","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1016\/0304-3975(80)90032-8","article-title":"Invertible terms in the lambda calculus","volume":"11","author":"Bergstra","year":"1980","journal-title":"Theoretical Computer Science,"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0230","doi-asserted-by":"crossref","first-page":"342","DOI":"10.1007\/BF01459101","article-title":"Zum Entscheidungsproblem der mathematischen Logik","volume":"99","author":"Bernays","year":"1928","journal-title":"Mathematische Annalen"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0235","series-title":"Constructivity in Mathematics","first-page":"1","article-title":"\u00dcber eine nat\u00fcarliche Erweiterung des Relationenkalkuls","author":"Bernays","year":"1958"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0240","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1016\/S0304-3975(82)80002-9","article-title":"Sequential algorithms on concrete data structures","volume":"20","author":"Berry","year":"1982","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0245","first-page":"47","article-title":"Bottom-up computation of recursive programs","volume":"10","author":"Berry","year":"1976","journal-title":"RAIRO Informatique Theorique et Applications"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0250","series-title":"Automata, Languages and Programming, Fifth Colloquium","first-page":"72","article-title":"Stable models of typed \u03bb-calculi","author":"Berry","year":"1978"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0255","series-title":"International Colloquium on Formalization of Programming Concepts, Proceedings","first-page":"218","article-title":"On the definition of \u03bb-calculus models","author":"Berry","year":"1981"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0260","unstructured":"I. Bethke. Annotated Bibliography of Lambda Calculi, Combinatory Logics and Type Theory. URL www.adam.science.uva.nl\/inge\/, 2000.File type \u2018.ps\u2019, 587 pp. if printed."},{"key":"10.1016\/S1874-5857(09)70018-4_bb0265","doi-asserted-by":"crossref","first-page":"151","DOI":"10.4064\/fm-77-2-151-166","article-title":"Degrees of indeterminacy of games","volume":"77","author":"Blass","year":"1972","journal-title":"Fundamenta Mathematicae"},{"issue":"1-3","key":"10.1016\/S1874-5857(09)70018-4_bb0270","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/0168-0072(92)90073-9","article-title":"A game semantics for linear logic","volume":"56","author":"Blass","year":"1992","journal-title":"Annals of Pure and Applied Logic"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0275","doi-asserted-by":"crossref","first-page":"375","DOI":"10.1016\/S0304-3975(97)00183-7","article-title":"Explicit substitution: on the edge of strong normalization","volume":"211","author":"Bloo","year":"1999","journal-title":"Theoretical Computer Science,"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0280","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1016\/0304-3975(85)90135-5","article-title":"Automatic synthesis of typed \u03bb- programs on term algebras","volume":"39","author":"B\u00f6hm","year":"1985","journal-title":"Theoretical Computer Science,"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0285","doi-asserted-by":"crossref","first-page":"171","DOI":"10.1007\/BF00995737","article-title":"A CUCH machine: The automatic treatment of bound variables","volume":"1","author":"B\u00f6hm","year":"1972","journal-title":"International Journal of Computer and Information Sciences"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0290","first-page":"37","article-title":"A parenthesis machine for string manipulation","volume":"8","author":"B\u00f6hm","year":"1974","journal-title":"Revue Francais d\u2019Automatique, Informatique et Recherche Op\u00e9rationelle"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0295","doi-asserted-by":"crossref","unstructured":"C. B\u00f6hm and M. Dezani. \u03bb-terms as total or partial functions on normal forms.In B\u00f6hm [1975], pages 96-121.","DOI":"10.1007\/BFb0029521"},{"issue":"4","key":"10.1016\/S1874-5857(09)70018-4_bb0300","doi-asserted-by":"crossref","first-page":"525","DOI":"10.3233\/FI-1989-12406","article-title":"Combinatory logic as monoids","volume":"12","author":"B\u00f6hm","year":"1989","journal-title":"Fundamenta Informaticae"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0305","unstructured":"C. B\u00f6hm and R. Giovannucci. Circuiti sequenziali e analogici e loro descrizione mediante il CUCH. Istituto per le Applicazioni del Calcolo, C.N.R., Roma, 1964"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0310","series-title":"Automata Theory","first-page":"35","article-title":"Introduction to the CUCH","author":"Bohm","year":"1966"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0315","series-title":"Automata, Languages and Programming, Fourth Colloquium","first-page":"95","article-title":"Termination tests inside \u03bb-calculus","author":"B\u00f6hm","year":"1977"},{"issue":"4","key":"10.1016\/S1874-5857(09)70018-4_bb0320","first-page":"1","article-title":"Calculatrices digitales. Du dechiffrage des formules logico-mathematiques par la machine meme dans la conception du programme","volume":"37","author":"B\u00f6hm","year":"1954","journal-title":"Annali di Matematica Pura e Applicata,"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0325","series-title":"Formal Language Description Languages for Computer Programming","first-page":"179","article-title":"The CUCH as a formal and description language","author":"B\u00f6hm","year":"1966"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0330","unstructured":"C. B\u00f6hm. Alcune proprieta delle forme \u03b2-n-normali nel \u03bb-K-calcolo. Pubblicazione no. 696, Istituto per le Applicazioni del Calcolo, C.N.R., Roma, 1968"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0335","series-title":"\u03bb-Calculus and Computer Science Theory","year":"1975"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0340","series-title":"Lambda Calcul et S\u00e9mantique Formelle des Langages de Programmation. Actes de la Sixi\u00e9me Ecole de Printemps d\u2019Informatique Theorique, La Ch\u00e2tre, 1978,","first-page":"97","article-title":"Un mod\u00e9le arithm\u00e9tique des termes de la logique combinatoire","author":"B\u00f6hm","year":"1979"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0345","series-title":"Modern Logic \u2014 A Survey","first-page":"297","article-title":"Logic and computers","author":"B\u00f6hm","year":"1980"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0350","series-title":"Combinatory foundations of functional programming","first-page":"29","author":"B\u00f6hm","year":"1982"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0355","series-title":"European Symposium on Programming, volume 213 of Lecture Notes in Computer Science,","doi-asserted-by":"crossref","first-page":"111","DOI":"10.1007\/3-540-16442-1_8","article-title":"Reducing recursion to iteration by algebraic extension","author":"B\u00f6hm","year":"1986"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0360","series-title":"Mathematical Foundations of Computer Science, volume 324 of Lecture Notes in Computer Science,","doi-asserted-by":"crossref","first-page":"14","DOI":"10.1007\/BFb0017128","article-title":"Functional programming and combinatory algebras","author":"B\u00f6hm","year":"1988"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0365","series-title":"Foundations of Logic and Functional Programming, volume 306 of Lecture Notes in Computer Science,","first-page":"58","article-title":"Reducing recursion to iteration by means of pairs and n-tuples","author":"B\u00f6hm","year":"1986"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0370","first-page":"108","article-title":"Subduing self-application","volume":"volume 372","author":"B\u00f6hm","year":"1989"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0375","series-title":"Typed Lambda Calculi and Applications, 4th International Conference, TLCA\u201999, volume 1581 of Lecture Notes in Computer Science,","first-page":"69","article-title":"Counting a type\u2019s principal inhabitants","author":"Broda","year":"1999"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0380","doi-asserted-by":"crossref","unstructured":"K. Bruce, A. A. Meyer, and J. C. Mitchell. The semantics of second-order lambda calculus. In Huet [1990b], pages 273-284.","DOI":"10.1016\/0890-5401(90)90044-I"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0385","series-title":"Symposium on Automatic Demonstration, volume 125 of Lecture Notes in Mathematics,","first-page":"29","article-title":"The mathematical language AUTOMATH","author":"de Bruijn","year":"1970"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0390","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1016\/1385-7258(72)90034-0","article-title":"Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation","volume":"34","author":"de Bruijn","year":"1972","journal-title":"Indagationes Mathematicae,"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0395","first-page":"579","article-title":"A survey of the project AUTOMATH","author":"de Bruijn","year":"1980"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0400","first-page":"201","article-title":"Reflections on Automath","author":"de Bruijn","year":"1994"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0405","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1305\/ndjfl\/1117755149","article-title":"Equivalences between pure type systems and systems of illative combinatory logic","volume":"46","author":"Bunder","year":"2005","journal-title":"Notre Dame Journal of Formal Logic"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0410","doi-asserted-by":"crossref","first-page":"99","DOI":"10.1007\/BF02023016","article-title":"A one axiom set theory based on higher order predicate calculus","volume":"23","author":"Bunder","year":"1983","journal-title":"Archiv f\u00fcr Mathematische Logik,"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0415","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/BF02023007","article-title":"Predicate calculus of arbitrarily high finite order","volume":"23","author":"Bunder","year":"1983","journal-title":"Archiv f\u00fcr Mathematische Logik,"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0420","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1007\/BF02023017","article-title":"Set theory in predicate calculus with equality","volume":"23","author":"Bunder","year":"1983","journal-title":"Archiv f\u00fcr Mathematische Logik,"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0425","series-title":"Logica Matematica","author":"Burali-Forti","year":"1894"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0430","series-title":"Recursive Programming Techniques","author":"Burge","year":"1978"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0435","series-title":"The Software Revolution; Proceedings of the Infotech State of the Art Conference, Copenhagen","first-page":"45","article-title":"Design considerations for a functional programming language","author":"Burstall","year":"1977"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0440","doi-asserted-by":"crossref","first-page":"471","DOI":"10.1145\/6041.6042","article-title":"On understanding types, data abstraction and polymorphism","volume":"17","author":"Cardelli","year":"1985","journal-title":"ACM Computing Surveys,"},{"issue":"1","key":"10.1016\/S1874-5857(09)70018-4_bb0445","doi-asserted-by":"crossref","first-page":"48","DOI":"10.1016\/0890-5401(91)90020-3","article-title":"Type inference with recursive types. Syntax and Semantics","volume":"92","author":"Cardone","year":"1991","journal-title":"Information and Computation,"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0450","doi-asserted-by":"crossref","first-page":"37","DOI":"10.1305\/ndjfl\/1093882400","article-title":"Theory of objects and set theory: introduction and semantics","volume":"10","author":"Chauvin","year":"1979","journal-title":"Notre Dame Journal of Formal Logic"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0455","series-title":"AFIPS Conference Proceedings, San Francisco, California,","first-page":"937","article-title":"On the basis of ELF \u2014 An extensible language facility","author":"Cheatham","year":"1968"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0460","doi-asserted-by":"crossref","first-page":"472","DOI":"10.1090\/S0002-9947-1936-1501858-0","article-title":"Some properties of conversion","volume":"39","author":"Church","year":"1936","journal-title":"Transactions of the American Mathematical Society,"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0465","doi-asserted-by":"crossref","first-page":"346","DOI":"10.2307\/1968337","article-title":"A set of postulates for the foundation of logic","volume":"33","author":"Church","year":"1932","journal-title":"Annals of Mathematics, Series 2,"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0470","doi-asserted-by":"crossref","first-page":"839","DOI":"10.2307\/1968702","article-title":"A set of postulates for the foundation of logic (second paper)","volume":"34","author":"Church","year":"1933","journal-title":"Annals of Mathematics, Series 2,"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0475","doi-asserted-by":"crossref","first-page":"275","DOI":"10.1073\/pnas.21.5.275","article-title":"A proof of freedom from contradiction","volume":"21","author":"Church","year":"1935","journal-title":"Proceedings of the National Academy of Sciences of the U.S.A"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0480","doi-asserted-by":"crossref","first-page":"40","DOI":"10.2307\/2269326","article-title":"A note on the Entscheidungsproblem","volume":"1","author":"Church","year":"1936","journal-title":"Journal of Symbolic Logic"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0485","doi-asserted-by":"crossref","first-page":"345","DOI":"10.2307\/2371045","article-title":"An unsolvable problem of elementary number theory","volume":"58","author":"Church","year":"1936","journal-title":"American Journal of Mathematics,"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0490","first-page":"333","article-title":"Combinatory logic as a semi-group","volume":"43","author":"Church","year":"1937","journal-title":"Bulletin of the American Mathematical Society"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0495","doi-asserted-by":"crossref","first-page":"56","DOI":"10.2307\/2266170","article-title":"A formulation of the simple theory of types","volume":"5","author":"Church","year":"1940","journal-title":"Journal of Symbolic Logic"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0500","series-title":"The Calculi of Lambda Conversion","author":"Church","year":"1941"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0505","series-title":"Structure, Method and Meaning, Essays in Honor of Henry M. Sheffer","first-page":"3","article-title":"A formulation of the logic of sense and denotation","author":"Church","year":"1951"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0510","series-title":"Kontrolliertes Denken, Untersuchungen zum Logikkalk\u00fcl und zur Logik der Einzelwissenschaften (Festgabe zum 60. Geburtstag von Prof. W. Britzelmayr)","first-page":"22","article-title":"The weak theory of implication","author":"Church","year":"1951"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0515","series-title":"Introduction to Mathematical Logic","author":"Church","year":"1956"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0520","unstructured":"A. Church, 7 July 1964. Unpublished letter to Harald Dickson"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0525","doi-asserted-by":"crossref","first-page":"24","DOI":"10.2307\/2216181","article-title":"Outline of a revised formulation of the logic of sense and denotation, Part I","volume":"7","author":"Church","year":"1973","journal-title":"No\u00fbs"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0530","doi-asserted-by":"crossref","first-page":"236","DOI":"10.1007\/BF01215902","article-title":"\u00dcber die Antinomien der Prinzipen der Mathematik","volume":"14","author":"Chwistek","year":"1922","journal-title":"Mathematische Zeitschrift"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0535","series-title":"Computability on continuous higher types and its role in the semantics of programming languages. Technical report TR-74-209","author":"Constable","year":"1974"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0540","series-title":"A Programming Logic","author":"Constable","year":"1978"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0545","series-title":"Implementing Mathematics with the Nuprl Proof Development System","author":"Constable","year":"1986"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0550","doi-asserted-by":"crossref","unstructured":"R. L. Constable. Constructive mathematics and automatic program writers. In Proceedings of the IFIP Congress, pages 229\u2013233, Ljubljana, 1971.","DOI":"10.1136\/bmj.1.5742.233-c"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0555","first-page":"118","article-title":"Programs and types","author":"Constable","year":"1980","journal-title":"21st IEEE Symposium on the Foundations of Computer Science,"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0560","series-title":"Technical report TR-82-532","article-title":"Programs as proofs","author":"Constable","year":"1982"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0565","first-page":"21","article-title":"Constructive mathematics as a programming logic I: Some principles of theory","volume":"24","author":"Constable","year":"1985","journal-title":"Annals of Discrete Mathematics"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0570","series-title":"On Numbers and Games, volume 6 of London Mathematical Society Monographs","author":"Conway","year":"1976"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0575","doi-asserted-by":"crossref","first-page":"139","DOI":"10.1007\/BF02011875","article-title":"A new type assignment for \u03bb-terms","volume":"19","author":"Coppo","year":"1978","journal-title":"Archiv f\u00fcr Mathematische Logik"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0580","doi-asserted-by":"crossref","first-page":"113","DOI":"10.1016\/0304-3975(93)90086-9","article-title":"Type inference, abstract interpretation and strictness analysis","volume":"121","author":"Coppo","year":"1993","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0585","series-title":"Automata, Languages and Programming, Sixth Colloquium, volume 71 of Lecture Notes in Computer Science","first-page":"133","article-title":"Functional characterization of some semantic equalities inside \u03bb-calculus","author":"Coppo","year":"1979"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0590","series-title":"Principal type-schemes and \u03bb- calculus semantics","first-page":"535","author":"Coppo","year":"1980"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0595","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1002\/malq.19810270205","article-title":"Functional characters of solvable terms","volume":"27","author":"Coppo","year":"1981","journal-title":"Zeitschrift f\u00fcr Mathematische Logik und Grundlagen der Mathematik"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0600","series-title":"Colloquium on Trees and Algebra in Programming, volume 159 of Lecture Notes in Computer Science,","doi-asserted-by":"crossref","first-page":"33","DOI":"10.1007\/3-540-12727-5_2","article-title":"Applicative information systems","author":"Coppo","year":"1983"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0605","series-title":"Logic Colloquium \u201982,","first-page":"241","article-title":"Extended type structures and filter lambda models","author":"Coppo","year":"1984"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0610","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1016\/0890-5401(87)90042-3","article-title":"Type theories, normal forms and D^-lambda models","volume":"72","author":"Coppo","year":"1987","journal-title":"Information and Computation,"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0615","series-title":"Automata, Languages and Programming, 12th International Colloquium, volume 194 of Lecture Notes in Computer Science","first-page":"120","article-title":"A completeness theorem for recursively defined types","author":"Coppo","year":"1985"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0620","series-title":"Foundations of Software Technology and Theoretical Computer Science","article-title":"Inductive definitions and type theory: an introduction (preliminary version)","author":"Coquand","year":"1994"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0625","series-title":"EUROCAL\u201985, Proceedings Volume 1, volume 203 of Lecture Notes in Computer Science,","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1007\/3-540-15983-5_13","article-title":"Constructions: a higher order proof system for mechanizing mathematics","author":"Coquand","year":"1985"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0630","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1016\/0890-5401(88)90005-3","article-title":"The calculus of constructions","volume":"76","author":"Coquand","year":"1988","journal-title":"Information and Computation,"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0635","article-title":"Une th\u00e9orie des constructions","author":"Coquand","year":"1985","journal-title":"These de Troisi\u00e9me Cycle, Uni- versit\u00e9 Paris VII,"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0640","first-page":"227","article-title":"An analysis of Girard\u2019s paradox","author":"Coquand","year":"1986","journal-title":"Proceedings First Annual IEEE Symposium on Logic In Computer Science,"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0645","series-title":"Logic and Computer Science, volume 31 of APIC Studies in Data Processing,","first-page":"91","article-title":"Metamathematical investigations of a calculus of constructions","author":"Coquand","year":"1990"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0650","doi-asserted-by":"crossref","first-page":"28","DOI":"10.2307\/2275174","article-title":"An intuitionistic proof of Tychonoff\u2019s theorem","volume":"57","author":"Coquand","year":"1992","journal-title":"Journal of Symbolic Logic,"},{"issue":"1","key":"10.1016\/S1874-5857(09)70018-4_bb0655","doi-asserted-by":"crossref","first-page":"325","DOI":"10.2307\/2275524","article-title":"A semantics of evidence for classical arithmetic","volume":"60","author":"Coquand","year":"1995","journal-title":"Journal of Symbolic Logic,"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0660","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1016\/0167-6423(87)90020-7","article-title":"The categorical abstract machine","volume":"8","author":"Cousineau","year":"1987","journal-title":"Science of Computer Programming,"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0665","series-title":"Logic in an Algebraic Form, Three Languages and Theories","author":"Craig","year":"1974"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0670","series-title":"Algebra and Logic, volume 450 of Lecture Notes in Mathematics,","first-page":"1","article-title":"Reminiscences of Logicians","author":"Crossley","year":"1975"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0675","doi-asserted-by":"crossref","first-page":"362","DOI":"10.1145\/226643.226675","article-title":"Confluence properties of weak and strong calculi of explicit substitutions","volume":"43","author":"Curien","year":"1996","journal-title":"Journal of the Association for Computing Machinery"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0680","series-title":"Lambda Calcul et Semantique Formelle des Langages de Programmation. Actes de la Sixi\u00e9me Ecole de Printemps d\u2019Informatique Th\u00e9orique","first-page":"157","article-title":"Algorithmes sequentiels sur structures de donnees concretes","author":"Curien","year":"1979"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0685","series-title":"Mathematical Foundations of Software Development, Proceedings 1985, Volume 1, CAAP\u201985, volume 185 of Lecture Notes in Computer Science,","first-page":"157","article-title":"Typed categorical combinatory logic","author":"Curien","year":"1985"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0690","series-title":"Categorical Combinators, Sequential Algorithms and Functional Programming","author":"Curien","year":"1986"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0695","series-title":"Mathematical Foundations of Programming Semantics, 9th International Conference, volume 802 of Lecture Notes in Computer Science,","first-page":"29","article-title":"On the symmetry of sequentiality","author":"Curien","year":"1994"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0700","series-title":"Combinatory Logic, Volume I","author":"Curry","year":"1958"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0705","volume":"Volume II","author":"Curry","year":"1972"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0710","series-title":"Sch\u00f6nfinkel, M. \u00dcber die Bausteine der mathematischen Logik, 1927","author":"Curry","year":"1927"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0715","doi-asserted-by":"crossref","first-page":"509","DOI":"10.2307\/2370619","article-title":"Grundlagen der kombinatorischen Logik","volume":"52","author":"Curry","year":"1930","journal-title":"American Journal of Mathematics"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0720","doi-asserted-by":"crossref","first-page":"551","DOI":"10.2307\/2370900","article-title":"Some additions to the theory of combinators","volume":"54","author":"Curry","year":"1932","journal-title":"American Journal of Mathematics"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0725","doi-asserted-by":"crossref","first-page":"584","DOI":"10.1073\/pnas.20.11.584","article-title":"Functionality in combinatory logic","volume":"20","author":"Curry","year":"1934","journal-title":"Proceedings of the National Academy of Sciences of the U.S.A"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0730","doi-asserted-by":"crossref","first-page":"849","DOI":"10.2307\/1968498","article-title":"Some properties of equality and implication in combinatory logic","volume":"35","author":"Curry","year":"1934","journal-title":"Annals of Mathematics, Series 2"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0735","first-page":"371","article-title":"First properties of functionality in combinatory logic","volume":"41","author":"Curry","year":"1936","journal-title":"T\u02c6ohoku Mathematical Journal"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0740","doi-asserted-by":"crossref","first-page":"39","DOI":"10.2307\/2268803","article-title":"Review of Church\u2019s lecture notes Mathematical Logic given at Princeton Univ. in 1936","volume":"2","author":"Curry","year":"1937","journal-title":"Journal of Symbolic Logic"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0745","doi-asserted-by":"crossref","first-page":"49","DOI":"10.2307\/2266302","article-title":"The combinatory foundations of mathematical logic","volume":"7","author":"Curry","year":"1942","journal-title":"Journal of Symbolic Logic"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0750","doi-asserted-by":"crossref","first-page":"115","DOI":"10.2307\/2269292","article-title":"The inconsistency of certain formal logics","volume":"7","author":"Curry","year":"1942","journal-title":"Journal of Symbolic Logic"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0755","article-title":"The logical structure of grammar, 1948","author":"Curry","year":"1948","journal-title":"Unfinished manuscript mimeographed at Univ. Chicago and privately distributed, from a lecture given in Nov"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0760","first-page":"391","article-title":"A simplification of the theory of combinators","volume":"7","author":"Curry","year":"1949","journal-title":"Synthese"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0765","series-title":"Outlines of a Formalist Philosophy of Mathematics","author":"Curry","year":"1951"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0770","series-title":"Applications Scientifiques de la Logique Math\u00e9matique, Actes du Deuxieme Colloque International de Logique Math\u00e9matique, Paris 1952","first-page":"97","article-title":"The logic of program composition","author":"Curry","year":"1954"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0775","series-title":"Structure of Language and its Mathematical Aspects, number 12 in Proceedings of Symposia in Applied Mathematics","first-page":"56","article-title":"Some logical aspects of grammatical structure","author":"Curry","year":"1961"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0780","series-title":"Foundations of Mathematical Logic","author":"Curry","year":"1963"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0785","series-title":"The Critical Approach to Science and Philosophy","first-page":"127","article-title":"The elimination of variables by regular combinators","author":"Curry","year":"1964"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0790","series-title":"Note dated March 17th","article-title":"Technique for evaluating principal functional character, 1966","author":"Curry","year":"1966"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0795","doi-asserted-by":"crossref","first-page":"8392","DOI":"10.1111\/j.1746-8361.1969.tb01183.x","article-title":"Modified basic functionality in combinatory logic","volume":"23","author":"Curry","year":"1969","journal-title":"Dialectica"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0800","series-title":"Foundations of Mathematics, Symposium Papers Commemorating the Sixtieth Birthday of Kurt G\u00f6del","first-page":"10","article-title":"The undecidability of \u03bbK-conversion","author":"Curry","year":"1969"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0805","series-title":"The Kleene Symposium","first-page":"85","article-title":"Some philosophical aspects of combinatory logic","author":"Curry","year":"1980"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0810","article-title":"A description of Automath and some aspects of its language theory","volume":"volume I","author":"van Daalen","year":"1973"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0815","series-title":"The Language Theory of AUTOMATH","author":"van Daalen","year":"1994"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0820","series-title":"Ninth Annual A.C.M. Symposium on the Principles of Programming Languages (POPL)","first-page":"207","article-title":"Principal type-schemes for functional programming languages","author":"Damas","year":"1982"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0825","series-title":"Type Assignment in Programming Languages","author":"Damas","year":"1984"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0830","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1007\/BF01622878","article-title":"The structure of multiplicatives","volume":"28","author":"Danos","year":"1989","journal-title":"Archive for Mathematical Logic"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0835","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/S0019-9958(82)91226-8","article-title":"Why G\u00f6del didn\u2019t have Church\u2019s Thesis","volume":"54","author":"Davis","year":"1982","journal-title":"Information and Control"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0840","doi-asserted-by":"crossref","first-page":"869","DOI":"10.2307\/2586717","article-title":"Completeness of the propositions-as-types interpretation of intuitionistic logic into illative combinatory logic","volume":"63","author":"Dekkers","year":"1998","journal-title":"Journal of Symbolic Logic"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0845","first-page":"130","article-title":"Maximal monoids of normal forms","volume":"2","author":"Dezani","year":"1982","journal-title":"Fundamenta Informaticae"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0850","series-title":"A Collection of Contributions in Honour of Corrado Bohm","year":"1993"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0855","series-title":"Proceedings of the Symposium Informatica 75","article-title":"A type theory for \u03bb-\u03b2-normal forms","author":"Dezani","year":"1975"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0860","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1016\/0304-3975(76)90085-2","article-title":"Characterization of normal forms possessing inverse in the \u03bb-\u03b2- calculus","volume":"2","author":"Dezani","year":"1976","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0865","series-title":"Contributions to Mathematical Logic","first-page":"109","article-title":"Zur Berechenbarkeit primitiv-rekursiver Funktionale endlicher Typen","author":"Diller","year":"1968"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0870","first-page":"3245","article-title":"The computation of primitive recursive terms of finite type, and primitive recusive realization","volume":"8","author":"Dragalin","year":"1968","journal-title":"Zapiski Naucnyh Seminarov Leningradskogo Otdeleniya Matematicheskogo Instituta imeni V.A. Steklova, Akademii Nauk S.S.S.R. (L.O.M.I.)"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0875","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1016\/0304-3975(96)00102-8","article-title":"Uniqueness of Scott\u2019s reflexive domain in P","volume":"155","author":"Drakengren","year":"1996","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0880","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1017\/S0960129500000177","article-title":"Universal domains and the amalgamation property","volume":"3","author":"Droste","year":"1993","journal-title":"Mathematical Structures in Computer Science"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0885","series-title":"The Scheme Programming Language","author":"Dybyg","year":"1996"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0890","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1016\/0304-3975(76)90029-3","article-title":"Computability concepts for programming language semantics","volume":"2","author":"Egli","year":"1976","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0895","series-title":"Proceedings of the Conference on Categorical Algebra, La Jolla, 1965","first-page":"412","article-title":"Closed categories","author":"Eilenberg","year":"1966"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0900","doi-asserted-by":"crossref","first-page":"486","DOI":"10.1017\/S1079898600008040","article-title":"In memoriam: Alonzo Church 1903\u20141995","volume":"1","author":"Enderton","year":"1995","journal-title":"Bulletin of Symbolic Logic"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0905","doi-asserted-by":"crossref","first-page":"172","DOI":"10.2307\/421021","article-title":"Alonzo Church and the Reviews","volume":"4","author":"Enderton","year":"1998","journal-title":"Bulletin of Symbolic Logic"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0910","doi-asserted-by":"crossref","first-page":"389","DOI":"10.1007\/BF02483849","article-title":"Algebras and combinators","volume":"13","author":"Engeler","year":"1981","journal-title":"Algebra Universalis"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0915","series-title":"Algebra and Logic, volume 450 of Lecture Notes in Mathematics","first-page":"87","article-title":"A language and axioms for explicit mathematics","author":"Feferman","year":"1975"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0920","series-title":"Proof Theory Symposion, Kiel 1974","first-page":"73","article-title":"Non-extensional type-free theories of partial operations and classifications, I","author":"Feferman","year":"1975"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0925","series-title":"Logic, Foundations of Mathematics and Computability Theory","first-page":"149","article-title":"Categorical foundations and foundations of category theory","author":"Feferman","year":"1977"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0930","doi-asserted-by":"crossref","first-page":"75","DOI":"10.2307\/2274093","article-title":"Towards useful type-free theories, I","volume":"49","author":"Feferman","year":"1984","journal-title":"Journal of Symbolic Logic"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0935","doi-asserted-by":"crossref","first-page":"205","DOI":"10.1016\/0304-3975(87)90109-5","article-title":"A syntactic theory of sequential control","volume":"52","author":"Felleisen","year":"1987","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0940","first-page":"341","article-title":"Dialogues as a foundation for intuitionistic logic","volume":"volume 3","author":"Felscher","year":"1986"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0945","doi-asserted-by":"crossref","first-page":"74","DOI":"10.3406\/phlou.1946.4039","article-title":"La technique de la logique combinatoire","volume":"44","author":"Feys","year":"1946","journal-title":"Revue Philosophique de Louvain"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0950","doi-asserted-by":"crossref","first-page":"370","DOI":"10.3406\/phlou.1946.4065","article-title":"Les methodes r\u00e9centes de deduction naturelle","volume":"44","author":"Feys","year":"1946","journal-title":"Revue Philosophique de Louvain,"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0955","doi-asserted-by":"crossref","first-page":"92","DOI":"10.2307\/2269029","article-title":"A system of formal logic without an analogue to the Curry W operator","volume":"1","author":"Fitch","year":"1936","journal-title":"Journal of Symbolic Logic,"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0960","series-title":"Symbolic Logic, an Introduction","author":"Fitch","year":"1952"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0965","doi-asserted-by":"crossref","first-page":"263","DOI":"10.1086\/287616","article-title":"Representation of sequential circuits in combinatory logic","volume":"25","author":"Fitch","year":"1958","journal-title":"Philosophy of Science,"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0970","doi-asserted-by":"crossref","first-page":"87","DOI":"10.2307\/2271340","article-title":"The system C\u0394 of combinatory logic","volume":"28","author":"Fitch","year":"1963","journal-title":"Journal of Symbolic Logic"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0975","series-title":"Elements of Combinatory Logic","author":"Fitch","year":"1974"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0980","series-title":"Set Theory with a Universal Set","year":"1995"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0985","series-title":"Centenary Symposium,","first-page":"107","article-title":"Formal spaces","author":"Fourman","year":"1982"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0990","series-title":"Advances in Programming and Non-numerical Computation.","year":"1966"},{"key":"10.1016\/S1874-5857(09)70018-4_bb0995","article-title":"Begriffsschrift","author":"Frege","year":"1879","journal-title":"Verlag Louis Nebert, Halle, 1879"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1000","first-page":"21","article-title":"Funktion und Begriff","author":"Frege","year":"1960"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1005","series-title":"Grundgesetze der Arithmetik","author":"Frege","year":"1964"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1010","doi-asserted-by":"crossref","first-page":"346","DOI":"10.1109\/LICS.1990.113760","article-title":"Extensional PERs","author":"Freyd","year":"1990","journal-title":"Proceedings Fifth Annual IEEE Symposium on Logic In Computer Science,"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1015","doi-asserted-by":"crossref","first-page":"498","DOI":"10.1109\/LICS.1990.113772","article-title":"Recursive types reduced to inductive types","author":"Freyd","year":"1990","journal-title":"Proceedings Fifth Annual IEEE Symposium on Logic In Computer Science,"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1020","series-title":"Proceedings of the 1990 Como Category Theory Conference, volume 1488 of Lecture Notes in Mathematics,","first-page":"131","article-title":"Algebraically complete categories","author":"Freyd","year":"1991"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1025","series-title":"Applications of Categories in Computer Science, volume 177 of London Math. Soc. Lecture Notes Series,","first-page":"95","article-title":"Remarks on algebraically compact categories","author":"Freyd","year":"1992"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1030","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1002\/malq.19590050703","article-title":"Reducibilities and completeness for sets of integers","volume":"5","author":"Friedberg","year":"1959","journal-title":"Zeitschrift f\u00fcr Mathematische Logik und Grundlagen der Mathematik"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1035","series-title":"Logic Colloquium, Symposium on Logic held at Boston, 1972-73, volume 453 of Lecture Notes in Mathematics,","first-page":"22","article-title":"Equality between functionals","author":"Friedman","year":"1975"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1040","series-title":"Higher Set Theory, volume 669 of Lecture Notes in Mathematics,","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1007\/BFb0103100","article-title":"Classically and intuitionistically provably recursive functions","author":"Friedman","year":"1978"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1045","series-title":"Logic and Computer Science, volume 31 of APIC Studies in Data Processing,","first-page":"123","article-title":"On Girard\u2019s \u201cCandidats de reductibilite\u201d","author":"Gallier","year":"1990"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1050","series-title":"Logic Colloquium \u201976,","first-page":"173","article-title":"The simple theory of types","author":"Gandy","year":"1977"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1055","series-title":"The Universal Turing Machine: A Half-Century Survey","first-page":"51","article-title":"The confluence of ideas in 1936","author":"Gandy","year":"1988"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1060","series-title":"Unpublished manuscript","article-title":"Dialogues, Blass games, sequentiality for objects of finite type","author":"Gandy","year":"1993"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1065","doi-asserted-by":"crossref","first-page":"176","DOI":"10.1007\/BF01201353","article-title":"Untersuchungen \u00fcber das logische Schliessen.","volume":"39","author":"Gentzen","year":"1935","journal-title":"Mathematische Zeit- schrift,"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1070","doi-asserted-by":"crossref","first-page":"36","DOI":"10.1016\/S0019-9958(84)80009-1","article-title":"Effectively given domains and lambda calculus semantics","volume":"62","author":"Giannini","year":"1984","journal-title":"Information and Control"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1075","series-title":"A Compendium of Continuous Lattices","author":"Gierz","year":"1980"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1080","series-title":"Computer Programming and Formal Systems,","first-page":"71","article-title":"An abstract computer with a LISP-like machine language without a label operator","author":"Gilmore","year":"1963"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1085","series-title":"Proofs and Types","author":"Girard","year":"1989"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1090","series-title":"Proceedings of the Second Scandinavian Logic Symposium,","first-page":"63","article-title":"Une extension de l\u2019interpr\u00e9tation de G\u00f6del \u00e0 l\u2019analyse, et son application \u00e0 l\u2019\u00e9limination des coupures dans l\u2019analyse et la th\u00e9orie des types","author":"Girard","year":"1971"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1095","series-title":"Th\u00e8se de Doctorat d\u2019\u00c9tat","article-title":"Interpr\u00e9tation fonctionnelle et \u00e9limination des coupures de l\u2019arithm\u00e9tique d\u2019ordre sup\u00e9rieur","author":"Girard","year":"1972"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1100","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1016\/0003-4843(81)90016-4","article-title":"II 1\/2-logic, part I: dilators","volume":"21","author":"Girard","year":"1981","journal-title":"Annals of Mathematical Logic,"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1105","doi-asserted-by":"crossref","first-page":"159","DOI":"10.1016\/0304-3975(86)90044-7","article-title":"The system F of variable types, fifteen years later","volume":"45","author":"Girard","year":"1986","journal-title":"Theoretical Computer Science,"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1110","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","article-title":"Linear logic","volume":"50","author":"Girard","year":"1987","journal-title":"Theoretical Computer Science,"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1115","series-title":"Rendiconti del Seminario Matematico dell\u2019 Universit\u00e0 e del Politecnico di Torino","first-page":"11","article-title":"Multiplicatives","author":"Girard","year":"1987"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1120","first-page":"129","article-title":"Normal functors, power series and \u03bb-calculus","volume":"37","author":"Girard","year":"1988","journal-title":"Annals of Mathematical Logic,"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1125","series-title":"Logic Colloquium \u201988","first-page":"221","article-title":"Geometry of interaction I: interpretation of system F","author":"Girard","year":"1989"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1130","series-title":"Categories in Computer Science and Logic, volume 92 of Contemporary Mathematics","first-page":"69","article-title":"Towards a geometry of interaction","author":"Girard","year":"1989"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1135","series-title":"Computational Logic,","first-page":"215","article-title":"On the meaning of logical rules I: syntax vs. semantics","author":"Girard","year":"1998"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1140","series-title":"Foundations of Secure Computation","article-title":"On the meaning of logical rules II: multiplicative\/additive case","author":"Girard","year":"2000"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1145","doi-asserted-by":"crossref","first-page":"299","DOI":"10.1017\/S096012950100336X","article-title":"Locus solum","volume":"11","author":"Girard","year":"2001","journal-title":"Mathematical Structures in Computer Science"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1150","doi-asserted-by":"crossref","first-page":"38","DOI":"10.2178\/bsl\/1182353852","article-title":"Groups and algebras of binary relations","volume":"8","author":"Givant","year":"2002","journal-title":"Bulletin of Symbolic Logic,"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1155","doi-asserted-by":"crossref","first-page":"280","DOI":"10.1111\/j.1746-8361.1958.tb01464.x","article-title":"\u00dcber eine bisher noch nicht benotzte Erweiterung des finiten Stand- punktes.","volume":"12","author":"G\u00f6del","year":"1958","journal-title":"Dialectica"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1160","article-title":"Collected Works, Vol. 2 Publications 1938-1974","author":"G\u00f6del","year":"1990"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1165","series-title":"Vol. 3:Unpublished Essays and Lectures","article-title":"Collected Works","author":"G\u00f6del","year":"1995"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1170","series-title":"Nineteenth Annual A.C.M. Symposium on the Principles of Programming Languages (POPL),","first-page":"15","article-title":"The geometry of optimal lambda reduction","author":"Gonthier","year":"1992"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1175","series-title":"Intuitionism and Proof Theory","first-page":"101","article-title":"A theory of constructions equivalent to arithmetic","author":"Goodman","year":"1970"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1180","article-title":"Edinburgh LCF","volume":"volume 78","author":"Gordon","year":"1979"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1185","series-title":"Proof, Language and Interaction: Essays in Honour of Robin Milner","article-title":"From LCF to HOL: a short history","author":"Gordon","year":"2000"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1190","series-title":"The Search for Mathematical Roots, 1870-1940","author":"Grattan-Guinness","year":"2000"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1195","series-title":"Seventeenth Annual A.C.M. Symposium on the Principles of Programming Languages (POPL)","first-page":"47","article-title":"The formulae-as-types notion of control","author":"Griffin","year":"1990"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1200","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1016\/0022-4049(90)90055-M","article-title":"Coherence and consistency in domain","volume":"63","author":"Gunter","year":"1990","journal-title":"Journal of Pure and Applied Algebra,"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1205","series-title":"Theoretical Aspects of Object-Oriented Programming: Types, Semantics and Language Design","author":"Gunter","year":"1994"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1210","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0890-5401(87)90048-4","article-title":"Universal profinite domains","volume":"72","author":"Gunter","year":"1987","journal-title":"Information and Computation"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1215","series-title":"Algebraic Logic","author":"Halmos","year":"1962"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1220","doi-asserted-by":"crossref","first-page":"19","DOI":"10.4288\/jafpos1956.3.19","article-title":"Calculabilit\u00e9 des fonctionnels recursives primitives de type fini sur les nombres naturels","volume":"3","author":"Hanatani","year":"1966","journal-title":"Annals of the Japan Association for the Philosophy of Science"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1225","series-title":"Syntax and semantics of the language of primitive recursive functions","author":"Hancock","year":"1975"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1230","series-title":"Lambda Calculi","author":"Hankin","year":"1994"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1235","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1145\/138027.138060","article-title":"A framework for defining logics","volume":"40","author":"Harper","year":"1993","journal-title":"Journal of the ACM"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1240","series-title":"From Frege to G\u00f6del: A Source Book in Mathematical Logic 1879-1931","author":"van Heijenoort","year":"1967"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1245","doi-asserted-by":"crossref","first-page":"81","DOI":"10.2307\/2266967","article-title":"Completeness in the theory of types","volume":"15","author":"Henkin","year":"1950","journal-title":"Journal of Symbolic Logic"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1250","series-title":"Intuitionism, an Introduction","author":"Heyting","year":"1956"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1255","series-title":"Philosophy in the Mid-century","first-page":"101","article-title":"Intuitionism in mathematics","author":"Heyting","year":"1958"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1260","series-title":"GrundzuUge der Theoretischen Logik","author":"Hilbert","year":"1928"},{"issue":"226","key":"10.1016\/S1874-5857(09)70018-4_bb1265","first-page":"42","article-title":"Calculability of primitive recursive functionals of finite type","volume":"9","author":"Hinata","year":"1967","journal-title":"Science Reports of the Tokyo Kyoiku Daigaku, Section A"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1270","doi-asserted-by":"crossref","first-page":"289","DOI":"10.1002\/malq.19800261902","article-title":"Lambda-calculus models and exten- sionality","volume":"26","author":"Hindley","year":"1980","journal-title":"Zeitschrift f\u00fcr Mathematische Logik und Grundlagen der Mathematik,"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1275","series-title":"To H. B. Curry, Essays on Combinatory Logic, Lambda Calculus and Formalism.","year":"1980"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1280","series-title":"Introduction to Combinators and \u03bb-calculus","author":"Hindley","year":"1986"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1285","series-title":"Introduction to Combinatory Logic","author":"Hindley","year":"1972"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1290","doi-asserted-by":"crossref","first-page":"545","DOI":"10.1017\/S0022481200128439","article-title":"An abstract form of the Church-Rosser theorem, I","volume":"34","author":"Hindley","year":"1969","journal-title":"Journal of Symbolic Logic"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1295","first-page":"29","article-title":"The principal type-scheme of an object in combinatory logic","volume":"146","author":"Hindley","year":"1969","journal-title":"Transactions of the American Mathematical Society"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1300","doi-asserted-by":"crossref","first-page":"345","DOI":"10.1090\/S0002-9947-1978-0489603-9","article-title":"Reductions of residuals are finite","volume":"240","author":"Hindley","year":"1978","journal-title":"Transactions of the American Mathematical Society"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1305","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1090\/S0002-9947-1978-0492300-7","article-title":"Standard and normal reductions","volume":"241","author":"Hindley","year":"1978","journal-title":"Transactions of the American Mathematical Society"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1310","first-page":"212","article-title":"The simple semantics for Coppo-Dezani-Sall\u00e9 types","volume":"volume 137","author":"Hindley","year":"1982"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1315","series-title":"Basic Simple Type Theory","author":"Hindley","year":"1997"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1320","article-title":"M.h. newman\u2019s typability algorithm for lambda-calculus","author":"Hindley","year":"2008","journal-title":"Journal of Logic and Computation"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1325","series-title":"Alan Turing: The Enigma","author":"Hodges","year":"1983"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1330","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1016\/0168-0072(91)90052-N","article-title":"Systems of combinatory logic related to Quine\u2019s \u2019New Foundations\u2019","volume":"53","author":"Holmes","year":"1991","journal-title":"Annals of Pure and Applied Logic"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1335","series-title":"Typed Lambda Calculi and Applications","first-page":"235","article-title":"Untyped \u03bb-calculus with relative typing","author":"Holmes","year":"1995"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1340","series-title":"Intuitionism and Proof Theory,","first-page":"443","article-title":"Assignment of ordinals to terms for primitive recursive functionals of finite type","author":"Howard","year":"1970"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1345","first-page":"479","article-title":"The formul\u00e6-as-types notion of construction","author":"Howard","year":"1980"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1350","doi-asserted-by":"crossref","first-page":"797","DOI":"10.1145\/322217.322230","article-title":"Confluent reductions","volume":"27","author":"Huet","year":"1980","journal-title":"Journal of the Association for Computing Machinery"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1355","series-title":"Cartesian closed categories and lambda-calculus","first-page":"7","author":"Huet","year":"1990"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1360","series-title":"Logical Foundations of Functional Programming","year":"1990"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1365","doi-asserted-by":"crossref","first-page":"154","DOI":"10.1016\/0304-3975(93)90087-A","article-title":"An analysis of B\u00f6hm\u2019s theorem","volume":"121","author":"Huet","year":"1993","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1370","series-title":"Logische Untersuchungen","author":"Husserl","year":"1922"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1375","doi-asserted-by":"crossref","first-page":"285","DOI":"10.1006\/inco.2000.2917","article-title":"On full abstraction for PCF: I. Models, observables and the full abstraction problem, II. Dialogue games and innocent strategies, III. A fully abstract and universal game model","volume":"163","author":"Hyland","year":"2000","journal-title":"Information and Computation"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1380","first-page":"83","article-title":"A survey of some useful partial order relations on terms of the lambda calculus","author":"Hyland","year":"1975"},{"issue":"2","key":"10.1016\/S1874-5857(09)70018-4_bb1385","doi-asserted-by":"crossref","first-page":"361","DOI":"10.1112\/jlms\/s2-12.3.361","article-title":"A syntactic characterization of the equality in some models for the lambda calculus","volume":"12","author":"Hyland","year":"1976","journal-title":"Journal of the London Mathematical Society"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1390","series-title":"The L.E.J. Brouwer Centenary Symposium","first-page":"165","article-title":"The effective topos","author":"Hyland","year":"1982"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1395","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1016\/0168-0072(88)90018-8","article-title":"A small complete category","volume":"40","author":"Hyland","year":"1988","journal-title":"Annals of Pure and Applied Logic"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1400","series-title":"Conference on Category Theory, number 1488 in Lecture Notes in Mathematics","first-page":"131","article-title":"First steps in synthetic domain theory","author":"Hyland","year":"1991"},{"issue":"4","key":"10.1016\/S1874-5857(09)70018-4_bb1405","doi-asserted-by":"crossref","first-page":"399","DOI":"10.1007\/BF00262943","article-title":"The inconsistency of higher order extensions of Martin-L\u00f6f\u2019s type theory","volume":"18","author":"Jacobs","year":"1989","journal-title":"Journal of Philosophical Logic"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1410","series-title":"Indexed Categories and their Applications","author":"Johnstone","year":"1978"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1415","series-title":"Stone Spaces","author":"Johnstone","year":"1982"},{"issue":"4","key":"10.1016\/S1874-5857(09)70018-4_bb1420","article-title":"Remarques sur la th\u00e9orie des jeux a deux personnes","volume":"1","author":"Joyal","year":"1977","journal-title":"Gazette des Sciences Math\u00e9matiques du Quebec"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1425","series-title":"Domains and denotational semantics: history, accomplishments and open problems","first-page":"227","volume":"59","year":"1996"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1430","first-page":"187","article-title":"Domaines concr\u00e9ts","volume":"121","author":"Kahn","year":"1978","journal-title":"Rapport 336, IRIA Laboria"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1435","series-title":"Programming of Future Generation Computers","first-page":"237","article-title":"Natural semantics","author":"Kahn","year":"1988"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1440","doi-asserted-by":"crossref","first-page":"443","DOI":"10.1007\/BF01371632","article-title":"Condensed detachment as a rule of inference","volume":"42","author":"Kalman","year":"1983","journal-title":"Studia Logica"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1445","doi-asserted-by":"crossref","first-page":"197","DOI":"10.1142\/S0129054193000146","article-title":"On stepwise explicit substitutions","volume":"4","author":"Kamareddine","year":"1993","journal-title":"International Journal of Foundations of Computer Science"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1450","doi-asserted-by":"crossref","first-page":"395","DOI":"10.1017\/S0956796897002785","article-title":"Extending a \u03bb-calculus with explicit substitution which preserves strong normalisation into a confluent calculus on open terms","volume":"7","author":"Kamareddine","year":"1997","journal-title":"Journal of Functional Programming,"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1455","doi-asserted-by":"crossref","first-page":"349","DOI":"10.1093\/logcom\/10.3.349","article-title":"Relating the lambda-sigma and lambda-s styles of explicit substitutions","volume":"10","author":"Kamareddine","year":"2000","journal-title":"Journal of Logic and Computation,"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1460","doi-asserted-by":"crossref","first-page":"185","DOI":"10.2178\/bsl\/1182353871","article-title":"Types in logic and mathematics before 1940","volume":"8","author":"Kamareddine","year":"2002","journal-title":"Bulletin of Symbolic Logic"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1465","series-title":"Mathematical Foundations of Computer Science","article-title":"Fully effective solutions of recursive domain equations","author":"Kanda","year":"1979"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1470","series-title":"Massachusetts Institute of Technology","article-title":"Optimal interpreters for lambda-calculus based functional languages","author":"Kathail","year":"1990"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1475","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1305\/ndjfl\/1093890995","article-title":"The completeness of combinatory logic with discriminators","volume":"14","author":"Kearns","year":"1973","journal-title":"Notre Dame Journal of Formal Logic"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1480","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1016\/0022-4049(71)90013-2","article-title":"Coherence in closed categories","volume":"1","author":"Kelly","year":"1972","journal-title":"Journal of Pure and Applied Algebra"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1485","doi-asserted-by":"crossref","first-page":"630","DOI":"10.2307\/1968646","article-title":"The inconsistency of certain formal logics","volume":"36","author":"Kleene","year":"1935","journal-title":"Annals of Mathematics, Series 2"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1490","doi-asserted-by":"crossref","first-page":"340","DOI":"10.1215\/S0012-7094-36-00227-2","article-title":"\u03bb-definability and recursiveness","volume":"2","author":"Kleene","year":"1936","journal-title":"Duke Mathematical Journal"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1495","doi-asserted-by":"crossref","first-page":"109","DOI":"10.2307\/2269016","article-title":"On the interpretation of intuitionistic number theory","volume":"10","author":"Kleene","year":"1945","journal-title":"Journal of Symbolic Logic"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1500","series-title":"Introduction to Metamathematics","author":"Kleene","year":"1952"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1505","series-title":"Generalized Recursion Theory II","first-page":"185","article-title":"Recursive functionals and quantifiers of finite types revisited I","author":"Kleene","year":"1978"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1510","series-title":"The Kleene Symposium","first-page":"1","article-title":"Recursive functionals and quantifiers of finite types revisited II","author":"Kleene","year":"1980"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1515","doi-asserted-by":"crossref","first-page":"52","DOI":"10.1109\/MAHC.1981.10004","article-title":"Origins of recursive function theory","volume":"3","author":"Kleene","year":"1981","journal-title":"Annals of the History of Computing"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1520","series-title":"Patras Logic Symposium","first-page":"1","article-title":"Recursive functionals and quantifiers of finite types revisited III","author":"Kleene","year":"1982"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1525","series-title":"Recursion Theory","first-page":"119","article-title":"Unimonotone functions of finite types (Recursive functionals and quantifiers of finite types revisited IV)","author":"Kleene","year":"1985"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1530","doi-asserted-by":"crossref","first-page":"15","DOI":"10.1080\/0144534031000076237","article-title":"Russell's 1903\u20141905 anticipation of the lambda calculus","volume":"24","author":"Klement","year":"2003","journal-title":"History and Philosophy of Logic,"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1535","doi-asserted-by":"crossref","first-page":"46","DOI":"10.2307\/2268665","article-title":"Review of: Yanovskaya, S. A.: Osnovaniya matematiki i matematich- eskaya logika (Foundations of mathematics and mathematical logic)","volume":"16","author":"Kline","year":"1951","journal-title":"Journal of Symbolic Logic,"},{"issue":"1-2","key":"10.1016\/S1874-5857(09)70018-4_bb1540","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1016\/0304-3975(93)90091-7","article-title":"Combinatory reduction systems: introduction and survey","volume":"121","author":"Klop","year":"1993","journal-title":"Theoretical Computer Science,"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1545","unstructured":"J.W Klop Combinatory Reduction Systems. PhD thesis, Univ. Utrecht, 1980. Publ. by Mathematisch Centrum, 413 Kruislaan, Amsterdam."},{"key":"10.1016\/S1874-5857(09)70018-4_bb1550","first-page":"1","article-title":"Term Rewriting Systems","author":"Klop","year":"1992"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1555","series-title":"Proceedings of the 13th Symposium on Semigroups,","article-title":"\u03bb-calculus with simultaneous substitution as a primitive symbol","author":"Komori","year":"1990"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1560","doi-asserted-by":"crossref","first-page":"306","DOI":"10.1016\/S0019-9958(82)90796-3","article-title":"Models of the lambda calculus","volume":"52","author":"Koymans","year":"1982","journal-title":"Information and Control"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1565","doi-asserted-by":"crossref","unstructured":"G. Kreisel. Mathematical significance of consistency proofs, Jour. Symb. Logic 23, 155-181, 1958.","DOI":"10.2307\/2964396"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1570","series-title":"Constructivity in Mathematics,","first-page":"101","article-title":"Interpretation of analysis by means of constructive functionals of finite type","author":"Kreisel","year":"1959"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1575","series-title":"Logic, Methodology, and the Philosophy of Science","first-page":"198","article-title":"Foundations of intuitionistic logic","author":"Kreisel","year":"1962"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1580","first-page":"95","article-title":"Mathematical logic","volume":"volume 3","author":"Kreisel","year":"1965"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1585","series-title":"Lambda-calcul, Types et Modeles","author":"Krivine","year":"1990"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1590","unstructured":"A. S. Kuzichev. Sequential systems of \u03bb-conversion and of combinatory logic. In Hindley and Seldin [1980], pages 141-155."},{"key":"10.1016\/S1874-5857(09)70018-4_bb1595","series-title":"Vestnik, Moscow State University, Series Math.\/Mechan","first-page":"36","article-title":"Set theory in type-free combinatorially complete systems","author":"Kuzichev","year":"1983"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1600","first-page":"424","article-title":"A version of formalization of Cantor's set theory","volume":"60","author":"Kuzichev","year":"1999","journal-title":"Doklady Mathematics"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1605","series-title":"The Evolution of Type Theory in Logic and Mathematics","author":"Laan","year":"1997"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1610","series-title":"Proceedings Sixth Annual IEEE Symposium on Logic In Computer Science","first-page":"43","article-title":"Games semantics for linear logic","author":"Lafont","year":"1991"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1615","unstructured":"F. Lamarche. Sequentiality, games and linear logic, 1992. Unpublished paper, from a lecture to the CLiCS Symposium (Aarhus Univ., March 23-27, 1992)."},{"key":"10.1016\/S1874-5857(09)70018-4_bb1620","unstructured":"J. Lambek and G. D. Findlay. Calculus of bimodules, 1955. Unpublished manuscript."},{"key":"10.1016\/S1874-5857(09)70018-4_bb1625","doi-asserted-by":"crossref","first-page":"154","DOI":"10.1080\/00029890.1958.11989160","article-title":"The mathematics of sentence structure","volume":"65","author":"Lambek","year":"1958","journal-title":"American Mathematical Monthly"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1630","series-title":"Structure of Language and its Mathematical Aspects","first-page":"56","article-title":"On the calculus of syntactic types","author":"Lambek","year":"1961"},{"issue":"4","key":"10.1016\/S1874-5857(09)70018-4_bb1635","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1007\/BF01703261","article-title":"Deductive systems and categories, I: syntactic calculus and residuated categories","volume":"2","author":"Lambek","year":"1968","journal-title":"Mathematical Systems Theory"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1640","first-page":"76","article-title":"Deductive systems and categories, II: standard constructions and closed categories","author":"Lambek","year":"1969"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1645","first-page":"57","article-title":"Deductive systems and categories, III: cartesian closed categories, intuitionist propositional calculus, and combinatory logic","author":"Lambek","year":"1972"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1650","doi-asserted-by":"crossref","first-page":"259","DOI":"10.1016\/0003-4843(74)90003-5","article-title":"Functional completeness of cartesian categories","volume":"6","author":"Lambek","year":"1974","journal-title":"Annals of Mathematical Logic"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1655","unstructured":"J. Lambek. From \u03bb-calculus to cartesian closed categories. In Hindley and Seldin [1980], pages 375-402."},{"key":"10.1016\/S1874-5857(09)70018-4_bb1660","doi-asserted-by":"crossref","first-page":"113","DOI":"10.1016\/0001-8708(80)90013-4","article-title":"From types to sets","volume":"36","author":"Lambek","year":"1980","journal-title":"Advances in Mathematics"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1665","series-title":"Categorial and Categorical Grammars","article-title":"Categorial grammars and natural language structures","author":"Lambek","year":"1988"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1670","series-title":"Advances in Linear Logic","first-page":"43","article-title":"Bilinear logic in algebra and linguistics","author":"Lambek","year":"1995"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1675","series-title":"Seventeenth Annual A.C.M. Symposium on the Principles of Programming Languages (POPL)","first-page":"16","article-title":"An algorithm for optimal lambda calculus reduction","author":"Lamping","year":"1990"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1680","doi-asserted-by":"crossref","first-page":"308","DOI":"10.1093\/comjnl\/6.4.308","article-title":"The mechanical evaluation of expressions","volume":"6","author":"Landin","year":"1964","journal-title":"The Computer Journal"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1685","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1145\/363744.363749","article-title":"A correspondence between ALGOL 60 and Church's lambda notation","volume":"8","author":"Landin","year":"1965","journal-title":"Communications of the ACM"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1690","series-title":"Advances in Programming and Non-numerical Computation","first-page":"97","article-title":"A lambda-calculus approach","author":"Landin","year":"1966"},{"issue":"3","key":"10.1016\/S1874-5857(09)70018-4_bb1695","doi-asserted-by":"crossref","first-page":"157","DOI":"10.1145\/365230.365257","article-title":"The next 700 programming languages","volume":"9","author":"Landin","year":"1966","journal-title":"Communications of the ACM"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1700","first-page":"263","article-title":"Intuitionistic propositional calculus and definably non-empty terms","volume":"30","author":"L\u00e4uchli","year":"1965","journal-title":"Journal of Symbolic Logic"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1720","series-title":"Intuitionism and Proof Theory","first-page":"227","article-title":"An abstract notion of realizability for which intuitionistic predicate calculus is complete","author":"L\u00e4auchli","year":"1970"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1725","article-title":"Functorial semantics of algebraic theories","author":"Lawvere","year":"1963","journal-title":"PhD thesis"},{"issue":"6","key":"10.1016\/S1874-5857(09)70018-4_bb1730","doi-asserted-by":"crossref","first-page":"1506","DOI":"10.1073\/pnas.52.6.1506","article-title":"An elementary theory of the category of sets","volume":"52","author":"Lawvere","year":"1964","journal-title":"Proceedings of the National Academy of Sciences of the U.S.A"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1735","series-title":"AIn Proceedings of the La Jolla conference on Categorical Algebra","first-page":"1","article-title":"The category of categories as a foundation for Mathematics","author":"Lawvere","year":"1966"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1740","doi-asserted-by":"crossref","first-page":"281","DOI":"10.1111\/j.1746-8361.1969.tb01194.x","article-title":"Adjointness in Foundations","volume":"23","author":"Lawvere","year":"1969","journal-title":"Dialectica"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1745","first-page":"134","article-title":"Diagonal arguments and cartesian closed categories","author":"Lawvere","year":"1969"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1750","first-page":"1","article-title":"Equality in hyperdoctrines and comprehension schema as an adjoint functor","author":"Lawvere","year":"1968"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1755","series-title":"In Actes du Congr\u00e8s International des Math\u00e8matiques","first-page":"329","article-title":"Quantifiers and sheaves","author":"Lawvere","year":"1970"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1760","unstructured":"F.W. Lawvere. Category theory over a base topos, 1972. Unpubl. lecture notes."},{"key":"10.1016\/S1874-5857(09)70018-4_bb1765","doi-asserted-by":"crossref","first-page":"101","DOI":"10.1016\/B978-0-12-339050-9.50014-6","article-title":"Variable quantities and variable structures in topoi","author":"Lawvere","year":"1976","journal-title":"In Algebra, Topology and Category Theory. A collection of Papers in Honor of Samuel Eilenberg"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1770","series-title":"Proceedings of the Aarhus Open House on Topos Theoretic Methods in Geometry, May 1978","article-title":"Categorical dynamics","author":"Lawvere","year":"1979"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1775","first-page":"181","article-title":"Adjoints in and among bicategories","author":"Lawvere","year":"1996"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1780","series-title":"Tenth Annual A.C.M. Symposium on the Principles of Programming Languages (POPL)","first-page":"88","article-title":"Polymorphic type inference","author":"Leivant","year":"1983"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1785","first-page":"279","article-title":"Contracting proofs to programs","author":"Leivant","year":"1990"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1790","unstructured":"E. J. Lemmon, C. A. Meredith, D. Meredith, A. N. Prior, and I. Thomas. Calculi of pure strict implication. Informally distributed, 1957. Publ. 1969 in Philosophical logic, ed. by Davis and Hockney and Wilson, D. Reidel Co., Dordrecht, Netherlands, pp. 215-250."},{"key":"10.1016\/S1874-5857(09)70018-4_bb1795","doi-asserted-by":"crossref","first-page":"272","DOI":"10.2307\/2269839","article-title":"Review of: K. Menger: the algebra of functions: past, present, future","volume":"31","author":"Lercher","year":"1966","journal-title":"Journal of Symbolic Logic"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1800","doi-asserted-by":"crossref","first-page":"1","DOI":"10.4064\/fm-14-1-1-81","article-title":"Grundziige eines neuen Systems der Grundlagen der Mathematik","volume":"14","author":"Le\u015bniewski","year":"1929","journal-title":"Fundamenta Mathematic\u00e6"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1805","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1016\/0304-3975(76)90009-8","article-title":"An algebraic interpretation of \u03bb\u03b2K-calculus, and an application of a labelled \u03bb-calculu","volume":"2","author":"L\u00e9vy","year":"1976","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1810","series-title":"R\u00e9ductions correctes et optimales dans le \u03bb-calcul","author":"L\u00e9vy","year":"1978"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1815","doi-asserted-by":"crossref","first-page":"341","DOI":"10.1016\/S0304-3975(00)00194-8","article-title":"Finitary PCF is not decidable","volume":"266","author":"Loader","year":"2001","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1820","first-page":"32","article-title":"Notions of computability at higher types, I","author":"Longley","year":"2001","journal-title":"Logic Colloquium 2000"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1825","doi-asserted-by":"crossref","first-page":"215","DOI":"10.1017\/S0960129500001298","article-title":"Constructive natural deduction and its modest interpretation","volume":"1","author":"Longo","year":"1992","journal-title":"Mathematical Structures in Computer Science"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1830","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1016\/0304-3975(93)90093-9","article-title":"The genericity theorem and para- metricity in the polymorphic A-calculus","volume":"121","author":"Longo","year":"1993","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1835","first-page":"41","article-title":"From numbered sets to type theories","author":"Longo","year":"1987"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1840","doi-asserted-by":"crossref","first-page":"69","DOI":"10.3233\/FI-1995-22124","article-title":"Parametric and type-dependent polymorphism","volume":"22","author":"Longo","year":"1995","journal-title":"Fundamenta Informaticae"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1845","doi-asserted-by":"crossref","first-page":"255","DOI":"10.1023\/A:1010367416884","article-title":"Basic objectives of dialogue logic in historical perspective","volume":"127","author":"Lorenz","year":"2001","journal-title":"Synthese"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1850","series-title":"Einf\u00fchrung in die Operative Logik und Mathematik","author":"Lorenzen","year":"1955"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1855","series-title":"Infinitistic Methods","first-page":"193","article-title":"Ein dialogisches Konstructivit\u00e4tskriterium","author":"Lorenzen","year":"1961"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1860","doi-asserted-by":"crossref","first-page":"1","DOI":"10.2307\/2269177","article-title":"Einkleidung der Mathematik in Schr\u00f6derschen Relativkalkul","volume":"5","author":"L\u00f6wenheim","year":"1940","journal-title":"Journal of Symbolic Logic"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1865","first-page":"30","article-title":"Untersuchungen \u00fcber den Aussagenkalk\u00fcl","volume":"23","author":"Lukasiewicz","year":"1930","journal-title":"Comptes Rendus des S\u00e9ances de la Societ\u00e9 des Sciences et des Lettres de Varso- vie"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1870","unstructured":"J. Lukasiewicz. Der \u00e4quivalenzenkalkul. Collectanea Logica, 1:145-169, 1939. Journal vol. never appeared. Engl. transl: The equivalential calculus, in Polish Logic, ed. by S. McCall, Clarendon Press, Oxford, pp. 88-115, and in Jan Lukasiewicz Selected Works, ed. by L. Borkowski, North-Holland Co., Amsterdam, 1970, pp. 250-277."},{"key":"10.1016\/S1874-5857(09)70018-4_bb1875","series-title":"Eleventh Annual A.C.M. Symposium on the Principles of Programming Languages (POPL)","first-page":"165","article-title":"An ideal model for recursive polymorphic types","author":"MacQueen","year":"1984"},{"issue":"3","key":"10.1016\/S1874-5857(09)70018-4_bb1880","doi-asserted-by":"crossref","first-page":"289","DOI":"10.1112\/plms\/s3-31.3.289","article-title":"The connection between equivalence of proofs and cartesian closed categories","volume":"31","author":"Mann","year":"1975","journal-title":"Proceedings of the London Mathematical Society"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1885","doi-asserted-by":"crossref","first-page":"211","DOI":"10.1080\/01445349708837290","article-title":"Alonzo Church: his life, his work and some of his miracles","volume":"18","author":"Manzano","year":"1997","journal-title":"History and Philosophy of Logic"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1890","unstructured":"P. Martin-L\u00f6f. On the strength of intuitionistic reasoning, 1971. Unpub-lished contribution to Symposium on Perspectives in the Philosophy of Mathematics at 4th International Congress for Logic, Methodology and Philosophy of Science, Bucharest."},{"key":"10.1016\/S1874-5857(09)70018-4_bb1895","unstructured":"P. Martin-L\u00f6f. A Theory of Types, 1971. Informally circulated."},{"issue":"1","key":"10.1016\/S1874-5857(09)70018-4_bb1900","first-page":"93","article-title":"Infinite terms and a system of natural deduction","volume":"24","author":"Martin-Lof","year":"1972","journal-title":"Compositio Mathematica"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1905","series-title":"Published in Twenty-Five Years of Constructive Type Theory","first-page":"127","article-title":"An Intuitionistic Theory of Types","author":"Martin-L\u00f6f.","year":"1998"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1910","series-title":"Logic Colloquium '73","first-page":"73","article-title":"An intuitionistic theory of types: Predicative part","author":"Martin-L\u00f6f","year":"1975"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1915","series-title":"Logic, Methodology and Philos-ophy of Science, VI","first-page":"153","article-title":"Constructive mathematics and computer programming","author":"Martin-L\u00f6f.","year":"1982"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1920","series-title":"Programming Methodology Group","article-title":"The domain interpretation of type theory","author":"Martin-L\u00f6f.","year":"1983"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1925","series-title":"Studies in Proof Theory.","article-title":"Intuitionistic Type Theory","author":"Martin-L\u00f6f.","year":"1984"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1930","series-title":"Atti degli Incontri di Logica Matematica","first-page":"203","article-title":"On the meanings of the logical constants and the justifica-tions of the logical laws","author":"Martin-L\u00f6f.","year":"1985"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1935","series-title":"Atti del congresso Logica e Filosofia della Scienza, Oggi, San Gimignano, 7-11 Dicembre 1983 volume I: Logica","first-page":"79","article-title":"Unifying Scott's theory of domains for denotational seman-tics and intuitionistic type theory","author":"Martin-L\u00f6f.","year":"1986"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1940","doi-asserted-by":"crossref","first-page":"407","DOI":"10.1007\/BF00484985","article-title":"Truth of a proposition, evidence of a judgement, validity of a proof","volume":"73","author":"Martin-L\u00f6f.","year":"1987","journal-title":"Synthese"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1945","doi-asserted-by":"crossref","first-page":"184","DOI":"10.1145\/367177.367199","article-title":"Recursive functions of symbolic expressions and their compu-tation by machine","volume":"3","author":"McCarthy.","year":"1960","journal-title":"Communications of the ACM"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1950","series-title":"Computer Programming and Formal Systems","first-page":"33","article-title":"A basis for a mathematical theory of computation","author":"McCarthy.","year":"1963"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1955","series-title":"Information Processing 62: Proceedings of the IFIP Congress 1962","first-page":"21","article-title":"Towards a mathematical science of computation","author":"McCarthy.","year":"1963"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1960","series-title":"History of Programming Languages","first-page":"173","article-title":"History of LISP","author":"McCarthy.","year":"1981"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1965","series-title":"An investigation of a programming language with a polymorphic type structure","author":"McCracken.","year":"1979"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1970","series-title":"A finitary retract model for the polymorphic lambda-calculus","author":"McCracken.","year":"1982"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1975","first-page":"227","article-title":"Finite problems","volume":"3","author":"Medvedev","year":"1962","journal-title":"Soviet Mathematics Doklady"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1980","first-page":"215","article-title":"Weaker D-complete logics","volume":"4","author":"Megill","year":"1996","journal-title":"Journal of the Interest Group on Propositional Logics"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1985","first-page":"3","article-title":"Tri-operational algebra","volume":"5","author":"Menger.","year":"1944","journal-title":"Reports of a Mathematical Colloquium"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1990","doi-asserted-by":"crossref","first-page":"81","DOI":"10.1002\/malq.19640100602","article-title":"On substitutive algebra and its syntax","volume":"10","author":"Menger.","year":"1964","journal-title":"Zeitschrift fur Mathematis-che Logik und Grundlagen der Mathematik"},{"key":"10.1016\/S1874-5857(09)70018-4_bb1995","doi-asserted-by":"crossref","first-page":"513","DOI":"10.1305\/ndjfl\/1093888116","article-title":"In memoriam Carew Arthur Meredith","volume":"18","author":"Meredith","year":"1977","journal-title":"Notre Dame Journal of Formal Logic"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2000","first-page":"136","article-title":"Problems in the analogy between A-calculus and positive logic","volume":"11","author":"Meredith","year":"1980","journal-title":"Bulletin of the European Association for Theoretical Computer Science"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2005","series-title":"Research School of the Social Sciences","article-title":"Condensed detachment and combinators","author":"Meyer","year":"1988"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2010","doi-asserted-by":"crossref","first-page":"597","DOI":"10.1007\/BF01880331","article-title":"Implementing the \"fool's model\" of combinatory logic","volume":"7","author":"Meyer","year":"1991","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2015","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1016\/S0019-9958(82)80087-9","article-title":"What is a model of the lambda calculus?","volume":"52","author":"Meyer","year":"1982","journal-title":"Information and Control"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2020","article-title":"Une nouvelle C\u03b2-r\u00e9duction dans la logique combinatoire","volume":"31","author":"Mezghiche","year":"1984","journal-title":"Theoretical Computer"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2025","doi-asserted-by":"crossref","unstructured":"R. Milner. Logic for computable functions; description of a machine implementation. Technical Report STAN-CS-72-288, Stanford Univ., 1972.","DOI":"10.21236\/AD0785072"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2030","first-page":"157","article-title":"Processes: a mathematical model of computing agents","author":"Milner","year":"1975"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2035","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0304-3975(77)90053-6","article-title":"Fully abstract models of typed \u03bb-calculi","volume":"4","author":"Milner","year":"1977","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2040","doi-asserted-by":"crossref","first-page":"348","DOI":"10.1016\/0022-0000(78)90014-4","article-title":"A theory of type polymorphism in programming","volume":"17","author":"Milner","year":"1978","journal-title":"Journal of Computer and System Sciences"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2045","doi-asserted-by":"crossref","first-page":"587","DOI":"10.1007\/BF01880330","article-title":"Condensed detachment is complete for relevance logic: a computer-aided proof","volume":"7","author":"Mints","year":"1991","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2050","first-page":"37","article-title":"Les antinomies de Russell et de Burali-Forti et le probl\u00e9me fondamental de la th\u00e9orie des ensembles","volume":"19","author":"Mirimanoff","year":"1917","journal-title":"L'Enseignement Mathematique"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2055","doi-asserted-by":"crossref","first-page":"146","DOI":"10.1007\/BF02008531","article-title":"Ein algebraischer Beweis f\u00fcr das Church-Rosser Theorem","volume":"15","author":"Mitschke","year":"1973","journal-title":"Archiv f\u00fcr Mathematische Logik"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2060","doi-asserted-by":"crossref","first-page":"29","DOI":"10.1002\/malq.19790250104","article-title":"The standardization theorem for the \u03bb-calculus","volume":"25","author":"Mitschke","year":"1979","journal-title":"Zeitschrift f\u00fcr Mathematische Logik und Grundlagen der Mathematik"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2065","series-title":"Computations in Higher Types","author":"Moldestad","year":"1977"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2070","series-title":"Formal Philosophy. Selected Papers","author":"Montague","year":"1903"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2075","series-title":"Lambda-calculus Models of Programming Languages","author":"Morris","year":"1968"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2080","unstructured":"J. Moses. The Function of FUNCTION in LISP, 1970. Massachusetts Institute of Technology, Project MAC report AI-199. Available on Web at ftp:\/\/publications.ai.mit.edu\/ ai-publications\/0-499\/AIM-199.ps"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2085","doi-asserted-by":"crossref","first-page":"96","DOI":"10.1109\/LICS.1991.151634","article-title":"An evaluation semantics for classical proofs","author":"Murthy","year":"1991","journal-title":"Proceedings Sixth Annual IEEE Symposium on Logic In Computer Science"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2090","doi-asserted-by":"crossref","first-page":"310","DOI":"10.1002\/malq.19550010407","article-title":"Effective operations on partial recursive functions","volume":"1","author":"Myhill","year":"1955","journal-title":"Zeitschrift f\u00fcr Mathematische Logik"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2095","first-page":"62","author":"Nakajima","year":"1975","journal-title":"Infinite normal forms for the \u03bb-calculus"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2100","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/366193.366201","article-title":"Revised report on the algorithmic language ALGOL 60","volume":"6","author":"Naur","year":"1963","journal-title":"Communications of the ACM"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2105","first-page":"3","author":"Nederpelt","year":"1994","journal-title":"Twenty-Five Years of Automath Research"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2110","series-title":"Selected Papers on Automath","year":"1994"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2115","series-title":"Strong normalization in a typed lambda calculus with lambda structured types","first-page":"389","author":"Nederpelt","year":"1973"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2120","unstructured":"A. Nerode. General topology and partial recursive functionals. Summaries of talks at the Cornell Summer Institute of Symbolic Logic, 1957."},{"key":"10.1016\/S1874-5857(09)70018-4_bb2125","doi-asserted-by":"crossref","first-page":"397","DOI":"10.1215\/S0012-7094-59-02637-7","article-title":"Some Stone spaces and recursion theory","volume":"26","author":"Nerode","year":"1959","journal-title":"Duke Mathematical Journal"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2130","doi-asserted-by":"crossref","first-page":"219","DOI":"10.1515\/crll.1925.154.219","article-title":"Eine Axiomatizierung der Mengenlehre","volume":"154","author":"von Neumann","year":"1925","journal-title":"Journal fUr die Reine und Angewandte Mathematik"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2135","doi-asserted-by":"crossref","first-page":"669","DOI":"10.1007\/BF01171122","article-title":"Die Axiomatizierung der Mengenlehre","volume":"27","author":"von Neumann","year":"1928","journal-title":"Mathematische Zeitschrift"},{"issue":"2","key":"10.1016\/S1874-5857(09)70018-4_bb2140","doi-asserted-by":"crossref","first-page":"223","DOI":"10.2307\/1968867","article-title":"On theories with a combinatorial definition of \"equivalence\"","volume":"43","author":"Newman","year":"1942","journal-title":"Annals of Mathematics"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2145","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1017\/S0305004100017722","article-title":"Stratified systems of logic","volume":"39","author":"Newman","year":"1943","journal-title":"Proceedings of the Cambridge Philosophical Society"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2150","series-title":"Proceedings of the Symposium on Logical Foundations of Computer Science, volume 813 of Lecture Notes in Computer Science","first-page":"253","article-title":"Hereditarily sequential functionals","author":"Nickau","year":"1994"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2155","series-title":"Automata, Languages and Programming","article-title":"Langages algebriques sur le magma libre et semantique des schemas de programme","author":"Nivat","year":"1973"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2160","series-title":"Programming in Martin-L\u00f6f's Type Theory","author":"Nordstr\u00f6m","year":"1990"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2165","article-title":"Computing in Systems Described by Equations","volume":"volume 58","author":"O'Donnell","year":"1977"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2170","article-title":"Correspondence between operational and denotational semantics","volume":"volume 4","author":"Ong","year":"1995"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2175","doi-asserted-by":"crossref","first-page":"239","DOI":"10.1017\/S0960129502003626","article-title":"Realizability: a historical essay","volume":"12","author":"van Oosten","year":"2002","journal-title":"Mathematical Structures in Computer Science"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2180","first-page":"47","article-title":"The Dialectica categories","author":"de Paiva","year":"1989"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2185","first-page":"341","article-title":"A Dialectica-like model of linear logic","author":"de Paiva","year":"1989"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2190","unstructured":"D. Park. The Y combinator in Scott's lambda calculus models. Theory of Computation Report 13, Dept. of Computer Science, Univ. Warwick, 1976. First version presented 1970 at Symposium on Theory of Programming, Univ. Warwick"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2195","unstructured":"G.Peano. Arithmetices Principia, Nova Methodo Exposita. Fratelli Bocca, Torino, Italy, 1889. Also in [Peano,1958], Vol.2, Item 16, pp.20-55. Engl. transls: (1) The Principles of Arithmetic, in Selected Works of Giuseppe Peano, ed. H.Kennedy, publ. Allen and Unwin, London, 1973, pp.101-134; (2) The Principles of Arithmetic, in [Peano, 1958], pp.83-97."},{"key":"10.1016\/S1874-5857(09)70018-4_bb2200","unstructured":"G. Peano. Formulaire de Math\u00e9matiques. Fratelli Bocca, Torino, Italy, 1895. Publ. in 5 vols. 1895-1908. Later vols. overlapped and revised earlier vols. Vol. 3 publ. Carr\u00e9et Naud, Paris, 1901. Vol. 5 titled Formulario Mathematico in Peano's language Latino sine flexione"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2205","series-title":"Opere Scelte","author":"Peano","year":"1958"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2210","series-title":"Johns Hopkins Studies in Logic","first-page":"187","article-title":"The logic of relatives","author":"Peirce","year":"1883"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2215","series-title":"The Implementation of Functional Programming Languages","author":"Peyton Jones","year":"1987"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2220","series-title":"In Proceedings Fifth Annual IEEE Symposium on Logic In Computer Science","first-page":"366","article-title":"Effective domains and intrinsic structure","author":"Phoa","year":"1990"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2225","series-title":"Types and Programming Languages","author":"Pierce","year":"2002"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2230","doi-asserted-by":"crossref","first-page":"149","DOI":"10.3233\/FI-1998-33203","article-title":"Lambda abstraction algebras: coordina- tizing models of lambda calculus","volume":"33","author":"Pigozzi","year":"1998","journal-title":"Fundamenta Informaticae,"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2235","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1016\/0304-3975(89)90143-6","article-title":"Abstraction problems in combinatory logic; a compositive approach","volume":"66","author":"Piperno","year":"1989","journal-title":"Theoretical Computer Science,"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2240","first-page":"12","article-title":"Polymorphism is set theoretic, constructively","volume":"283","author":"Pitts","year":"1987"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2245","unstructured":"R. A. Platek Foundations of Recursion Theory. PhD thesis, Stanford Univ., 1966."},{"key":"10.1016\/S1874-5857(09)70018-4_bb2250","first-page":"361","article-title":"A logic for parametric polymorphism","volume":"664","author":"Plotkin","year":"1993"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2255","unstructured":"G. D. Plotkin. Lambda-definability and logical relations. Technical Report SAIRM-4, School of Artificial Intelligence, Univ. Edinburgh, U.K., 1973."},{"key":"10.1016\/S1874-5857(09)70018-4_bb2260","doi-asserted-by":"crossref","first-page":"313","DOI":"10.2307\/2272645","article-title":"The \u03bb-calculus is \u03c9-incomplete","volume":"39","author":"Plotkin","year":"1974","journal-title":"Journal of Symbolic Logic"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2265","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1016\/0304-3975(75)90017-1","article-title":"Call-by-name, call-by-value and the \u03bb-calculus","volume":"1","author":"Plotkin","year":"1975","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2270","doi-asserted-by":"crossref","first-page":"223","DOI":"10.1016\/0304-3975(77)90044-5","article-title":"LCF considered as a programming language","volume":"5","author":"Plotkin","year":"1977","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2275","series-title":"Lectures, summer school, Dipartimento di Informatica","article-title":"The category of complete partial orders: a tool for making meanings","author":"Plotkin","year":"1978"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2280","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1016\/0022-0000(78)90006-5","article-title":"T\u03c9as a universal domain","volume":"17","author":"Plotkin","year":"1978","journal-title":"Journal of Computer and System Sciences"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2285","unstructured":"G. D. Plotkin. Lambda-definability in the full type hierarchy. In Hindley and Seldin [1980], pages 363-373."},{"key":"10.1016\/S1874-5857(09)70018-4_bb2290","unstructured":"G. D. Plotkin. Post-graduate lecture notes in advanced domain theory. Dept. Computer Science, Univ. Edinburgh, 1981."},{"key":"10.1016\/S1874-5857(09)70018-4_bb2295","doi-asserted-by":"crossref","first-page":"351","DOI":"10.1016\/0304-3975(93)90094-A","article-title":"Set-theoretical and other elementary models of the \u03bb-calculus","volume":"121 (Bohm Volume)","author":"Plotkin","year":"1993","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2300","doi-asserted-by":"crossref","first-page":"256","DOI":"10.1006\/inco.1994.1018","article-title":"A semantics for static type-inference","volume":"109","author":"Plotkin","year":"1994","journal-title":"Information and Computation"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2305","doi-asserted-by":"crossref","first-page":"445","DOI":"10.1305\/ndjfl\/1093888405","article-title":"Proofs of the normalization and Church-Rosser theorems for the typed \u03bb-calculus","volume":"19","author":"Pottinger","year":"1978","journal-title":"Notre Dame Journal of Formal Logic"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2310","unstructured":"G. Pottinger. A type assignment for the strongly normalizable \u03bb-terms. In Hindley and Seldin [1980], pages 561-579."},{"key":"10.1016\/S1874-5857(09)70018-4_bb2315","series-title":"Natural Deduction.","author":"Prawitz","year":"1965"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2320","doi-asserted-by":"crossref","first-page":"246","DOI":"10.1111\/j.1755-2567.1967.tb00622.x","article-title":"Completeness and Haupsatz for second order logic","volume":"33","author":"Prawitz","year":"1967","journal-title":"Theoria"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2325","doi-asserted-by":"crossref","first-page":"452","DOI":"10.2307\/2270331","article-title":"Hauptsatz for higher order logic","volume":"33","author":"Prawitz","year":"1968","journal-title":"Journal of Symbolic Logic"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2330","series-title":"Proceedings of the Second Scandinavian Logic Symposium","first-page":"235","article-title":"Ideas and results in proof theory","author":"Prawitz","year":"1971"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2335","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1090\/S0002-9904-1936-06239-7","article-title":"A reinterpretation of Schonfinkel's logical operators","volume":"42","author":"Quine","year":"1936","journal-title":"Bulletin of the American Mathematical Society"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2340","doi-asserted-by":"crossref","first-page":"2","DOI":"10.2307\/2269323","article-title":"Towards a calculus of concepts","volume":"1","author":"Quine","year":"1936","journal-title":"Journal of Symbolic Logic"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2345","doi-asserted-by":"crossref","first-page":"70","DOI":"10.1080\/00029890.1937.11987928","article-title":"New foundations for mathematical logic","volume":"44","author":"Quine","year":"1937","journal-title":"American Mathematical Monthly"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2350","series-title":"Set Theory and its Logic","author":"Quine","year":"1963"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2355","series-title":"Logic and Art: Essays in Honor of Nelson Goodman","first-page":"214","article-title":"Algebraic logic and predicate functors","author":"Quine","year":"1972"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2360","doi-asserted-by":"crossref","first-page":"338","DOI":"10.1112\/plms\/s2-25.1.338","article-title":"The foundations of mathematics","volume":"25","author":"Ramsey","year":"1926","journal-title":"Proceeding of the London Mathematical Society, Series 2"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2365","unstructured":"G. R\u00e9v\u00e9sz. \u22cb-calculus without substitution. Technical report, Computer and Automation Institute, Hungarian Academy of Sciences, 1978"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2370","doi-asserted-by":"crossref","first-page":"373","DOI":"10.1137\/0214028","article-title":"Axioms for the theory of lambda-conversion","volume":"14","author":"R\u00e9v\u00e9sz","year":"1985","journal-title":"SIAM Journal of Computing"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2375","unstructured":"J.C.Reynoldsand G.D.Plotkin.On functors expressible in the polymorphic typed lambda calculus.In Huet [1990b], pages 127-152"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2380","unstructured":"J. C. Reynolds. Notes on a lattice-theoretic approach to the theory of computation. Report, Syracuse Univ., Syracuse, New York, October 1972. Revised March 1979"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2385","first-page":"408","article-title":"Towards a theory of type structure","author":"Reynolds","year":"1974"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2390","series-title":"Information Processing 83","first-page":"513","article-title":"Types, abstraction and parametric polymorphism","author":"Reynolds","year":"1983"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2395","first-page":"704","article-title":"Syntactic control of interference, part 2","author":"Reynolds","year":"1989"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2400","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1007\/BF01019459","article-title":"The discoveries of continuations","volume":"6","author":"Reynolds","year":"1993","journal-title":"Lisp and Symbolic Computation"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2405","series-title":"A Bibliography of Lambda-Calculi, Combinatory Logics and Related Topics","author":"Rezus","year":"1982"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2410","first-page":"1","article-title":"Semantics of constructive type theory","volume":"6","author":"Rezus","year":"1986","journal-title":"Libertas Mathematica (Arlington, TX)"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2415","doi-asserted-by":"crossref","first-page":"65","DOI":"10.1007\/BF02011139","article-title":"Mengentheoretische Modelle des AK-Kalkiils","volume":"20","author":"von Rimscha","year":"1980","journal-title":"Archiv fur Mathematische Logik"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2420","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1145\/321250.321253","article-title":"A machine-oriented logic based on the resolution principle","volume":"12","author":"Robinson","year":"1965","journal-title":"Journal of the Association for Computing Machinery"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2425","series-title":"Theory of Recursive Functions and Effective Computability","author":"Rogers","year":"1967"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2430","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1016\/0304-3975(83)90069-5","article-title":"Principal type schemes for an extended type theory","volume":"28","author":"Ronchi della Rocca","year":"1984","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2435","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1016\/0304-3975(88)90101-6","article-title":"Principal type schemes and unification for intersection type discipline","volume":"59","author":"Ronchi della Rocca","year":"1988","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2440","doi-asserted-by":"crossref","first-page":"160","DOI":"10.1145\/321738.321750","article-title":"Tree manipulating systems and Church-Rosser theorems","volume":"20","author":"Rosen","year":"1973","journal-title":"Journal of the Association for Computing Machinery"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2445","series-title":"The Elements of Mathematical Logic","author":"Rosenbloom","year":"1950"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2450","series-title":"Continuity and Effectiveness in Topoi.","author":"Rosolini.","year":"1986"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2455","doi-asserted-by":"crossref","first-page":"127","DOI":"10.2307\/1968669","article-title":"A mathematical logic without variables, Part 1","volume":"36","author":"Rosser","year":"1935","journal-title":"Annals of Mathematics, Series 2"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2460","doi-asserted-by":"crossref","first-page":"18","DOI":"10.2307\/2267551","article-title":"New sets of postulates for combinatory logics","volume":"7","author":"Rosser.","year":"1942","journal-title":"Journal of Symbolic Logic,"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2465","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1109\/MAHC.1984.10040","article-title":"Highlights of the history of the lambda calculus","volume":"6","author":"Rosser.","year":"1984","journal-title":"Annals of the History of Computing,"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2470","series-title":"Principia Mathematica.","first-page":"1925","author":"Russell","year":"1913"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2475","series-title":"The Principles of Mathematics","author":"Russell","year":"1903"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2480","series-title":"Introduction to Mathematical Philosophy","author":"Russell","year":"1919"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2485","series-title":"Automata, Languages and Programming, Fifth Colloquium","first-page":"398","article-title":"Une extension de la theorie des types en A-calcul","author":"Salle","year":"1978"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2490","series-title":"Mathematical Logic and its Applications","first-page":"187","article-title":"Intuitionistic formal spaces: a first communication","author":"Sambin","year":"1987"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2495","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1305\/ndjfl\/1093956080","article-title":"Functionals defined by recursion","volume":"8","author":"Sanchis","year":"1967","journal-title":"Notre Dame Journal of Formal Logic"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2500","series-title":"Mathematical Foundations of Computer Science","first-page":"517","article-title":"Degrees of parallelism in computations","author":"Sazonov","year":"1976"},{"issue":"3","key":"10.1016\/S1874-5857(09)70018-4_bb2505","doi-asserted-by":"crossref","first-page":"308","DOI":"10.1007\/BF01876321","article-title":"Expressibility of functionals in D. Scott's LCF language","volume":"15","author":"Sazonov","year":"1976","journal-title":"Algebra i Logika"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2510","first-page":"648","article-title":"Functionals computable in series and in parallel","volume":"17","author":"Sazonov","year":"1976","journal-title":"Sibirskii Matematicheskii Zhurnal"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2515","doi-asserted-by":"crossref","first-page":"305","DOI":"10.1007\/BF01448013","article-title":"Uber die Bausteine der mathematischen Logik","volume":"92","author":"Schonfinkel","year":"1924","journal-title":"Mathematische Annalen"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2520","article-title":"Vorlesungen uber die Algebra der Logik (Exakte Logik)","author":"Schroder","year":"1905","journal-title":"Teubner, Leipzig, Germany"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2525","unstructured":"The Church-Rosser Theorem. PhD thesis, Cornell Univ., 1965. Informally circulated 1963. 673 pp. Obtainable from University Microfilms Inc., Ann Arbor, Michigan, U.S.A., Publication No. 66-41."},{"key":"10.1016\/S1874-5857(09)70018-4_bb2530","doi-asserted-by":"crossref","first-page":"305","DOI":"10.2307\/2963525","article-title":"Syntactical and semantical properties of simple type theory","volume":"25","author":"Schuotte","year":"1960","journal-title":"Journal of Symbolic Logic"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2535","unstructured":"D. S. Scott. A System of Functional Abstraction, 1963. Lecture notes, Stanford Univ., informally distributed."},{"key":"10.1016\/S1874-5857(09)70018-4_bb2540","series-title":"An Abstract Theory of Constructions","author":"Scott","year":"1968"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2545","unstructured":"D. S. Scott. A construction of a model for the A-calculus. Informally distributed, 1969. Notes for a November 1969 seminar, Oxford Univ."},{"key":"10.1016\/S1874-5857(09)70018-4_bb2550","series-title":"Lattice-theoretic models for the A-calculus","first-page":"50","author":"Scott","year":"1969"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2555","series-title":"Models for the A-calculus","author":"Scott","year":"1969"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2560","series-title":"A theory of computable functions of higher type","author":"Scott","year":"1969"},{"issue":"1-2","key":"10.1016\/S1874-5857(09)70018-4_bb2565","first-page":"411","article-title":"A type-theoretical alternative to ISWIM, CUCH, OWHY","volume":"121","author":"Scott","year":"1969","journal-title":"Dated October 1969. Publ. with additions by author in Theoretical Computer Science"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2570","first-page":"237","article-title":"Constructive validity","volume":"125","author":"Scott","year":"1970"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2575","series-title":"Formal Semantics of Programming Languages","first-page":"65","article-title":"Lattice theory, data types and semantics","author":"Scott","year":"1970"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2580","first-page":"169","article-title":"Outline of a mathematical theory of computation","author":"Scott","year":"1970","journal-title":"In Proceedings of the Fourth Annual Princeton Conference on Information Sciences and Systems"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2585","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0073967","article-title":"Continuous lattices","author":"Scott","year":"1972"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2590","series-title":"Logic, Methodology and Philosophy of Science IV","first-page":"157","article-title":"Models for various type-free calculi","author":"Scott","year":"1973"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2595","doi-asserted-by":"crossref","unstructured":"D.S. Scott Some philosophical issues concerning theories of combinators. In Bohm [1975], pages 346-366.","DOI":"10.1007\/BFb0029537"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2600","doi-asserted-by":"crossref","first-page":"522","DOI":"10.1137\/0205037","article-title":"Data types as lattices","volume":"5","author":"Scott","year":"1976","journal-title":"SIAM Journal on Computing,"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2605","doi-asserted-by":"crossref","first-page":"634","DOI":"10.1145\/359810.359826","article-title":"Logic and programming languages","volume":"20","author":"Scott","year":"1977","journal-title":"Communications of the ACM,"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2610","series-title":"The Kleene Symposium","first-page":"223","article-title":"Lambda calculus: some models, some philosophy","author":"Scott","year":"1980"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2615","unstructured":"D. S. Scott. Relating theories of the A-calculus. In Hindley and Seldin [1980],pages 403-450."},{"key":"10.1016\/S1874-5857(09)70018-4_bb2620","first-page":"577","article-title":"Domains for denotational semantics","author":"Scott","year":"1982"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2625","series-title":"Theoretical Foundations of Programming Methodology","article-title":"Lectures on a mathematical theory of computation","author":"Scott","year":"1982"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2630","unstructured":"D. S. Scott. Church's thesis and a unification of type universes. Lecture at conference in Utrecht on Church's Thesis fifty years later, 14-15 June 1986."},{"key":"10.1016\/S1874-5857(09)70018-4_bb2635","unstructured":"D. S. Scott. A new category? Domains, Spaces and Equivalence relations. Unpublished manuscript, December 1996."},{"key":"10.1016\/S1874-5857(09)70018-4_bb2640","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1023\/A:1010018211714","article-title":"Some reflections on Strachey and his work","volume":"13","author":"Scott","year":"2000","journal-title":"Higher order and Symbolic Computation"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2645","first-page":"371","article-title":"Linear logic, *-autonomous categories and cofree coalgebras","author":"Seely","year":"1989"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2650","series-title":"Studies in Illative Combinatory Logic","author":"Seldin","year":"1968"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2655","doi-asserted-by":"crossref","first-page":"29","DOI":"10.1016\/0003-4843(79)90020-2","article-title":"Progress report on generalized functionality","volume":"17","author":"Seldin","year":"1979","journal-title":"Annals of Mathematical Logic"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2660","unstructured":"[1980], pages 3-33."},{"key":"10.1016\/S1874-5857(09)70018-4_bb2665","unstructured":"J. P. Seldin. A short biography of Haskell B. Curry. In Hindley and Seldin [1980], pages vii-xx. Includes a bibliography"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2670","unstructured":". P. Seldin. MATHESIS: The mathematical foundation of ULYSSES. Technical Report RADC-TR-87-223, Odyssey Research Associates, Rome Air Development Center, Air Force Systems Command, Griffiss Air Force Base, NY 13441-5700, 1987."},{"key":"10.1016\/S1874-5857(09)70018-4_bb2675","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1016\/S0168-0072(96)00008-5","article-title":"On the proof theory of Coquand's calculus of constructions","volume":"83","author":"Seldin","year":"1997","journal-title":"Annals of Pure and Applied Logic"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2680","first-page":"148","article-title":"Curry's anticipation of the types used in programming languages","volume":"15","author":"Seldin","year":"2002","journal-title":"Proceedings of the Canadian Society for History and Philosophy of Mathematics"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2685","article-title":"Church and Curry: the lambda calculus and combinatory logic","volume":"5","author":"Seldin","year":"2008"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2690","doi-asserted-by":"crossref","first-page":"154","DOI":"10.2307\/421012","article-title":"Step by recursive step: Church's analysis of effective calculability","volume":"3","author":"Sieg","year":"1997","journal-title":"Bulletin of Symbolic Logic"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2695","first-page":"761","article-title":"The category-theoretic solution of recursive domain equations","volume":"11","author":"Smyth","year":"1982","journal-title":"S.I.A.M. Journal of Computing"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2700","doi-asserted-by":"crossref","first-page":"257","DOI":"10.1016\/0304-3975(77)90045-7","article-title":"Effectively given domains","volume":"5","author":"Smyth","year":"1977","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2705","first-page":"662","article-title":"Powerdomains and predicate transformers: a topological view","author":"Smyth","year":"1983"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2710","doi-asserted-by":"crossref","first-page":"391","DOI":"10.1002\/malq.19810272503","article-title":"Efficient combinatory reduction","volume":"27","author":"Staples","year":"1981","journal-title":"Zeitschrift fur Mathematische Logik,"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2715","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1007\/BF02023009","article-title":"\u03bb-definable functionals and \u03b2\u03b7conversion","volume":"23","author":"Statman","year":"1983","journal-title":"Archiv fur Mathematische Logik,"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2720","first-page":"85","article-title":"Logical relations and the typed \u03bbcalculus","volume":"65","author":"Statman","year":"1985","journal-title":"Information and Computation,"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2725","series-title":"History of Programming Languages-II","first-page":"233","article-title":"The evolution of LISP","author":"Steele","year":"1996"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2730","first-page":"256","article-title":"Trees and term rewriting in 1910: on a paper by Axel Thue","volume":"72","author":"Steinby","year":"2000","journal-title":"Bulletin of the European Association for Theoretical Computer Science,"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2735","series-title":"Combinators, \u00bb-terms and Proof Theory.","author":"Stenlund","year":"1972"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2740","series-title":"Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory.","author":"Stoy.","year":"1977"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2745","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1023\/A:1010026413531","article-title":"Continuations: a mathematical semantics for handling full jumps","volume":"13","author":"Strachey","year":"2000","journal-title":"Reprinted in Higher-Order and Symbolic Computation"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2750","first-page":"11","article-title":"Fundamental concepts in programming languages","volume":"13","author":"Strachey","year":"1967"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2755","series-title":"Handbook of Philosophical Logic, Volume III,","first-page":"471","article-title":"Proof theory and meaning","author":"Sundholm","year":"1986"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2760","doi-asserted-by":"crossref","first-page":"177","DOI":"10.1305\/ndjfl\/1093891297","article-title":"A categorical equivalence of proofs","volume":"15","author":"Szabo","year":"1974","journal-title":"Notre Dame Journal of Formal Logic"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2765","series-title":"Algebra of Proofs.","year":"1978"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2770","series-title":"Formal Systems and Recursive Functions","first-page":"176","article-title":"Infinitely long terms of transfinite type","author":"Tait","year":"1965"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2775","doi-asserted-by":"crossref","first-page":"980","DOI":"10.1090\/S0002-9904-1966-11611-7","article-title":"A nonconstructive proof of Gentzen's Haupsatz for second order predicate logic","volume":"72","author":"Tait","year":"1966","journal-title":"Bulletin of the American Math. Society,"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2780","doi-asserted-by":"crossref","first-page":"198","DOI":"10.2307\/2271658","article-title":"Intensional interpretations of functionals of finite type","volume":"32","author":"Tait","year":"1967","journal-title":"Journal of Symbolic Logic"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2785","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1093\/philmat\/9.1.87","article-title":"Godel's unpublished papers on foundations of mathematics","volume":"9","author":"Tait","year":"2001","journal-title":"Philo- sophiae Mathematica"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2790","doi-asserted-by":"crossref","first-page":"751","DOI":"10.2178\/jsl\/1058448436","article-title":"The completeness of Heyting first-order logic","volume":"68","author":"Tait","year":"2003","journal-title":"Journal of Symbolic Logic"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2795","doi-asserted-by":"crossref","first-page":"399","DOI":"10.2969\/jmsj\/01940399","article-title":"A proof of cut-elimination in simple type-theory","volume":"19","author":"Takahashi","year":"1967","journal-title":"Journal of the Mathematical Society of Japan"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2800","doi-asserted-by":"crossref","first-page":"113","DOI":"10.1016\/S0747-7171(89)80045-8","article-title":"Parallel reductions in \u03bb-calculus","volume":"7","author":"Takahashi","year":"1989","journal-title":"Journal of Symbolic Computation"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2805","series-title":"Theory of Computation, Computability and Lambdacalculus.","author":"Takahashi","year":"1991"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2810","doi-asserted-by":"crossref","first-page":"39","DOI":"10.4099\/jjm1924.23.0_39","article-title":"On a generalised logical calculus","volume":"23","author":"Takeuti","year":"1953","journal-title":"Japanese Journal of Mathematics"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2815","series-title":"A Formalization of Set Theory Without Variables","author":"Tarski","year":"1987"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2820","doi-asserted-by":"crossref","first-page":"73","DOI":"10.2307\/2268577","article-title":"On the calculus of relations","volume":"6","author":"Tarski","year":"1941","journal-title":"Journal of Symbolic Logic"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2825","first-page":"189","article-title":"A formalization of set theory without variables","volume":"18","author":"Tarski","year":"1953","journal-title":"Journal of Symbolic Logic"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2830","series-title":"Proceedings Sixth Annual IEEE Symposium on Logic In Computer Science","first-page":"152","article-title":"The fixed point property in synthetic domain theory","author":"Taylor","year":"1991"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2835","series-title":"Term Rewriting Systems","author":"Terese","year":"2003"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2840","series-title":"Enzyklopadie Philosophic und Wissenschaftstheorie","first-page":"726","article-title":"Schonfinkel, Moses","author":"Thiel","year":"1995"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2845","article-title":"Die Losung eines Spezialfalles eines generellen logischen Problems","volume":"8","author":"Thue","year":"1910","journal-title":"Cris- tiania Videnskabsselskabs Skrifter. I. Mat.-Nat. Kl. 1910"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2850","first-page":"105","article-title":"Type inference problems: a survey","author":"Tiuryn","year":"1990"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2855","year":"1973"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2860","first-page":"230","article-title":"On computable numbers, with an application to the Entschei- dungsproblem","volume":"42","author":"Turing","year":"1936","journal-title":"Proceedings of the London Mathematical Society, Series 2"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2865","doi-asserted-by":"crossref","first-page":"153","DOI":"10.2307\/2268280","article-title":"Computability and A-definability","volume":"2","author":"Turing","year":"1937","journal-title":"Journal of Symbolic Logic"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2870","doi-asserted-by":"crossref","first-page":"164","DOI":"10.2307\/2268281","article-title":"The p-function in A -K-conversion","volume":"2","author":"Turing","year":"1937","journal-title":"Journal of Symbolic Logic"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2875","unstructured":"A. M. Turing. Proof that every typed formula has a normal form. Manuscript undated but probably 1941 or '42. Publ. in An early proof of normalization by A. M. Turing by R. O. Gandy, in [Hindley and Seldin, 1980], pages 453-455, 1980."},{"key":"10.1016\/S1874-5857(09)70018-4_bb2880","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1002\/spe.4380090105","article-title":"A new implementation technique for applicative languages","volume":"9","author":"Turner","year":"1979","journal-title":"Software - Practice and Experience"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2885","first-page":"773","article-title":"On enumeration operators","volume":"103","author":"Uspenskii","year":"1955","journal-title":"Doklady Akademii Nauk S.S.S.R."},{"key":"10.1016\/S1874-5857(09)70018-4_bb2890","series-title":"Topology via Logic","author":"Vickers","year":"1989"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2895","doi-asserted-by":"crossref","first-page":"339","DOI":"10.2307\/2274219","article-title":"A direct proof of the finite developments theorem","volume":"50","author":"de Vrijer","year":"1985","journal-title":"Journal of Symbolic Logic"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2900","doi-asserted-by":"crossref","first-page":"332","DOI":"10.1016\/S0022-0000(74)80048-6","article-title":"Correct and optimal implementations of recursion in a simple programming language","volume":"9","author":"Vuillemin","year":"1974","journal-title":"Journal of Computer and System Science"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2905","series-title":"Syntaxe, s\u00e9mantique et axiomatique d'un langage de program- mation simple","author":"Vuillemin","year":"1974"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2910","unstructured":"C. P.Wadsworth Semantics and pragmatics of the lambda-calculus Univ. PhD thesis Oxford England 1971"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2915","doi-asserted-by":"crossref","first-page":"488","DOI":"10.1137\/0205036","article-title":"The relation between computational and denotational properties for Scott's D \u221emodels of the lambda-calculus","volume":"5","author":"Wadsworth","year":"1976","journal-title":"SIAM Journal of Computing"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2920","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1137\/0207028","article-title":"Approximate reduction and lambda-calculus models","volume":"7","author":"Wadsworth","year":"1978","journal-title":"SIAM Journal of Computing"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2925","unstructured":"C. P. Wadsworth. Some unusual \u03bb-calculus numeral systems. In Hindley and Seldin [1980], pages 215-230."},{"key":"10.1016\/S1874-5857(09)70018-4_bb2930","doi-asserted-by":"crossref","first-page":"131","DOI":"10.1023\/A:1010074329461","article-title":"Continuations revisited","volume":"13","author":"Wadsworth","year":"2000","journal-title":"Higher-Order and Symbolic Computation"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2935","first-page":"214","article-title":"On the recursive specification of data types","author":"Wand","year":"1974"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2940","series-title":"Fixed-point constructions in order-enriched categories. Technical Report 23","author":"Wand","year":"1977"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2945","doi-asserted-by":"crossref","first-page":"13","DOI":"10.1016\/0304-3975(79)90053-7","article-title":"Fixed-point constructions in order-enriched categories","volume":"8","author":"Wand","year":"1979","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2950","doi-asserted-by":"crossref","first-page":"115","DOI":"10.3233\/FI-1987-10202","article-title":"A simple algorithm and proof for type inference","volume":"10","author":"Wand","year":"1987","journal-title":"Fundamenta Informaticae"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2955","doi-asserted-by":"crossref","unstructured":"P. H. Welch. Continuous semantics and inside-out reductions. In B\u00f6hm [1975], pages 122-146.","DOI":"10.1007\/BFb0029522"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2960","series-title":"Proceedings Ninth Annual IEEE Symposium on Logic In Computer Science","first-page":"176","article-title":"Typability and type checking in the second-order lambda-calculus are equivalent and undecidable","author":"Wells","year":"1994"},{"issue":"1-3","key":"10.1016\/S1874-5857(09)70018-4_bb2965","doi-asserted-by":"crossref","first-page":"111","DOI":"10.1016\/S0168-0072(98)00047-5","article-title":"Typability and type checking in System F are equivalent and unde- cidable","volume":"98","author":"Wells","year":"1999","journal-title":"Annals of Pure and Applied Logic"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2970","series-title":"Sharp upper bounds for the depths of reduction trees of typed \u03bb-calculus with recursors","author":"Wilken","year":"1997"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2975","series-title":"Methods and Means for Computation with Objects","author":"Wolfengagen","year":"2004"},{"key":"10.1016\/S1874-5857(09)70018-4_bb2980","series-title":"Matematika v SSSR za Tridkat let 1917-1947","first-page":"9","article-title":"Osnovaniya matematiki i matematicheskaya logika","author":"Yanovskaya","year":"1948"}],"container-title":["Handbook of the History of Logic","Logic from Russell to Church"],"original-title":[],"link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1874585709700184?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1874585709700184?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2023,5,25]],"date-time":"2023-05-25T21:14:23Z","timestamp":1685049263000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1874585709700184"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9780444516206"],"references-count":592,"URL":"https:\/\/doi.org\/10.1016\/s1874-5857(09)70018-4","relation":{},"ISSN":["1874-5857"],"issn-type":[{"value":"1874-5857","type":"print"}],"subject":[],"published":{"date-parts":[[2009]]}}}