Amy Felty: Publications

• A Certified Access Control Policy Language: TEpla, by Amir Eaman and Amy Felty. In Innovations in Systems and Software Engineering, 16 pages, August 2023 (pdf, article web page).

• Computational Logic for Biomedicine and Neurosciences, by Elisabetta De Maria, Joëlle Despeyroux, Amy Felty, Pietro Lió, Carlos Olarte, and Abdorrahim Bahrami. In Symbolic Approaches to the Modeling and Analysis of Biological Systems, ISTE-Wiley, July 2023 (pdf, article web page, book web page).

• Logique calculatoire pour la biomédecine et les neurosciences, by Elisabetta De Maria, Joëlle Despeyroux, Amy Felty, Pietro Lió, Carlos Olarte, and Abdorrahim Bahrami. In Approches symboliques de la modélisation et de l'analyse des systèmes biologiques, ISTE-Wiley, July 2022 French version of previous entry (book web page).

• On the Use of Formal Methods to Model and Verify Neuronal Archetypes, by Elisabetta De Maria, Abdorrahim Bahrami, Thibaud L'Yvonnet, Amy Felty, Daniel Gaffé, Annie Ressouche, and Franck Grammont. Frontiers of Computer Science, 16(3), Article number: 163404, 22 pages, June 2022 (pdf, article web page).

• A Focused Linear Logical Framework and its Application to Metatheory of Object Logics, by Amy Felty, Carlos Olarte, and Bruno Xavier. Mathematical Structures in Computer Science, 31(3):312-340, November 2021 (pdf, article web page, Coq formalization).

• Formal Verification of a Certified Policy Language, by Amir Eaman and Amy Felty. In Proceedings of the 14th International Conference on Verification and Evaluation of Computer and Communication Systems (VECoS), Springer LNCS 12519, pages 180-194, 2020 (pdf).

• Towards Formal Verification of Program Obfuscation, by Bahman Sistany, Amy Felty, Weiyun Lu, and Philip Scott. Workshop on Software Attacks and Defenses (SAD), in Proceedings of the 2020 IEEE European Symposium on Security and Privacy Workshops (EUROS&PW), IEEE, pages 635-644, September 2020 (pdf).

• Resolving XACML Rule Conflicts Using Artificial Intelligence, by Bernard Stepien and Amy Felty. In Proceedings of the 3rd International Conference on Information Science and System (ICISS 2020), ACM, pages 121-127, March 2020 (pdf).

• Formalization of Metatheory of the Quipper Quantum Programming Language in a Linear Logic, by Mohamed Yousri Mahmoud and Amy P. Felty. Journal of Automated Reasoning, 63:967-1002, June 2019 (SpringerLink, pdf, Coq code).

• A Logical Framework for Modelling Breast Cancer Progression, by Joëlle Despeyroux, Amy Felty, Pietro Lio, and Carlos Olarte. In Proceedings of the International Symposium on Molecular Logic and Computational Synthetic Biology (MLCSB 2018), Springer Nature, LNCS 11415, pages 121-141, 2019 (pdf, Coq code).

• Benchmarks for Reasoning with Syntax Trees Containing Binders and Contexts of Assumptions, by Amy Felty, Alberto Momigliano, and Brigitte Pientka. In Mathematical Structures in Computer Science, Cambridge University Press, 28:1507-1540, 2018, (pdf).

• Modelling and Verifying Dynamic Properties of Biological Neural Networks in Coq, by Abdorrahim Bahrami, Elisabetta De Maria, and Amy Felty. In Proceedings of the 9th International Conference on Computational Systems-Biology and Bioinformatics (CSBio 2018), ACM, Article No.: 12, pages 1-11, 2018, (pdf, Electronic appendix).

• Formal Meta-level Analysis Framework for Quantum Programming Languages, by Mohamed Yousri Mahmoud and Amy P. Felty. In Proceedings of the 12th Workshop on Logical and Semantic Frameworks with Applications (LSFA 2017), in Electronic Notes in Theoretical Computer Science, Volume 338, pages 185-201, 2018, (pdf).

• Formalizing Abstract Computability: Turing Categories in Coq, by Polina Vinogradova, Amy P. Felty, and Philip Scott In Proceedings of the 12th Workshop on Logical and Semantic Frameworks with Applications (LSFA 2017), in Electronic Notes in Theoretical Computer Science, Volume 338, pages 203-218, 2018, (pdf).

• A Certified Core Policy Language, by Bahman Sistany and Amy Felty In 15th Annual International Conference on Privacy, Security, and Trust (PST 2017), pages 391-393, 2017, (pdf).

• Review of Existing Analysis Tools for SELinux Security Policies: Challenges and a Proposed Solution, by Amir Eaman, Bahman Sistany, and Amy Felty In E-Technologies: Embracing the Internet of Things, Proceedings of the 7th International MCETECH Conference, Springer LNBIP 289, pages 116-135, May 2017 (pdf).

• The Logic of Hereditary Harrop Formulas as a Specification Logic for Hybrid, by Chelsea Battell and Amy Felty. In Proceedings of the Eleventh International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP), Article No.: 3, pages 1-10, June 2016 (pdf, Coq formalization).

• Using Expert Systems to Statically Detect "Dynamic" Conflicts in XACML, by Bernard Stepien and Amy Felty. In Proceedings of the Eleventh International Conference on Availability, Reliability and Security (ARES), pages 127-136, August 2016 (pdf).

• A Verified Algorithm for Detecting Conflicts in XACML Access Control Rules, by Michel St-Martin and Amy P. Felty. In Proceedings of the Fifth ACM SIGPLAN Conference on Certified Programs and Proofs (CPP), pages 166-175, January 2016 (pdf, Coq formalization).

• The Next 700 Challenge Problems for Reasoning with Higher-Order Abstract Syntax Representations: Part 1–A Common Infrastructure for Benchmarks, by Amy P. Felty, Alberto Momigliano, and Brigitte Pientka, March 2015 (arXiv, pdf).

• The Next 700 Challenge Problems for Reasoning with Higher-Order Abstract Syntax Representations: Part 2–A Survey, by Amy P. Felty, Alberto Momigliano, and Brigitte Pientka. Journal of Automated Reasoning, 55(4):307-372, December 2015, DOI 10.1007/s10817-015-9327-3 (SpringerLink, pdf).

• An Open Challenge Problem Repository for Systems Supporting Binders, by Amy Felty, Alberto Momigliano, and Brigitte Pientka. In Proceedings of the Tenth International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP), in Electronic Proceedings in Theoretical Computer Science, Volume 185, pages 18-32, August 2015 (pdf).

• A Logical Framework for Systems Biology, by Elisabetta De Maria, Joëlle Despeyroux, and Amy P. Felty. In 1st International Conference Formal Methods in Macro-Biology (FMMB), Springer LNCS 8738, pages 136-155, September 2014, (pdf, electronic appendix).

• Challenges of Composing XACML Policies, by Bernard Stepien, Amy Felty, and Stan Matwin. In Proceedings of the Ninth International Conference on Availability, Reliability and Security (ARES), pages 234-241, September 2014, (pdf).

• A Non-Technical XACML Target Editor for Dynamic Access Control Systems, by Bernard Stepien, Amy Felty, and Stan Matwin. In Proceedings of the 2014 International Conference on Collaboration Technologies and Systems (CTS), pages 150-157, May 2014, (pdf).

• Translating Higher-Order Specifications to Coq Libraries Supporting Hybrid Proofs, by Nada Habli and Amy Felty. In Third International Workshop on Proof Exchange for Theorem Proving, EasyChair Proceedings in Computing, Volume 14, pages 67-76, 2013, (pdf).

• A Verified Algorithm for Detecting Conflicts in XACML Access Control Rules, by Michel St-Martin and Amy Felty. In Informal Proceedings of the First International Workshop on Automated Reasoning in Security and Software Verification, pages 4-11, 2013, (pdf).

• Hybrid: A Definitional Two Level Approach to Reasoning with Higher-Order Abstract Syntax, by Amy Felty and Alberto Momigliano. Journal of Automated Reasoning, 48(1):43-105, 2012, DOI 10.1007/s10817-010-9194-x (SpringerLink, pdf).

• An Algorithm for Compression of XACML Access Control Policy Sets by Recursive Subsumption, by Bernard Stepien, Amy Felty, and Stan Matwin. In 7th International Conference on Availability, Reliability, and Security (ARES), pp. 161-167, August 2012 (pdf).

• An Improved Implementation and Abstract Interface for Hybrid, by Alan J. Martin, and Amy P. Felty. In Proceedings of the Sixth International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP), August 2011, (pdf).

• Advantages of a Non-Technical XACML Notation in Role-Based Models, by Bernard Stepien, Stan Matwin, and Amy Felty. In 9th Annual International Conference on Privacy, Security, and Trust (PST), July 2011, (pdf).

• An Implementation of a Verification Condition Generator for Foundational Proof-Carrying Code by Jiangong Weng and Amy Felty. In 9th Annual International Conference on Privacy, Security, and Trust (PST) , July 2011, (pdf).

• Reasoning with Higher-Order Abstract Syntax and Contexts: A Comparison, by Amy Felty and Brigitte Pientka. In International Conference on Interactive Theorem Proving, Springer-Verlag LNCS, July 2010, (SpringerLink, pdf).

• Strategies for Reducing Risks of Inconsistencies in Access Control Policies, by Bernard Stepien, Stan Matwin, and Amy Felty. In 5th International Conference on Availability, Reliability, and Security, February 2010 (pdf).

• Higher-Order Abstract Syntax in Type Theory, by Venanzio Capretta and Amy Felty. In Logic Colloquium '06, ASL Lecture Notes in Logic, 32, Cambridge University Press, October 2009 (pdf, Coq formalization, Example application).

• Reasoning with Hypothetical Judgments and Open Terms in Hybrid, by Amy Felty and Alberto Momigliano. In 11th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming, September 2009 (pdf).

• A Non-technical User-Oriented Display Notation for XACML Conditions, by Bernard Stepien, Amy Felty, and Stan Matwin. In E-Technologies: Innovation in an Open World, Proceedings of the 4th International MCETECH Conference, Springer LNBIP 26, 2009 (pdf).

• Two-level Hybrid: A System for Reasoning Using Higher-Order Abstract Syntax, by Alberto Momigliano, Alan J. Martin, and Amy P. Felty. In Proceedings of the Second International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2007), in Electronic Notes in Theoretical Computer Science, 196:85-93, January 2008 (pdf).

• Genetic Programming with Polymorphic Types and Higher-Order Functions, by Franck Binard and Amy Felty. In Proceedings of the Tenth Annual Conference on Genetic and Evolutionary Computation, ACM Press, 2008 (pdf).

• Formal Correctness of Conflict Detection for Firewalls, by Venanzio Capretta, Bernard Stepien, Amy Felty, and Stan Matwin. In ACM Workshop on Formal Methods in Security Engineering, November 2007 (pdf, Coq formalization).

• Tutorial Examples of the Semantic Approach to Foundational Proof-Carrying Code, by Amy P. Felty. Fundamenta Informaticae, 7(4):303-330, 2007 (pdf).

• Combining de Bruijn Indices and Higher-Order Abstract Syntax in Coq, by Venanzio Capretta and Amy Felty. In Types for Proofs and Programs, International Workshop, TYPES 2006, Revised Selected Papers, Springer-Verlag LNCS 4502, 2007 (pdf, Coq formalization).

• An Abstraction-Based Genetic Programming System, by Franck Binard and Amy Felty. In Genetic and Evolutionary Computation Conference: Late Breaking Papers, 2007 (pdf).

• Privacy-Sensitive Information Flow with JML, by Guillaume Dufay, Amy Felty, and Stan Matwin. In Twentieth International Conference on Automated Deduction, Springer-Verlag LNCS, July 2005 (pdf).

• Privacy in Data Mining Using Formal Methods, by Stan Matwin, Amy Felty, Istvan Hernadvolgyi, and Venanzio Capretta. In Seventh International Conference on Typed Lambda Calculi and Applications, Springer-Verlag LNCS 3461, April 2005 (pdf).

• A Tutorial Example of the Semantic Approach to Foundational Proof-Carrying Code, by Amy P. Felty, In Sixteenth International Conference on Rewriting Techniques and Applications, Springer-Verlag LNCS 3467, April 2005 (pdf).

• Polymorphic Lemmas and Definitions in Lambda Prolog and Twelf, by Andrew W. Appel and Amy P. Felty. Theory and Practice of Logic Programming, 4(1&2):1-39, January & March 2004 (pdf).

• Dependent Types Ensure Partial Correctness of Theorem Provers, by Andrew W. Appel and Amy P. Felty. Journal of Functional Programming, 14(1):3-19, January 2004 (pdf).

• Feature Specification and Automatic Conflict Detection, by Amy P. Felty and Kedar S. Namjoshi. ACM Transactions on Software Engineering and Methodology, 12(1):3-27, January 2003 (pdf).

• Interactive Theorem Proving in Twelf, by Amy P. Felty. In The Association of Logic Programming Newsletter, Volume 15 n.3, August 2002 (pdf).

• Two-Level Meta-Reasoning in Coq, by Amy P. Felty. In Fifteenth International Conference on Theorem Proving in Higher Order Logics, Springer-Verlag LNCS 2410, August 2002 (pdf).

• Privacy-Oriented Data Mining by Proof Checking, by Amy Felty and Stan Matwin In Sixth European Conference on Principles of Data Mining and Knowledge Discovery, Springer-Verlag LNCS 2431, August 2002 (pdf).

• Temporal Logic Theorem Proving and its Application to the Feature Interaction Problem, by Amy Felty. In E. Giunchiglia and F. Massacci, editors, Issues in the Design and Experimental Evaluation of Systems for Modal and Temporal Logics, Technical Report DII 14/01, University of Siena, June 2001 (pdf).

• Feature Specification and Automatic Conflict Detection, by Amy P. Felty and Kedar S. Namjoshi. In M. Calder and E. Magill, editors, Feature Interactions in Telecommunications and Software Systems VI, IOS Press, May 2000 (pdf).

• A Semantic Model of Types and Machine Instructions for Proof-Carrying Code, by Andrew W. Appel and Amy P. Felty. In The 27th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, January 2000 (pdf).

• The Calculus of Constructions as a Framework for Proof Search with Set Variable Instantiation, by Amy Felty. Theoretical Computer Science, 232(1-2):187-229, February 2000 (pdf).

• Cache Coherency in SCI: Specification and a Sketch of Correctness, by Amy Felty and Frank Stomp. Formal Aspects of Computing, 11(5):475-497, 1999 (pdf, abstract).

• Lightweight Lemmas in lambda Prolog, by Andrew W. Appel and Amy P. Felty In International Conference on Logic Programming, MIT Press, November 1999 (pdf). Extended version: Princeton University Technical Report CS-TR-607-99, October 1999.

• Formal Metatheory Using Implicit Syntax, and an Application to Data Abstraction for Asynchronous Systems, by Amy P. Felty, Douglas J. Howe, and Abhik Roychoudhury. In Sixteenth International Conference on Automated Deduction, Springer-Verlag LNCS 1632, July 1999 (pdf).

• Protocol Verification in Nuprl, by Amy P. Felty, Douglas J. Howe and Frank A. Stomp. In Tenth International Conference on Computer-Aided Verification, Springer-Verlag LNCS 1427, June 1998 (pdf).

• Hybrid Interactive Theorem Proving using Nuprl and HOL, by Amy P. Felty and Douglas J. Howe. In Fourteenth International Conference on Automated Deduction, Springer-Verlag LNCS 1249, July 1997 (pdf).

• Interactive Theorem Proving with Temporal Logic, by Amy Felty and Laurent Théry, Journal of Symbolic Computation, 23(4):367-397, April 1997 (pdf).

• Proof Search with Set Variable Instantiation in the Calculus of Constructions, by Amy Felty. In Thirteenth International Conference on Automated Deduction, Springer-Verlag LNCS 1104, July 1996 (pdf).

• A Correctness Proof of a Cache Coherence Protocol, by Amy Felty and Frank Stomp. In 11th Annual Conference on Computer Assurance, June 1996, (pdf).

• Formalizing Inductive Proofs of Network Algorithms, by Ramesh Bharadwaj, Amy Felty, and Frank Stomp. In 1995 Asian Computing Conference, Springer-Verlag LNCS 1023, December 1995 (pdf).

• Higher-Order Abstract Syntax in Coq, by Joëlle Despeyroux, Amy Felty, and André Hirschowitz. In Second International Conference on Typed Lambda Calculi and Applications, Springer-Verlag LNCS 902, April 1995 (pdf).

• Generalization and Reuse of Tactic Proofs, by Amy Felty and Douglas Howe. In Fifth International Conference on Logic Programming and Automated Reasoning, Springer-Verlag LNCS, 822, July 1994 (pdf).

• Tactic Theorem Proving with Refinement-Tree Proofs and Metavariables, by Amy Felty and Douglas Howe. In Twelfth International Conference on Automated Deduction, Springer-Verlag LNCS, 814, June 1994 (pdf).

• Implementing Tactics and Tacticals in a Higher-Order Logic Programming Language, by Amy Felty. Journal of Automated Reasoning, 11(1):43-81, August 1993 (pdf).

• Encoding the Calculus of Constructions in a Higher-Order Logic, by Amy Felty. In Eighth Annual Symposium on Logic in Computer Science, IEEE Computer Society Press, June 1993 (pdf).

• Definite Clause Grammars for Parsing Higher-Order Syntax. By Amy Felty. Presented at the 1993 International Symposium on Logic Programming, October 1993 (abstract). Preliminary version: Defining Object-Level Parsers in lambda Prolog. In Proceedings of the Workshop on the lambda Prolog Programming Language, Dale Miller, ed., University of Pennsylvania Technical Report MS-CIS-92-86, November 1992.

• Higher-Order Conditional Rewriting in the L-lambda Logic Programming Language, by Amy Felty. In Third International Workshop on Extensions to Logic Programming: Preprints of the Proceedings, Evelina Lamma and Paola Mello, eds., February 1992 (pdf).

• A Logic Programming Approach to Implementing Higher-Order Term Rewriting, by Amy Felty. In Proceedings of the January 1991 Workshop on Extensions to Logic Programming, Springer-Verlag LNCS, 596, 1992 (pdf).

• Encoding Dependent Types in an Intuitionistic Logic, by Amy Felty. In Gérard Huet and Gordon D. Plotkin, editors, Logical Frameworks, Cambridge University Press, 1991 (pdf).

• A Logic Program for Transforming Sequent Proofs to Natural Deduction Proofs, by Amy Felty. In Proceedings of the 1989 International Workshop on Extensions of Logic Programming. Springer-Verlag LNCS, 475, 1991 (pdf).

• Encoding a Dependent-Type Lambda-Calculus in a Logic Programming Language, by Amy Felty and Dale Miller. In Tenth International Conference on Automated Deduction, Springer-Verlag LNCS, 449, July 1990 (abstract). Nadathur and Southern have written a short report that provides a counterexample to our claim that our encoding is faithful.

• Specifying and Implementing Theorem Provers in a Higher-Order Logic Programming Language, by Amy Felty. PhD thesis, University of Pennsylvania, September 1989 (pdf).

• Explaining Modal Logic Proofs, by Amy Felty and Greg Hager. In Proceedings of the IEEE 1988 International Conference on Systems, Man, and Cybernetics, August 1988 (abstract).

• Specifying Theorem Provers in a Higher-Order Logic Programming Language, by Amy Felty and Dale Miller. In Ninth International Conference on Automated Deduction, Springer-Verlag LNCS, 310, May 1988 (abstract).

• Proof Explanation and Revision, by Amy Felty and Dale Miller. University of Pennsylvania, Technical Report MS-CIS-88-17, 1987 (pdf).

• An Integration of Resolution and Natural Deduction Theorem Proving, by Dale Miller and Amy Felty. In 1986 National Conference on Artificial Intelligence (pdf).