| Publication | Date of Publication | Type |
|---|
| Defining trace semantics for CSP-Agda | 2026-02-20 | Paper |
The extended predicative Mahlo universe in Martin-Löf type theory
Journal Of Logic And Computation | 2024-11-12 | Paper |
| Verification of bitcoin script in Agda using weakest preconditions for access control | 2024-08-01 | Paper |
| Martin Hofmann's Case for Non-Strictly Positive Data Types | 2022-07-21 | Paper |
How to reason coinductively informally
Advances in Proof Theory | 2020-08-07 | Paper |
| Undecidability of equality for codata types | 2018-10-23 | Paper |
Interactive programming in Agda -- objects and graphical user interfaces
Journal of Functional Programming | 2017-10-23 | Paper |
The use of trustworthy principles in a revised Hilbert's program
Gentzen's Centenary | 2017-09-27 | Paper |
Fibred data types
2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science | 2017-07-03 | Paper |
A light-weight integration of automated and interactive theorem proving
Mathematical Structures in Computer Science | 2016-07-28 | Paper |
Coalgebras as types determined by their elimination rules
Epistemology versus Ontology | 2015-06-05 | Paper |
Automated Verification of Signalling Principles in Railway Interlocking Systems
Electronic Notes in Theoretical Computer Science | 2015-03-18 | Paper |
Copatterns, programming infinite structures by observations
Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages | 2014-11-27 | Paper |
Unnesting of copatterns
Lecture Notes in Computer Science | 2014-07-24 | Paper |
| A finite axiomatisation of inductive-inductive definitions | 2014-06-24 | Paper |
| State dependent IO-monads in type theory | 2013-09-20 | Paper |
A categorical semantics for inductive-inductive definitions
Algebra and Coalgebra in Computer Science | 2011-09-02 | Paper |
| scientific article; zbMATH DE number 5862936 (Why is no real title available?) | 2011-03-09 | Paper |
Inductive-inductive definitions
Computer Science Logic | 2010-09-03 | Paper |
A provably correct translation of the \(\lambda \)-calculus into a mathematical model of C++
Theory of Computing Systems | 2009-05-08 | Paper |
Weak Bisimulation Approximants
Computer Science Logic | 2009-03-12 | Paper |
| Universes in type theory. I. Inaccessibles and Mahlo | 2008-04-14 | Paper |
| Proof theory of Martin-Löf type theory. An overview | 2008-02-08 | Paper |
Logical Approaches to Computational Barriers
Lecture Notes in Computer Science | 2007-04-30 | Paper |
Indexed induction-recursion
The Journal of Logic and Algebraic Programming | 2005-12-22 | Paper |
Induction-recursion and initial algebras.
Annals of Pure and Applied Logic | 2003-11-25 | Paper |
| scientific article; zbMATH DE number 2006633 (Why is no real title available?) | 2003-11-23 | Paper |
| scientific article; zbMATH DE number 2003162 (Why is no real title available?) | 2003-11-12 | Paper |
| scientific article; zbMATH DE number 1670486 (Why is no real title available?) | 2001-11-11 | Paper |
| scientific article; zbMATH DE number 1420856 (Why is no real title available?) | 2000-12-17 | Paper |
| scientific article; zbMATH DE number 1390279 (Why is no real title available?) | 2000-09-15 | Paper |
Extending Martin-Löf type theory by one Mahlo-universe
Archive for Mathematical Logic | 2000-09-05 | Paper |
| scientific article; zbMATH DE number 1342277 (Why is no real title available?) | 1999-09-22 | Paper |
The proof-theoretic analysis of transfinitely iterated fixed point theories
Journal of Symbolic Logic | 1999-09-16 | Paper |
Well-ordering proofs for Martin-Löf type theory
Annals of Pure and Applied Logic | 1999-08-16 | Paper |
| scientific article; zbMATH DE number 1302068 (Why is no real title available?) | 1999-06-16 | Paper |
| scientific article; zbMATH DE number 1114019 (Why is no real title available?) | 1998-11-10 | Paper |
| scientific article; zbMATH DE number 1088206 (Why is no real title available?) | 1997-11-17 | Paper |
| scientific article; zbMATH DE number 1086681 (Why is no real title available?) | 1997-11-13 | Paper |
| scientific article; zbMATH DE number 946307 (Why is no real title available?) | 1996-11-17 | Paper |
