{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T01:37:03Z","timestamp":1760146623474,"version":"3.28.0"},"publisher-location":"New York, NY, USA","reference-count":50,"publisher":"ACM","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2005,9,27]]},"DOI":"10.1145\/1088454.1088456","type":"proceedings-article","created":{"date-parts":[[2005,11,7]],"date-time":"2005-11-07T17:34:39Z","timestamp":1131384879000},"page":"2-12","update-policy":"http:\/\/dx.doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":8,"title":["A computational approach to reflective meta-reasoning about languages with bindings"],"prefix":"10.1145","author":[{"given":"Aleksey","family":"Nogin","sequence":"first","affiliation":[{"name":"California Institute of Technology, Pasadena, CA"}]},{"given":"Alexei","family":"Kopylov","sequence":"additional","affiliation":[{"name":"California Institute of Technology, Pasadena, CA"}]},{"given":"Xin","family":"Yu","sequence":"additional","affiliation":[{"name":"California Institute of Technology, Pasadena, CA"}]},{"given":"Jason","family":"Hickey","sequence":"additional","affiliation":[{"name":"California Institute of Technology, Pasadena, CA"}]}],"member":"320","published-online":{"date-parts":[[2005,9,27]]},"reference":[{"key":"e_1_3_2_1_2_1","volume-title":"Mechanized metatheory for the masses: The POPLmark challenge. Available from http:\/\/www.cis.upenn.edu\/group\/proj\/plclub\/mmm\/","author":"Aydemir Brian E.","year":"2005","unstructured":"Brian E. Aydemir , Aaron Bohannon , Matthew Fairbairn , J. Nathan Foster , Benjamin C. Pierce , Peter Sewell , Dimitrios Vytiniotis , Geoffrey Washburn , Stephanie Weirich , and Steve Zdancewic . Mechanized metatheory for the masses: The POPLmark challenge. Available from http:\/\/www.cis.upenn.edu\/group\/proj\/plclub\/mmm\/ , 2005 .]] Brian E. Aydemir, Aaron Bohannon, Matthew Fairbairn, J. Nathan Foster, Benjamin C. Pierce, Peter Sewell, Dimitrios Vytiniotis, Geoffrey Washburn, Stephanie Weirich, and Steve Zdancewic. Mechanized metatheory for the masses: The POPLmark challenge. Available from http:\/\/www.cis.upenn.edu\/group\/proj\/plclub\/mmm\/, 2005.]]"},{"key":"e_1_3_2_1_3_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_4_1","series-title":"Lecture Notes in Artificial Intelligence","first-page":"170","volume-title":"Proceedings of the 17th International Conference on Automated Deduction","author":"Allen Stuart","year":"2000","unstructured":"Stuart Allen , Robert Constable , Richard Eaton , Christoph Kreitz , and Lori Lorigo . The Nuprl open logical environment . In David McAllester, editor, Proceedings of the 17th International Conference on Automated Deduction , volume 1831 of Lecture Notes in Artificial Intelligence , pages 170 -- 176 . Springer Verlag , 2000 .]] Stuart Allen, Robert Constable, Richard Eaton, Christoph Kreitz, and Lori Lorigo. The Nuprl open logical environment. In David McAllester, editor, Proceedings of the 17th International Conference on Automated Deduction, volume 1831 of Lecture Notes in Artificial Intelligence, pages 170--176. Springer Verlag, 2000.]]"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1990.113737"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.5555\/646529.695204"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/976571.976572"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1005929703675"},{"key":"e_1_3_2_1_9_1","first-page":"215","volume-title":"Proceedings of the 2nd IEEE Symposium on Logic in Computer Science","author":"Allen Stuart F.","year":"1987","unstructured":"Stuart F. Allen . A Non-type-theoretic Definition of Martin-L\u00f6f's Types. In D. Gries, editor , Proceedings of the 2nd IEEE Symposium on Logic in Computer Science , pages 215 -- 224 . IEEE Computer Society Press , June 1987 .]] Stuart F. Allen. A Non-type-theoretic Definition of Martin-L\u00f6f's Types. In D. Gries, editor, Proceedings of the 2nd IEEE Symposium on Logic in Computer Science, pages 215--224. IEEE Computer Society Press, June 1987.]]"},{"key":"e_1_3_2_1_11_1","first-page":"267","volume-title":"Ganzinger {30}","author":"Artemov Sergei","unstructured":"Sergei Artemov . On explicit reflection in theorem proving and formal verification . In Ganzinger {30} , pages 267 -- 281 .]] Sergei Artemov. On explicit reflection in theorem proving and formal verification. In Ganzinger {30}, pages 267--281.]]"},{"key":"e_1_3_2_1_13_1","first-page":"23","volume-title":"Theorem Proving in Higher Order Logics","author":"Barzilay Eli","year":"2002","unstructured":"Eli Barzilay and Stuart Allen . Reflecting higher-order abstract syntax in Nuprl . In Victor A. Carreno, C\u00e9zar A. Munoz, and Sophi\u00e8ne Tahar, editors, Theorem Proving in Higher Order Logics ; Track B Proceedings of the 15th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2002 ), Hampton, VA, August 2002, pages 23 -- 32 . National Aeronautics and Space Administration , 2002.]] Eli Barzilay and Stuart Allen. Reflecting higher-order abstract syntax in Nuprl. In Victor A. Carreno, C\u00e9zar A. Munoz, and Sophi\u00e8ne Tahar, editors, Theorem Proving in Higher Order Logics; Track B Proceedings of the 15th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2002), Hampton, VA, August 2002, pages 23--32. National Aeronautics and Space Administration, 2002.]]"},{"key":"e_1_3_2_1_14_1","volume-title":"June 22--25","author":"Barzilay Eli","year":"2003","unstructured":"Eli Barzilay , Stuart Allen , and Robert Constable . Practical reflection in Nuprl. Short paper presented at 18th Annual IEEE Symposium on Logic in Computer Science , June 22--25 , Ottawa , Canada , 2003 .]] Eli Barzilay, Stuart Allen, and Robert Constable. Practical reflection in Nuprl. Short paper presented at 18th Annual IEEE Symposium on Logic in Computer Science, June 22--25, Ottawa, Canada, 2003.]]"},{"key":"e_1_3_2_1_17_1","volume-title":"Implementing Mathematics with the NuPRL Proof Development System","author":"Constable Robert L.","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 Proof Development System . Prentice-Hall , NJ , 1986 .]] 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 Proof Development System. Prentice-Hall, NJ, 1986.]]"},{"key":"e_1_3_2_1_18_1","first-page":"66","volume-title":"Slind et al. phols2004","author":"Crus-Filipe L\u00fais","unstructured":"L\u00fais Crus-Filipe and Freek Weidijk . Hierarchical reflection . In Slind et al. phols2004 , pages 66 -- 81 .]] L\u00fais Crus-Filipe and Freek Weidijk. Hierarchical reflection. In Slind et al. phols2004, pages 66--81.]]"},{"key":"e_1_3_2_1_19_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_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/1385-7258(72)90034-0"},{"key":"e_1_3_2_1_21_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"124","DOI":"10.1007\/BFb0014049","volume-title":"Proceedings of the International Conference on Typed Lambda Calculus and its Applications","author":"Despeyroux Jo\u00eblle","year":"1995","unstructured":"Jo\u00eblle Despeyroux , Amy Felty , and Andr\u00e9 Hirschowitz . Higher-order abstract syntax in Coq . In M. Dezani-Ciancaglini and G. Plotkin, editors, Proceedings of the International Conference on Typed Lambda Calculus and its Applications , volume 902 of Lecture Notes in Computer Science , pages 124 -- 138 . Springer-Verlag , April 1995 . Also appears as http:\/\/www.inria.fr\/rrrt\/rr-2556.htmlINRIA research report RR-2556.]] Jo\u00eblle Despeyroux, Amy Felty, and Andr\u00e9 Hirschowitz. Higher-order abstract syntax in Coq. In M. Dezani-Ciancaglini and G. Plotkin, editors, Proceedings of the International Conference on Typed Lambda Calculus and its Applications, volume 902 of Lecture Notes in Computer Science, pages 124--138. Springer-Verlag, April 1995. Also appears as http:\/\/www.inria.fr\/rrrt\/rr-2556.htmlINRIA research report RR-2556.]]"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.5555\/645708.664171"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.3115\/222020.222073"},{"key":"e_1_3_2_1_24_1","volume-title":"Types for Proofs and Programs: International Workshop, TYPES '98","volume":"1657","author":"Despeyroux Jo\u00eblle","year":"1998","unstructured":"Jo\u00eblle Despeyroux and Pierre Leleu . A modal lambda calculus with iteration and case constructs. In T. Altenkirch, W. Naraschewski, and B. Reus, editors , Types for Proofs and Programs: International Workshop, TYPES '98 , Kloster Irsee, Germany , March 1998 , volume 1657 of Lecture Notes in Computer Science, pages 47--61, 1999.]] Jo\u00eblle Despeyroux and Pierre Leleu. A modal lambda calculus with iteration and case constructs. In T. Altenkirch, W. Naraschewski, and B. Reus, editors, Types for Proofs and Programs: International Workshop, TYPES '98, Kloster Irsee, Germany, March 1998, volume 1657 of Lecture Notes in Computer Science, pages 47--61, 1999.]]"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129501003346"},{"key":"e_1_3_2_1_26_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1007\/3-540-62688-3_34","volume-title":"Proceedings of the Third International Conference on Typed Lambda Calculus and Applications (TLCA'97)","author":"Despeyroux Jo\u00eblle","year":"1997","unstructured":"Jo\u00eblle Despeyroux , Frank Pfenning , and Carsten Sch\u00fcrmann . Primitive recursion for higher--order abstract syntax . In R. Hindley, editor, Proceedings of the Third International Conference on Typed Lambda Calculus and Applications (TLCA'97) , volume 1210 of Lecture Notes in Computer Science , pages 147 -- 163 . Springer-Verlag , April 1997 . An extended version is available as http:\/\/reports-archive.adm.cs.cmu.edu\/anon\/1996\/CMU-CS-96-172.ps.gz Technical Report CMU-CS-96-172, Carnegie Mellon University.]] Jo\u00eblle Despeyroux, Frank Pfenning, and Carsten Sch\u00fcrmann. Primitive recursion for higher--order abstract syntax. In R. Hindley, editor, Proceedings of the Third International Conference on Typed Lambda Calculus and Applications (TLCA'97), volume 1210 of Lecture Notes in Computer Science, pages 147--163. Springer-Verlag, April 1997. An extended version is available as http:\/\/reports-archive.adm.cs.cmu.edu\/anon\/1996\/CMU-CS-96-172.ps.gz Technical Report CMU-CS-96-172, Carnegie Mellon University.]]"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9904-1971-12696-4"},{"key":"e_1_3_2_1_28_1","volume-title":"editors","author":"Solomon Feferman","year":"1986","unstructured":"Solomon Feferman et al. , editors . Kurt G\u00f6del Collected Works, volume 1 . Oxford University Press, Oxford, Clarendon Press , New York, 1986 .]] Solomon Feferman et al., editors. Kurt G\u00f6del Collected Works, volume 1. Oxford University Press, Oxford, Clarendon Press, New York, 1986.]]"},{"key":"e_1_3_2_1_29_1","volume-title":"Proceedings of 14th IEEE Symposium on Logic in Computer Science","author":"Fiore Marcelo","year":"1999","unstructured":"Marcelo Fiore , Gordon Plotkin , and Daniele Turi . Abstract syntax and variable binding . In Proceedings of 14th IEEE Symposium on Logic in Computer Science , pages 193+. IEEE Computer Society Press , 1999 .]] Marcelo Fiore, Gordon Plotkin, and Daniele Turi. Abstract syntax and variable binding. In Proceedings of 14th IEEE Symposium on Logic in Computer Science, pages 193+. IEEE Computer Society Press, 1999.]]"},{"key":"e_1_3_2_1_30_1","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Proceedings of the 16th International Conference onAutomated Deduction","author":"Ganzinger Harald","year":"1999","unstructured":"Harald Ganzinger , editor. Proceedings of the 16th International Conference onAutomated Deduction , volume 1632 of Lecture Notes in Artificial Intelligence , Berlin, July 7--10 1999 . Trento, Italy .]] Harald Ganzinger, editor. Proceedings of the 16th International Conference onAutomated Deduction, volume 1632 of Lecture Notes in Artificial Intelligence, Berlin, July 7--10 1999. Trento, Italy.]]"},{"key":"e_1_3_2_1_31_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1007\/BFb0105404","volume-title":"Theorem Proving in Higher Order Logics: 9th International Conference, Turku, Finland","author":"Gordon A. D.","year":"1996","unstructured":"A. D. Gordon and T. Melham . Five axioms of alpha-conversion . In J. von Wright, J. Grundy, and J. Harrison, editors, Theorem Proving in Higher Order Logics: 9th International Conference, Turku, Finland , August 1996 : Proceedings, volume 1125 of Lecture Notes in Computer Science , pages 173 -- 190 . Springer-Verlag , 1996.]] A. D. Gordon and T. Melham. Five axioms of alpha-conversion. In J. von Wright, J. Grundy, and J. Harrison, editors, Theorem Proving in Higher Order Logics: 9th International Conference, Turku, Finland, August 1996: Proceedings, volume 1125 of Lecture Notes in Computer Science, pages 173--190. Springer-Verlag, 1996.]]"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01700692"},{"key":"e_1_3_2_1_34_1","first-page":"397","volume-title":"\u00dcber die L\u00e4nge von beweisen. Ergebnisse eines mathematischen Kolloquiums, 7:23--24","author":"G\u00f6del K.","year":"1936","unstructured":"K. G\u00f6del . \u00dcber die L\u00e4nge von beweisen. Ergebnisse eines mathematischen Kolloquiums, 7:23--24 , 1936 . English translation in {28}, pages 397 -- 399 .]] K. G\u00f6del. \u00dcber die L\u00e4nge von beweisen. Ergebnisse eines mathematischen Kolloquiums, 7:23--24, 1936. English translation in {28}, pages 397--399.]]"},{"key":"e_1_3_2_1_35_1","first-page":"123","volume-title":"Reflection in constructive and non-constructive automated reasoning","author":"Giunchiglia F.","year":"1989","unstructured":"F. Giunchiglia and A. Smaill . Reflection in constructive and non-constructive automated reasoning . In H. Abramson and M. H. Rogers, editors, Meta-Programming in Logic Programming, pages 123 -- 140 . MIT Press , Cambridge, Mass., 1989 .]] F. Giunchiglia and A. Smaill. Reflection in constructive and non-constructive automated reasoning. In H. Abramson and M. H. Rogers, editors, Meta-Programming in Logic Programming, pages 123--140. MIT Press, Cambridge, Mass., 1989.]]"},{"key":"e_1_3_2_1_36_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"162","DOI":"10.1007\/3-540-44659-1_11","volume-title":"Theorem Proving in Higher Order Logics: 13th International Conference, TPHOLs","author":"Geuvers H.","year":"2000","unstructured":"H. Geuvers , F. Wiedijk , and J. Zwanenburg . Equational reasoning via partial reflection . 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 162 -- 178 . Springer-Verlag , 2000.]] H. Geuvers, F. Wiedijk, and J. Zwanenburg. Equational reasoning via partial reflection. 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 162--178. Springer-Verlag, 2000.]]"},{"key":"e_1_3_2_1_37_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_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/138027.138060"},{"key":"e_1_3_2_1_40_1","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"395","DOI":"10.1007\/3-540-63104-6_37","volume-title":"Proceedings of the 14th International Conference on Automated Deduction","author":"Hickey Jason J.","year":"1997","unstructured":"Jason J. Hickey . NuPRL-Light: An implementation framework for higher-order logics . In William McCune, editor, Proceedings of the 14th International Conference on Automated Deduction , volume 1249 of Lecture Notes in Artificial Intelligence , pages 395 -- 399 . Springer , July 13--17 1997 . An extended version of the paper can be found at http:\/\/www.cs.caltech.edu\/ jyh\/papers\/cade14_nl\/default.html.]] Jason J. Hickey. NuPRL-Light: An implementation framework for higher-order logics. In William McCune, editor, Proceedings of the 14th International Conference on Automated Deduction, volume 1249 of Lecture Notes in Artificial Intelligence, pages 395--399. Springer, July 13--17 1997. An extended version of the paper can be found at http:\/\/www.cs.caltech.edu\/ jyh\/papers\/cade14_nl\/default.html.]]"},{"key":"e_1_3_2_1_41_1","first-page":"227","volume-title":"Ganzinger {30}","author":"Hickey Jason J.","unstructured":"Jason J. Hickey . Fault-tolerant distributed theorem proving . In Ganzinger {30} , pages 227 -- 231 .]] Jason J. Hickey. Fault-tolerant distributed theorem proving. In Ganzinger {30}, pages 227--231.]]"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00264598"},{"key":"e_1_3_2_1_44_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_45_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_46_1","volume-title":"Sentences undecidable in formalized arithmetic: an exposition of the theory of Kurt G\u00f6del","author":"Mostowski Andrzej","year":"1952","unstructured":"Andrzej Mostowski . Sentences undecidable in formalized arithmetic: an exposition of the theory of Kurt G\u00f6del . Amsterdam : North-Holland , 1952 .]] Andrzej Mostowski. Sentences undecidable in formalized arithmetic: an exposition of the theory of Kurt G\u00f6del. Amsterdam: North-Holland, 1952.]]"},{"key":"e_1_3_2_1_47_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_49_1","first-page":"241","volume-title":"Slind et al. phols2004","author":"Norrish Michael","unstructured":"Michael Norrish . Recursive function definition for types with binders . In Slind et al. phols2004 , pages 241 -- 256 .]] Michael Norrish. Recursive function definition for types with binders. In Slind et al. phols2004, pages 241--256.]]"},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.2307\/2269958"},{"key":"e_1_3_2_1_51_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle: A Generic Theorem Prover","author":"Paulson Lawrence C.","year":"1994","unstructured":"Lawrence C. Paulson . Isabelle: A Generic Theorem Prover , volume 828 of Lecture Notes in Computer Science . Springer-Verlag , New York , 1994 .]] Lawrence C. Paulson. Isabelle: A Generic Theorem Prover, volume 828 of Lecture Notes in Computer Science. Springer-Verlag, New York, 1994.]]"},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/960116.54010"},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.5555\/77350.77383"},{"key":"e_1_3_2_1_54_1","first-page":"133","volume-title":"An illative theory of relations","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_55_1","volume-title":"Isabelle tutorial and user's manual. Technical report","author":"Paulson L.","year":"1990","unstructured":"L. Paulson and T. Nipkow . Isabelle tutorial and user's manual. Technical report , University of Cambridge Computing Laboratory , 1990 .]] L. Paulson and T. Nipkow. Isabelle tutorial and user's manual. Technical report, University of Cambridge Computing Laboratory, 1990.]]"},{"key":"e_1_3_2_1_56_1","volume-title":"Proceedings of the 17th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2004","volume":"3223","author":"Slind Konrad","year":"2004","unstructured":"Konrad Slind , Annette Bunker , and Ganesh Gopalakrishnan , editors. Proceedings of the 17th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2004 ), volume 3223 of Lecture Notes in Computer Science. Springer-Verlag , 2004 .]] Konrad Slind, Annette Bunker, and Ganesh Gopalakrishnan, editors. Proceedings of the 17th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2004), volume 3223 of Lecture Notes in Computer Science. Springer-Verlag, 2004.]]"},{"key":"e_1_3_2_1_57_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"585","DOI":"10.1007\/3-540-44802-0_41","volume-title":"Computer Science Logic, Proceedings of the 10th Annual Conference of the EACSL","author":"Sch\u00fcrmann Carsten","year":"2001","unstructured":"Carsten Sch\u00fcrmann . Recursion for higher-order encodings . In L. Fribourg, editor, Computer Science Logic, Proceedings of the 10th Annual Conference of the EACSL , volume 2142 of Lecture Notes in Computer Science , pages 585 -- 599 . Springer-Verlag , 2001 .]] Carsten Sch\u00fcrmann. Recursion for higher-order encodings. In L. Fribourg, editor, Computer Science Logic, Proceedings of the 10th Annual Conference of the EACSL, volume 2142 of Lecture Notes in Computer Science, pages 585--599. Springer-Verlag, 2001.]]"},{"key":"e_1_3_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/800017.800513"},{"key":"e_1_3_2_1_59_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":"MERLIN05: Mechanized Reasoning about Languages with Variable Binding 2005 Workshop","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","ACM Association for Computing Machinery"],"location":"Tallinn Estonia","acronym":"MERLIN05"},"container-title":["Proceedings of the 3rd ACM SIGPLAN workshop on Mechanized reasoning about languages with variable binding"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1088454.1088456","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,11]],"date-time":"2023-01-11T14:16:14Z","timestamp":1673446574000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1088454.1088456"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,9,27]]},"references-count":50,"alternative-id":["10.1145\/1088454.1088456","10.1145\/1088454"],"URL":"https:\/\/doi.org\/10.1145\/1088454.1088456","relation":{},"subject":[],"published":{"date-parts":[[2005,9,27]]},"assertion":[{"value":"2005-09-27","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}