{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:23:03Z","timestamp":1725664983477},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540626886"},{"type":"electronic","value":"9783540684381"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/3-540-62688-3_44","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T17:48:37Z","timestamp":1330278517000},"page":"319-335","source":"Crossref","is-referenced-by-count":4,"title":["Computational reflection in the calculus of constructions and its application to theorem proving"],"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,3]]},"reference":[{"key":"20_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":"20_CR2","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":"20_CR3","doi-asserted-by":"crossref","unstructured":"T. Coquand and G. Huet. Constructions: a Higher-Order Proof System for Mechanizing Mathematics. In B. Buchberger, editor, EUROCAL'85: European Conference on Computer Algebra, volume 203 of Lecture Notes in Computer Science, pages 151\u2013184. Springer-Verlag, 1985.","DOI":"10.1007\/3-540-15983-5_13"},{"issue":"2\/3","key":"20_CR4","doi-asserted-by":"crossref","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":"20_CR5","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":"20_CR6","volume-title":"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":"20_CR7","doi-asserted-by":"crossref","unstructured":"R. Harper and R. Pollack. Type Checking, Universal Polymorphism, and Type Ambiguity in the Calculus of Constructions. In TAPSOFT'89, volume II, Lecture Notes in Computer Science, pages 240\u2013256. Springer-Verlag, 1989.","DOI":"10.1007\/3-540-50940-2_39"},{"key":"20_CR8","volume-title":"Technical Report CRC-053","author":"J. Harrison","year":"1995","unstructured":"J. Harrison. Metatheory and Reflection in Theorem Proving: A Survey and Critique. Technical Report CRC-053, SRI Cambridge, UK, 1995. See http:\/\/www.cl.cam.ac.uk\/ftp\/hvg\/papers."},{"key":"20_CR9","doi-asserted-by":"crossref","unstructured":"D.J. Howe. Computational Metatheory in Nuprl. In Proc. 9th International Conference on Automated Deduction, volume 310, pages 238\u2013257. Springer-Verlag Lecture Notes in Computer Science, 1988.","DOI":"10.1007\/BFb0012835"},{"key":"20_CR10","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":"20_CR11","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":"20_CR12","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":"20_CR13","unstructured":"Z. Luo. CC \u2282 \u03c9 and its Metatheory. Technical Report ECS-LFCS-88-57, Laboratory for the Foundations of Computer Science, Edinburgh University, July 1988."},{"key":"20_CR14","unstructured":"Z. Luo and R. Pollack. The Lego Proof Development System: A User's Manual. Technical Report ECS-LFCS-92-211, University of Edinburgh, 1992."},{"issue":"3","key":"20_CR15","doi-asserted-by":"crossref","first-page":"345","DOI":"10.1017\/S0956796800000423","volume":"2","author":"T. Mogensen","year":"1992","unstructured":"T. Mogensen. Efficient Self-Interpretation in Lambda Calculus. J. Functional Programming, 2(3):345\u2013364, 1992.","journal-title":"J. Functional Programming"},{"key":"20_CR16","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":"20_CR17","doi-asserted-by":"crossref","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":"20_CR18","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1016\/0304-3975(90)90109-U","volume":"89","author":"F. Pfenning","year":"1991","unstructured":"F. Pfenning and P. Lee. Metacircularity in the Polymorphic \u03bb-Calculus. Theoretical Computer Science, 89:137\u2013159, 1991.","journal-title":"Theoretical Computer Science"},{"key":"20_CR19","unstructured":"H. Rue\u00df. Formal M eta-Programming in the Calculus of Constructions. PhD thesis, Universit\u00e4t Ulm, 1995."},{"key":"20_CR20","doi-asserted-by":"crossref","unstructured":"H. Rue\u00df. Reflection of Formal Tactics in a Deductive Reflection Framework. In M.A. McRobbie and J.K.Slaney, editors, Automated Deduction \u2014 CADE-13, volume 1104 of Lecture Notes in Computer Science. Springer-Verlag, 1996.","DOI":"10.1007\/3-540-61511-3_118"},{"key":"20_CR21","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, volume 45 of Lecture Notes in Computer Science. Springer-Verlag, 1976.","DOI":"10.1007\/3-540-07854-1_195"},{"issue":"1","key":"20_CR22","doi-asserted-by":"crossref","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","Typed Lambda Calculi and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-62688-3_44.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T16:14:05Z","timestamp":1605629645000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-62688-3_44"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540626886","9783540684381"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/3-540-62688-3_44","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1997]]}}}