Amy Felty's Research Papers

Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
Amy Felty's Research Papers

Amy Felty: Publications

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, abstract).
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, abstract).
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, abstract).
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, abstract).
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, abstract).
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 (postscript, abstract).
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, abstract).
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, abstract).
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, abstract).
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, extended version).
Lightweight Lemmas in lambda Prolog, by Andrew W. Appel and Amy P. Felty In International Conference on Logic Programming, MIT Press, November 1999 (postscript, abstract). 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, abstract).
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, abstract).
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, abstract).
Interactive Theorem Proving with Temporal Logic, by Amy Felty and Laurent Théry, Journal of Symbolic Computation, 23(4):367-397, April 1997 (postscript, abstract).
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, abstract).
A Correctness Proof of a Cache Coherence Protocol, by Amy Felty and Frank Stomp. In 11th Annual Conference on Computer Assurance, June 1996, (postscript, abstract).
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, abstract).
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, abstract).
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, abstract).
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, abstract).
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, abstract).
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, abstract).
Proving Properties About a Lazy Functional Language with the Coq Proof Development System, by Jill Seaman and Amy Felty, 1993 (postscript, abstract).
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, abstract).
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, abstract).
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, abstract).
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, abstract).
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).
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, abstract).
An Integration of Resolution and Natural Deduction Theorem Proving, by Dale Miller and Amy Felty. In 1986 National Conference on Artificial Intelligence, (pdf, abstract).