Publications

• 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 Library.
• 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, Coq formalization).
• A. Momigliano, A. Martin and A. Felty. Two-level Hybrid: A System for Reasoning using HOAS. (PDF). LFMTP 2007, August 2007. Appeared in ENTCS, Volume 196, Pages 85-93. (22 Jan 2008).
• A.Felty and A.M. Reasoning with Hypothetical Judgments and Open Terms in Hybrid. PPDP 2009
• A.Felty and B.Pientka. Reasoning 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]