Simon Ambler, Roy Crole & Alberto Momigliano (2002):
Combining Higher Order Abstract Syntax with Tactical Theorem Proving and (Co)Induction.
In: 15th International Conference on Theorem Proving in Higher Order Logics,
LNCS 2410.
Springer,
pp. 13–30,
doi:10.1007/3-540-45685-6\voidb@x .06em width.4em height-.2pt depth.6pt .06em 3.
N. G. de Bruijn (1972):
Lambda-calculus notation with nameless dummies: a tool for automatic formula manipulation with application to the Church-Rosser theorem.
Indagationes Mathematicae 34(5),
pp. 381–392.
Venanzio Capretta & Amy P. Felty (2009):
Higher-Order Abstract Syntax in Type Theory.
In: Logic Colloquium '06,
ASL Lecture Notes in Logic 32.
Cambridge University Press,
pp. 65–90.
Joëlle Despeyroux, Amy Felty & André Hirschowitz (1995):
Higher-Order Abstract Syntax in Coq.
In: 2nd International Conference on Typed Lambda Calculi and Applications,
LNCS 902.
Springer,
pp. 124–138,
doi:10.1007/BFb0014049.
Amy Felty & Alberto Momigliano (2010):
Web appendix of the paper ``Hybrid: a Definitional Two Level Approach to Reasoning with Higher Order Abstract Syntax'' felty/momigliano:2008.
http://hybrid.dsi.unimi.it/jar/index.html.
Amy P. Felty & AlbertoMomigliano (2010):
Hybrid: A Definitional Two-Level Approach to Reasoning with Higher-Order Abstract Syntax,
doi:10.1007/s10817-010-9194-x.
To appear in Journal of Automated Reasoning. Available at Springer Online First (http://www.springerlink.com/content/92q14113413462t0/).
Murdoch Gabbay & Andrew M. Pitts (2002):
A New Approach to Abstract Syntax with Variable Binding.
Formal Aspects of Computing 13(3–5),
pp. 341–363,
doi:10.1007/s001650200016.
Alan J. Martin (2010).
http://hybrid.dsi.unimi.it/martinPhD/.
Isabelle/HOL theory files.
Alan J. Martin (2010):
Reasoning Using Higher-Order Abstract Syntax in a Higher-Order Logic Proof Environment: Improvements to Hybrid and a Case Study.
University of Ottawa.
Alberto Momigliano, Simon Ambler & Roy L. Crole (2002):
A Hybrid Encoding of Howe's Method for Establishing Congruence of Bisimilarity.
Electronic Notes in Theoretical Computer Science 70(2),
pp. 60–75,
doi:10.1016/S1571-0661(04)80506-1.
Proceedings of LFM'02.
Alberto Momigliano, Alan J. Martin & Amy P. Felty (2008):
Two-Level Hybrid: A System for Reasoning Using Higher-Order Abstract Syntax.
Electronic Notes in Theoretical Computer Science 196,
pp. 85–93,
doi:10.1016/j.entcs.2007.09.019.
Proceedings of LFMTP'07.
Tobias Nipkow, Lawrence C. Paulson & Markus Wenzel (2002):
Isabelle/HOL: A Proof Assistant for Higher-Order Logic.
LNCS 2283.
Springer.
Tobias Nipkow, LawrenceC. Paulson & Markus Wenzel (2011):
Isabelle's Logics: HOL.
http://isabelle.in.tum.de/doc/logics-HOL.pdf.
Accessed July 2011.
Michael Norrish (2006):
Mechanising λ-Calculus using a Classical First Order Theory of Terms with Permutations.
Journal of Higher Order Symbolic Computation 19(2–3),
pp. 169–195,
doi:10.1007/s10990-006-8745-7.
Brigitte Pientka & Joshua Dunfield (2010):
Beluga:A Framework for Programming and Reasoning with Deductive Systems (System Description).
In: 5th International Joint Conference on Automated Reasoning,
LNCS 6173.
Springer,
pp. 15–21,
doi:10.1007/978-3-642-14203-1\voidb@x .06em width.4em height-.2pt depth.6pt .06em 2.
Andrew M. Pitts (2003):
Nominal Logic, a First Order Theory of Names and Binding.
Information and Computation 186(2),
pp. 165–193,
doi:10.1016/S0890-5401(03)00138-X.
Andrei Popescu, Elsa L. Gunter & Christopher J. Osborn (2010):
Strong Normalization for System F by HOAS on Top of FOAS.
In: 25th Annual IEEE Symposium on Logic in Computer Science,
pp. 31–40,
doi:10.1109/LICS.2010.48.
Christian Urban (2008):
Nominal Techniques in Isabelle/HOL.
Journal of Automated Reasoning 40(4),
pp. 327–356,
doi:10.1007/s10817-008-9097-2.
eptcs@eptcs.org