| Publication | Date of Publication | Type |
|---|
| Open bar -- a Brouwerian intuitionistic logic with a pinch of excluded middle | 2026-03-23 | Paper |
Expressing computational complexity in constructive type theory
Lecture Notes in Computer Science | 2023-12-12 | Paper |
Type theory as a foundation for computer science
Lecture Notes in Computer Science | 2022-08-16 | Paper |
Computability beyond Church-Turing via choice sequences
Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science | 2021-01-20 | Paper |
| Bar induction. The good, the bad, and the ugly | 2021-01-19 | Paper |
Bar induction is compatible with constructive type theory
Journal of the ACM | 2019-11-21 | Paper |
Intuitionistic ancestral logic
Journal Of Logic And Computation | 2019-07-29 | Paper |
Implementing Euclid's straightedge and compass constructions in type theory
Annals of Mathematics and Artificial Intelligence | 2019-05-16 | Paper |
On building constructive formal theories of computation noting the roles of Turing, Church, and Brouwer
2012 27th Annual IEEE Symposium on Logic in Computer Science | 2017-05-16 | Paper |
Intuitionistic ancestral logic as a dependently typed abstract programming language
Logic, Language, Information, and Computation | 2015-09-24 | Paper |
| scientific article; zbMATH DE number 6307924 (Why is no real title available?) | 2014-06-24 | Paper |
Intuitionistic completeness of first-order logic
Annals of Pure and Applied Logic | 2014-01-13 | Paper |
Russell's Orders in Kripke's Theory of Truth and Computational Type Theory
Handbook of the History of Logic | 2012-10-12 | Paper |
Extracting the resolution algorithm from a completeness proof for the propositional calculus
Annals of Pure and Applied Logic | 2011-08-26 | Paper |
Knowledge-based synthesis of distributed systems using event structures
Logical Methods in Computer Science | 2011-05-26 | Paper |
Building Mathematics-Based Software Systems to Advance Science and Create Knowledge
Lecture Notes in Computer Science | 2009-11-12 | Paper |
Extracting Programs from Constructive HOL Proofs Via IZF Set-Theoretic Semantics
Automated Reasoning | 2009-03-12 | Paper |
Extracting Programs from Constructive HOL Proofs via IZF Set-Theoretic Semantics
Logical Methods in Computer Science | 2008-11-13 | Paper |
| Information-intensive proof technology | 2008-01-14 | Paper |
Extracting the Resolution Algorithm from a Completeness Proof for the Propositional Calculus
Logical Foundations of Computer Science | 2008-01-04 | Paper |
Innovations in computational type theory using Nuprl
Journal of Applied Logic | 2007-02-20 | Paper |
Logic for Programming, Artificial Intelligence, and Reasoning
Lecture Notes in Computer Science | 2005-11-10 | Paper |
Mathematical Knowledge Management
Lecture Notes in Computer Science | 2005-08-26 | Paper |
| scientific article; zbMATH DE number 2154393 (Why is no real title available?) | 2005-04-09 | Paper |
| scientific article; zbMATH DE number 2110617 (Why is no real title available?) | 2004-10-26 | Paper |
| scientific article; zbMATH DE number 1870418 (Why is no real title available?) | 2003-02-18 | Paper |
| Nuprl's class theory and its applications | 2002-10-23 | Paper |
| Logical aspects of digital mathematics libraries. (Extended abstract) | 2002-02-14 | Paper |
| scientific article; zbMATH DE number 1614694 (Why is no real title available?) | 2001-07-05 | Paper |
Metalogical frameworks. II: Developing a reflected decision procedure
Journal of Automated Reasoning | 1999-10-18 | Paper |
| scientific article; zbMATH DE number 1342250 (Why is no real title available?) | 1999-09-22 | Paper |
| scientific article; zbMATH DE number 1331927 (Why is no real title available?) | 1999-09-02 | Paper |
A note on complexity measures for inductive classes in constructive type theory
Information and Computation | 1999-07-06 | Paper |
| scientific article; zbMATH DE number 1215502 (Why is no real title available?) | 1999-06-21 | Paper |
| scientific article; zbMATH DE number 1070622 (Why is no real title available?) | 1997-10-07 | Paper |
| scientific article; zbMATH DE number 785045 (Why is no real title available?) | 1996-02-13 | Paper |
Computational foundations of basic recursive function theory
Theoretical Computer Science | 1994-11-03 | Paper |
| scientific article; zbMATH DE number 65537 (Why is no real title available?) | 1992-09-27 | Paper |
| scientific article; zbMATH DE number 4155932 (Why is no real title available?) | 1990-01-01 | Paper |
Proofs as programs
ACM Transactions on Programming Languages and Systems | 1985-01-01 | Paper |
| scientific article; zbMATH DE number 3894466 (Why is no real title available?) | 1985-01-01 | Paper |
| scientific article; zbMATH DE number 3928338 (Why is no real title available?) | 1985-01-01 | Paper |
Writing programs that construct proofs
Journal of Automated Reasoning | 1985-01-01 | Paper |
The Type Theory of PL/CV3
ACM Transactions on Programming Languages and Systems | 1984-01-01 | Paper |
| scientific article; zbMATH DE number 3911699 (Why is no real title available?) | 1984-01-01 | Paper |
Programs as proofs: A synopsis
Information Processing Letters | 1983-01-01 | Paper |
| scientific article; zbMATH DE number 3850461 (Why is no real title available?) | 1983-01-01 | Paper |
| scientific article; zbMATH DE number 3795950 (Why is no real title available?) | 1982-01-01 | Paper |
| scientific article; zbMATH DE number 3797728 (Why is no real title available?) | 1982-01-01 | Paper |
On the Computational Complexity of Program Scheme Equivalence
SIAM Journal on Computing | 1980-01-01 | Paper |
| scientific article; zbMATH DE number 3735149 (Why is no real title available?) | 1980-01-01 | Paper |
A Hierarchical Approach to Formal Semantics With Application to the Definition of PL/ CS
ACM Transactions on Programming Languages and Systems | 1979-01-01 | Paper |
| scientific article; zbMATH DE number 3679150 (Why is no real title available?) | 1978-01-01 | Paper |
| scientific article; zbMATH DE number 3566134 (Why is no real title available?) | 1977-01-01 | Paper |
| scientific article; zbMATH DE number 3635474 (Why is no real title available?) | 1977-01-01 | Paper |
Computability concepts for programming language semantics
Theoretical Computer Science | 1976-01-01 | Paper |
| scientific article; zbMATH DE number 3560704 (Why is no real title available?) | 1975-01-01 | Paper |
| scientific article; zbMATH DE number 3480091 (Why is no real title available?) | 1973-01-01 | Paper |
| scientific article; zbMATH DE number 3403733 (Why is no real title available?) | 1972-01-01 | Paper |
Subrecursive Programming Languages, Part I
Journal of the ACM | 1972-01-01 | Paper |
The Operator Gap
Journal of the ACM | 1972-01-01 | Paper |
On Classes of Program Schemata
SIAM Journal on Computing | 1972-01-01 | Paper |
| scientific article; zbMATH DE number 3551849 (Why is no real title available?) | 1972-01-01 | Paper |
Subrecursive program schemata I P II. I: Undecidable equivalence problems. II: Decidable equivalence problems
Journal of Computer and System Sciences | 1972-01-01 | Paper |
| scientific article; zbMATH DE number 3407149 (Why is no real title available?) | 1971-01-01 | Paper |
Subrecursive programming languages. II. On program size
Journal of Computer and System Sciences | 1971-01-01 | Paper |
| scientific article; zbMATH DE number 3418614 (Why is no real title available?) | 1971-01-01 | Paper |
| scientific article; zbMATH DE number 3407138 (Why is no real title available?) | 1971-01-01 | Paper |
