Amy P. Felty

Orcid: 0000-0001-7195-2613

Affiliations:
  • University of Ottawa, Canada


According to our database1, Amy P. Felty authored at least 82 papers between 1986 and 2024.

Collaborative distances:

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2024
A certified access control policy language: TEpla.
Innov. Syst. Softw. Eng., March, 2024

2022
Preface to Special Issue: LSFA 2019 and 2020.
Math. Struct. Comput. Sci., October, 2022

On the use of formal methods to model and verify neuronal archetypes.
Frontiers Comput. Sci., 2022

Modelling and Verifying Properties of Biological Neural Networks (Invited Talk).
Proceedings of the 13th International Conference on Interactive Theorem Proving, 2022

2021
A focused linear logical framework and its application to metatheory of object logics.
Math. Struct. Comput. Sci., 2021

2020
Computational Logic for Biomedicine and Neurosciences.
CoRR, 2020

Formal Verification of a Certified Policy Language.
Proceedings of the Verification and Evaluation of Computer and Communication Systems, 2020

Resolving XACML Rule Conflicts using Artificial Intelligence.
Proceedings of the ICISS 2020: The 3rd International Conference on Information Science and System, 2020

Towards Formal Verification of Program Obfuscation.
Proceedings of the IEEE European Symposium on Security and Privacy Workshops, 2020

2019
Women in Logic 2018 workshop report.
ACM SIGLOG News, 2019

A special issue on structural proof theory, automated reasoning and computation in celebration of Dale Miller's 60th birthday.
Math. Struct. Comput. Sci., 2019

Formalization of Metatheory of the Quipper Quantum Programming Language in a Linear Logic.
J. Autom. Reason., 2019

Preface.
Proceedings of the 14th Workshop on Logical and Semantic Frameworks with Applications, 2019

A linear logical framework in hybrid (invited talk).
Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2019

2018
Benchmarks for reasoning with syntax trees containing binders and contexts of assumptions.
Math. Struct. Comput. Sci., 2018

A Logical Framework for Modelling Breast Cancer Progression.
Proceedings of the Molecular Logic and Computational Synthetic Biology, 2018

2017
Preface: Selected Extended Papers of CADE 2015.
J. Autom. Reason., 2017

Formalizing Abstract Computability: Turing Categories in Coq.
Proceedings of the 12th Workshop on Logical and Semantic Frameworks, with Applications, 2017

Formal Meta-level Analysis Framework for Quantum Programming Languages.
Proceedings of the 12th Workshop on Logical and Semantic Frameworks, with Applications, 2017

A Certified Core Policy Language.
Proceedings of the 15th Annual Conference on Privacy, Security and Trust, 2017

Review of Existing Analysis Tools for SELinux Security Policies: Challenges and a Proposed Solution.
Proceedings of the E-Technologies: Embracing the Internet of Things, 2017

2016
The Logic of Hereditary Harrop Formulas as a Specification Logic for Hybrid.
Proceedings of the Eleventh Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, 2016

A verified algorithm for detecting conflicts in XACML access control rules.
Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, 2016

Using Expert Systems to Statically Detect "Dynamic" Conflicts in XACML.
Proceedings of the 11th International Conference on Availability, Reliability and Security, 2016

2015
The Next 700 Challenge Problems for Reasoning with Higher-Order Abstract Syntax Representations - Part 2 - A Survey.
J. Autom. Reason., 2015

An Open Challenge Problem Repository for Systems Supporting Binders.
Proceedings of the Proceedings Tenth International Workshop on Logical Frameworks and Meta Languages: Theory and Practice, 2015

The Next 700 Challenge Problems for Reasoning with Higher-Order Abstract Syntax Representations: Part 1-A Common Infrastructure for Benchmarks.
CoRR, 2015

2014
A Logical Framework for Systems Biology.
Proceedings of the Formal Methods in Macro-Biology - First International Conference, 2014

A non-technical XACML target editor for dynamic access control systems.
Proceedings of the 2014 International Conference on Collaboration Technologies and Systems, 2014

Challenges of Composing XACML Policies.
Proceedings of the Ninth International Conference on Availability, 2014

2013
Translating Higher-Order Specifications to Coq Libraries Supporting Hybrid Proofs.
Proceedings of the Third International Workshop on Proof Exchange for Theorem Proving, 2013

2012
Hybrid - A Definitional Two-Level Approach to Reasoning with Higher-Order Abstract Syntax.
J. Autom. Reason., 2012

An Algorithm for Compression of XACML Access Control Policy Sets by Recursive Subsumption.
Proceedings of the Seventh International Conference on Availability, 2012

2011
An Improved Implementation and Abstract Interface for Hybrid
Proceedings of the Proceedings Sixth International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, 2011

An implementation of a verification condition generator for foundational proof-carrying code.
Proceedings of the Ninth Annual Conference on Privacy, Security and Trust, 2011

Advantages of a non-technical XACML notation in role-based models.
Proceedings of the Ninth Annual Conference on Privacy, Security and Trust, 2011

2010
Reasoning with Higher-Order Abstract Syntax and Contexts: A Comparison.
Proceedings of the Interactive Theorem Proving, First International Conference, 2010

Hybrid: Reasoning with Higher-Order Abstract Syntax in Coq and Isabelle.
Proceedings of the 3rd ACM SIGPLAN Workshop on Mathematically Structured Functional Programming, 2010

Strategies for Reducing Risks of Inconsistencies in Access Control Policies.
Proceedings of the ARES 2010, 2010

2009
Reasoning with hypothetical judgments and open terms in hybrid.
Proceedings of the 11th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 2009

A Non-technical User-Oriented Display Notation for XACML Conditions.
Proceedings of the E-Technologies: Innovation in an Open World, 2009

2008
Genetic programming with polymorphic types and higher-order functions.
Proceedings of the Genetic and Evolutionary Computation Conference, 2008

2007
Tutorial Examples of the Semantic Approach to Foundational Proof-Carrying Code.
Fundam. Informaticae, 2007

Two-Level Hybrid: A System for Reasoning Using Higher-Order Abstract Syntax.
Proceedings of the Second International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, 2007

An abstraction-based genetic programming system.
Proceedings of the Genetic and Evolutionary Computation Conference, 2007

Formal correctness of conflict detection for firewalls.
Proceedings of the 2007 ACM workshop on Formal methods in security engineering, 2007

2006
Combining de Bruijn Indices and Higher-Order Abstract Syntax in Coq.
Proceedings of the Types for Proofs and Programs, International Workshop, 2006

2005
Privacy in Data Mining Using Formal Methods.
Proceedings of the Typed Lambda Calculi and Applications, 7th International Conference, 2005

A Tutorial Example of the Semantic Approach to Foundational Proof-Carrying Code: Abstract.
Proceedings of the Typed Lambda Calculi and Applications, 7th International Conference, 2005

A Tutorial Example of the Semantic Approach to Foundational Proof-Carrying Code.
Proceedings of the Term Rewriting and Applications, 16th International Conference, 2005

Privacy-Sensitive Information Flow with JML.
Proceedings of the Automated Deduction, 2005

2004
Polymorphic Lemmas and Definitions in lambda-Prolog and Twelf.
Theory Pract. Log. Program., 2004

Dependent types ensure partial correctness of theorem provers.
J. Funct. Program., 2004

2003
Feature specification and automated conflict detection.
ACM Trans. Softw. Eng. Methodol., 2003

Preface.
J. Autom. Reason., 2003

2002
Two-Level Meta-reasoning in Coq.
Proceedings of the Theorem Proving in Higher Order Logics, 15th International Conference, 2002

Privacy-Oriented Data Mining by Proof Checking.
Proceedings of the Principles of Data Mining and Knowledge Discovery, 2002

2001
Current Trends in Logical Frameworks and Metalanguages.
J. Autom. Reason., 2001

2000
The calculus of constructions as a framework for proof search with set variable instantiation.
Theor. Comput. Sci., 2000

A Semantic Model of Types and Machine Instructions for Proof-Carrying Code.
Proceedings of the POPL 2000, 2000

Feature Specification and Automatic Conflict Detection.
Proceedings of the Feature Interactions in Telecommunications and Software Systems VI, 2000

1999
Cache Coherency in SCI: Specification and a Sketch of Correctness.
Formal Aspects Comput., 1999

Lightweight Lemmas in lambda-Prolog.
Proceedings of the Logic Programming: The 1999 International Conference, Las Cruces, New Mexico, USA, November 29, 1999

Formal Metatheory using Implicit Syntax, and an Application to Data Abstraction for Asynchronous Systems.
Proceedings of the Automated Deduction, 1999

1998
Protocol Verification in Nuprl.
Proceedings of the Computer Aided Verification, 10th International Conference, 1998

1997
Interactive Theorem Proving with Temporal Logic.
J. Symb. Comput., 1997

Hybrid Interactive Theorem Proving Using Nuprl and HOL.
Proceedings of the Automated Deduction, 1997

1996
Proof Search with Set Variable Instantiation in the Calculus of Constructions.
Proceedings of the Automated Deduction - CADE-13, 13th International Conference on Automated Deduction, New Brunswick, NJ, USA, July 30, 1996

1995
Higher-Order Abstract Syntax in Coq.
Proceedings of the Typed Lambda Calculi and Applications, 1995

Formalizing Inductive Proofs of Network Algorithms.
Proceedings of the Algorithms, 1995

1994
Generalization and Reuse of Tactic Proofs.
Proceedings of the Logic Programming and Automated Reasoning, 5th International Conference, 1994

Tactic Theorem Proving with Refinement-Tree Proofs and Metavariables.
Proceedings of the Automated Deduction - CADE-12, 12th International Conference on Automated Deduction, Nancy, France, June 26, 1994

1993
Implementing Tactics and Tacticals in a Higher-Order Logic Programming Language.
J. Autom. Reason., 1993

Definite Clause Grammars for Parsing Higher-Order Syntax.
Proceedings of the Logic Programming, 1993

Encoding the Calculus of Constructions in a Higher-Order Logic
Proceedings of the Eighth Annual Symposium on Logic in Computer Science (LICS '93), 1993

1991
A Logic Programming Approach to Implementing Higher-Order Term Rewriting.
Proceedings of the Extensions of Logic Programming, Second International Workshop, 1991

1990
Encoding a Dependent-Type Lambda-Calculus in a Logic Programming Language.
Proceedings of the 10th International Conference on Automated Deduction, 1990

Tutorial on Lambda-Prolog.
Proceedings of the 10th International Conference on Automated Deduction, 1990

1989
A Logic Program for Transforming Sequent Proofs to Natural Deduction Proofs.
Proceedings of the Extensions of Logic Programming, 1989

1988
Specifying Theorem Provers in a Higher-Order Logic Programming Language.
Proceedings of the 9th International Conference on Automated Deduction, 1988

Lambda-Prolog: An Extended Logic Programming Language.
Proceedings of the 9th International Conference on Automated Deduction, 1988

1986
An Integration of Resolution and Natural Deduction Theorem Proving.
Proceedings of the 5th National Conference on Artificial Intelligence. Philadelphia, 1986


  Loading...