Amy Felty: Publications

• Hybrid: A Defintional Two Level Approach to Reasoning with Higher-Order Abstract Syntax, by Amy Felty and Alberto Momigliano. Submitted September 2008 (pdf).

• 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).

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

• 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 (postscript).

• 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 (postscript).

• 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 (postscript).

• 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 (postscript).

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

• 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 (postscript).

• 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 (postscript).

• 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 (postscript).

• 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 (postscript).

• 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 (postscript).

• 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 (postscript, abstract).

• Lightweight Lemmas in lambda Prolog, by Andrew W. Appel and Amy P. Felty In International Conference on Logic Programming, MIT Press, November 1999 (postscript). 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 (postscript).

• 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 (postscript).

• 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 (postscript).

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

• 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 (postscript).

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

• 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 (postscript).

• 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 (postscript).

• 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 (postscript).

• 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 (postscript).

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

• 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 (postscript).

• Proving Properties About a Lazy Functional Language with the Coq Proof Development System, by Jill Seaman and Amy Felty, 1993 (postscript).

• 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 (postscript).

• 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 (postscript).

• 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 (postscript).

• 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 (postscript).

• 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).

• 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 (postscript).

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