{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,3,29]],"date-time":"2022-03-29T02:18:07Z","timestamp":1648520287328},"reference-count":126,"publisher":"Elsevier BV","issue":"3","license":[{"start":{"date-parts":[[1985,9,1]],"date-time":"1985-09-01T00:00:00Z","timestamp":494380800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,17]],"date-time":"2013-07-17T00:00:00Z","timestamp":1374019200000},"content-version":"vor","delay-in-days":10181,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Journal of Symbolic Computation"],"published-print":{"date-parts":[[1985,9]]},"DOI":"10.1016\/s0747-7171(85)80040-7","type":"journal-article","created":{"date-parts":[[2008,4,9]],"date-time":"2008-04-09T14:00:48Z","timestamp":1207749648000},"page":"323-328","source":"Crossref","is-referenced-by-count":1,"title":["A Selected Bibliography on Constructive Mathematics, Intuitionistic Type Theory and Higher Order Deduction"],"prefix":"10.1016","volume":"1","author":[{"given":"Thierry","family":"Coquand","sequence":"first","affiliation":[]},{"given":"G\u00e9rard","family":"Huet","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/S0747-7171(85)80040-7_bib1","series-title":"Transfinite Type Theory","author":"Andrews","year":"1965"},{"key":"10.1016\/S0747-7171(85)80040-7_bib2","doi-asserted-by":"crossref","first-page":"414","DOI":"10.2307\/2269949","article-title":"Resolution in Type Theory","volume":"3","author":"Andrews","year":"1971","journal-title":"J. Symbolic Logic 36,"},{"key":"10.1016\/S0747-7171(85)80040-7_bib3","series-title":"Dept of Math","article-title":"Automating higher-order logic","author":"Andrews","year":"1983"},{"key":"10.1016\/S0747-7171(85)80040-7_bib4","series-title":"Algorithm development in Martin-L\u00f6f's type theory","author":"Backhouse","year":"1984"},{"key":"10.1016\/S0747-7171(85)80040-7_bib5","series-title":"The while-rule in Martin-L\u00f6fs theory of types","author":"Backhouse","year":"1984"},{"key":"10.1016\/S0747-7171(85)80040-7_bib6","series-title":"The Lambda-Calculus: Its Syntax and Semantics","author":"Barendregt","year":"1980"},{"key":"10.1016\/S0747-7171(85)80040-7_bib7","series-title":"Fibered categories and the foundations of naive category theory","author":"Benabou","year":"1983"},{"key":"10.1016\/S0747-7171(85)80040-7_bib8","series-title":"Foundations of Constructive Analysis","author":"Bishop","year":"1967"},{"key":"10.1016\/S0747-7171(85)80040-7_bib9","series-title":"Intuitionism and Proof Theory","first-page":"53","article-title":"Mathematics as a numerical language","author":"Bishop","year":"1970"},{"key":"10.1016\/S0747-7171(85)80040-7_bib10","series-title":"Toward an Automatic Synthesis of Polyrnorphic Typed Lambda Terms","author":"B\u00f6hm","year":"1983"},{"key":"10.1016\/S0747-7171(85)80040-7_bib11","series-title":"Automatic Synthesis of Typed Lambda-Programs on Term Algebras","author":"B\u00f6hm","year":"1984"},{"key":"10.1016\/S0747-7171(85)80040-7_bib12","series-title":"5th International Joint Conference on Artificial Intelligence","first-page":"511","article-title":"A Lemma Driven Automatic Theorem Prover for Recursive Function Theory","author":"Boyer","year":"1977"},{"key":"10.1016\/S0747-7171(85)80040-7_bib13","doi-asserted-by":"crossref","first-page":"129","DOI":"10.1145\/321864.321875","article-title":"Proving Theorems About LISP Functions","volume":"22","author":"Boyer","year":"1975","journal-title":"J. Assoc. Comp. Mach."},{"key":"10.1016\/S0747-7171(85)80040-7_bib14","series-title":"Report ICSCA-CMP-28, Institute for Computing Science\u2014University of Texas at Austin","article-title":"A mechanical proof of the unsolvability of the halting problem","author":"Boyer","year":"1982"},{"key":"10.1016\/S0747-7171(85)80040-7_bib15","series-title":"Report ICSCA-CMP-33, Institute for Computing Science\u2014University of Texas at Austin","article-title":"Proof Checking the RSA Public Key Encryption Algorithm","author":"Boyer","year":"1982"},{"key":"10.1016\/S0747-7171(85)80040-7_bib16","series-title":"Report ICSA-CMP-35, Institute for Computing Science\u2014University of Texas at Austin","article-title":"Proof checking theorem proving and program verification","author":"Boyer","year":"1983"},{"key":"10.1016\/S0747-7171(85)80040-7_bib17","series-title":"Institute for Computing Science\u2014University of Texas at Austin","article-title":"A mechanical proof of the Turing completeness of pure LISP.","author":"Boyer","year":"1983"},{"key":"10.1016\/S0747-7171(85)80040-7_bib18","doi-asserted-by":"crossref","first-page":"29","DOI":"10.1007\/BFb0060623","article-title":"The mathematical language AUTOMATH, its usage and some of its extensions","volume":"125","author":"de Bruijn","year":"1968","journal-title":"Symposium on Automatic Demonstration, IRIA, Versailles. Springer Lee. Notes Math."},{"key":"10.1016\/S0747-7171(85)80040-7_bib19","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, with Application to the Church-Rosser Theorem","volume":"5","author":"de Bruijn","year":"1972","journal-title":"Indag. Math. 34,"},{"key":"10.1016\/S0747-7171(85)80040-7_bib20","series-title":"Montr\u00e9al: Les Presses de I'Universite de Montr\u00e9al","article-title":"Automath a language for mathematics","author":"de Bruijn","year":"1973"},{"key":"10.1016\/S0747-7171(85)80040-7_bib21","series-title":"Essays on Combinatory Logic, Lambda Calculus and Formalism","article-title":"A survey of the project Automath","author":"de Bruijn","year":"1980"},{"key":"10.1016\/S0747-7171(85)80040-7_bib22","series-title":"Formalization of constructivity in Automath","author":"de Bruijn","year":"1984"},{"key":"10.1016\/S0747-7171(85)80040-7_bib23","first-page":"33","article-title":"A set of postulates for the foundation of logic","author":"Church","year":"1932","journal-title":"Ann. Math."},{"key":"10.1016\/S0747-7171(85)80040-7_bib24","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":"J. Symbolic Logic"},{"key":"10.1016\/S0747-7171(85)80040-7_bib25","series-title":"The Calculi of Lambda-Conversion","author":"Church","year":"1941"},{"key":"10.1016\/S0747-7171(85)80040-7_bib26","series-title":"Proofs as Programs","author":"Constable","year":"1983"},{"key":"10.1016\/S0747-7171(85)80040-7_bib27","series-title":"The Nearly Ultimate Pearl","author":"Constable","year":"1983"},{"key":"10.1016\/S0747-7171(85)80040-7_bib28","series-title":"Writing Programs that Construct Proofs","author":"Constable","year":"1985"},{"key":"10.1016\/S0747-7171(85)80040-7_bib29","series-title":"Writing Programs that Construct Proofs","author":"Constable","year":"1984"},{"key":"10.1016\/S0747-7171(85)80040-7_bib30","series-title":"Une theorie des constructions","author":"Coquand","year":"1985"},{"key":"10.1016\/S0747-7171(85)80040-7_bib31","series-title":"Preliminary version, presented at the International Symposium on Semantics of Data Types, Sophia-Antipolis","article-title":"A Theory of Constructions","author":"Coquand","year":"1984"},{"key":"10.1016\/S0747-7171(85)80040-7_bib32","series-title":"Eurocal 85, Linz, Austria. Springer Lee. Notes Comp. Sci.","article-title":"Constructions: A Higher Order Proof System for Mechanizing Mathematics","author":"Coquand","year":"1985"},{"key":"10.1016\/S0747-7171(85)80040-7_bib33","series-title":"Combinatory Logic Vol. 1","author":"Curry","year":"1958"},{"key":"10.1016\/S0747-7171(85)80040-7_bib34","article-title":"A description of AUTOMATH and some aspects of its language theory","volume":"1","author":"Van Daalen","year":"1973"},{"key":"10.1016\/S0747-7171(85)80040-7_bib35","series-title":"PhD Dissertation","article-title":"The language theory of Automath","author":"Van Daalen","year":"1980"},{"key":"10.1016\/S0747-7171(85)80040-7_bib36","series-title":"Principal type-schemas for functional programs","author":"Damas","year":"1982"},{"key":"10.1016\/S0747-7171(85)80040-7_bib37","series-title":"Elements of Intuitionism","author":"Dummet","year":"1977"},{"key":"10.1016\/S0747-7171(85)80040-7_bib38","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1145\/322358.322370","article-title":"The expressiveness of simple and second-order type structures","volume":"1","author":"Fortuhe","year":"1983","journal-title":"J. Assoc. Comp. Mach. 30,"},{"key":"10.1016\/S0747-7171(85)80040-7_bib39","series-title":"Begriffvchrift, a formula language, modeled upon that of arithmetic, for pure thought.","author":"Frege","year":"1879"},{"key":"10.1016\/S0747-7171(85)80040-7_bib40","article-title":"\u00dcber eine bisher noch nicht ben\u00fctzte Erweiterung des finiten Standpunktes","volume":"12","author":"G\u00f6del","year":"1958"},{"key":"10.1016\/S0747-7171(85)80040-7_bib41","series-title":"The Collected Papers of Gerhard Gentzen","author":"Gentzen","year":"1964"},{"key":"10.1016\/S0747-7171(85)80040-7_bib42","series-title":"Proceedings of the Second Scandinavian Logic Symposium","article-title":"Une extension de !'interpretation de G\u00f6del \u00e0 l'analyse, et son application \u00e0 l'\u00e9limination des coupures Bans l'analyse et la th\u00e9orie des types","author":"Girard","year":"1970"},{"key":"10.1016\/S0747-7171(85)80040-7_bib43","series-title":"Interpr\u00e9tation fonctionnelle et \u00e9limination des coupures dans I'arithm\u00e9tique d'ordre superieure","author":"Girard","year":"1972"},{"key":"10.1016\/S0747-7171(85)80040-7_bib44","series-title":"Proof theory & logical complexity","author":"Girard","year":"1984"},{"key":"10.1016\/S0747-7171(85)80040-7_bib45","series-title":"Automatic Construction of Special Purpose Programs","author":"Goad","year":"1980"},{"key":"10.1016\/S0747-7171(85)80040-7_bib46","series-title":"ARPA image understanding workshop","article-title":"Special purpose automatic programming for 3D model-based vision","author":"Goad","year":"1983"},{"key":"10.1016\/S0747-7171(85)80040-7_bib47","series-title":"Ph.D. thesis","article-title":"Computational Uses of the Manipulation of Formal Proofs","author":"Goad","year":"1980"},{"key":"10.1016\/S0747-7171(85)80040-7_bib48","first-page":"225","article-title":"The Undecidability of the Second-order Unification Problem","volume":"13","author":"Goldfarb","year":"1981"},{"key":"10.1016\/S0747-7171(85)80040-7_bib49","series-title":"Internal Report CSR-16-77","article-title":"A Metalanguage for Interactive Proof in LCF","author":"Gordon","year":"1977"},{"key":"10.1016\/S0747-7171(85)80040-7_bib50","series-title":"Edinburgh LCF. Springer Lee. Notes Comp. Sci. 78.","author":"Gordon","year":"1979"},{"key":"10.1016\/S0747-7171(85)80040-7_bib51","series-title":"Program Synthesis from Natural Deduction Proofs","article-title":"Proceedings International Joint Conference on Artificial Intelligence. Tokyo","author":"Goto","year":"1979"},{"key":"10.1016\/S0747-7171(85)80040-7_bib52","first-page":"3250","article-title":"A Matching Procedure for Omega Order Logic","volume":"628","author":"Gould","year":"1966","journal-title":"Scientific Report 1, AFCRL 66-781, contract AF19"},{"key":"10.1016\/S0747-7171(85)80040-7_bib53","series-title":"Scientific Report 1, AFCRL","article-title":"Automated Logic, for Semi-Automated Mathematics","author":"Guard","year":"1964"},{"key":"10.1016\/S0747-7171(85)80040-7_bib54","series-title":"SIAM Comput. J.","article-title":"Foundation of Logic Programming Based on Inductive Definition","author":"Hagiya","year":"1984"},{"key":"10.1016\/S0747-7171(85)80040-7_bib55","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":"J. Symbolic Logic"},{"key":"10.1016\/S0747-7171(85)80040-7_bib56","series-title":"Recherches sur la th\u00e9orie de la d\u00e9monstration","author":"Herbrand","year":"1930"},{"key":"10.1016\/S0747-7171(85)80040-7_bib57","first-page":"29","article-title":"The principal type scheme of an object in combinatory logic","volume":"146","author":"Hindley","year":"1979","journal-title":"Trans Amer. Math. Soc."},{"key":"10.1016\/S0747-7171(85)80040-7_bib58","series-title":"Introduction to Combinatory Logic","author":"Hindley","year":"1972"},{"key":"10.1016\/S0747-7171(85)80040-7_bib59","series-title":"The formulae-as-types notion of construction","author":"Howard","year":"1969"},{"key":"10.1016\/S0747-7171(85)80040-7_bib60","series-title":"PhD Thesis, Jennings Computing Center Report 1117","article-title":"Constrained Resolution: a Complete Method for Type Theory","author":"Huet","year":"1972"},{"key":"10.1016\/S0747-7171(85)80040-7_bib61","series-title":"Proceedings, 3rd IJCAI. Stanford","article-title":"A Mechanization of Type Theory","author":"Huet","year":"1973"},{"key":"10.1016\/S0747-7171(85)80040-7_bib62","doi-asserted-by":"crossref","first-page":"257","DOI":"10.1016\/S0019-9958(73)90301-X","article-title":"The Undecidability of Unification in Third Order Logic","volume":"22","author":"Huet","year":"1973","journal-title":"Inf. Control"},{"key":"10.1016\/S0747-7171(85)80040-7_bib63","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1016\/0304-3975(75)90011-0","article-title":"A Unification Algorithm for Typed Lambda Calculus","volume":"1.1","author":"Huet","year":"1975","journal-title":"Theor. Comp. Sci."},{"key":"10.1016\/S0747-7171(85)80040-7_bib64","series-title":"Resolution d'\u00e9quations dans des langages d'ordre 1, 2, ... omega","author":"Huet","year":"1976"},{"key":"10.1016\/S0747-7171(85)80040-7_bib65","series-title":"A translation of Landau's \"Grundlagen\" in AUTO MATH","author":"Jutting","year":"1976"},{"key":"10.1016\/S0747-7171(85)80040-7_bib66","series-title":"The language theory of A, a lambda-calculus where terms are types","author":"Jutting","year":"1984"},{"key":"10.1016\/S0747-7171(85)80040-7_bib67","series-title":"A mechanical proof of Ramsey theorem","author":"Ketonen","year":"1983"},{"key":"10.1016\/S0747-7171(85)80040-7_bib68","first-page":"65","volume":"170","author":"Ketonen","year":"1984"},{"key":"10.1016\/S0747-7171(85)80040-7_bib69","series-title":"The language of an interactive proof' checker","author":"Ketonen","year":"1984"},{"key":"10.1016\/S0747-7171(85)80040-7_bib70","first-page":"109","article-title":"On the interpretation of intuitionistic number theory","volume":"31","author":"Kleene","year":"1945"},{"key":"10.1016\/S0747-7171(85)80040-7_bib71","first-page":"000","article-title":"On the interpretation of nonfinitist proofs, Part I, II","volume":"16","author":"Kreisel","year":"1952","journal-title":"J. Symbolic Logic"},{"key":"10.1016\/S0747-7171(85)80040-7_bib72","first-page":"123","article-title":"Some Uses of Proof Theory for Finding Computer Programs","volume":"249","author":"Kreisel","year":"1975"},{"key":"10.1016\/S0747-7171(85)80040-7_bib73","series-title":"Finiteness Theorems in Arithmetic","author":"Kreisel","year":"1982"},{"key":"10.1016\/S0747-7171(85)80040-7_bib74","series-title":"Reductions correctes et optimales dans le lambda-calcul","author":"Levy","year":"1978"},{"key":"10.1016\/S0747-7171(85)80040-7_bib75","series-title":"Polymorphic type inference","author":"Leivant","year":"1983"},{"key":"10.1016\/S0747-7171(85)80040-7_bib76","series-title":"Reasoning about functional programs and complexity classes associated with type disciplines","first-page":"460","author":"Leivant","year":"1983"},{"key":"10.1016\/S0747-7171(85)80040-7_bib77","series-title":"Structural semantics for polymorphic data types","author":"Leivant","year":"1983"},{"key":"10.1016\/S0747-7171(85)80040-7_bib78","series-title":"PhD Thesis","article-title":"An investigation of a programming language with a polymor phic type structure","author":"McCracken","year":"1979"},{"key":"10.1016\/S0747-7171(85)80040-7_bib79","series-title":"A theory of types","author":"Martin-L\u00f6f","year":"1971"},{"key":"10.1016\/S0747-7171(85)80040-7_bib80","series-title":"Paper read at the Orleans Logic Conference.","article-title":"About models for intuitionistic type theories and the notion of defznitional equality","author":"Martin-L\u00f6f","year":"1972"},{"key":"10.1016\/S0747-7171(85)80040-7_bib81","first-page":"73","article-title":"An intuitionistic Theory of Types: predicative part","volume":"73","author":"Martin-L\u00f6f","year":"1974"},{"key":"10.1016\/S0747-7171(85)80040-7_bib82","first-page":"153","article-title":"Constructive Mathematics and Computer Programming. Logic","volume":"VI","author":"Martin-L\u00f6f","year":"1980"},{"key":"10.1016\/S0747-7171(85)80040-7_bib83","series-title":"Studies in Proof Theory, Bibliopolis","article-title":"Intuitionistic Type Theory","author":"Martin L\u00f6f","year":"1984"},{"key":"10.1016\/S0747-7171(85)80040-7_bib84","series-title":"PhD Dissertation","article-title":"Proofs in Higher-order Logic","author":"Miller","year":"1983"},{"key":"10.1016\/S0747-7171(85)80040-7_bib85","series-title":"Pennsylvania: Technical report MS-CIS-84-6","article-title":"Expansion tree proofs and their conversion to natural deduction proofs","author":"Miller","year":"1984"},{"key":"10.1016\/S0747-7171(85)80040-7_bib86","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":"J. Comp. Syst. Sci."},{"key":"10.1016\/S0747-7171(85)80040-7_bib87","doi-asserted-by":"crossref","first-page":"501","DOI":"10.1007\/BF01084980","article-title":"E-Theorems","volume":"7","author":"Mints","year":"1977","journal-title":"J. Soviet Math."},{"key":"10.1016\/S0747-7171(85)80040-7_bib88","series-title":"PhD Thesis, Eindhoven University of Technology","article-title":"Strong normalization in a typed lambda calculus with lambda structured types","author":"Nederpelt","year":"1973"},{"key":"10.1016\/S0747-7171(85)80040-7_bib89","first-page":"182","article-title":"An approach to theorem proving on the basis of a typed lambda-calculus","volume":"87","author":"Nederpelt","year":"1980","journal-title":"5th Conference on Automated Deduction, Les Arcs, France. Springer Lec. Notes Comp. Sci."},{"key":"10.1016\/S0747-7171(85)80040-7_bib90","series-title":"Programming in Constructive Set Theory: Some Examples","first-page":"141","author":"Nordstr\u00f6m","year":"1981"},{"key":"10.1016\/S0747-7171(85)80040-7_bib91","first-page":"915","article-title":"Types and Specifications","volume":"83","author":"Nordstr\u00f6m","year":"1983"},{"key":"10.1016\/S0747-7171(85)80040-7_bib92","doi-asserted-by":"crossref","first-page":"288","DOI":"10.1007\/BF02136027","article-title":"Propositions and Specifications of Programs in Martin-Lof s Type Theory","volume":"24","author":"Nordstrom","year":"1984","journal-title":"BIT"},{"key":"10.1016\/S0747-7171(85)80040-7_bib93","series-title":"Examples of structural induction","article-title":"Recent Developments in LCF","author":"Paulson","year":"1983"},{"key":"10.1016\/S0747-7171(85)80040-7_bib94","series-title":"Tactics and Tacticals in Cambridge LCF","author":"Paulson","year":"1983"},{"key":"10.1016\/S0747-7171(85)80040-7_bib95","series-title":"Verifying the unification algorithm in LCF","author":"Paulson","year":"1984"},{"key":"10.1016\/S0747-7171(85)80040-7_bib96","series-title":"Constructing Recursion Operators in Intuitionistic Type Theory","author":"Paulson","year":"1984"},{"key":"10.1016\/S0747-7171(85)80040-7_bib97","series-title":"A complete mechanization of w-order type theory","author":"Pietrzykowski","year":"1972"},{"key":"10.1016\/S0747-7171(85)80040-7_bib98","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1145\/321752.321764","article-title":"A Complete Mechanization of Second-Order Type Theory","volume":"20","author":"Pietrzykowski","year":"1973","journal-title":"J. Assoc. Comp. Mach."},{"key":"10.1016\/S0747-7171(85)80040-7_bib99","series-title":"IRIA Colloquium on Proving and Improving Programs, Arc et Senans, France.","article-title":"LCF considered as a programming language","author":"Plotkin","year":"1975"},{"key":"10.1016\/S0747-7171(85)80040-7_bib100","series-title":"Natural Deduction","author":"Prawitz","year":"1965"},{"key":"10.1016\/S0747-7171(85)80040-7_bib101","series-title":"Ideas and results in proof theory","author":"Prawitz","year":"1971"},{"key":"10.1016\/S0747-7171(85)80040-7_bib102","series-title":"Definitional Interpreters for Higher Order Programming Languages","first-page":"717","author":"Reynolds","year":"1972"},{"key":"10.1016\/S0747-7171(85)80040-7_bib103","first-page":"408","article-title":"Towards a Theory of Type Structure","volume":"19","author":"Reynolds","year":"1974","journal-title":"Programming Symposium, Paris. Springer Lee, Notes Comp. Sci."},{"key":"10.1016\/S0747-7171(85)80040-7_bib104","series-title":"Types, abstraction, and parametric polymorphism","author":"Reynolds","year":"1983"},{"key":"10.1016\/S0747-7171(85)80040-7_bib105","series-title":"International Symposium on Semantics of Data Types. Sophia-Antipolis","article-title":"Polymorphism is not set-theoretic","author":"Reynolds","year":"1984"},{"key":"10.1016\/S0747-7171(85)80040-7_bib106","series-title":"TAPSOFT Advanced Seminar on the Role of Semantics in Software Development","article-title":"Three approaches to type structure","author":"Reynolds","year":"1985"},{"key":"10.1016\/S0747-7171(85)80040-7_bib107","article-title":"Mechanizing Higher-Order Logic","volume":"4.","author":"Robinson","year":"1969"},{"key":"10.1016\/S0747-7171(85)80040-7_bib108","series-title":"Proceedings International Joint Conference on Artificial Intelligence","article-title":"Toward a Mathematical Theory of Program Synthesis","author":"Sato","year":"1979"},{"key":"10.1016\/S0747-7171(85)80040-7_bib109","first-page":"4","article-title":"Definierbare Funktionen im Lambda-Kalkiil mit Typen","volume":"173","author":"Schwichtenberg","year":"1975","journal-title":"Arch. Math. Logic"},{"key":"10.1016\/S0747-7171(85)80040-7_bib110","doi-asserted-by":"crossref","first-page":"237","DOI":"10.1007\/BFb0060636","article-title":"Constructive validity, Symposium on Automatic Demonstration","volume":"125","author":"Scott","year":"1970","journal-title":"Springer Lee. Notes Math."},{"key":"10.1016\/S0747-7171(85)80040-7_bib111","series-title":"Identity and Existence in Intuitionistic Logic","author":"Scott","year":"1975"},{"key":"10.1016\/S0747-7171(85)80040-7_bib112","series-title":"Reading, Mass: Addison-Wesley","article-title":"Mathematical Logic","author":"Shoenfield","year":"1967"},{"key":"10.1016\/S0747-7171(85)80040-7_bib113","series-title":"Course-of-values recursion oil lists in intuitionistic type theory","author":"Smith","year":"1981"},{"key":"10.1016\/S0747-7171(85)80040-7_bib114","first-page":"445","article-title":"The identification of propositions and types in Martin-LOf's type theory: a programming example","volume":"158","author":"Smith","year":"1983","journal-title":"International Conference on Foundations of Computation Theory, Borgholm, Sweden, Springer Lee. Notes Comp. Sci."},{"key":"10.1016\/S0747-7171(85)80040-7_bib115","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1016\/0304-3975(79)90006-9","article-title":"Intuitionistic Propositional Logic is Polynomial-space Complete","volume":"9","author":"Statman","year":"1979","journal-title":"Theor. Comp. Sci."},{"key":"10.1016\/S0747-7171(85)80040-7_bib116","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1016\/0304-3975(79)90007-0","article-title":"The typed Lambda-Calculus is not Elementary Recursive","volume":"9","author":"Statman","year":"1979","journal-title":"Theor. Comp. Sci."},{"key":"10.1016\/S0747-7171(85)80040-7_bib117","series-title":"Combinators lambda-terms, and proof theory","author":"Stenlund","year":"1972"},{"key":"10.1016\/S0747-7171(85)80040-7_bib118","first-page":"151","article-title":"Constructions, proofs and the meaning of the logical constants","volume":"12","author":"Sundholm","year":"1978","journal-title":"J. Philosophical Logic"},{"key":"10.1016\/S0747-7171(85)80040-7_bib119","series-title":"Algebra of proofs","author":"Szabo","year":"1978"},{"key":"10.1016\/S0747-7171(85)80040-7_bib120","doi-asserted-by":"crossref","first-page":"980","DOI":"10.1090\/S0002-9904-1966-11611-7","article-title":"A non constructive proof of Gentzen's Hauptsatz for second order predicate logic","volume":"72","author":"Tait","year":"1966","journal-title":"Bull. Amer. Math. Soc."},{"key":"10.1016\/S0747-7171(85)80040-7_bib121","doi-asserted-by":"crossref","first-page":"198","DOI":"10.2307\/2271658","article-title":"Intensional interpretation of functionals of finite type","volume":"32","author":"Tait","year":"1967","journal-title":"J. Symbolic Logic"},{"key":"10.1016\/S0747-7171(85)80040-7_bib122","doi-asserted-by":"crossref","first-page":"399","DOI":"10.2969\/jmsj\/01940399","article-title":"A proof of cut-elimination theorem in simple type theory","volume":"19","author":"Takahashi","year":"1967","journal-title":"J. Math. Soc. Japan"},{"key":"10.1016\/S0747-7171(85)80040-7_bib123","series-title":"Proofs and Programs","author":"Takasu","year":"1978"},{"key":"10.1016\/S0747-7171(85)80040-7_bib124","doi-asserted-by":"crossref","first-page":"39","DOI":"10.4099\/jjm1924.23.0_39","article-title":"On a generalized logic calculus","volume":"23","author":"Takeuti","year":"1953","journal-title":"Japan J. Math."},{"key":"10.1016\/S0747-7171(85)80040-7_bib125","series-title":"Handbook of Mathematical Logic","article-title":"Aspects of constructive mathematics","author":"Troelstra","year":"1977"},{"key":"10.1016\/S0747-7171(85)80040-7_bib126","series-title":"M\u00e9thodes et probl\u00e8mes de la synthese de programmes dans un univers typ\u00e8","author":"Werner","year":"1983"}],"container-title":["Journal of Symbolic Computation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0747717185800407?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0747717185800407?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,5,10]],"date-time":"2019-05-10T01:48:04Z","timestamp":1557452884000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0747717185800407"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1985,9]]},"references-count":126,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1985,9]]}},"alternative-id":["S0747717185800407"],"URL":"https:\/\/doi.org\/10.1016\/s0747-7171(85)80040-7","relation":{},"ISSN":["0747-7171"],"issn-type":[{"value":"0747-7171","type":"print"}],"subject":[],"published":{"date-parts":[[1985,9]]}}}