{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,20]],"date-time":"2025-11-20T12:19:12Z","timestamp":1763641152604},"reference-count":96,"publisher":"Elsevier","isbn-type":[{"value":"9780444508133","type":"print"}],"license":[{"start":{"date-parts":[[2001,1,1]],"date-time":"2001-01-01T00:00:00Z","timestamp":978307200000},"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":[[2001]]},"DOI":"10.1016\/b978-044450813-3\/50020-5","type":"book-chapter","created":{"date-parts":[[2007,6,11]],"date-time":"2007-06-11T13:04:11Z","timestamp":1181567051000},"page":"1149-1238","source":"Crossref","is-referenced-by-count":26,"title":["Proof-Assistants Using Dependent Type Systems"],"prefix":"10.1016","author":[{"given":"Henk","family":"Barendregt","sequence":"first","affiliation":[]},{"given":"Herman","family":"Geuvers","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/B978-044450813-3\/50020-5_bb0010","series-title":"Handbook of Logic in Computer Science, Volume 2: Background: Computational Structures","year":"1992"},{"key":"10.1016\/B978-044450813-3\/50020-5_bb0015","series-title":"Applicative Common Lisp","author":"ACL2","year":"2000"},{"key":"10.1016\/B978-044450813-3\/50020-5_bb0020","series-title":"Altenkirch, Naraschewski and Reus","article-title":"On relating type theories and set theories","author":"Aczel","year":"1999"},{"key":"10.1016\/B978-044450813-3\/50020-5_bb0025","series-title":"A system for incrementally developing proofs and programs","author":"Agda","year":"2000"},{"key":"10.1016\/B978-044450813-3\/50020-5_bb0030","series-title":"International Workshop TYPES '98, Kloster Irsee, Germany, 1998: selected papers","year":"1999"},{"key":"10.1016\/B978-044450813-3\/50020-5_bb0035","series-title":"Proceedings of the Symposium on Logic in Computing Science","first-page":"86","article-title":"Partial objects in the Calculus of Constructions","author":"Audebaud","year":"1991"},{"key":"10.1016\/B978-044450813-3\/50020-5_bb0040","series-title":"Handbook of Logic in Computer Science, Volume 2: Background: Computational Structures","first-page":"117","article-title":"Lambda calculi with types","author":"Barendregt","year":"1992"},{"issue":"2","key":"10.1016\/B978-044450813-3\/50020-5_bb0045","doi-asserted-by":"crossref","first-page":"181","DOI":"10.2307\/421013","article-title":"The impact of the lambda calculus","volume":"3","author":"Barendregt","year":"1997","journal-title":"Bulletin of Symbolic Logic"},{"key":"10.1016\/B978-044450813-3\/50020-5_bb0050","series-title":"Types for proofs and programs: international workshop TYPES '93, Nijmegen, The Netherlands, 1993: selected papers","year":"1994"},{"key":"10.1016\/B978-044450813-3\/50020-5_bb0055","series-title":"Types for proofs and programs: international workshop TYPES '95, Torino, Italy, 1995: selected papers","first-page":"1","article-title":"Implicit coercions in type systems","author":"Barthe","year":"1996"},{"key":"10.1016\/B978-044450813-3\/50020-5_bb0060","series-title":"Types for proofs and programs: international workshop TYPES '95, Torino, Italy, 1995: selected papers","first-page":"16","article-title":"A two-level approach towards lean proof-checking","author":"Barthe","year":"1996"},{"key":"10.1016\/B978-044450813-3\/50020-5_rf0065","doi-asserted-by":"crossref","first-page":"417","DOI":"10.1017\/S0956796800003750","article-title":"Domain-free Pure Type Systems","volume":"10","author":"Barthe","year":"2000","journal-title":"Journal of Functional Programming"},{"key":"10.1016\/B978-044450813-3\/50020-5_bb0070","series-title":"Hyperproof","author":"Barwise","year":"1995"},{"key":"10.1016\/B978-044450813-3\/50020-5_bb0075","article-title":"Towards a mathematical analysis of the Coquand-Huet Calculus of Constructions and the other systems in Barendregt's cube","author":"Berardi","year":"1988","journal-title":"Technical report, Dept. of Computer Science, Carnegie-Mellon University and Dipartimento Matematica, Universita di Torino"},{"key":"10.1016\/B978-044450813-3\/50020-5_bb0080","article-title":"Type Dependence and Constructive Mathematics","author":"Berardi","year":"1990","journal-title":"PhD thesis, Dipartimento Matematica, Universit\u00e0 di Torino"},{"key":"10.1016\/B978-044450813-3\/50020-5_bb0085","series-title":"Types for proofs and programs: international workshop TYPES '95, Torino, Italy, 1995: selected papers","year":"1996"},{"key":"10.1016\/B978-044450813-3\/50020-5_rf0090","series-title":"Typed Lambda Calculi and Applications, TLCA '93","year":"1993"},{"key":"10.1016\/B978-044450813-3\/50020-5_bb0095","series-title":"Automated Deduction\u2014A Basis for Applications","year":"1998"},{"key":"10.1016\/B978-044450813-3\/50020-5_bb0100","series-title":"A Computational Logic Handbook","author":"Boyer","year":"1997"},{"key":"10.1016\/B978-044450813-3\/50020-5_bb0105","series-title":"Automated deduction, CADE-12: 12th International Conference on Automated Deduction, Nancy, France, June 26\u2013July 1, 1994, proceedings","year":"1994"},{"key":"10.1016\/B978-044450813-3\/50020-5_bb0110","doi-asserted-by":"crossref","DOI":"10.1006\/jsco.2001.0457","article-title":"Formal and efficient primality proofs by use of computer algebra oracles","author":"Caprotti","year":"2001","journal-title":"Journal of Symbolic Computation"},{"key":"10.1016\/B978-044450813-3\/50020-5_bb0115","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\/B978-044450813-3\/50020-5_bb0120","series-title":"Implementing Mathematics with the Nuprl Proof Development System","author":"Constable","year":"1986"},{"key":"10.1016\/B978-044450813-3\/50020-5_bb0125","series-title":"The Coq proof assistant version 6.9","author":"COQ","year":"1999"},{"key":"10.1016\/B978-044450813-3\/50020-5_bb0130","article-title":"Une th\u00e9orie des Constructions","author":"Coquand","year":"1985","journal-title":"PhD thesis, Universit\u00e9 Paris VII, Th\u00e8se de troisi\u00e8me cycle"},{"key":"10.1016\/B978-044450813-3\/50020-5_bb0135","series-title":"Proceedings of the Symposium on Logic in Computing Science","article-title":"An analysis of Girard's paradox","author":"Coquand","year":"1986"},{"key":"10.1016\/B978-044450813-3\/50020-5_bb0140","series-title":"Logical Frameworks","article-title":"An algorithm for testing conversion in type theory","author":"Coquand","year":"1991"},{"key":"10.1016\/B978-044450813-3\/50020-5_bb0145","series-title":"Preliminary Proceedings 1st Annual Workshop on Logical Frameworks","first-page":"479","article-title":"A proof of strong normalization for the theory of Constructions using a Kripke-like interpretation","author":"Coquand","year":"1990"},{"key":"10.1016\/B978-044450813-3\/50020-5_bb0150","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\/B978-044450813-3\/50020-5_bb0155","series-title":"Logical Frameworks","article-title":"Inductively defined types","author":"Coquand","year":"1990"},{"key":"10.1016\/B978-044450813-3\/50020-5_bb0160","article-title":"The Language Theory of Automath","author":"Daalen","year":"1980","journal-title":"PhD thesis, Eindhoven University of Technology, The Netherlands"},{"key":"10.1016\/B978-044450813-3\/50020-5_bb0165","series-title":"To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism","first-page":"579","article-title":"A survey of the project Automath","author":"de Bruijn","year":"1980"},{"key":"10.1016\/B978-044450813-3\/50020-5_bb0170","series-title":"Symposium on Automatic Demonstration","first-page":"29","article-title":"The mathematical language AUTOMATH, its usage and some of its extensions","volume":"125","author":"de Bruijn","year":"1970"},{"key":"10.1016\/B978-044450813-3\/50020-5_bb0175","series-title":"Second International Conference on Typed Lambda Calculi and Applications, TLCA '95","year":"1995"},{"key":"10.1016\/B978-044450813-3\/50020-5_bb0180","series-title":"A list of computer math systems","author":"Digimath","year":"2000"},{"key":"10.1016\/B978-044450813-3\/50020-5_bb0185","series-title":"Typed Lambda Calculi and Applications, TLCA '93","first-page":"139","article-title":"The undecidability of typability in the \u03bb\u03c0-calculus","author":"Dowek","year":"1993"},{"key":"10.1016\/B978-044450813-3\/50020-5_bb0190","series-title":"Types for proofs and programs: international workshop TYPES '94, Bstad, Sweden, 1994: selected papers","year":"1995"},{"key":"10.1016\/B978-044450813-3\/50020-5_bb0195","series-title":"Proceedings of the seventh annual symposium on Logic in Computer Science","first-page":"453","article-title":"The Church-Rosser property for \u03b2\u03b7-reduction in typed lambda calculi","author":"Geuvers","year":"1992"},{"key":"10.1016\/B978-044450813-3\/50020-5_bb0200","article-title":"Logics and Type Systems","author":"Geuvers","year":"1993","journal-title":"PhD thesis, Catholic University of Nijmegen, The Netherlands"},{"key":"10.1016\/B978-044450813-3\/50020-5_bb0205","series-title":"Types for proofs and programs: international workshop TYPES '94, Bstad, Sweden, 1994: selected papers","first-page":"14","article-title":"A short and flexible proof of strong normalization for the Calculus of Constructions","author":"Geuvers","year":"1995"},{"issue":"2","key":"10.1016\/B978-044450813-3\/50020-5_bb0210","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1017\/S0956796800020037","article-title":"A modular proof of strong normalization for the Calculus of Constructions","volume":"1","author":"Geuvers","year":"1991","journal-title":"Journal of Functional Programming"},{"key":"10.1016\/B978-044450813-3\/50020-5_bb0215","series-title":"Computer Science Logic (CSL '99)","first-page":"439","article-title":"Safe proof checking in type theory with Y","author":"Geuvers","year":"1999"},{"key":"10.1016\/B978-044450813-3\/50020-5_bb0220","series-title":"International Workshop TYPES '96, Aussois, France, 1996: selected papers","year":"1998"},{"key":"10.1016\/B978-044450813-3\/50020-5_bb0225","article-title":"Interpr\u00e9tation fonctionelle et \u00e9limination des coupures de l'arithm\u00e9tique d'ordre sup\u00e9rieur","author":"Girard","year":"1972","journal-title":"PhD thesis, Th\u00e8se d'Etat, Universit\u00e9 Paris VII"},{"key":"10.1016\/B978-044450813-3\/50020-5_bb0230","series-title":"Typed Lambda Calculus and Applications, TLCA '99","year":"1999"},{"key":"10.1016\/B978-044450813-3\/50020-5_bb0235","series-title":"Proofs and Types, Vol. 7 of Cambridge Tracts in Theoretical Computer Science","author":"Girard","year":"1989"},{"key":"10.1016\/B978-044450813-3\/50020-5_bb0240","series-title":"Logical Environments","first-page":"198","article-title":"Inductive data types: Well-orderings revisited","author":"Goguen","year":"1993"},{"issue":"1","key":"10.1016\/B978-044450813-3\/50020-5_bb0245","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\/B978-044450813-3\/50020-5_bb0250","series-title":"Types for proofs and programs: international workshop TYPES '93, Nijmegen, The Netherlands, 1993: selected papers","first-page":"166","article-title":"Elimination of extensionality and quotient types in Martin-L\u00f6f type theory","author":"Hofmann","year":"1994"},{"key":"10.1016\/B978-044450813-3\/50020-5_bb0255","series-title":"Higher order logic theorem prover","author":"HOL","year":"1998"},{"key":"10.1016\/B978-044450813-3\/50020-5_bb0260","series-title":"To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism","first-page":"479","article-title":"The formulas-as-types notion of construction","author":"Howard","year":"1980"},{"key":"10.1016\/B978-044450813-3\/50020-5_bb0265","series-title":"Proceedings of the Ninth International Conference of Automated Deduction","first-page":"238","article-title":"Computational metatheory in Nuprl","author":"Howe","year":"1988"},{"key":"10.1016\/B978-044450813-3\/50020-5_bb0270","series-title":"Logical Frameworks","year":"1991"},{"key":"10.1016\/B978-044450813-3\/50020-5_bb0275","series-title":"Logical Environments","year":"1993"},{"key":"10.1016\/B978-044450813-3\/50020-5_bb0280","series-title":"Second International Conference on Typed Lambda Calculi and Applications, TLCA '95","first-page":"266","article-title":"A simplification of Girard's paradox","author":"Hurkens","year":"1995"},{"key":"10.1016\/B978-044450813-3\/50020-5_bb0285","series-title":"A framework for building interactive proof editors","author":"JAPE","year":"1997"},{"key":"10.1016\/B978-044450813-3\/50020-5_bb0290","series-title":"The Lego proof assistant","author":"LEGO","year":"1998"},{"key":"10.1016\/B978-044450813-3\/50020-5_rf0295","series-title":"Logic in Computer Science","article-title":"ECC, the Extended Calculus of Constructions","author":"Luo","year":"1989"},{"key":"10.1016\/B978-044450813-3\/50020-5_bb0300","series-title":"Computation and Reasoning: A Type Theory for Computer Science, Vol. 11 of Intl. Series of Monographs in Computer Science","author":"Luo","year":"1994"},{"issue":"1","key":"10.1016\/B978-044450813-3\/50020-5_bb0305","doi-asserted-by":"crossref","DOI":"10.1093\/logcom\/9.1.105","article-title":"Coercive subtyping","volume":"9","author":"Luo","year":"1999","journal-title":"Journal of Logic and Computation"},{"key":"10.1016\/B978-044450813-3\/50020-5_bb0310","article-title":"The implementation of ALF: a proof-editor based on Martin-L\u00f6f's monomorphic type theory with explicit substitution","author":"Magnusson","year":"1994","journal-title":"PhD thesis, Dept. of Comp. Science, Chalmers University, Sweden"},{"key":"10.1016\/B978-044450813-3\/50020-5_bb0315","series-title":"Studies in Proof Theory","article-title":"Intuitionistic Type Theory","author":"Martin-L\u00f6f","year":"1984"},{"key":"10.1016\/B978-044450813-3\/50020-5_bb0320","series-title":"COLOG-88: International conference on computer logic","year":"1990"},{"key":"10.1016\/B978-044450813-3\/50020-5_bb0325","series-title":"Mathpert","author":"Mathpert","year":"1997"},{"key":"10.1016\/B978-044450813-3\/50020-5_bb0330","series-title":"Proceedings of the Symposium in Pure Mathematics 5","doi-asserted-by":"crossref","DOI":"10.1090\/pspum\/005\/9998","article-title":"Computer programs for checking mathematical proofs","author":"McCarthy","year":"1962"},{"key":"10.1016\/B978-044450813-3\/50020-5_bb0335","series-title":"International Workshop TYPES '96, Aussois, France, 1996: selected papers","article-title":"A generic proof of strong normalisation for Pure Type Systems","author":"Mellies","year":"1998"},{"key":"10.1016\/B978-044450813-3\/50020-5_bb0340","series-title":"Architects: Andrzej Trybulec, Czeslaw Bylinski","author":"Mizar","year":"1989"},{"key":"10.1016\/B978-044450813-3\/50020-5_bb0345","series-title":"Proceedings of the First Symposium on Logic in Computer Science","first-page":"84","article-title":"Algorithm development in the Calculus of Constructions","author":"Mohring","year":"1986"},{"key":"10.1016\/B978-044450813-3\/50020-5_bb0350","article-title":"Strong normalisation in a lambda calculus with lambda structured types","author":"Nederpelt","year":"1973","journal-title":"PhD thesis, Eindhoven University of Technology, The Netherlands"},{"key":"10.1016\/B978-044450813-3\/50020-5_bb0355","series-title":"Selected Papers on Automath","volume":"133","year":"1994"},{"key":"10.1016\/B978-044450813-3\/50020-5_bb0360","series-title":"Programming in Martin-L\u00f6f's Type Theory","author":"Nordstr\u00f6m","year":"1990"},{"key":"10.1016\/B978-044450813-3\/50020-5_bb0365","series-title":"Theoretical Computer Sci","article-title":"Proof by computation in the Coq system","author":"Oostdijk","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50020-5_bb0370","series-title":"OpenMath","year":"1998"},{"key":"10.1016\/B978-044450813-3\/50020-5_bb0375","series-title":"Architect: William McCune","author":"Otter","year":"1998"},{"key":"10.1016\/B978-044450813-3\/50020-5_bb0380","series-title":"Proceedings 3rd Intl. Conf. on Mathematics of Program Construction, MPC'95","first-page":"351","article-title":"Synthesizing proofs from programs in the Calculus of Inductive Constructions","author":"Parent","year":"1995"},{"key":"10.1016\/B978-044450813-3\/50020-5_bb0385","series-title":"Typed Lambda Calculi and Applications, TLCA '93","first-page":"328","article-title":"Inductive definitions in the system Coq; rules and properties","author":"Paulin-Mohring","year":"1994"},{"key":"10.1016\/B978-044450813-3\/50020-5_bb0390","doi-asserted-by":"crossref","first-page":"607","DOI":"10.1016\/S0747-7171(06)80007-6","article-title":"Synthesis of ML programs in the system Coq","volume":"15","author":"Paulin-Mohring","year":"1993","journal-title":"Journal of Symbolic Computation"},{"key":"10.1016\/B978-044450813-3\/50020-5_bb0395","series-title":"Logical Frameworks","first-page":"149","article-title":"Logic programming in the LF logical framework","author":"Pfenning","year":"1991"},{"key":"10.1016\/B978-044450813-3\/50020-5_bb0400","first-page":"1063","article-title":"Logical frameworks","volume":"Vol. II","author":"Pfenning","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50020-5_bb0405","series-title":"Second International Conference on Typed Lambda Calculi and Applications, TLCA '95","first-page":"365","article-title":"A verified type checker","author":"Pollack","year":"1995"},{"key":"10.1016\/B978-044450813-3\/50020-5_bb0410","series-title":"Specification and verification system","author":"PVS","year":"1999"},{"key":"10.1016\/B978-044450813-3\/50020-5_bb0415","series-title":"Proceedings of the London Mathematical Society","first-page":"338","article-title":"The foundations of mathematics","author":"Ramsey","year":"1925"},{"key":"10.1016\/B978-044450813-3\/50020-5_rf0420","first-page":"123","article-title":"Modular verification of SRT division","author":"Ruess","year":"1996"},{"issue":"1","key":"10.1016\/B978-044450813-3\/50020-5_bb0425","doi-asserted-by":"crossref","first-page":"13","DOI":"10.1109\/32.210304","article-title":"Formal verification of algorithms for critical systems","volume":"19","author":"Rushby","year":"1993","journal-title":"IEEE Transactions on Software Engineering"},{"key":"10.1016\/B978-044450813-3\/50020-5_bb0430","series-title":"The Principles of Mathematics","author":"Russell","year":"1903"},{"key":"10.1016\/B978-044450813-3\/50020-5_bb0435","series-title":"Symposium on Automated Demonstration","first-page":"237","article-title":"Constructive validity","author":"Scott","year":"1970"},{"key":"10.1016\/B978-044450813-3\/50020-5_bb0440","series-title":"To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism","year":"1980"},{"key":"10.1016\/B978-044450813-3\/50020-5_bb0445","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1006\/inco.1998.2708","article-title":"Type inference for Pure Type Systems","volume":"143\u20131","author":"Severi","year":"1998","journal-title":"Information and Computation"},{"key":"10.1016\/B978-044450813-3\/50020-5_bb0450","series-title":"Proceedings of LFCS'94, St. Petersburg, Russia","first-page":"316","article-title":"Pure Type Systems with definitions","author":"Severi","year":"1994"},{"key":"10.1016\/B978-044450813-3\/50020-5_bb0455","article-title":"Weak and strong sum-elimination in intuitionistic type theory","author":"Swaen","year":"1989","journal-title":"PhD thesis, University of Amsterdam,"},{"key":"10.1016\/B978-044450813-3\/50020-5_bb0460","article-title":"Een nadere bewijstheoretische analyse van GSTT's (Dutch)","author":"Terlouw","year":"1989","journal-title":"Technical report, Department of Computer Science, Catholic University of Nijmegen"},{"issue":"1","key":"10.1016\/B978-044450813-3\/50020-5_bb0465","doi-asserted-by":"crossref","first-page":"30","DOI":"10.1006\/inco.1993.1038","article-title":"Typing in Pure Type Systems","volume":"105","author":"van Benthem Jutting","year":"1993","journal-title":"Information and Computation"},{"key":"10.1016\/B978-044450813-3\/50020-5_bb0470","series-title":"Types for proofs and programs: international workshop TYPES '93, Nijmegen, The Netherlands, 1993: selected papers","first-page":"19","article-title":"Checking algorithms for Pure Type Systems","author":"van Benthem Jutting","year":"1994"},{"key":"10.1016\/B978-044450813-3\/50020-5_bb0475","volume":"Vol 1","author":"Whitehead","year":"1910"},{"key":"10.1016\/B978-044450813-3\/50020-5_bb0480","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-7091-6639-0","article-title":"Mechanical Theorem Proving in Geometries","author":"Wu","year":"1994"},{"key":"10.1016\/B978-044450813-3\/50020-5_bb0485","series-title":"Typed Lambda Calculus and Applications, TLCA '99","article-title":"Pure Type Systems with subtyping","author":"Zwanenburg","year":"1999"}],"container-title":["Handbook of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:B9780444508133500205?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:B9780444508133500205?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,4,23]],"date-time":"2020-04-23T01:26:14Z","timestamp":1587605174000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/B9780444508133500205"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9780444508133"],"references-count":96,"URL":"https:\/\/doi.org\/10.1016\/b978-044450813-3\/50020-5","relation":{},"subject":[],"published":{"date-parts":[[2001]]}}}