Amy P. Felty - researchr alias

researchr

You are not signed in
Sign in
Sign up

2010

Reasoning with Higher-Order Abstract Syntax and Contexts: A ComparisonAmy P. Felty, Brigitte Pientka. itp 2010: 227-242 [doi]

Strategies for Reducing Risks of Inconsistencies in Access Control PoliciesBernard Stepien, Stan Matwin, Amy P. Felty. IEEEares 2010: 140-147 [doi]

2009

Reasoning with hypothetical judgments and open terms in hybridAmy P. Felty, Alberto Momigliano. ppdp 2009: 83-92 [doi]

2008

Genetic programming with polymorphic types and higher-order functionsFranck Binard, Amy P. Felty. gecco 2008: 1187-1194 [doi]

Hybrid: A Definitional Two-Level Approach to Reasoning with Higher-Order Abstract SyntaxAmy P. Felty, Alberto Momigliano. corr, abs/0811.4367, 2008. [doi]

Two-Level Hybrid: A System for Reasoning Using Higher-Order Abstract SyntaxAlberto Momigliano, Alan J. Martin, Amy P. Felty. ENTCS, 196:85-93, 2008. [doi]

2007

An abstraction-based genetic programming systemFranck Binard, Amy P. Felty. gecco 2007: 2415-2422 [doi]

Formal correctness of conflict detection for firewallsVenanzio Capretta, Bernard Stepien, Amy P. Felty, Stan Matwin. ccs 2007: 22-30 [doi]

Tutorial Examples of the Semantic Approach to Foundational Proof-Carrying CodeAmy P. Felty. FUIN, 77(4):303-330, 2007. [doi]

2006

Combining de Bruijn Indices and Higher-Order Abstract Syntax in CoqVenanzio Capretta, Amy P. Felty. TYPES 2007: 63-77 [doi]

2005

2004

Dependent types ensure partial correctness of theorem proversAndrew W. Appel, Amy P. Felty. JFP, 14(1):3-19, 2004. [doi]

Polymorphic lemmas and definitions in Lambda Prolog and TwelfAndrew W. Appel, Amy P. Felty. corr, cs.LO/0403010, 2004. [doi]

Polymorphic Lemmas and Definitions in lambda-Prolog and TwelfAndrew W. Appel, Amy P. Felty. tplp, 4(1-2):1-39, 2004.

2003

Feature specification and automated conflict detectionAmy P. Felty, Kedar S. Namjoshi. TOSEM, 12(1):3-27, 2003. [doi]

PrefaceAmy P. Felty. JAR, 31(3-4):189-190, 2003. [doi]

2002

Privacy-Oriented Data Mining by Proof CheckingAmy P. Felty, Stan Matwin. pkdd 2002: 138-149 [doi]

Two-Level Meta-reasoning in CoqAmy P. Felty. tphol 2002: 198-213 [doi]

2001

Current Trends in Logical Frameworks and MetalanguagesDavid A. Basin, Amy P. Felty. JAR, 27(1):1-2, 2001.

2000

A Semantic Model of Types and Machine Instuctions for Proof-Carrying CodeAndrew W. Appel, Amy P. Felty. POPL 2000: 243-253 [doi]

Feature Specification and Automatic Conflict DetectionAmy P. Felty, Kedar S. Namjoshi. fiw 2000: 179-192

The calculus of constructions as a framework for proof search with set variable instantiationAmy P. Felty. TCS, 232(1-2):187-229, 2000. [doi]

1999

Lightweight Lemmas in lambda-PrologAndrew W. Appel, Amy P. Felty. ICLP 1999: 411-425

Cache Coherency in SCI: Specification and a Sketch of CorrectnessAmy P. Felty, Frank A. Stomp. fac, 11(5):475-497, 1999. [doi]

Formal Metatheory using Implicit Syntax, and an Application to Data Abstraction for Asynchronous SystemsAmy P. Felty, Douglas J. Howe, Abhik Roychoudhury. cade 1999: 237-251 [doi]

1998

Protocol Verification in NuprlAmy P. Felty, Douglas J. Howe, Frank A. Stomp. cav 1998: 428-439

1997

Hybrid Interactive Theorem Proving Using Nuprl and HOLAmy P. Felty, Douglas J. Howe. cade 1997: 351-365

Interactive Theorem Proving with Temporal LogicAmy P. Felty, Laurent Théry. JSC, 23(4):367-397, 1997.

Theorem Proving in Higher Order Logics, 10th International Conference, TPHOLs 97, Murray Hill, NJ, USA, August 19-22, 1997, ProceedingsElsa L. Gunter, Amy P. Felty, editors, Volume 1275 of Lecture Notes in Computer Science, Springer, 1997.

1996

Proof Search with Set Variable Instantiation in the Calculus of ConstructionsAmy P. Felty. cade 1996: 658-672

1995

Formalizing Inductive Proofs of Network AlgorithmsRamesh Bharadwaj, Amy P. Felty, Frank A. Stomp. asian 1995: 335-349

Higher-Order Abstract Syntax in CoqJoëlle Despeyroux, Amy P. Felty, André Hirschowitz. tlca 1995: 124-138

1994

Tactic Theorem Proving with Refinement-Tree Proofs and MetavariablesAmy P. Felty, Douglas J. Howe. cade 1994: 605-619

Generalization and Reuse of Tactic ProofsAmy P. Felty, Douglas J. Howe. lpar 1994: 1-15

1993

Encoding the Calculus of Constructions in a Higher-Order LogicAmy P. Felty. lics 1993: 233-244

Implementing Tactics and Tacticals in a Higher-Order Logic Programming LanguageAmy P. Felty. JAR, 11(1):41-81, 1993.

Definite Clause Grammars for Parsing Higher-Order SyntaxAmy P. Felty. slp 1993: 668

1991

A Logic Programming Approach to Implementing Higher-Order Term RewritingAmy P. Felty. elp 1992: 135-161

1990

Tutorial on Lambda-PrologAmy P. Felty, Elsa L. Gunter, Dale Miller, Frank Pfenning. cade 1990: 682

Encoding a Dependent-Type Lambda-Calculus in a Logic Programming LanguageAmy P. Felty, Dale Miller. cade 1990: 221-235

1989

A Logic Program for Transforming Sequent Proofs to Natural Deduction ProofsAmy P. Felty. elp 1991: 157-178

1988

Specifying Theorem Provers in a Higher-Order Logic Programming LanguageAmy P. Felty, Dale Miller. cade 1988: 61-80

Lambda-Prolog: An Extended Logic Programming LanguageAmy P. Felty, Elsa L. Gunter, John Hannan, Dale Miller, Gopalan Nadathur, Andre Scedrov. cade 1988: 754-755

1986

An Integration of Resolution and Natural Deduction Theorem ProvingDale Miller, Amy P. Felty. AAAI 1986: 198-202

Home PageAmy P. Felty.