| 2022 | ITP | Modelling and Verifying Properties of Biological Neural Networks (Invited Talk). | Amy P. Felty |
| 2020 | VECoS | Formal Verification of a Certified Policy Language. | Amir Eaman, Amy P. Felty |
| 2019 | CPP | A linear logical framework in hybrid (invited talk). | Amy P. Felty |
| 2017 | PST | A Certified Core Policy Language. | Bahman Sistany, Amy P. Felty |
| 2016 | CPP | A verified algorithm for detecting conflicts in XACML access control rules. | Michel St-Martin, Amy P. Felty |
| 2013 | CADE | Translating Higher-Order Specifications to Coq Libraries Supporting Hybrid Proofs. | Nada Habli, Amy P. Felty |
| 2011 | PST | Advantages of a non-technical XACML notation in role-based models. | Bernard Stepien, Stan Matwin, Amy P. Felty |
| 2011 | PST | An implementation of a verification condition generator for foundational proof-carrying code. | Jiangong Weng, Amy P. Felty |
| 2010 | ICFP | Hybrid: Reasoning with Higher-Order Abstract Syntax in Coq and Isabelle. | Amy P. Felty |
| 2010 | ITP | Reasoning with Higher-Order Abstract Syntax and Contexts: A Comparison. | Amy P. Felty, Brigitte Pientka |
| 2009 | PPDP | Reasoning with hypothetical judgments and open terms in hybrid. | Amy P. Felty, Alberto Momigliano |
| 2008 | GECCO | Genetic programming with polymorphic types and higher-order functions. | Franck Binard, Amy P. Felty |
| 2007 | CCS | Formal correctness of conflict detection for firewalls. | Venanzio Capretta, Bernard Stepien, Amy P. Felty, Stan Matwin |
| 2007 | GECCO | An abstraction-based genetic programming system. | Franck Binard, Amy P. Felty |
| 2005 | CADE | Privacy-Sensitive Information Flow with JML. | Guillaume Dufay, Amy P. Felty, Stan Matwin |
| 2000 | POPL | A Semantic Model of Types and Machine Instructions for Proof-Carrying Code. | Andrew W. Appel, Amy P. Felty |
| 1999 | CADE | Formal Metatheory using Implicit Syntax, and an Application to Data Abstraction for Asynchronous Systems. | Amy P. Felty, Douglas J. Howe, Abhik Roychoudhury |
| 1999 | ICLP | Lightweight Lemmas in lambda-Prolog. | Andrew W. Appel, Amy P. Felty |
| 1998 | CAV | Protocol Verification in Nuprl. | Amy P. Felty, Douglas J. Howe, Frank A. Stomp |
| 1997 | CADE | Hybrid Interactive Theorem Proving Using Nuprl and HOL. | Amy P. Felty, Douglas J. Howe |
| 1996 | CADE | Proof Search with Set Variable Instantiation in the Calculus of Constructions. | Amy P. Felty |
| 1994 | CADE | Tactic Theorem Proving with Refinement-Tree Proofs and Metavariables. | Amy P. Felty, Douglas J. Howe |
| 1994 | LPAR | Generalization and Reuse of Tactic Proofs. | Amy P. Felty, Douglas J. Howe |
| 1993 | LICS | Encoding the Calculus of Constructions in a Higher-Order Logic | Amy P. Felty |
| 1990 | CADE | Tutorial on Lambda-Prolog. | Amy P. Felty, Elsa L. Gunter, Dale Miller, Frank Pfenning |
| 1990 | CADE | Encoding a Dependent-Type Lambda-Calculus in a Logic Programming Language. | Amy P. Felty, Dale Miller |
| 1988 | CADE | Lambda-Prolog: An Extended Logic Programming Language. | Amy P. Felty, Elsa L. Gunter, John Hannan, Dale Miller, Gopalan Nadathur, Andre Scedrov |
| 1988 | CADE | Specifying Theorem Provers in a Higher-Order Logic Programming Language. | Amy P. Felty, Dale Miller |
| 1986 | AAAI | An Integration of Resolution and Natural Deduction Theorem Proving. | Dale Miller, Amy P. Felty |