{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:32:00Z","timestamp":1750307520308,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":32,"publisher":"ACM","license":[{"start":{"date-parts":[[2009,9,7]],"date-time":"2009-09-07T00:00:00Z","timestamp":1252281600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2009,9,7]]},"DOI":"10.1145\/1599410.1599422","type":"proceedings-article","created":{"date-parts":[[2009,9,8]],"date-time":"2009-09-08T12:53:09Z","timestamp":1252414389000},"page":"83-92","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":9,"title":["Reasoning with hypothetical judgments and open terms in hybrid"],"prefix":"10.1145","author":[{"given":"Amy P.","family":"Felty","sequence":"first","affiliation":[{"name":"School of Information Technology and Engineering, University of Ottawa, , Ottawa, ON, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alberto","family":"Momigliano","sequence":"additional","affiliation":[{"name":"School of Informatics, University of Edinburgh, Edinburgh, Scotland, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2009,9,7]]},"reference":[{"key":"e_1_3_2_1_1_1","first-page":"13","volume-title":"Carre\u00f1o et al. {2002}","author":"Ambler Simon","unstructured":"Simon Ambler , Roy L. Crole , and Alberto Momigliano . Combining higher order abstract syntax with tactical theorem proving and (co)induction . In Carre\u00f1o et al. {2002} , pages 13 -- 30 . Simon Ambler, Roy L. Crole, and Alberto Momigliano. Combining higher order abstract syntax with tactical theorem proving and (co)induction. In Carre\u00f1o et al. {2002}, pages 13--30."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/11541868_4"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions","author":"Bertot Yves","year":"2004","unstructured":"Yves Bertot and Pierre Cast\u00e9ran . Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions . Springer , 2004 . Yves Bertot and Pierre Cast\u00e9ran. Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions. Springer, 2004."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45685-6"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.5555\/645892.671587"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"crossref","unstructured":"Lars-Henrik\n      Eriksson\n    .\n  Pi: an interactive derivation editor\n   for the calculus of partial inductive definitions. In Alan Bundy editor 12th International Conference on Automated Deduction volume \n  814\n   of \n  Lecture Notes in Computer Science pages \n  821\n  --\n  825\n  . \n  Springer 1994\n  .   Lars-Henrik Eriksson. Pi: an interactive derivation editor for the calculus of partial inductive definitions. In Alan Bundy editor 12th International Conference on Automated Deduction volume 814 of Lecture Notes in Computer Science pages 821--825. Springer 1994.","DOI":"10.1007\/3-540-58156-1_68"},{"key":"e_1_3_2_1_7_1","first-page":"198","volume-title":"Carre\u00f1o et al. {2002}","author":"Felty Amy P.","unstructured":"Amy P. Felty . Two-level meta-reasoning in Coq . In Carre\u00f1o et al. {2002} , pages 198 -- 213 . Amy P. Felty. Two-level meta-reasoning in Coq. In Carre\u00f1o et al. {2002}, pages 198--213."},{"key":"e_1_3_2_1_8_1","volume-title":"Felty and Alberto Momigliano. Hybrid: A definitional two-level approach to reasoning with higher-order abstract syntax. CoRR, abs\/0811.4367","author":"Amy","year":"2008","unstructured":"Amy P. Felty and Alberto Momigliano. Hybrid: A definitional two-level approach to reasoning with higher-order abstract syntax. CoRR, abs\/0811.4367 , 2008 . Amy P. Felty and Alberto Momigliano. Hybrid: A definitional two-level approach to reasoning with higher-order abstract syntax. CoRR, abs\/0811.4367, 2008."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71070-7_13"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2008.33"},{"key":"e_1_3_2_1_11_1","first-page":"561","volume-title":"Higher Order Logic Theorem Proving and its Applications","author":"Gunter Elsa L.","year":"1992","unstructured":"Elsa L. Gunter . Why we can't have SML-style datatype declarations in HOL . In Luc J.M. Claesen and Michael J.C. Gordon, editors, Higher Order Logic Theorem Proving and its Applications , volume A-20 , pages 561 -- 568 . North-Holland\/Elsevier , 1992 . Elsa L. Gunter. Why we can't have SML-style datatype declarations in HOL. In Luc J.M. Claesen and Michael J.C. Gordon, editors, Higher Order Logic Theorem Proving and its Applications, volume A-20, pages 561--568. North-Holland\/Elsevier, 1992."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796807006430"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"crossref","unstructured":"Furio\n      Honsell Marino\n      Miculan and \n      Ivan\n      Scagnetto\n    .\n  An axiomatic approach to metareasoning on nominal algebras in HOAS\n  . In Fernando Orejas Paul G. Spirakis and Jan van Leeuwen editors 28th International Colloquium on Automata Languages and Programming volume \n  2076\n   of \n  Lecture Notes in Computer Science pages \n  963\n  --\n  978\n  . \n  Springer 2001\n  .   Furio Honsell Marino Miculan and Ivan Scagnetto. An axiomatic approach to metareasoning on nominal algebras in HOAS. In Fernando Orejas Paul G. Spirakis and Jan van Leeuwen editors 28th International Colloquium on Automata Languages and Programming volume 2076 of Lecture Notes in Computer Science pages 963--978. Springer 2001.","DOI":"10.1007\/3-540-48224-5_78"},{"key":"e_1_3_2_1_14_1","volume-title":"Hybrid: A package for higher-order syntax in Isabelle and Coq. www.hybrid.dsi.unimi.it","author":"Hybrid Group","year":"2009","unstructured":"Hybrid Group . Hybrid: A package for higher-order syntax in Isabelle and Coq. www.hybrid.dsi.unimi.it , 2009 . Hybrid Group. Hybrid: A package for higher-order syntax in Isabelle and Coq. www.hybrid.dsi.unimi.it, 2009."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/504077.504080"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1006294005493"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1094622.1094628"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"crossref","unstructured":"Dale\n      Miller\n     and \n      Alwen Fernanto\n      Tiu\n    .\n  Encoding generic judgments\n  . In Manindra Agrawal and Anil Seth editors 22nd Conference on Foundations of Software Technology and Theoretical Computer Science volume \n  2556\n   of \n  Lecture Notes in Computer Science pages \n  18\n  --\n  32\n  . \n  Springer 2002\n  .   Dale Miller and Alwen Fernanto Tiu. Encoding generic judgments. In Manindra Agrawal and Anil Seth editors 22nd Conference on Foundations of Software Technology and Theoretical Computer Science volume 2556 of Lecture Notes in Computer Science pages 18--32. Springer 2002.","DOI":"10.1007\/3-540-36206-1_3"},{"key":"e_1_3_2_1_20_1","series-title":"Lecture Notes in Computer Science","first-page":"293","volume-title":"Types for Proofs and Programs","author":"Momigliano Alberto","year":"2003","unstructured":"Alberto Momigliano and Alwen Fernanto Tiu . Induction and co-induction in sequent calculus . In Stefano Berardi, Mario Coppo, and Ferruccio Damiani, editors, Types for Proofs and Programs , International Workshop, TYPES 2003 , Revised Selected Papers, volume 3085 of Lecture Notes in Computer Science , pages 293 -- 308 . Springer , 2003. Alberto Momigliano and Alwen Fernanto Tiu. Induction and co-induction in sequent calculus. In Stefano Berardi, Mario Coppo, and Ferruccio Damiani, editors, Types for Proofs and Programs, International Workshop, TYPES 2003, Revised Selected Papers, volume 3085 of Lecture Notes in Computer Science, pages 293--308. Springer, 2003."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2007.09.019"},{"key":"e_1_3_2_1_22_1","series-title":"phLecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"A Proof Assistant for Higher-Order Logic","author":"Nipkow Tobias","year":"2002","unstructured":"Tobias Nipkow , Lawrence C. Paulson , and Markus Wenzel . Isabelle\/HOL : A Proof Assistant for Higher-Order Logic , volume 2283 of phLecture Notes in Computer Science . Springer , 2002 . Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle\/HOL: A Proof Assistant for Higher-Order Logic, volume 2283 of phLecture Notes in Computer Science. Springer, 2002."},{"key":"e_1_3_2_1_23_1","volume-title":"isabelle.in.tum.de\/nominal\/","author":"Nominal Methods Group","year":"2009","unstructured":"Nominal Methods Group . Nominal Isabelle . isabelle.in.tum.de\/nominal\/ , 2009 . Nominal Methods Group. Nominal Isabelle. isabelle.in.tum.de\/nominal\/, 2009."},{"key":"e_1_3_2_1_24_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"328","DOI":"10.1007\/BFb0037116","volume-title":"International Conference on Typed Lambda Calculi and Applications","author":"Paulin-Mohring Christine","year":"1993","unstructured":"Christine Paulin-Mohring . Inductive definitions in the system Coq: Rules and properties . In M. Bezem and J.F. Groote, editors, International Conference on Typed Lambda Calculi and Applications , volume 664 of Lecture Notes in Computer Science , pages 328 -- 345 . Springer , 1993 . Christine Paulin-Mohring. Inductive definitions in the system Coq: Rules and properties. In M. Bezem and J.F. Groote, editors, International Conference on Typed Lambda Calculi and Applications, volume 664 of Lecture Notes in Computer Science, pages 328--345. Springer, 1993."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"crossref","unstructured":"Lawrence C.\n      Paulson\n    .\n  A fixed point approach to implementing (co)inductive definitions\n  . In Alan Bundy editor 12th International Conference on Automated Deduction volume \n  814\n   of \n  Lecture Notes in Computer Science pages \n  148\n  --\n  161\n  . \n  Springer 1994\n  .   Lawrence C. Paulson. A fixed point approach to implementing (co)inductive definitions. In Alan Bundy editor 12th International Conference on Automated Deduction volume 814 of Lecture Notes in Computer Science pages 148--161. Springer 1994.","DOI":"10.1007\/3-540-58156-1_11"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"crossref","unstructured":"Frank\n      Pfenning\n     and \n      Carsten\n      Sch\u00fcrmann\n    .\n  System description: Twelf -- a meta-logical framework for deductive systems\n  . In H. Ganzinger editor 16th International Conference on Automated Deduction volume \n  1632\n   of \n  Lecture Notes in Computer Science pages \n  202\n  --\n  206\n  . \n  Springer 1999\n  .   Frank Pfenning and Carsten Sch\u00fcrmann. System description: Twelf -- a meta-logical framework for deductive systems. In H. Ganzinger editor 16th International Conference on Automated Deduction volume 1632 of Lecture Notes in Computer Science pages 202--206. Springer 1999.","DOI":"10.1007\/3-540-48660-7_14"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-005-6534-3"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"crossref","unstructured":"Brigitte\n      Pientka\n    .\n  Proof pearl: The power of higher-order encodings in the logical framework lf\n  . In Klaus Schneider and Jens Brandt editors 20th International Conference on Theorem Proving in Higher Order Logics volume \n  4732\n   of \n  Lecture Notes in Computer Science pages \n  246\n  --\n  261\n  . \n  Springer 2007\n  .   Brigitte Pientka. Proof pearl: The power of higher-order encodings in the logical framework lf. In Klaus Schneider and Jens Brandt editors 20th International Conference on Theorem Proving in Higher Order Logics volume 4732 of Lecture Notes in Computer Science pages 246--261. Springer 2007.","DOI":"10.1007\/978-3-540-74591-4_19"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00138-X"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"crossref","unstructured":"Carsten\n      Sch\u00fcrmann\n    .\n  A type-theoretic approach to induction with higher-order encodings\n  . In Robert Nieuwenhuis and Andrei Voronkov editors 8th International Conference Logic for Programming Artificial Intelligence and Reasoning volume \n  2250\n   of \n  Lecture Notes in Computer Science pages \n  266\n  --\n  281\n  . \n  Springer 2001\n  .   Carsten Sch\u00fcrmann. A type-theoretic approach to induction with higher-order encodings. In Robert Nieuwenhuis and Andrei Voronkov editors 8th International Conference Logic for Programming Artificial Intelligence and Reasoning volume 2250 of Lecture Notes in Computer Science pages 266--281. Springer 2001.","DOI":"10.1007\/3-540-45653-8_18"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"crossref","unstructured":"Carsten\n      Sch\u00fcrmann\n     and \n      Frank\n      Pfenning\n    .\n  A coverage checking algorithm for LF\n  . In David A. Basin and Burkhart Wolff editors 16th International Conference on Theorem Proving in Higher Order Logics volume \n  2758\n   of \n  Lecture Notes in Computer Science pages \n  120\n  --\n  135\n  . \n  Springer 2003\n  .  Carsten Sch\u00fcrmann and Frank Pfenning. A coverage checking algorithm for LF. In David A. Basin and Burkhart Wolff editors 16th International Conference on Theorem Proving in Higher Order Logics volume 2758 of Lecture Notes in Computer Science pages 120--135. Springer 2003.","DOI":"10.1007\/10930755_8"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(93)90095-B"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2007.01.016"}],"event":{"name":"PPDP '09: Principles and Practice of Declarative Programming","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","ACM Association for Computing Machinery"],"location":"Coimbra Portugal","acronym":"PPDP '09"},"container-title":["Proceedings of the 11th ACM SIGPLAN conference on Principles and practice of declarative programming"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1599410.1599422","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1599410.1599422","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T12:18:15Z","timestamp":1750249095000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1599410.1599422"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,9,7]]},"references-count":32,"alternative-id":["10.1145\/1599410.1599422","10.1145\/1599410"],"URL":"https:\/\/doi.org\/10.1145\/1599410.1599422","relation":{},"subject":[],"published":{"date-parts":[[2009,9,7]]},"assertion":[{"value":"2009-09-07","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}