- A. Momigliano, Simon Ambler and Roy Crole. Combining Higher Order
Abstract Syntax with Tactical Theorem Proving and (Co)Induction. In
15th International Conference on Theorem Proving in Higher Order Logics
(TPHOLs02), Hampton, VA, 20-23 August 2002 PDF,
LNCS @ Springer-Verlag.
- A. Momigliano, Simon Ambler and Roy Crole. A Hybrid Encoding of
Howe's Method for Establishing Congruence of Bisimilarity. LFM'02,
Volume 70.2 of ENTCS (PDF)
- Amy P. Felty. Two-Level Meta-Reasoning in Coq. In Fifteenth
International Conference on Theorem Proving in Higher Order Logics,
Springer-Verlag LNCS 2410, August 2002. (PS).
- A. Momigliano and Simon Ambler. Multi-Level Meta-Reasoning with
Higher Order Abstract Syntax. Foundations of Software Science and
Computational Structures 6th International Conference, FOSSACS 2003, PDF
- A. Momigliano and Jeff Polakow. A Formalization of an Ordered
Logical Framework in Hybrid with Applications to Continuation
Machines, June 2003. MERLIN 2003 @ACM Press. Link, ACM Digital
- Venanzio Capretta and Amy Felty. Combining de Bruijn Indices and
Higher-Order Abstract Syntax in Coq by . In Proceedings of TYPES 2006,
LNCS @ Springer-Verlag. (postscript,
Momigliano, A. Martin and A. Felty. Two-level Hybrid:
A System for Reasoning using HOAS. (PDF).
2007, August 2007. Appeared in ENTCS, Volume 196, Pages 85-93. (22
- A.Felty and A.M.
Reasoning with Hypothetical
Judgments and Open Terms in Hybrid. PPDP
- A.Felty and B.Pientka.
with Higher-Order Abstract Syntax and Contexts: A Comparison. ITP 2010. July 2010. [DOI].
- A.Felty and A. Momigliano. Hybrid: a
Definitional Two-Level Approach
to Reasoning with Higher
Order Abstract Syntax. Journal of Automated Reasoning, July 2010. [DOI]