| Publication | Date of Publication | Type |
|---|
| Expressing computational complexity in constructive type theory | 2023-12-12 | Paper |
| Type theory as a foundation for computer science | 2022-08-16 | Paper |
| Computability beyond Church-Turing via choice sequences | 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 | 2019-11-21 | Paper |
| Intuitionistic ancestral logic | 2019-07-29 | Paper |
| Implementing Euclid's straightedge and compass constructions in type theory | 2019-05-16 | Paper |
| On building constructive formal theories of computation noting the roles of Turing, Church, and Brouwer | 2017-05-16 | Paper |
| Intuitionistic ancestral logic as a dependently typed abstract programming language | 2015-09-24 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4981439 | 2014-06-24 | Paper |
| Intuitionistic completeness of first-order logic | 2014-01-13 | Paper |
| Russell's Orders in Kripke's Theory of Truth and Computational Type Theory | 2012-10-12 | Paper |
| Extracting the resolution algorithm from a completeness proof for the propositional calculus | 2011-08-26 | Paper |
| Knowledge-based synthesis of distributed systems using event structures | 2011-05-26 | Paper |
| Building Mathematics-Based Software Systems to Advance Science and Create Knowledge | 2009-11-12 | Paper |
| Extracting Programs from Constructive HOL Proofs Via IZF Set-Theoretic Semantics | 2009-03-12 | Paper |
| Extracting Programs from Constructive HOL Proofs via IZF Set-Theoretic Semantics | 2008-11-13 | Paper |
| Information-intensive proof technology | 2008-01-14 | Paper |
| Extracting the Resolution Algorithm from a Completeness Proof for the Propositional Calculus | 2008-01-04 | Paper |
| Innovations in computational type theory using Nuprl | 2007-02-20 | Paper |
| Logic for Programming, Artificial Intelligence, and Reasoning | 2005-11-10 | Paper |
| Mathematical Knowledge Management | 2005-08-26 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4664919 | 2005-04-09 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4823137 | 2004-10-26 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4793030 | 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 |
| https://portal.mardi4nfdi.de/entity/Q2723417 | 2001-07-05 | Paper |
| Metalogical frameworks. II: Developing a reflected decision procedure | 1999-10-18 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4263836 | 1999-09-22 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4261732 | 1999-09-02 | Paper |
| A note on complexity measures for inductive classes in constructive type theory | 1999-07-06 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4215639 | 1999-06-21 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4357062 | 1997-10-07 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4842534 | 1996-02-13 | Paper |
| Computational foundations of basic recursive function theory | 1994-11-03 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4012886 | 1992-09-27 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3484381 | 1990-01-01 | Paper |
| Proofs as programs | 1985-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5186727 | 1985-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3702502 | 1985-01-01 | Paper |
| Writing programs that construct proofs | 1985-01-01 | Paper |
| The Type Theory of PL/CV3 | 1984-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3687706 | 1984-01-01 | Paper |
| Programs as proofs: A synopsis | 1983-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3319764 | 1983-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4740562 | 1982-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4742765 | 1982-01-01 | Paper |
| On the Computational Complexity of Program Scheme Equivalence | 1980-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3922177 | 1980-01-01 | Paper |
| A Hierarchical Approach to Formal Semantics With Application to the Definition of PL/ CS | 1979-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3875311 | 1978-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4138096 | 1977-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4195920 | 1977-01-01 | Paper |
| Computability concepts for programming language semantics | 1976-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4131618 | 1975-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4062633 | 1973-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5670174 | 1972-01-01 | Paper |
| Subrecursive Programming Languages, Part I | 1972-01-01 | Paper |
| The Operator Gap | 1972-01-01 | Paper |
| On Classes of Program Schemata | 1972-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4125721 | 1972-01-01 | Paper |
| Subrecursive program schemata I P II. I: Undecidable equivalence problems. II: Decidable equivalence problems | 1972-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5672170 | 1971-01-01 | Paper |
| Subrecursive programming languages. II. On program size | 1971-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5681525 | 1971-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5672158 | 1971-01-01 | Paper |
