| Publication | Date of Publication | Type |
|---|
| Adelfa: a system for reasoning about LF specifications | 2025-08-19 | Paper |
| Abella: a system for reasoning about relational specifications | 2019-09-18 | Paper |
Combining deduction modulo and logics of fixed-point definitions
2012 27th Annual IEEE Symposium on Logic in Computer Science | 2017-05-16 | Paper |
Reasoning in Abella about structural operational semantics specifications
Electronic Notes in Theoretical Computer Science | 2016-05-06 | Paper |
A higher-order abstract syntax approach to verified transformations on functional programs
Programming Languages and Systems | 2016-04-26 | Paper |
A two-level logic approach to reasoning about computations
Journal of Automated Reasoning | 2013-08-01 | Paper |
The suspension notation for lambda terms and its use in metalanguage implementations
Electronic Notes in Theoretical Computer Science | 2013-04-19 | Paper |
| Programming with higher-order logic. | 2012-06-15 | Paper |
Nominal abstraction
Information and Computation | 2011-01-13 | Paper |
Optimizing the Runtime Processing of Types in Polymorphic Logic Programming Languages
Logic for Programming, Artificial Intelligence, and Reasoning | 2008-05-27 | Paper |
Choices in representation and reduction strategies for lambda terms in intensional contexts
Journal of Automated Reasoning | 2007-01-29 | Paper |
FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science
Lecture Notes in Computer Science | 2006-11-14 | Paper |
Logic Programming
Lecture Notes in Computer Science | 2006-06-27 | Paper |
A treatment of higher-order features in logic programming
Theory and Practice of Logic Programming | 2006-02-08 | Paper |
| scientific article; zbMATH DE number 2090073 (Why is no real title available?) | 2004-08-12 | Paper |
| scientific article; zbMATH DE number 1692888 (Why is no real title available?) | 2002-01-21 | Paper |
Correspondences between classical, intuitionistic and uniform provability
Theoretical Computer Science | 2000-08-23 | Paper |
| scientific article; zbMATH DE number 1332647 (Why is no real title available?) | 1999-09-09 | Paper |
Uniform provability in classical logic
Journal Of Logic And Computation | 1999-04-12 | Paper |
A notation for lambda terms. A generalization of environments
Theoretical Computer Science | 1998-08-13 | Paper |
| scientific article; zbMATH DE number 1158760 (Why is no real title available?) | 1998-06-03 | Paper |
| scientific article; zbMATH DE number 1158756 (Why is no real title available?) | 1998-06-03 | Paper |
Scoping constructs in logic programming: Implementation problems and their solution
The Journal of Logic Programming | 1997-10-05 | Paper |
A proof procedure for the logic of hereditary Harrop formulas
Journal of Automated Reasoning | 1994-09-26 | Paper |
Implementing polymorphic typing in a logic programming language
Computer Languages | 1994-07-21 | Paper |
Uniform proofs as a foundation for logic programming
Annals of Pure and Applied Logic | 1991-01-01 | Paper |
Higher-order Horn clauses
Journal of the ACM | 1990-01-01 | Paper |
| scientific article; zbMATH DE number 3988745 (Why is no real title available?) | 1986-01-01 | Paper |
