An Integration of Resolution and Natural Deduction Theorem Proving. - Dale Miller 001; Amy P. Felty (AAAI, 1986)

Lambda-Prolog: An Extended Logic Programming Language. - Amy P. Felty; Elsa L. Gunter; John Hannan; Dale Miller 001; Gopalan Nadathur; Andre Scedrov (CADE, 1988)

Specifying Theorem Provers in a Higher-Order Logic Programming Language. - Amy P. Felty; Dale Miller 001 (CADE, 1988)

A Logic Program for Transforming Sequent Proofs to Natural Deduction Proofs. - Amy P. Felty (ELP, 1989)

Tutorial on Lambda-Prolog. - Amy P. Felty; Elsa L. Gunter; Dale Miller 001; Frank Pfenning (CADE, 1990)

Encoding a Dependent-Type Lambda-Calculus in a Logic Programming Language. - Amy P. Felty; Dale Miller 001 (CADE, 1990)

A Logic Programming Approach to Implementing Higher-Order Term Rewriting. - Amy P. Felty (ELP, 1991)

Encoding the Calculus of Constructions in a Higher-Order Logic - Amy P. Felty (LICS, 1993)

Definite Clause Grammars for Parsing Higher-Order Syntax. - Amy P. Felty (ILPS, 1993)

Implementing Tactics and Tacticals in a Higher-Order Logic Programming Language. - Amy P. Felty (J. Autom. Reason., 1993)

Tactic Theorem Proving with Refinement-Tree Proofs and Metavariables. - Amy P. Felty; Douglas J. Howe (CADE, 1994)

Generalization and Reuse of Tactic Proofs. - Amy P. Felty; Douglas J. Howe (LPAR, 1994)

Formalizing Inductive Proofs of Network Algorithms. - Ramesh Bharadwaj; Amy P. Felty; Frank A. Stomp (ASIAN, 1995)

Higher-Order Abstract Syntax in Coq. - Joëlle Despeyroux; Amy P. Felty; André Hirschowitz (TLCA, 1995)

Proof Search with Set Variable Instantiation in the Calculus of Constructions. - Amy P. Felty (CADE, 1996)

Hybrid Interactive Theorem Proving Using Nuprl and HOL. - Amy P. Felty; Douglas J. Howe (CADE, 1997)

Interactive Theorem Proving with Temporal Logic. - Amy P. Felty; Laurent Théry (J. Symb. Comput., 1997)

Protocol Verification in Nuprl. - Amy P. Felty; Douglas J. Howe; Frank A. Stomp (CAV, 1998)

Formal Metatheory using Implicit Syntax, and an Application to Data Abstraction for Asynchronous Systems. - Amy P. Felty; Douglas J. Howe; Abhik Roychoudhury (CADE, 1999)

Lightweight Lemmas in lambda-Prolog. - Andrew W. Appel; Amy P. Felty (ICLP, 1999)

Cache Coherency in SCI: Specification and a Sketch of Correctness. - Amy P. Felty; Frank A. Stomp (Formal Aspects Comput., 1999)

Feature Specification and Automatic Conflict Detection. - Amy P. Felty; Kedar S. Namjoshi (FIW, 2000)

A Semantic Model of Types and Machine Instructions for Proof-Carrying Code. - Andrew W. Appel; Amy P. Felty (POPL, 2000)

The calculus of constructions as a framework for proof search with set variable instantiation. - Amy P. Felty (Theor. Comput. Sci., 2000)

Current Trends in Logical Frameworks and Metalanguages. - David A. Basin; Amy P. Felty (J. Autom. Reason., 2001)

Privacy-Oriented Data Mining by Proof Checking. - Amy P. Felty; Stan Matwin (PKDD, 2002)

Two-Level Meta-reasoning in Coq. - Amy P. Felty (TPHOLs, 2002)

Preface. - Amy P. Felty (J. Autom. Reason., 2003)

Feature specification and automated conflict detection. - Amy P. Felty; Kedar S. Namjoshi (ACM Trans. Softw. Eng. Methodol., 2003)

Dependent types ensure partial correctness of theorem provers. - Andrew W. Appel; Amy P. Felty (J. Funct. Program., 2004)

Polymorphic Lemmas and Definitions in lambda-Prolog and Twelf. - Andrew W. Appel; Amy P. Felty (Theory Pract. Log. Program., 2004)

Privacy-Sensitive Information Flow with JML. - Guillaume Dufay; Amy P. Felty; Stan Matwin (CADE, 2005)

A Tutorial Example of the Semantic Approach to Foundational Proof-Carrying Code. - Amy P. Felty (RTA, 2005)

A Tutorial Example of the Semantic Approach to Foundational Proof-Carrying Code: Abstract. - Amy P. Felty (TLCA, 2005)

Privacy in Data Mining Using Formal Methods. - Stan Matwin; Amy P. Felty; István T. Hernádvölgyi; Venanzio Capretta (TLCA, 2005)

Combining de Bruijn Indices and Higher-Order Abstract Syntax in Coq. - Venanzio Capretta; Amy P. Felty (TYPES, 2006)

Formal correctness of conflict detection for firewalls. - Venanzio Capretta; Bernard Stepien; Amy P. Felty; Stan Matwin (FMSE, 2007)

An abstraction-based genetic programming system. - Franck Binard; Amy P. Felty (GECCO (Companion), 2007)

Two-Level Hybrid: A System for Reasoning Using Higher-Order Abstract Syntax. - Alberto Momigliano; Alan J. Martin; Amy P. Felty (LFMTP@CADE, 2007)

Tutorial Examples of the Semantic Approach to Foundational Proof-Carrying Code. - Amy P. Felty (Fundam. Informaticae, 2007)

Genetic programming with polymorphic types and higher-order functions. - Franck Binard; Amy P. Felty (GECCO, 2008)

A Non-technical User-Oriented Display Notation for XACML Conditions. - Bernard Stepien; Amy P. Felty; Stan Matwin (MCETECH, 2009)

Reasoning with hypothetical judgments and open terms in hybrid. - Amy P. Felty; Alberto Momigliano (PPDP, 2009)

Strategies for Reducing Risks of Inconsistencies in Access Control Policies. - Bernard Stepien; Stan Matwin; Amy P. Felty (ARES, 2010)

Hybrid: Reasoning with Higher-Order Abstract Syntax in Coq and Isabelle. - Amy P. Felty (MSFP@ICFP, 2010)

Reasoning with Higher-Order Abstract Syntax and Contexts: A Comparison. - Amy P. Felty; Brigitte Pientka (ITP, 2010)

Advantages of a non-technical XACML notation in role-based models. - Bernard Stepien; Stan Matwin; Amy P. Felty (PST, 2011)

An implementation of a verification condition generator for foundational proof-carrying code. - Jiangong Weng; Amy P. Felty (PST, 2011)

An Improved Implementation and Abstract Interface for Hybrid - Alan J. Martin; Amy P. Felty (LFMTP, 2011)

An Algorithm for Compression of XACML Access Control Policy Sets by Recursive Subsumption. - Bernard Stepien; Stan Matwin; Amy P. Felty (ARES, 2012)

Hybrid - A Definitional Two-Level Approach to Reasoning with Higher-Order Abstract Syntax. - Amy P. Felty; Alberto Momigliano (J. Autom. Reason., 2012)

Translating Higher-Order Specifications to Coq Libraries Supporting Hybrid Proofs. - Nada Habli; Amy P. Felty (PxTP@CADE, 2013)

Challenges of Composing XACML Policies. - Bernard Stepien; Amy P. Felty; Stan Matwin (ARES, 2014)

A non-technical XACML target editor for dynamic access control systems. - Bernard Stepien; Amy P. Felty; Stan Matwin (CTS, 2014)

A Logical Framework for Systems Biology. - Elisabetta De Maria; Joëlle Despeyroux; Amy P. Felty (FMMB, 2014)

The Next 700 Challenge Problems for Reasoning with Higher-Order Abstract Syntax Representations: Part 1-A Common Infrastructure for Benchmarks. - Amy P. Felty; Alberto Momigliano; Brigitte Pientka (CoRR, 2015)

An Open Challenge Problem Repository for Systems Supporting Binders. - Amy P. Felty; Alberto Momigliano; Brigitte Pientka (LFMTP, 2015)

The Next 700 Challenge Problems for Reasoning with Higher-Order Abstract Syntax Representations - Part 2 - A Survey. - Amy P. Felty; Alberto Momigliano; Brigitte Pientka (J. Autom. Reason., 2015)

Using Expert Systems to Statically Detect "Dynamic" Conflicts in XACML. - Bernard Stepien; Amy P. Felty (ARES, 2016)

A verified algorithm for detecting conflicts in XACML access control rules. - Michel St-Martin; Amy P. Felty (CPP, 2016)

The Logic of Hereditary Harrop Formulas as a Specification Logic for Hybrid. - Chelsea Battell; Amy P. Felty (LFMTP, 2016)

Review of Existing Analysis Tools for SELinux Security Policies: Challenges and a Proposed Solution. - Amir Eaman; Bahman Sistany; Amy P. Felty (MCETECH, 2017)

A Certified Core Policy Language. - Bahman Sistany; Amy P. Felty (PST, 2017)

Formal Meta-level Analysis Framework for Quantum Programming Languages. - Mohamed Yousri Mahmoud; Amy P. Felty (LSFA, 2017)

Formalizing Abstract Computability: Turing Categories in Coq. - Polina Vinogradova; Amy P. Felty; Philip J. Scott (LSFA, 2017)

Preface: Selected Extended Papers of CADE 2015. - Amy P. Felty; Aart Middeldorp (J. Autom. Reason., 2017)

A Logical Framework for Modelling Breast Cancer Progression. - Joëlle Despeyroux; Amy P. Felty; Pietro Liò; Carlos Olarte (MLCSB, 2018)

Benchmarks for reasoning with syntax trees containing binders and contexts of assumptions. - Amy P. Felty; Alberto Momigliano; Brigitte Pientka (Math. Struct. Comput. Sci., 2018)

Preface. - Amy P. Felty; João Marcos 001 (LSFA, 2019)

A Linear Logical Framework in Hybrid (Invited Talk). - Amy P. Felty (FSCD, 2019)

Formalization of Metatheory of the Quipper Quantum Programming Language in a Linear Logic. - Mohamed Yousri Mahmoud; Amy P. Felty (J. Autom. Reason., 2019)

A special issue on structural proof theory, automated reasoning and computation in celebration of Dale Miller's 60th birthday. - David Baelde; Amy P. Felty; Gopalan Nadathur; Alexis Saurin (Math. Struct. Comput. Sci., 2019)

Women in Logic 2018 workshop report. - Mihaela Rozman; Valeria de Paiva; Amy P. Felty; Ursula Martin (ACM SIGLOG News, 2019)

Towards Formal Verification of Program Obfuscation. - Weiyun Lu; Bahman Sistany; Amy P. Felty; Philip J. Scott (EuroS&P Workshops, 2020)

Resolving XACML Rule Conflicts using Artificial Intelligence. - Bernard Stepien; Amy P. Felty (ICISS, 2020)

Formal Verification of a Certified Policy Language. - Amir Eaman; Amy P. Felty (VECoS, 2020)

Computational Logic for Biomedicine and Neurosciences. - Abdorrahim Bahrami; Elisabetta De Maria; Joëlle Despeyroux; Amy P. Felty; Pietro Lió; Carlos Olarte (CoRR, 2020)

A focused linear logical framework and its application to metatheory of object logics. - Amy P. Felty; Carlos Olarte; Bruno Xavier (Math. Struct. Comput. Sci., 2021)

Modelling and Verifying Properties of Biological Neural Networks (Invited Talk). - Amy P. Felty (ITP, 2022)

On the use of formal methods to model and verify neuronal archetypes. - Elisabetta De Maria; Abdorrahim Bahrami; Thibaud L'Yvonnet; Amy P. Felty; Daniel Gaffé; Annie Ressouche; Franck Grammont (Frontiers Comput. Sci., 2022)

Preface to Special Issue: LSFA 2019 and 2020. - Amy P. Felty; Giselle Reis (Math. Struct. Comput. Sci., 2022)

A certified access control policy language: TEpla. - Amir Eaman; Amy P. Felty (Innov. Syst. Softw. Eng., 2024)

Modelling and Verifying Neuronal Archetypes in Coq. - Abdorrahim Bahrami; Rébecca Zucchini; Elisabetta De Maria; Amy P. Felty (CoRR, 2025)