@inproceedings(ambler/crole/momigliano:2002, author = "Simon Ambler and Roy Crole and Alberto Momigliano", year = "2002", title = "Combining Higher Order Abstract Syntax with Tactical Theorem Proving and (Co)Induction", booktitle = "15th International Conference on Theorem Proving in Higher Order Logics", series = "LNCS", volume = "2410", publisher = "Springer", pages = "13--30", doi = "10.1007/3-540-45685-6\relax \unhbox \voidb@x \kern .06em \vrule width.4em height-.2pt depth.6pt \kern .06em \relax 3", ) @article(debruijn:1972, author = "N. G. de Bruijn", year = "1972", title = "Lambda-calculus notation with nameless dummies: a tool for automatic formula manipulation with application to the {Church-Rosser} theorem", journal = "Indagationes Mathematicae", volume = "34", number = "5", pages = "381--392", ) @inproceedings(capretta/felty:2006, author = "Venanzio Capretta and Amy P. Felty", year = "2007", title = "Combining de {B}ruijn Indices and Higher-Order Abstract Syntax in {C}oq", booktitle = "Types for Proofs and Programs, Intl.\ Workshop, TYPES 2006", series = "LNCS", volume = "4502", publisher = "Springer", pages = "63--77", doi = "10.1007/978-3-540-74464-1\relax \unhbox \voidb@x \kern .06em \vrule width.4em height-.2pt depth.6pt \kern .06em \relax 5", ) @inproceedings(capretta/felty:2009, author = "Venanzio Capretta and Amy P. Felty", year = "2009", title = "Higher-Order Abstract Syntax in Type Theory", booktitle = "Logic Colloquium '06", series = "ASL Lecture Notes in Logic", volume = "32", publisher = "Cambridge University Press", pages = "65--90", ) @inproceedings(despeyroux/felty/hirschowitz:1995, author = "Jo{\"e}lle Despeyroux and Amy Felty and Andr{\'e} Hirschowitz", year = "1995", title = "Higher-Order Abstract Syntax in {Coq}", booktitle = "2nd International Conference on Typed Lambda Calculi and Applications", series = "LNCS", volume = "902", publisher = "Springer", pages = "124--138", doi = "10.1007/BFb0014049", ) @misc(felty/momigliano:2010, author = "Amy Felty and Alberto Momigliano", year = "2010", title = "Web appendix of the paper ``{H}ybrid: a Definitional Two Level Approach to Reasoning with Higher Order Abstract Syntax'' \cite {felty/momigliano:2008}", howpublished = "\url {http://hybrid.dsi.unimi.it/jar/index.html}", ) @inproceedings(felty/pientka:ITP2011, author = "Amy Felty and Brigitte Pientka", year = "2010", title = "Reasoning with Higher-Order Abstract Syntax and Contexts: A Comparison", booktitle = "International Conference on Interactive Theorem Proving", series = "LNCS", volume = "6172", publisher = "Springer", pages = "227--242", doi = "10.1007/978-3-642-14052-5\relax \unhbox \voidb@x \kern .06em \vrule width.4em height-.2pt depth.6pt \kern .06em \relax 17", ) @unpublished(felty/momigliano:2008, author = "Amy P. Felty and Alberto{\relax \unhcopy \strutbox } Momigliano", year = "2010", title = "{H}ybrid: A Definitional Two-Level Approach to Reasoning with Higher-Order Abstract Syntax", doi = "10.1007/s10817-010-9194-x", note = "To appear in \emph {Journal of Automated Reasoning}. Available at Springer Online First (\url {http://www.springerlink.com/content/92q14113413462t0/)}", ) @article(GabbayPitts:FAC2002, author = "Murdoch Gabbay and Andrew M. Pitts", year = "2002", title = "A New Approach to Abstract Syntax with Variable Binding", journal = "Formal Aspects of Computing", volume = "13", number = "3--5", pages = "341--363", doi = "10.1007/s001650200016", ) @inproceedings(gacek:2008, author = "Andrew Gacek", year = "2008", title = "The {Abella} Interactive Theorem Prover (System Description)", booktitle = "4th Intl.\ Joint Conf.\ on Automated Reasoning", series = "LNCS", volume = "5195", publisher = "Springer", pages = "154--161", doi = "10.1007/978-3-540-71070-7\relax \unhbox \voidb@x \kern .06em \vrule width.4em height-.2pt depth.6pt \kern .06em \relax 13", ) @misc(martin:2010b, author = "Alan J. Martin", year = "2010", howpublished = "\url {http://hybrid.dsi.unimi.it/martinPhD/}", note = "{I}sabelle/\penalty \exhyphenpenalty {HOL} theory files", ) @phdthesis(martin:2010a, author = "Alan J. Martin", year = "2010", title = "Reasoning Using Higher-Order Abstract Syntax in a Higher-Order Logic Proof Environment: Improvements to {H}ybrid and a Case Study", school = "University of Ottawa", ) @article(momigliano/ambler/crole:2002, author = "Alberto Momigliano and Simon Ambler and Roy L. Crole", year = "2002", title = "A {H}ybrid Encoding of {H}owe's Method for Establishing Congruence of Bisimilarity", journal = "Electronic Notes in Theoretical Computer Science", volume = "70", number = "2", pages = "60--75", doi = "10.1016/S1571-0661(04)80506-1", note = "Proceedings of LFM'02", ) @article(momigliano/martin/felty:2008, author = "Alberto Momigliano and Alan J. Martin and Amy P. Felty", year = "2008", title = "Two-Level {H}ybrid: A System for Reasoning Using Higher-Order Abstract Syntax", journal = "Electronic Notes in Theoretical Computer Science", volume = "196", pages = "85--93", doi = "10.1016/j.entcs.2007.09.019", note = "Proceedings of LFMTP'07", ) @book(nipkow/paulson/wenzel:2002, author = "Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel", year = "2002", title = "Isabelle/{HOL}: A Proof Assistant for Higher-Order Logic", series = "LNCS", volume = "2283", publisher = "Springer", ) @misc(nipkow/paulson/wenzel:2011, author = "Tobias Nipkow and Lawrence{\relax \unhcopy \strutbox } C. Paulson and Markus Wenzel", year = "2011", title = "Isabelle's Logics: {HOL}", howpublished = "\url {http://isabelle.in.tum.de/doc/logics-HOL.pdf}", note = "Accessed July 2011", ) @article(Norrish:HOSC2006, author = "Michael Norrish", year = "2006", title = "Mechanising $\lambda $-Calculus using a Classical First Order Theory of Terms with Permutations", journal = "Journal of Higher Order Symbolic Computation", volume = "19", number = "2--3", pages = "169--195", doi = "10.1007/s10990-006-8745-7", ) @inproceedings(pfenning/schurmann:1999, author = "Frank Pfenning and Carsten Sch{\"u}rmann", year = "1999", title = "System Description: {T}welf --- {A} Meta-Logical Framework for Deductive Systems", booktitle = "16th Intl.\ Conf.\ on Automated Deduction", series = "LNCS", volume = "1632", publisher = "Springer", pages = "202--206", doi = "10.1007/3-540-48660-7\relax \unhbox \voidb@x \kern .06em \vrule width.4em height-.2pt depth.6pt \kern .06em \relax 14", ) @inproceedings(pientka/dunfield:2010, author = "Brigitte Pientka and Joshua Dunfield", year = "2010", title = "Beluga:A Framework for Programming and Reasoning with Deductive Systems (System Description)", booktitle = "5th International Joint Conference on Automated Reasoning", series = "LNCS", volume = "6173", publisher = "Springer", pages = "15--21", doi = "10.1007/978-3-642-14203-1\relax \unhbox \voidb@x \kern .06em \vrule width.4em height-.2pt depth.6pt \kern .06em \relax 2", ) @article(Pitts:IandC2003, author = "Andrew M. Pitts", year = "2003", title = "Nominal Logic, a First Order Theory of Names and Binding", journal = "Information and Computation", volume = "186", number = "2", pages = "165--193", doi = "10.1016/S0890-5401(03)00138-X", ) @inproceedings(popescu/gunter/osborn:2010, author = "Andrei Popescu and Elsa L. Gunter and Christopher J. Osborn", year = "2010", title = "Strong Normalization for System {F} by {HOAS} on Top of {FOAS}", booktitle = "25th Annual IEEE Symposium on Logic in Computer Science", pages = "31--40", doi = "10.1109/LICS.2010.48", ) @article(Urban:JAR2008, author = "Christian Urban", year = "2008", title = "Nominal Techniques in Isabelle/HOL", journal = "Journal of Automated Reasoning", volume = "40", number = "4", pages = "327--356", doi = "10.1007/s10817-008-9097-2", )