{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T02:30:52Z","timestamp":1774837852811,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":36,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540605799","type":"print"},{"value":"9783540477709","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/3-540-60579-7_8","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T20:42:44Z","timestamp":1330288964000},"page":"140-161","source":"Crossref","is-referenced-by-count":8,"title":["On extensibility of proof checkers"],"prefix":"10.1007","author":[{"given":"Robert","family":"Pollack","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,1]]},"reference":[{"key":"8_CR1","unstructured":"Allen, Constable, Howe, and Aitken. The semantics of reflected proof. In LICS Proceedings. IEEE, 1990."},{"key":"8_CR2","unstructured":"William Aitkin, Robert Constable, and Judith Underwood. Metalogical frameworks II: Using reflected decision procedures. Technical report, Cornell University. To appear."},{"key":"8_CR3","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1016\/0890-5401(91)90023-U","volume":"92","author":"A. Avron","year":"1991","unstructured":"Arnon Avron. Simple consequence relations. Information and Computation, 92:105\u2013139, 1991.","journal-title":"Information and Computation"},{"key":"8_CR4","first-page":"103","volume-title":"The Correctness Problem in Computer Science","author":"R. S. Boyer","year":"1981","unstructured":"Robert S. Boyer and J S. Moore. Metafunctions: Proving them correct and using them efficiently as new proof procedures. In Robert S. Boyer and J S. Moore, editors, The Correctness Problem in Computer Science, pages 103\u2013184. Academic Press, New York, 1981."},{"key":"8_CR5","unstructured":"Robert S. Boyer and J S. Moore. A Computational Logic Handbook. Academic Press, 1988."},{"key":"8_CR6","volume-title":"Implementing Mathematics with the Nuprl Proof Development System","author":"R. L. Constable","year":"1986","unstructured":"Robert L. Constable, et. al. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, Englewood Cliffs, NJ, 1986."},{"key":"8_CR7","unstructured":"Nicolas G. de Bruijn. Generalizing automath by means of a lambda-typed lambda calculus. In Proceedings of the Maryland 1984\u20131985 Special Year in Mathematical Logic and Theoretical Computer Science, 1985."},{"key":"8_CR8","unstructured":"Dowek, Felty, Herbelin, Huet, Paulin-Mohring, and Werner. The Coq proof assistant user's guide, version 5.6. Technical Report 134, INRIA-Rocquencourt, December 1991."},{"key":"8_CR9","doi-asserted-by":"crossref","unstructured":"Solomon Feferman. Finitary inductively presented logics. In Logic Colloquium '88, Padova. August 1988.","DOI":"10.1016\/S0049-237X(08)70270-2"},{"key":"8_CR10","unstructured":"Amy P. Felty. Specifying and Implementing Theorem Provers in a Higher-Order Logic Programming Language. PhD thesis, University of Pennsylvania, September 1989. MS-CIS-89-53."},{"key":"8_CR11","unstructured":"Mick Francis, Simon Finn, and Ellie Mayger. Reference manual for the Lambda system. Technical report, Abstract Hardware Limited, 1990."},{"key":"8_CR12","doi-asserted-by":"crossref","unstructured":"Michael Gordon, Robin Milner, and Christopher Wadsworth. Edinburgh LCF: A Mechanized Logic of Computation. Springer-Verlag, 1979.","DOI":"10.1007\/3-540-09724-4"},{"key":"8_CR13","doi-asserted-by":"crossref","unstructured":"Michael Gordon. HOL: A proof generating system for higher-order logic. In Birtwistle and Subrahmanyam, editors, VLSI Specification, Verification and Synthesis, pages 73\u2013128. Kluwer Academic Publishers, 1988.","DOI":"10.1007\/978-1-4613-2007-4_3"},{"key":"8_CR14","doi-asserted-by":"crossref","unstructured":"John Harrison. Binary decision diagrams as a HOL derived rule. The Computer Journal, 38(5), 1995.","DOI":"10.1093\/comjnl\/38.2.162"},{"key":"8_CR15","volume-title":"Technical Report CRC-053","author":"J. Harrison","year":"1995","unstructured":"John Harrison. Metatheory and reflection in theorem proving: A survey and critique. Technical Report CRC-053, SRI Cambridge, UK, 1995."},{"issue":"1","key":"8_CR16","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1145\/138027.138060","volume":"40","author":"R. Harper","year":"1992","unstructured":"Robert Harper, Furio Honsell, and Gordon Plotkin. A framework for defining logics. Journal of the ACM, 40(1):143\u2013184, 1992. Preliminary version in LICS'87.","journal-title":"Journal of the ACM"},{"key":"8_CR17","unstructured":"Susumu Hayashi and Hiroshi Nakano. PX: A Computational Logic. MIT Press, 1988."},{"key":"8_CR18","unstructured":"Douglas Howe. Automating Reasoning in an Implementation of Constructive Type Theory. PhD thesis, Cornell University, June 1988."},{"key":"8_CR19","unstructured":"J. Roger Hindley and Jonathan P. Seldin. Introduction to Combinators and \u03bb-Calculus, volume 1 of London Mathematical Society Student Texts. Cambridge University Press, 1986."},{"key":"8_CR20","unstructured":"T. Knoblock and R. Constable. Formalized metareasoning in type theory. In LICS Proceedings. IEEE, 1986."},{"key":"8_CR21","volume-title":"Mathematical Logic","author":"S. C. Kleene","year":"1967","unstructured":"Stephen C. Kleene. Mathematical Logic. Wiley, New York, 1967."},{"key":"8_CR22","unstructured":"Todd Knoblock. Metamathematical Extensibility in Type Theory. PhD thesis, Corness University, December 1987. Technical Report 87-892."},{"key":"8_CR23","volume-title":"Technical Report ECS-LFCS-92-211, LFCS","author":"Z. Luo","year":"1992","unstructured":"Zhaohui Luo and Robert Pollack. LEGO proof development system: User's manual. Technical Report ECS-LFCS-92-211, LFCS, Computer Science Dept., University of Edinburgh, The King's Buildings, Edinburgh EH9 3JZ, May 1992. Updated version. See http:\/\/www.des.ed. ac. uk\/packages\/lego\/"},{"key":"8_CR24","doi-asserted-by":"crossref","unstructured":"Z. Luo. Computation and Reasoning: A Type Theory for Computer Science. International Series of Monographs on Computer Science. Oxford University Press, 1994.","DOI":"10.1093\/oso\/9780198538356.001.0001"},{"key":"8_CR25","unstructured":"Per Martin-L\u00f6f. On the meanings of the logical constants and the justifications of the logical laws. Technical Report 2, Scuola di Specializzazione in Logica Matematica, Dipartimento di Matematica, Universit\u00e0 di Siena, 1985."},{"key":"8_CR26","doi-asserted-by":"crossref","first-page":"321","DOI":"10.1016\/0747-7171(92)90011-R","volume":"14","author":"D. Miller","year":"1992","unstructured":"Dale Miller. Unification under a mixed prefix. Journal of Symbolic Computation, 14:321\u2013358, 1992.","journal-title":"Journal of Symbolic Computation"},{"key":"8_CR27","doi-asserted-by":"crossref","unstructured":"James McKinna and Robert Pollack. Pure Type Sytems formalized. In M.Bezem and J.F.Groote, editors, Proceedings of the International Conference on Typed Lambda Calculi and Applications, TLCA'93, pages 289\u2013305. Springer-Verlag, LNCS 664, March 1993.","DOI":"10.1007\/BFb0037113"},{"key":"8_CR28","volume-title":"Logical Environments","author":"S. Matthews","year":"1993","unstructured":"Sean Matthews, Alan Smaill, and David Basin. Experience with FS 0 as a framework theory. In G. Huet and G.D. Plotkin, editors, Logical Environments. Cambridge University Press, 1993. Formal Proceedings of the Second Workshop on Logical Frameworks, Edinburgh, May 1991."},{"key":"8_CR29","unstructured":"Robin Milner, Mads Tofte, and Robert Harper. The Definition of Standard ML. MIT Press, 1990."},{"key":"8_CR30","doi-asserted-by":"crossref","unstructured":"Lawrence C. Paulson. Introduction to isabelle. Technical Report 280, University of Cambridge, Computer Laboratory, 1993. See http:\/\/www. cl. cam. ac. uk\/Research\/HVG\/isabelle.html","DOI":"10.1007\/BFb0030541"},{"key":"8_CR31","doi-asserted-by":"crossref","unstructured":"Christine Paulin-Mohring. Extracting 160-01's programs from proofs in the Calculus of Constructions. In Association for Computing Machinery, editor, Sixteenth Annual ACM Symposium on Principles of Programming Languages, Austin, 1989.","DOI":"10.1145\/75277.75285"},{"key":"8_CR32","unstructured":"Robert Pollack. The Theory of LEGO: A Proof Checker for the Extended Calculus of Constructions. PhD thesis, University of Edinburgh, 1994. Available by anonymous ftp from ftp. cs. chalmers. se in directory pub\/users\/pollack."},{"key":"8_CR33","volume-title":"LNCS","author":"R. Pollack","year":"1995","unstructured":"Robert Pollack. A verified typechecker. In TLCA'95, Proceedings of the Second International Conference on Typed Lambda Calculi and Applications, Edinburgh. Springer-Verlag, LNCS, April 1995."},{"key":"8_CR34","first-page":"537","volume-title":"number 607 in LNAI","author":"F. Pfenning","year":"1992","unstructured":"Frank Pfenning and Ekkehard Rohwedder. Implementing the meta-theory of inductive systems. In D. Kapur, editor, Proceedings of the Eleventh Annual Conference on Automated Deduction, Saratoga Springs, New York, number 607 in LNAI, pages 537\u2013551. Springer-Verlag, June 1992."},{"key":"8_CR35","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1016\/0167-6423(90)90056-J","volume":"14","author":"Mike Spivey","year":"1990","unstructured":"Mike Spivey. A functional theory of exceptions. Science of Computer Programming, 14:25\u201342, 1990. North Holland.","journal-title":"Science of Computer Programming"},{"key":"8_CR36","doi-asserted-by":"crossref","unstructured":"Philip Wadler. The essence of functional programming. In Nineteenth Annual Symposium on Principles of Programming Languages, Santa Fe, New Mexico, January 1992.","DOI":"10.1145\/143165.143169"}],"container-title":["Lecture Notes in Computer Science","Types for Proofs and Programs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-60579-7_8.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,20]],"date-time":"2024-04-20T17:01:27Z","timestamp":1713632487000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-60579-7_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540605799","9783540477709"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/3-540-60579-7_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1995]]}}}