Higher-order abstract syntax in Coq J Despeyroux, A Felty, A Hirschowitz International Conference on Typed Lambda Calculi and Applications, 124-138, 1995 | 225* | 1995 |
A semantic model of types and machine instructions for proof-carrying code AW Appel, AP Felty Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of …, 2000 | 212 | 2000 |
Specifying theorem provers in a higher-order logic programming language A Felty, D Miller International Conference on Automated Deduction, 61-80, 1988 | 187 | 1988 |
The Coq proof assistant user's guide: version 5.8 G Dowek, A Felty, H Herbelin, G Huet, C Parent, C Paulin-Mohring, ... INRIA, 1993 | 138 | 1993 |
Implementing tactics and tacticals in a higher-order logic programming language A Felty Journal of Automated reasoning 11, 43-81, 1993 | 126 | 1993 |
Feature specification and automated conflict detection AP Felty, KS Namjoshi ACM Transactions on Software Engineering and Methodology (TOSEM) 12 (1), 3-27, 2003 | 124 | 2003 |
Hybrid: A definitional two-level approach to reasoning with higher-order abstract syntax A Felty, A Momigliano Journal of automated reasoning 48 (1), 43-105, 2012 | 97 | 2012 |
Specifying and implementing theorem provers in a higher-order logic programming language AP Felty University of Pennsylvania, 1989 | 97 | 1989 |
Formal correctness of conflict detection for firewalls V Capretta, B Stepien, A Felty, S Matwin Proceedings of the 2007 ACM workshop on Formal methods in security …, 2007 | 76 | 2007 |
Control access rule conflict detection A Felty, V Capretta, B Stepien, S Matwin US Patent App. 12/289,342, 2009 | 57 | 2009 |
Generalization and reuse of tactic proofs A Felty, D Howe Logic Programming and Automated Reasoning: 5th International Conference …, 1994 | 56 | 1994 |
Encoding a dependent-type λ-calculus in a logic programming language A Felty, D Miller International Conference on Automated Deduction, 221-235, 1990 | 55 | 1990 |
A logic programming approach to implementing higher-order term rewriting A Felty International Workshop on Extensions of Logic Programming, 135-161, 1991 | 47 | 1991 |
The next 700 challenge problems for reasoning with higher-order abstract syntax representations: Part 2—a survey AP Felty, A Momigliano, B Pientka Journal of Automated Reasoning 55, 307-372, 2015 | 44 | 2015 |
Advantages of a non-technical XACML notation in role-based models B Stepien, S Matwin, A Felty 2011 Ninth Annual International Conference on Privacy, Security and Trust …, 2011 | 43 | 2011 |
Privacy-sensitive information flow with JML G Dufay, A Felty, S Matwin International Conference on Automated Deduction, 116-130, 2005 | 43 | 2005 |
Two-level Hybrid: A system for reasoning using higher-order abstract syntax A Momigliano, AJ Martin, AP Felty Electronic Notes in Theoretical Computer Science 196, 85-93, 2008 | 42 | 2008 |
Hybrid interactive theorem proving using Nuprl and HOL AP Felty, DJ Howe Automated Deduction—CADE-14: 14th International Conference on Automated …, 1997 | 36 | 1997 |
A non-technical user-oriented display notation for XACML conditions B Stepien, A Felty, S Matwin E-Technologies: Innovation in an Open World: 4th International Conference …, 2009 | 33 | 2009 |
Combining de Bruijn indices and higher-order abstract syntax in Coq V Capretta, AP Felty International Workshop on Types for Proofs and Programs, 63-77, 2006 | 29 | 2006 |