{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:46:10Z","timestamp":1772163970098,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":23,"publisher":"ACM","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2006,9,16]]},"DOI":"10.1145\/1159803.1159826","type":"proceedings-article","created":{"date-parts":[[2006,10,18]],"date-time":"2006-10-18T18:04:00Z","timestamp":1161194640000},"page":"172-183","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["Mechanized meta-reasoning using a hybrid HOAS\/de bruijn representation and reflection"],"prefix":"10.1145","author":[{"given":"Jason","family":"Hickey","sequence":"first","affiliation":[{"name":"California Institute of Technology"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Aleksey","family":"Nogin","sequence":"additional","affiliation":[{"name":"California Institute of Technology"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xin","family":"Yu","sequence":"additional","affiliation":[{"name":"California Institute of Technology"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alexei","family":"Kopylov","sequence":"additional","affiliation":[{"name":"California Institute of Technology"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2006,9,16]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Reflecting on NuPRL: Lessons 1-4. Technical report","author":"Aitken William","year":"1992","unstructured":"William Aitken and Robert L. Constable . Reflecting on NuPRL: Lessons 1-4. Technical report , Cornell University, Computer Science Department , Ithaca, NY, 1992 . William Aitken and Robert L. Constable. Reflecting on NuPRL: Lessons 1-4. Technical report, Cornell University, Computer Science Department, Ithaca, NY, 1992."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1005929703675"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1990.113737"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/11541868_4"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1088454.1088459"},{"key":"e_1_3_2_1_6_1","series-title":"NATO Advanced Study Institute","first-page":"65","volume-title":"Proof and Computation","author":"Constable Robert L.","year":"1994","unstructured":"Robert L. Constable . Using reflection to explain and enhance type theory . In Helmut Schwichtenberg, editor, Proof and Computation , volume 139 of NATO Advanced Study Institute , International Summer School held in Marktoberdorf, Germany, July 20-August 1, NATO Series F, pages 65 -- 100 . Springer , Berlin, 1994 . Robert L. Constable. Using reflection to explain and enhance type theory. In Helmut Schwichtenberg, editor, Proof and Computation, volume 139 of NATO Advanced Study Institute, International Summer School held in Marktoberdorf, Germany, July 20-August 1, NATO Series F, pages 65--100. Springer, Berlin, 1994."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/1385-7258(72)90034-0"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01700692"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/138027.138060"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1021923116629"},{"key":"e_1_3_2_1_12_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1007\/10930755_19","volume-title":"Proceedings of the 16th International Conference on Theorem Proving in Higher Order Logics (TPHOLs","author":"Hickey Jason","year":"2003","unstructured":"Jason Hickey , Aleksey Nogin , Robert L. Constable , Brian E. Aydemir , Eli Barzilay , Yegor Bryukhov , Richard Eaton , Adam Granicz , Alexei Kopylov , Christoph Kreitz , Vladimir N. Krupski , Lori Lorigo , Stephan Schmitt , Carl Witty , and Xin Yu . MetaPRL-A modular logical environment . In David Basin and Burkhart Wolff, editors, Proceedings of the 16th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2003 ), volume 2758 of Lecture Notes in Computer Science , pages 287 -- 303 . Springer-Verlag , 2003 Jason Hickey, Aleksey Nogin, Robert L. Constable, Brian E. Aydemir, Eli Barzilay, Yegor Bryukhov, Richard Eaton, Adam Granicz, Alexei Kopylov, Christoph Kreitz, Vladimir N. Krupski, Lori Lorigo, Stephan Schmitt, Carl Witty, and Xin Yu. MetaPRL-A modular logical environment. In David Basin and Burkhart Wolff, editors, Proceedings of the 16th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2003), volume 2758 of Lecture Notes in Computer Science, pages 287--303. Springer-Verlag, 2003"},{"key":"e_1_3_2_1_13_1","volume-title":"Proceedings of the International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP'06)","author":"Hickey Jason","year":"2006","unstructured":"Jason Hickey , Aleksey Nogin , Xin Yu , and Alexei Kopylov . Practical reflection for sequent logics . In Proceedings of the International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP'06) , Electronic Notes in Theoretical Computer Science , 2006 . To appear. Jason Hickey, Aleksey Nogin, Xin Yu, and Alexei Kopylov. Practical reflection for sequent logics. In Proceedings of the International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP'06), Electronic Notes in Theoretical Computer Science, 2006. To appear."},{"key":"e_1_3_2_1_14_1","unstructured":"Jason J. Hickey Brian Aydemir Yegor Bryukhov Alexei Kopylov Aleksey Nogin and Xin Yu. A listing of MetaPRL theories. http:\/\/metaprl.org\/theories.pdf.  Jason J. Hickey Brian Aydemir Yegor Bryukhov Alexei Kopylov Aleksey Nogin and Xin Yu. A listing of MetaPRL theories. http:\/\/metaprl.org\/theories.pdf."},{"key":"e_1_3_2_1_15_1","unstructured":"Jason J. Hickey Aleksey Nogin Alexei Kopylov etal MetaPRL home page. http:\/\/metaprl.org\/.  Jason J. Hickey Aleksey Nogin Alexei Kopylov et al. MetaPRL home page. http:\/\/metaprl.org\/."},{"key":"e_1_3_2_1_16_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"281","DOI":"10.1007\/3-540-45685-6_19","volume-title":"Proceedings of the 15th International Conference on Theorem Proving in Higher Order Logics (TPHOLs","author":"Nogin Aleksey","year":"2002","unstructured":"Aleksey Nogin and Jason Hickey . Sequent schema for derived rules . In Victor A. Carre\u00f1o, C\u00e9zar A. Mu\u00f1oz, and Sophi\u00e8ne Tahar, editors, Proceedings of the 15th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2002 ), volume 2410 of Lecture Notes in Computer Science , pages 281 -- 297 . Springer-Verlag , 2002. Aleksey Nogin and Jason Hickey. Sequent schema for derived rules. In Victor A. Carre\u00f1o, C\u00e9zar A. Mu\u00f1oz, and Sophi\u00e8ne Tahar, editors, Proceedings of the 15th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2002), volume 2410 of Lecture Notes in Computer Science, pages 281--297. Springer-Verlag, 2002."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.05.041"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1088454.1088456"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/11541868_16"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/53990.54010"},{"key":"e_1_3_2_1_21_1","series-title":"Lecture Notes in Computer Science","first-page":"230","volume-title":"Mathematics of Program Construction","author":"Andrew","year":"2000","unstructured":"Andrew M. Pitts and Murdoch Gabbay. A metalanguage for programming with bound names modulo renaming . In R. Backhouse and J.N. Oliveira, editors, Mathematics of Program Construction , volume 1837 of Lecture Notes in Computer Science , pages 230 -- 255 . Springer-Verlag , Heidelberg , 2000 . Andrew M. Pitts and Murdoch Gabbay. A metalanguage for programming with bound names modulo renaming. In R. Backhouse and J.N. Oliveira, editors, Mathematics of Program Construction, volume 1837 of Lecture Notes in Computer Science, pages 230--255. Springer-Verlag, Heidelberg, 2000."},{"key":"e_1_3_2_1_22_1","first-page":"133","volume-title":"Situation Theory and Its Applications","author":"Plotkin Gordon","year":"1990","unstructured":"Gordon Plotkin . An illative theory of relations . In R. Cooper, K. Mukai, and J. Perry, editors, Situation Theory and Its Applications , Volume 1 , number 22 in CSLI Lecture Notes, pages 133 -- 146 . Centre for the Study of Language and Information, 1990 . Gordon Plotkin. An illative theory of relations. In R. Cooper, K. Mukai, and J. Perry, editors, Situation Theory and Its Applications, Volume 1, number 22 in CSLI Lecture Notes, pages 133--146. Centre for the Study of Language and Information, 1990."},{"key":"e_1_3_2_1_23_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the International Conference on Typed Lambda Calculus and its Applications (TLCA'97)","author":"Rue\u00df Harald","year":"1997","unstructured":"Harald Rue\u00df . Computational reflection in the calculus of constructions and its application to theorem proving . In R. Hindley, editor, Proceedings of the International Conference on Typed Lambda Calculus and its Applications (TLCA'97) , volume 1210 of Lecture Notes in Computer Science , Nancy, France, April 1997 . Springer-Verlag . Harald Rue\u00df. Computational reflection in the calculus of constructions and its application to theorem proving. In R. Hindley, editor, Proceedings of the International Conference on Typed Lambda Calculus and its Applications (TLCA'97), volume 1210 of Lecture Notes in Computer Science, Nancy, France, April 1997. Springer-Verlag."},{"key":"e_1_3_2_1_24_1","volume-title":"From Frege to G\u00f6del: A Source Book in Mathematical Logic","author":"van Heijenoort J.","year":"1879","unstructured":"J. van Heijenoort , editor. From Frege to G\u00f6del: A Source Book in Mathematical Logic , 1879 --1931. Harvard University Press , Cambridge, MA , 1967. J. van Heijenoort, editor. From Frege to G\u00f6del: A Source Book in Mathematical Logic, 1879--1931. Harvard University Press, Cambridge, MA, 1967."}],"event":{"name":"ICFP06: ACM SIGPLAN International Conference on Functional Programming","location":"Portland Oregon USA","acronym":"ICFP06","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","ACM Association for Computing Machinery"]},"container-title":["Proceedings of the eleventh ACM SIGPLAN international conference on Functional programming"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1159803.1159826","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,9,4]],"date-time":"2023-09-04T16:04:21Z","timestamp":1693843461000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1159803.1159826"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,9,16]]},"references-count":23,"alternative-id":["10.1145\/1159803.1159826","10.1145\/1159803"],"URL":"https:\/\/doi.org\/10.1145\/1159803.1159826","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/1160074.1159826","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2006,9,16]]},"assertion":[{"value":"2006-09-16","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}