{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:10:36Z","timestamp":1725664236476},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540615118"},{"type":"electronic","value":"9783540686873"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61511-3_118","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T21:51:23Z","timestamp":1330293083000},"page":"628-642","source":"Crossref","is-referenced-by-count":1,"title":["Reflection of formal tactics in a deductive reflection framework"],"prefix":"10.1007","author":[{"given":"Harald","family":"Rue\u00df","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,4]]},"reference":[{"key":"55_CR1","doi-asserted-by":"crossref","unstructured":"S.F. Allen, R.L. Constable, D.J. Howe, and W.E. Aitken. The Semantics of Reflected Proof. In Proc. 5th Annual IEEE Symposium on Logic in Computer Science, pages 95\u2013105. IEEE CS Press, 1990.","DOI":"10.1109\/LICS.1990.113737"},{"key":"55_CR2","unstructured":"H.P. Barendregt. The Lambda Calculus: Its Syntax and Semantics, volume 103 of Studies in Logic and The Foundations of Mathematics. North-Holland, revised edition edition, 1984."},{"key":"55_CR3","unstructured":"D.A. Basin. Beyond Tactic Based Theorem Proving. In J. Kunze and H. Stoyan, editors, KI-94 Workshops: Extended Abstracts. Gesellschaft f\u00fcr Informatik e.V, 1994. 18. Deutsche Jahrestagung f\u00fcr K\u00fcnstliche Intelligenz, Saarbr\u00fccken."},{"key":"55_CR4","unstructured":"D.A. Basin and R.L. Constable. Metalogical Frameworks. Technical Report TR 91-1235, Department of Computer Science, Cornell University, September 1991."},{"key":"55_CR5","unstructured":"R.S. Boyer and J.S. Moore. Metafunctions: Proving them Correct and Using them Efficiently as New Proof Procedures. In R.S. Boyer and J.S. Moore, editors, The Correctness Problem in Computer Science, chapter 3. Academic Press, 1981."},{"key":"55_CR6","unstructured":"R.L. Constable, S.F. Allen, and H.M. Bromley et al. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, 1986."},{"issue":"2\/3","key":"55_CR7","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/0890-5401(88)90005-3","volume":"76","author":"T. Coquand","year":"1988","unstructured":"T. Coquand and G. Huet. The Calculus of Constructions. Information and Computation, 76(2\/3):95\u2013120, 1988.","journal-title":"Information and Computation"},{"key":"55_CR8","unstructured":"J.-Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types, volume 7 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1989."},{"key":"55_CR9","volume-title":"volume 78 of Lecture Notes in Computer Science","author":"M. J. Gordon","year":"1979","unstructured":"M. J. Gordon, A. J. R. Milner, and C. P. Wadsworth. Edinburgh LCF: a Mechanized Logic of Computation, volume 78 of Lecture Notes in Computer Science. Springer-Verlag, Berlin, 1979."},{"key":"55_CR10","unstructured":"M.J.C Gordon and T.F. Melham. Introduction to HOL: A Theorem Proving Environment for Higher-Order Logic. Cambridge University Press, 1993."},{"issue":"1","key":"55_CR11","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":"55_CR12","unstructured":"D.J. Howe. Automating Reasoning in an Implementation of Constructive Type Theory. PhD thesis, Cornell University, 1988. Available as technical report TR 88-925 from the Department of Computer Science, Cornell University."},{"key":"55_CR13","doi-asserted-by":"crossref","unstructured":"D.J. Howe. Reflecting the Semantics of Reflected Proof. In P. Aczel, H. Simmons, and S. Wainer, editors, Proof Theory, pages 227\u2013250. Cambridge University Press, 1992.","DOI":"10.1017\/CBO9780511896262.010"},{"key":"55_CR14","unstructured":"T.B. Knoblock and R.L. Constable. Formalized Metareasoning in Type Theory. In Proceedings of LICS, pages 237\u2013248. IEEE, 1986. Also available as technical report TR 86-742, Department of Computer Science, Cornell University."},{"key":"55_CR15","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1002\/malq.19680140702","volume":"14","author":"G. Kreisel","year":"1968","unstructured":"G. Kreisel and A. L\u00e9vy. Reflection Principles and their Use for Establishing the Complexity of Axiomatic Systems. Zeitschrift f\u00fcr math. Logik und Grundlagen der Mathematik, Bd. 14:97\u2013142, 1968.","journal-title":"Zeitschrift f\u00fcr math. Logik und Grundlagen der Mathematik"},{"key":"55_CR16","unstructured":"J. Meseguer and M.G. Clavel. Axiomatizing reflective logics and languages. Submitted for publication, November 1995."},{"key":"55_CR17","unstructured":"B. Nordstr\u00f6m, K. Petersson, and J.M. Smith. Programming in Martin-L\u00f6f's Type Theory. Number 7 in International Series of Monographs on Computer Science. Oxford Science Publications, 1990."},{"issue":"2","key":"55_CR18","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1109\/32.345827","volume":"21","author":"S. Owre","year":"1995","unstructured":"S. Owre, J. Rushby, N. Shankar, and F. von Henke. Formal Verification for Fault-Tolerant Architectures: Prolegomena to the Design of PVS. IEEE Transactions on Software Engineering, 21(2):107\u2013125, February 1995.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"55_CR19","doi-asserted-by":"crossref","unstructured":"L.C. Paulson. Logic and Computation: Interactive Proof with Cambridge LCF. Number 2 in Cambride Tracts in Theoretical Computer Science. Cambridge University Press, 1987.","DOI":"10.1017\/CBO9780511526602"},{"key":"55_CR20","doi-asserted-by":"crossref","unstructured":"L.C. Paulson. Isabelle: A Generic Theorem Prover. Number 828 in Lecture Notes in Computer Science. Springer-Verlag, 1994.","DOI":"10.1007\/BFb0030541"},{"key":"55_CR21","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1016\/0304-3975(94)00125-3","volume":"136","author":"E. Ritter","year":"1994","unstructured":"E. Ritter. Cagegorical Abstract Machines for Higher-Order Typed \u03bb-Calculi. Theoretical Computer Science, 136:125\u2013162, 1994.","journal-title":"Theoretical Computer Science"},{"key":"55_CR22","unstructured":"H. Rue\u00df. Formal Meta-Programming in the Calculus of Constructions. PhD thesis, Universit\u00e4t Ulm, 1995."},{"key":"55_CR23","doi-asserted-by":"crossref","unstructured":"C. Smorynski. Self-Reference and Modal Logic. Springer-Verlag, 1985.","DOI":"10.1007\/978-1-4613-8601-8"},{"key":"55_CR24","doi-asserted-by":"crossref","unstructured":"F. W. von Henke. An Algebraic Approach to Data Types, Program Verification, and Program Synthesis. In Mathematical Foundations of Computer Science, Proceedings. Springer-Verlag Lecture Notes in Computer Science 45, 1976.","DOI":"10.1007\/3-540-07854-1_195"},{"key":"55_CR25","doi-asserted-by":"crossref","unstructured":"F.W. von Henke, A. Dold, H. Rue\u00df, D. Schwier, and M. Strecker. Construction and deduction methods for the formal development of software. In M. Broy and S. J\u00e4hnichen, editors, KORSO, Correct Software by Formal Methods, number 1009 in LNCS. Springer-Verlag, Lecture Notes in Computer Science, 1995.","DOI":"10.1007\/BFb0015465"},{"issue":"1","key":"55_CR26","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1016\/0004-3702(80)90015-6","volume":"13","author":"R. W. Weyhrauch","year":"1980","unstructured":"R. W. Weyhrauch. Prolegomena to a Theory of Mechanized Formal Reasoning. Artificial Intelligence, 13(1):133\u2013170, 1980.","journal-title":"Artificial Intelligence"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2014 Cade-13"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-61511-3_118.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:07:16Z","timestamp":1605647236000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61511-3_118"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540615118","9783540686873"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/3-540-61511-3_118","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}