{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:11:25Z","timestamp":1725484285986},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540440390"},{"type":"electronic","value":"9783540456858"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45685-6_19","type":"book-chapter","created":{"date-parts":[[2007,5,19]],"date-time":"2007-05-19T16:47:53Z","timestamp":1179593273000},"page":"281-297","source":"Crossref","is-referenced-by-count":11,"title":["Sequent Schema for Derived Rules"],"prefix":"10.1007","author":[{"given":"Aleksey","family":"Nogin","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jason","family":"Hickey","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,7,25]]},"reference":[{"key":"19_CR1","volume-title":"Implementing Mathematics with the NuPRL Development System","author":"R. L. Constable","year":"1986","unstructured":"Robert L. Constable, Stuart F. Allen, H.M. Bromley, W.R. Cleaveland, J.F. Cremer, R.W. Harper, Douglas J. Howe, T.B. Knoblock, N.P. Mendler, P. Panangaden, James T. Sasaki, and Scott F. Smith. Implementing Mathematics with the NuPRL Development System. Prentice-Hall, NJ, 1986."},{"key":"19_CR2","volume-title":"Introduction to HOL: A Theorem Proving Environment for Higher-Oder Logic","author":"M. Gordon","year":"1993","unstructured":"Michael Gordon and T. Melham. Introduction to HOL: A Theorem Proving Environment for Higher-Oder Logic. Cambridge University Press, Cambridge, 1993."},{"key":"19_CR3","doi-asserted-by":"crossref","unstructured":"Robert Harper, Furio Honsell, and Gordon Plotkin. A framework for defining logics. Journal of the Association for Computing Machinery, 40(1):143\u2013184, January 1993. A revised and expanded verion of\u2019 87 paper.","DOI":"10.1145\/138027.138060"},{"key":"19_CR4","series-title":"PhD thesis","volume-title":"The MetaPRL Logical Programming Environment","author":"J. J. Hickey","year":"2001","unstructured":"Jason J. Hickey. The MetaPRL Logical Programming Environment. PhD thesis, Cornell University, Ithaca, NY, January 2001."},{"key":"19_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"252","DOI":"10.1007\/3-540-44659-1_16","volume-title":"Theorem Proving in Higher Order Logics: 13th International Conference, TPHOLs 2000","author":"J. J. Hickey","year":"2000","unstructured":"Jason J. Hickey and Aleksey Nogin. Fast tactic-based theorem proving. In J. Harrison and M. Aagaard, editors, Theorem Proving in Higher Order Logics: 13th International Conference, TPHOLs 2000, volume 1869 of Lecture Notes in Computer Science, pages 252\u2013266. Springer-Verlag, 2000."},{"key":"19_CR6","unstructured":"Jason J. Hickey, Aleksey Nogin, Alexei Kopylov, et al. MetaPRL home page. http:\/\/metaprl.org\/ ."},{"key":"19_CR7","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/BF00264598","volume":"11","author":"G. P. Huet","year":"1978","unstructured":"G\u00e9rard P. Huet and Bernard Lang. Proving and applying program transformations expressed with second-order patterns. Acta Informatica, 11:31\u201355, 1978.","journal-title":"Acta Informatica"},{"key":"19_CR8","unstructured":"Alexei Kopylov. Dependent intersection: A new way of defining records in type theory. Department of Computer Science TR2000-1809, Cornell University, 2000."},{"key":"19_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1007\/3-540-44755-5_23","volume-title":"The 14th International Conference on Theorem Proving in Higher Order Logics, Edinburgh, Scotland","author":"P. Naumov","year":"2001","unstructured":"Pavel Naumov, Mark-Olivar Stehr, and Jos\u00e9 Meseguer. The HOL\/NuPRL proof translator: A practical approach to formal interoperability. In The 14th International Conference on Theorem Proving in Higher Order Logics, Edinburgh, Scotland, Lecture Notes in Computer Science, pages 329\u2013345. Springer-Verlag, September 2001."},{"key":"19_CR10","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle: A Generic Theorem Prover","author":"L. C. Paulson","year":"1994","unstructured":"Lawrence C. Paulson. Isabelle: A Generic Theorem Prover, volume 828. Springer-Verlag, New York, 1994."},{"key":"19_CR11","doi-asserted-by":"crossref","unstructured":"Frank Pfenning. Elf: A language for logic definition and verified metaprogramming. In Proceedings of Fourth Annual Symposium on Logic in Computer Science, pages 313\u2013322, Pacific Grove, California, June 1989. IEEE Computer Society Press.","DOI":"10.1109\/LICS.1989.39186"},{"key":"19_CR12","doi-asserted-by":"crossref","unstructured":"Frank Pfenning and Conal Elliott. Higher-order abstract syntax. In Proceedings of the ACM SIGPLAN\u201988 Conference on Programming Language Design and Implementation (PLDI), pages 199\u2013208, Atlanta, Georgia, June 1988. ACM Press.","DOI":"10.1145\/53990.54010"}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45685-6_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T01:38:02Z","timestamp":1556415482000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45685-6_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540440390","9783540456858"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/3-540-45685-6_19","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}