{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:28:51Z","timestamp":1725488931913},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540439318"},{"type":"electronic","value":"9783540456209"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45620-1_32","type":"book-chapter","created":{"date-parts":[[2007,8,12]],"date-time":"2007-08-12T03:18:26Z","timestamp":1186888706000},"page":"392-407","source":"Crossref","is-referenced-by-count":7,"title":["Faster Proof Checking in the Edinburgh Logical Framework"],"prefix":"10.1007","author":[{"given":"Aaron","family":"Stump","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David L.","family":"Dill","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,7,4]]},"reference":[{"key":"32_CR1","unstructured":"S. Abramsky, D. Gabbay, and T. Maibaum, editors. Handbook of Logic in Computer Science. Oxford University Press, 1992."},{"key":"32_CR2","doi-asserted-by":"crossref","unstructured":"A. Appel and E. Felten. Proof-carrying authentication. In 6th ACM Conference on Computer and Communication Security, 1999.","DOI":"10.1145\/319709.319718"},{"key":"32_CR3","unstructured":"H. Barendregt. Lambda Calculi with Types, pages 117\u2013309. Volume 2 of D. Gabbay, and T. Maibaum, editors. Handbook of Logic in Computer Science. Oxford University Press Abramsky et al. [1], 1992."},{"key":"32_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44659-1_3","volume-title":"Theorem Proving in Higher Order Logics, 13th International Conference","author":"S. Berghofer","year":"2000","unstructured":"S. Berghofer and T. Nipkow. Proof terms for simply typed higher order logic. In Theorem Proving in Higher Order Logics, 13th International Conference, volume 1869 of LNCS, 2000."},{"key":"32_CR5","doi-asserted-by":"crossref","unstructured":"H. Cirstea, C. Kirchner, and L. Liquori. The Rho Cube. In F. Honsell, editor, Foundations of Software Science and Computation Structures (FOSSACS), 2001.","DOI":"10.1007\/3-540-45315-6_11"},{"key":"32_CR6","unstructured":"H. Comon, M. Dauchet, R. Gilleron, F. Jacquemard, D. Lugiez, S. Tison, and M. Tommasi. Tree automata techniques and applications. Available at http:\/\/www.grappa.univ-lille3.fr\/tata , 1997."},{"key":"32_CR7","doi-asserted-by":"crossref","unstructured":"T. Coquand. An algorithm for testing conversion in Type Theory, pages 255\u201379. In A. Voronkov, editors. Handbook of Automated Reasoning. Elsevier and MIT Press Huet and Plotkin [12], 1991.","DOI":"10.1017\/CBO9780511569807.011"},{"key":"32_CR8","doi-asserted-by":"crossref","unstructured":"A. Degtyarev and A. Voronkov. The Inverse Method, chapter IV. In A. Voronkov, editors. Handbook of Automated Reasoning. Elsevier and MIT Press Robinson and Voronkov [19], 2001.","DOI":"10.1016\/B978-044450813-3\/50006-0"},{"issue":"1","key":"32_CR9","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1023\/A:1026744827863","volume":"66","author":"W. Farmer","year":"2000","unstructured":"W. Farmer and J. Guttman. A Set Theory with Support for Partial Functions. Logica Studia, 66(1):59\u201378, 2000.","journal-title":"Logica Studia"},{"issue":"1","key":"32_CR10","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1145\/138027.138060","volume":"40","author":"R. Harper","year":"1993","unstructured":"R. Harper, F. Honsell, and G. Plotkin. A Framework for Defining Logics. Journal of the Association for Computing Machinery, 40(1):143\u2013184, January 1993.","journal-title":"Journal of the Association for Computing Machinery"},{"key":"32_CR11","unstructured":"R. Harper and F. Pfenning. On Equivalence and Canonical Forms in the LF Type Theory. Technical Report CMU-CS-00-148, Carnegie Mellon University, July 2000."},{"key":"32_CR12","doi-asserted-by":"crossref","unstructured":"G. Huet and G. Plotkin, editors. Logical Frameworks. Cambridge University Press, 1991.","DOI":"10.1017\/CBO9780511569807"},{"key":"32_CR13","doi-asserted-by":"crossref","unstructured":"F. Kamareddine. Reviewing the classical and the de Bruijn notation for \u03bb-calculus and pure type systems. Logic and Computation, 11(3):363\u2013394.","DOI":"10.1093\/logcom\/11.3.363"},{"key":"32_CR14","unstructured":"Z. Luo and R. Pollack. LEGO Proof Development System: User\u2019s Manual. Technical Report ECS-LFCS-92-211, Edinburgh LFCS, 1992."},{"key":"32_CR15","doi-asserted-by":"crossref","unstructured":"G. Necula. Proof-Carrying Code. In 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 106\u2013119, January 1997.","DOI":"10.1145\/263699.263712"},{"key":"32_CR16","doi-asserted-by":"crossref","unstructured":"G. Necula and P. Lee. Efficient representation and validation of proofs. In 13th Annual IEEE Symposium on Logic in Computer Science, pages 93\u2013104, 1998.","DOI":"10.1109\/LICS.1998.705646"},{"key":"32_CR17","doi-asserted-by":"crossref","unstructured":"F. Pfenning. Logical Frameworks, chapter XXI. In A. Voronkov, editors. Handbook of Automated Reasoning. Elsevier and MIT Press Robinson and Voronkov [19], 2001.","DOI":"10.1016\/B978-044450813-3\/50019-9"},{"key":"32_CR18","doi-asserted-by":"crossref","unstructured":"F. Pfenning and Carsten Sch\u00fcrmann. System Description: Twelf \u2014 A Meta-Logical Framework for Deductive Systems. In 16th International Conference on Automated Deduction, 1999.","DOI":"10.1007\/3-540-48660-7_14"},{"key":"32_CR19","unstructured":"A. Robinson and A. Voronkov, editors. Handbook of Automated Reasoning. Elsevier and MIT Press, 2001."},{"key":"32_CR20","unstructured":"A. Stump. Checking Validities and Proofs with CVC and flea. PhD thesis, Stanford University, 2002. In preparation: check http:\/\/verify.stanford.edu\/~stump\/ for a draft ."},{"key":"32_CR21","doi-asserted-by":"crossref","unstructured":"A. Stump, C. Barrett, and D. Dill. CVC: a Cooperating Validity Checker. In 14th International Conference on Computer-Aided Verification, 2002.","DOI":"10.1007\/3-540-45657-0_40"},{"key":"32_CR22","unstructured":"R. Virga. Higher-Order Rewriting with Dependent Types. PhD thesis, Carnegie Mellon University, October 1999."},{"issue":"2","key":"32_CR23","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1023\/A:1008643803725","volume":"14","author":"W. Wong","year":"1999","unstructured":"W. Wong. Validation of HOL Proofs by Proof Checking. Formal Methods in System Design, 14(2):193\u2013212, 1999.","journal-title":"Formal Methods in System Design"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction\u2014CADE-18"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45620-1_32","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T19:55:52Z","timestamp":1556740552000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45620-1_32"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540439318","9783540456209"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/3-540-45620-1_32","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}