{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,29]],"date-time":"2026-01-29T23:55:49Z","timestamp":1769730949042,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":57,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540159834","type":"print"},{"value":"9783540396840","type":"electronic"}],"license":[{"start":{"date-parts":[[1985,1,1]],"date-time":"1985-01-01T00:00:00Z","timestamp":473385600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1985]]},"DOI":"10.1007\/3-540-15983-5_13","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T18:26:37Z","timestamp":1330194397000},"page":"151-184","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":69,"title":["Constructions: A higher order proof system for mechanizing mathematics"],"prefix":"10.1007","author":[{"given":"Thierry","family":"Coquand","sequence":"first","affiliation":[]},{"given":"G\u00e9rard","family":"Huet","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"issue":"3","key":"13_CR1","doi-asserted-by":"crossref","first-page":"414","DOI":"10.2307\/2269949","volume":"36","author":"P. B. Andrews","year":"1971","unstructured":"P. B. Andrews, Resolution in Type Theory, Journal of Symbolic Logic 36,3 pp. 414\u2013432 (1971).","journal-title":"Journal of Symbolic Logic"},{"key":"13_CR2","doi-asserted-by":"crossref","unstructured":"P. B. Andrews, Dale A. Miller, Eve Longini Cohen, and Frank Pfenning, Automating higher-order logic, Dept of Math. University Carnegie-Mellon (1983 January).","DOI":"10.1090\/conm\/029\/09"},{"key":"13_CR3","unstructured":"R. Backhouse, Algorithm development in Martin-L\u00f6f's type theory, University of Essex (July 1984)."},{"key":"13_CR4","unstructured":"A. Berarducci and C. B\u00f6hm, Toward an Automatic Synthesis of Polymorphic Typed Lambda Terms, ICALP (1984)."},{"key":"13_CR5","volume-title":"Foundations of Constructive Analysis","author":"E. Bishop","year":"1967","unstructured":"E. Bishop, Foundations of Constructive Analysis, McGraw-Hill, New-York (1967)."},{"key":"13_CR6","first-page":"53","volume-title":"Intuitionism and Proof Theory","author":"E. Bishop","year":"1970","unstructured":"E. Bishop, Mathematics as a numerical language, Intuitionism and Proof Theory, Edited by J. Myhill, A. Kino and R.E. Vesley, North-Holland, Amsterdam, pp. 53\u201371 (1970)."},{"key":"13_CR7","unstructured":"R. Boyer and J Moore, A Lemma Driven Automatic Theorem Prover for Recursive Function Theory, 5th International Joint Conference on Artificial Intelligence, pp. 511\u2013519 (1977)."},{"key":"13_CR8","unstructured":"R. Boyer and J. Moore, A mechanical proof of the unsolvability of the halting problem, Report ICSCA-CMP-28, Institute for Computing Science \u2014 University of Texas at Austin (July 1982)."},{"key":"13_CR9","unstructured":"R. Boyer and J. Moore, Proof Checking the RSA Public Key Encryption Algorithm, Report ICSCA-CMP-33, Institute for Computing Science \u2014 University of Texas at Austin (September 1982)."},{"key":"13_CR10","doi-asserted-by":"crossref","unstructured":"R. Boyer and J. Moore, Proof checking theorem proving and program verification, Report ICSA-CMP-35, Institute for Computing Science \u2014 University of Texas at Austin (January 1983).","DOI":"10.1090\/conm\/029\/07"},{"key":"13_CR11","unstructured":"N.G. de Bruijn, Automath a language for mathematics, Les Presses de l'Universite de Montr\u00e9al (1973)."},{"key":"13_CR12","unstructured":"N.G. de Bruijn, A survey of the project Automath, Curry Volume, Academic Press (1980)."},{"key":"13_CR13","volume-title":"The Calculi of Lambda-Conversion","author":"A. Church","year":"1941","unstructured":"A. Church, The Calculi of Lambda-Conversion, Princeton U. Press, Princeton N.J. (1941)."},{"key":"13_CR14","unstructured":"R.L. Constable and J.L. Bates, Proofs as Programs, Dept. of Computer Science, Cornell University. (Feb. 1983)."},{"key":"13_CR15","unstructured":"R.L. Constable and J.L. Bates, The Nearly Ultimate Pearl, Dept. of Computer Science, Cornell University. (Dec. 1983)."},{"key":"13_CR16","unstructured":"Th. Coquand, Une th\u00e9orie des constructions, Th\u00e8se de troisi\u00e8me cycle, Universit\u00e9 Paris VII (Janvier 85)."},{"key":"13_CR17","unstructured":"Th. Coquand and G. Huet, A Theory of Constructions, Preliminary version, presented at the International Symposium on Semantics of Data Types, Sophia-Antipolis (June 84)."},{"key":"13_CR18","unstructured":"D. Van Daalen, The language of Automath, Ph. D. Dissertation, Technological Univ. Eindhoven (1980)."},{"issue":"1","key":"13_CR19","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1145\/322358.322370","volume":"30","author":"S. Fortune","year":"1983","unstructured":"S. Fortune, D. Leivant, and O'Michael Donnell, The Expressiveness of Simple and Second-Order Type Structures, Journal of the Association for Computing Machinery, Vol 30, No 1, pp 151\u2013185 (January 1983).","journal-title":"Journal of the Association for Computing Machinery"},{"key":"13_CR20","unstructured":"G. Frege, Begriffschrift, in Heijenoort, From Frege to G\u00f6del (1879)."},{"key":"13_CR21","volume-title":"The Collected Paper of Gerhard Gentzen","author":"G. Gentzen","year":"1969","unstructured":"G. Gentzen, The Collected Paper of Gerhard Gentzen, edited by E. Szabo, North-Holland, Amsterdam, 1969 (1969)."},{"key":"13_CR22","doi-asserted-by":"crossref","unstructured":"J.Y. Girard, Une extension de l'interpr\u00e9tation de G\u00f6del \u00e0 l'analyse, et son application a l'\u00e9limination des coupures dans l'analyse et la th\u00e9orie des types, Proceedings of the Second Scandinavian Logic Symposium, Ed. J.E. Fenstad, North Holland, pp. 63\u201392 (1970).","DOI":"10.1016\/S0049-237X(08)70843-7"},{"key":"13_CR23","unstructured":"J.Y. Girard, Interpr\u00e9tation fonctionnelle et \u00e9limination des coupures dans l'arithm\u00e9tique d'ordre sup\u00e9rieure, Th\u00e8se d'Etat, Universit\u00e9 Paris VII (1972)."},{"key":"13_CR24","unstructured":"M. Gordon, R. Milner, and C. Wadsworth, A Metalanguage for Interactive Proof in LCF, Internal Report CSR-16-77, department of Computer Science, University of Edinburgh (Sept. 1977)."},{"key":"13_CR25","doi-asserted-by":"crossref","unstructured":"M.J. Gordon, A. J. Milner, and C.P. Wadsworth, Edinburgh LCF, Springer-Verlag LNCS 78 (1979).","DOI":"10.1007\/3-540-09724-4"},{"key":"13_CR26","unstructured":"G. Huet, Constrained Resolution: a Complete Method for Type Theory, Ph.D. Thesis, Jennings Computing Center Report 1117, Case Western Reserve University (1972)."},{"key":"13_CR27","unstructured":"G. Huet, A Mechanization of Type Theory. Proceedings, 3rd IJCAI, Stanford (Aug. 1973)."},{"key":"13_CR28","doi-asserted-by":"crossref","unstructured":"G. Huet, A Unification Algorithm for Typed Lambda Calculus, Theoretical Computer Science, 1.1, pp. 27\u201357 (1975).","DOI":"10.1016\/0304-3975(75)90011-0"},{"issue":"4","key":"13_CR29","doi-asserted-by":"crossref","first-page":"797","DOI":"10.1145\/322217.322230","volume":"27","author":"G. Huet","year":"1980","unstructured":"G. Huet, Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems, J. Assoc. Comp. Mach. 27,4 pp. 797\u2013821 (Oct. 1980).","journal-title":"J. Assoc. Comp. Mach."},{"key":"13_CR30","unstructured":"L.S. Jutting, A translation of Landau's \"Grundlagen\" in AUTOMATH, Eindhoven University of Technology, Dept of Mathematics (October 1976)."},{"key":"13_CR31","unstructured":"J. Ketonen, A mechanical proof of Ramsey theorem, Stanford Univ. CA (October 1983)."},{"key":"13_CR32","doi-asserted-by":"crossref","unstructured":"J. Ketonen, EKL-A Mathematically Oriented Proof Checker, 7th International Conference on Automated Deduction, Napa, California. LNCS 170, Springer-Verlag (May 1984).","DOI":"10.1007\/978-0-387-34768-4_4"},{"key":"13_CR33","unstructured":"J. Ketonen and J. S. Weening, The language of an interactive proof checker, Stanford University (1984)."},{"key":"13_CR34","doi-asserted-by":"crossref","unstructured":"D. Leivant, Polymorphic type inference, 10th POPL (1983).","DOI":"10.1145\/567067.567077"},{"key":"13_CR35","unstructured":"P. Martin-L\u00f6f, A theory of types. October 1971."},{"key":"13_CR36","unstructured":"P. Martin-L\u00f6f, About models for intuitionistic type theories and the notion of definitional equality, Paper read at the Orl\u00e9ans Logic Conference (1972)."},{"key":"13_CR37","first-page":"73","volume":"73","author":"P. Martin-L\u00f6f","year":"1974","unstructured":"P. Martin-L\u00f6f, An intuitionistic Theory of Types, predicative part, Logic Colloquium 73, pp. 73\u2013118, North-Holland (1974).","journal-title":"Logic Colloquium"},{"key":"13_CR38","first-page":"153","volume":"VI","author":"P. Martin-L\u00f6f","year":"1980","unstructured":"P. Martin-L\u00f6f, Constructive Mathematics and Computer Programming, Logic, Methodology and Philosophy of Science VI, pp. 153\u2013175, North-Holland (1980).","journal-title":"Logic, Methodology and Philosophy of Science"},{"key":"13_CR39","volume-title":"Intuitionistic Type Theory","author":"P. Martin-L\u00f6f","year":"1984","unstructured":"P. Martin-L\u00f6f, Intuitionistic Type Theory, Studies in Proof Theory, Bibliopolis (1984)."},{"key":"13_CR40","unstructured":"D.A. Miller, Proofs in Higher-order Logic, Ph. D. Dissertation, Carnegie-Mellon University (Aug. 1983)."},{"key":"13_CR41","unstructured":"R.P. Nederpelt, Strong normalization in a typed lambda calculus with lambda structured types, Ph. D. Thesis, Eindhoven University of Technology (1973)."},{"key":"13_CR42","series-title":"Lecture Notes in Computer Science","volume-title":"An approach to theorem proving on the basis of a typed lambda-calculus","author":"R.P. Nederpelt","year":"1980","unstructured":"R.P. Nederpelt, An approach to theorem proving on the basis of a typed lambda-calculus, Lecture Notes in Computer Science 87: 5th Conference on Automated Deduction, Les Arcs, France, Springer-Verlag (1980)."},{"issue":"2","key":"13_CR43","doi-asserted-by":"crossref","first-page":"223","DOI":"10.2307\/1968867","volume":"43","author":"M.H.A. Newman","year":"1942","unstructured":"M.H.A. Newman, On Theories with a Combinatorial Definition of \"Equivalence\", Annals of Math. 43,2 pp.223\u2013243 (1942).","journal-title":"Annals of Math."},{"key":"13_CR44","doi-asserted-by":"crossref","unstructured":"B. Nordstr\u00f6m, Programming in Constructive Set Theory: Some Examples, Proceedings of the Conference on Functional Programming Languages and Computer Architecture, Portmouth, New Hampshire, p. 141\u2013154 (Oct. 1981).","DOI":"10.1145\/800223.806773"},{"key":"13_CR45","series-title":"Technical Report","volume-title":"Recent Developments in LCF: Examples of structural induction","author":"L. Paulson","year":"1983","unstructured":"L. Paulson, Recent Developments in LCF: Examples of structural induction, Technical Report No 34, University of Cambridge, England (Janvier 1983)."},{"key":"13_CR46","unstructured":"L. Paulson, Tactics and Tacticals in Cambridge LCF, Technical Report No 39, Computer Laboratory, University of Cambridge (July 1983)."},{"key":"13_CR47","unstructured":"L. Paulson, Verifying the unification algorithm in LCF, Technical report No 50, Computer Laboratory, University of Cambridge (March 1984)."},{"key":"13_CR48","doi-asserted-by":"crossref","unstructured":"T Pietrzykowski and D.C Jensen, A complete mechanization of \u03c9-order type theory, Proceedings of The ACM Annual Conference (1972).","DOI":"10.1145\/800193.805824"},{"key":"13_CR49","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1145\/321752.321764","volume":"20","author":"T. Pietrzykowski","year":"1973","unstructured":"T. Pietrzykowski, A Complete Mechanization of Second-Order Type Theory, JACM 20, pp. 333\u2013364 (1973).","journal-title":"JACM"},{"key":"13_CR50","unstructured":"D. Prawitz, Natural Deduction, Almqist and Wiskell, Stockolm (1965)."},{"key":"13_CR51","first-page":"408","volume":"19","author":"J.C. Reynolds","year":"1974","unstructured":"J.C. Reynolds, Towards a Theory of Type Structure, Programming Symposium, Paris. Springer Verlag LNCS 19, pp. 408\u2013425 (Apr. 1974).","journal-title":"Springer Verlag LNCS"},{"key":"13_CR52","unstructured":"J. C. Reynolds, Types, abstraction. and parametric polymorphism, IFIP Congress'83, Paris (September 1983)."},{"key":"13_CR53","doi-asserted-by":"crossref","unstructured":"J. C. Reynolds, Polymorphism is not set-theoretic, International Symposium on Semantics of Data Types, Sophia-Antipolis (June 1984).","DOI":"10.1007\/3-540-13346-1_7"},{"key":"13_CR54","doi-asserted-by":"crossref","unstructured":"D. Scott, Constructive validity, Symposium on Automatic Demonstration, Lecture Notes in Mathematics, vol. 125 (1970).","DOI":"10.1007\/BFb0060636"},{"key":"13_CR55","unstructured":"J. Smith, Course-of-values recursion on lists in intuitionistic type theory, G\u00f6teborg (September 1981)."},{"key":"13_CR56","doi-asserted-by":"crossref","unstructured":"J. Smith, The identification of propositions and types in Martin-Lof's type theory: a programming example, University of Goteborg Sweden (November 1982).","DOI":"10.1007\/3-540-12689-9_125"},{"issue":"2\/3","key":"13_CR57","first-page":"242","volume":"12","author":"A. Tarski","year":"1955","unstructured":"A. Tarski, A lattice-theoretical fixpoint theorem and its applications, Pacific J. Math. 12,2\/3, pp. 242\u2013248 (1955).","journal-title":"Pacific J. Math."}],"container-title":["Lecture Notes in Computer Science","EUROCAL '85"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-15983-5_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,21]],"date-time":"2025-03-21T20:24:17Z","timestamp":1742588657000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-15983-5_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1985]]},"ISBN":["9783540159834","9783540396840"],"references-count":57,"URL":"https:\/\/doi.org\/10.1007\/3-540-15983-5_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1985]]},"assertion":[{"value":"31 May 2005","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}