| Publication | Date of Publication | Type |
|---|
Connection-based proof construction in linear logic
Automated Deduction—CADE-14 | 2019-10-01 | Paper |
Deciding intuitionistic propositional logic via translation into classical logic
Automated Deduction—CADE-14 | 2019-10-01 | Paper |
Formal reasoning about modules, reuse and their correctness
Practical Reasoning | 2019-04-29 | Paper |
Converting non-classical matrix proofs into sequent-style systems
Automated Deduction — Cade-13 | 2019-01-15 | Paper |
T-string unification: unifying prefixes in non-classical proof methods
Theorem Proving with Analytic Tableaux and Related Methods | 2019-01-10 | Paper |
Nuprl as logical framework for automating proofs in category theory
Logic and Program Semantics | 2012-07-16 | Paper |
Specifying and verifying organizational security properties in first-order logic
Verification, Induction, Termination Analysis | 2010-11-22 | Paper |
Automating Proofs in Category Theory
Automated Reasoning | 2009-03-12 | Paper |
The ILTP problem library for intuitionistic logic
Journal of Automated Reasoning | 2007-05-04 | Paper |
Innovations in computational type theory using Nuprl
Journal of Applied Logic | 2007-02-20 | Paper |
Automated Reasoning with Analytic Tableaux and Related Methods
Lecture Notes in Computer Science | 2006-07-07 | Paper |
Building reliable, high-performance networks with the Nuprl proof development system
Journal of Functional Programming | 2004-09-27 | Paper |
A matrix characterization for multiplicative exponential linear logic
Journal of Automated Reasoning | 2004-08-16 | Paper |
scientific article; zbMATH DE number 1863380 (Why is no real title available?)
| 2003-02-04 | Paper |
A uniform procedure for converting matrix proofs into sequent-style systems
Information and Computation | 2003-01-14 | Paper |
Connection-driven inductive theorem proving
Studia Logica | 2002-09-16 | Paper |
scientific article; zbMATH DE number 1765687 (Why is no real title available?)
| 2002-07-10 | Paper |
scientific article; zbMATH DE number 1748580 (Why is no real title available?)
| 2002-06-03 | Paper |
Program synthesis
| 2001-11-06 | Paper |
scientific article; zbMATH DE number 1614694 (Why is no real title available?)
| 2001-07-05 | Paper |
scientific article; zbMATH DE number 1612558 (Why is no real title available?)
| 2001-07-01 | Paper |
scientific article; zbMATH DE number 1543301 (Why is no real title available?)
| 2001-02-27 | Paper |
scientific article; zbMATH DE number 1389654 (Why is no real title available?)
| 2000-01-17 | Paper |
scientific article; zbMATH DE number 1301753 (Why is no real title available?)
| 1999-10-03 | Paper |
scientific article; zbMATH DE number 1324439 (Why is no real title available?)
| 1999-08-16 | Paper |
scientific article; zbMATH DE number 1189109 (Why is no real title available?)
| 1999-04-08 | Paper |
scientific article; zbMATH DE number 877748 (Why is no real title available?)
| 1996-01-01 | Paper |
Type 2 computational complexity of functions on Cantor's space
Theoretical Computer Science | 1991-01-01 | Paper |
Compactness in constructive analysis revisited
Annals of Pure and Applied Logic | 1987-01-01 | Paper |
Representations of the real numbers and of the open subsets of the set of real numbers
Annals of Pure and Applied Logic | 1987-01-01 | Paper |
Theory of representations
Theoretical Computer Science | 1985-01-01 | Paper |
scientific article; zbMATH DE number 3952751 (Why is no real title available?)
| 1984-01-01 | Paper |
scientific article; zbMATH DE number 3887669 (Why is no real title available?)
| 1984-01-01 | Paper |
scientific article; zbMATH DE number 3926913 (Why is no real title available?)
| 1984-01-01 | Paper |
scientific article; zbMATH DE number 3788601 (Why is no real title available?)
| 1982-01-01 | Paper |
