The following pages link to Amy P. Felty (Q590551):
Displayed 36 items.
- (Q220706) (redirect page) (← links)
- The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey (Q287277) (← links)
- Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax (Q438569) (← links)
- Implementing tactics and tacticals in a higher-order logic programming language (Q1311396) (← links)
- Interactive theorem proving with temporal logic (Q1355780) (← links)
- The calculus of constructions as a framework for proof search with set variable instantiation (Q1575927) (← links)
- Cache coherency in SCI: Specification and a sketch of correctness (Q1977123) (← links)
- Formalization of metatheory of the Quipper quantum programming language in a linear logic (Q2331074) (← links)
- Formal meta-level analysis framework for quantum programming languages (Q2333324) (← links)
- Formalizing abstract computability: Turing categories in Coq (Q2333325) (← links)
- (Q2871875) (← links)
- (Q3024831) (← links)
- (Q3593496) (← links)
- Combining de Bruijn Indices and Higher-Order Abstract Syntax in Coq (Q3612436) (← links)
- (Q3656423) (← links)
- (Q3789101) (← links)
- (Q4012881) (← links)
- (Q4406017) (← links)
- (Q4484341) (← links)
- Proof search with set variable instantiation in the Calculus of Constructions (Q4647555) (← links)
- Benchmarks for reasoning with syntax trees containing binders and contexts of assumptions (Q4691183) (← links)
- Polymorphic lemmas and definitions in $\lambda$Prolog and Twelf (Q4819003) (← links)
- Dependent types ensure partial correctness of theorem provers (Q4819651) (← links)
- A focused linear logical framework and its application to metatheory of object logics (Q5022931) (← links)
- A logic program for transforming sequent proofs to natural deduction proofs (Q5053007) (← links)
- A Linear Logical Framework in Hybrid (Invited Talk) (Q5089001) (← links)
- A semantic model of types and machine instructions for proof-carrying code (Q5178856) (← links)
- Tactic theorem proving with refinement-tree proofs and metavariables (Q5210800) (← links)
- Hybrid interactive theorem proving using nuprl and HOL (Q5234717) (← links)
- A Logical Framework for Systems Biology (Q5500406) (← links)
- Term Rewriting and Applications (Q5703864) (← links)
- Typed Lambda Calculi and Applications (Q5704014) (← links)
- Typed Lambda Calculi and Applications (Q5704016) (← links)
- Reasoning with Higher-Order Abstract Syntax and Contexts: A Comparison (Q5747652) (← links)
- Current trends in logical frameworks and metalanguages (Q5951520) (← links)
- A logical framework for modelling breast cancer progression (Q6074998) (← links)