| Publication | Date of Publication | Type |
|---|
Positive Hennessy-Milner logic for branching bisimulation
Logical Methods in Computer Science | 2026-02-13 | Paper |
| Classical natural deduction from truth tables | 2024-11-26 | Paper |
| Congruence types | 2024-06-21 | Paper |
Conservativity between logics and typed λ calculi
Lecture Notes in Computer Science | 2023-12-08 | Paper |
A short and flexible proof of strong normalization for the calculus of constructions
Lecture Notes in Computer Science | 2023-12-08 | Paper |
| Proof Terms for Generalized Natural Deduction | 2023-11-03 | Paper |
Apartness and distinguishing formulas in Hennessy-Milner logic
Lecture Notes in Computer Science | 2023-07-26 | Paper |
Characteristics of de Bruijn’s early proof checker Automath
Fundamenta Informaticae | 2022-07-14 | Paper |
| The construction of set-truncated higher inductive types | 2022-04-29 | Paper |
Characteristics of de Bruijn's early proof checker Automath
(available as arXiv preprint) | 2022-03-02 | Paper |
scientific article; zbMATH DE number 7407787 (Why is no real title available?)
(available as arXiv preprint) | 2021-10-08 | Paper |
| scientific article; zbMATH DE number 7407787 (Why is no real title available?) | 2021-10-08 | Paper |
| Continuation calculus | 2021-09-09 | Paper |
Continuation calculus
(available as arXiv preprint) | 2021-09-09 | Paper |
| A type system for continuation calculus | 2021-06-24 | Paper |
A type system for continuation calculus
(available as arXiv preprint) | 2021-06-24 | Paper |
The Tactician. A seamless, interactive tactic learner and prover for Coq
(available as arXiv preprint) | 2021-01-20 | Paper |
Strong normalization for truth table natural deduction
Fundamenta Informaticae | 2020-01-24 | Paper |
Deriving natural deduction rules from truth tables
Logic and Its Applications | 2019-07-24 | Paper |
Modular properties of algebraic type systems
Higher-Order Algebra, Logic, and Term Rewriting | 2019-01-11 | Paper |
Type theory based on dependent inductive and coinductive types
Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science | 2018-04-23 | Paper |
| A formalisation of consistent consequence for Boolean equation systems | 2018-01-04 | Paper |
| A mathematical proof proved correct: the most efficient way to pack spheres | 2017-05-18 | Paper |
| Type theory and formal proof. An introduction | 2014-10-22 | Paper |
N. G. de Bruijn's contribution to the formalization of mathematics
Indagationes Mathematicae. New Series | 2014-09-03 | Paper |
Developing corpus-based translation methods between informal and formal mathematics: project description
Lecture Notes in Computer Science | 2014-08-07 | Paper |
Deduction graphs with universal quantification
Electronic Notes in Theoretical Computer Science | 2014-01-17 | Paper |
A logical framework with explicit conversions
Electronic Notes in Theoretical Computer Science | 2014-01-10 | Paper |
| A calculus of tactics and its operational semantics | 2013-09-09 | Paper |
Formal mathematics on display: a wiki for Flyspeck
Lecture Notes in Computer Science | 2013-08-09 | Paper |
Communicating formal proofs: the case of Flyspeck
Interactive Theorem Proving | 2013-08-07 | Paper |
The \(\lambda \mu^{\mathbf{T}}\)-calculus
Annals of Pure and Applied Logic | 2013-04-15 | Paper |
Learning2Reason
Lecture Notes in Computer Science | 2011-07-29 | Paper |
The correctness of Newman's typability algorithm and some of its extensions
Theoretical Computer Science | 2011-07-07 | Paper |
Levels of undecidability in rewriting
Information and Computation | 2011-02-21 | Paper |
Automated Machine-Checked Hybrid System Safety Proofs
Interactive Theorem Proving | 2010-09-14 | Paper |
Proviola: a tool for proof re-animation
Lecture Notes in Computer Science | 2010-08-24 | Paper |
A Wiki for Mizar: motivation, considerations, and initial prototype
Lecture Notes in Computer Science | 2010-08-24 | Paper |
Proof assistants: history, ideas and future
Sādhanā | 2009-11-23 | Paper |
Degrees of Undecidability in Term Rewriting
Computer Science Logic | 2009-11-12 | Paper |
Social processes, program verification and all that
Mathematical Structures in Computer Science | 2009-11-11 | Paper |
Introduction to Type Theory
Language Engineering and Rigorous Software Development | 2009-07-28 | Paper |
A Logically Saturated Extension of ${{\bar\lambda\mu\tilde{\mu}}}$
Lecture Notes in Computer Science | 2009-07-09 | Paper |
Rewriting Techniques and Applications
Lecture Notes in Computer Science | 2009-04-30 | Paper |
(In)consistency of Extensions of Higher Order Logic and Type Theory
Lecture Notes in Computer Science | 2009-03-10 | Paper |
Natural deduction via graphs: formal definition and computation rules
Mathematical Structures in Computer Science | 2007-09-26 | Paper |
From Deduction Graphs to Proof Nets: Boxes and Sharing in the Graphical Presentation of Deductions
Lecture Notes in Computer Science | 2007-09-05 | Paper |
Constructive analysis, types and exact real numbers
Mathematical Structures in Computer Science | 2007-04-12 | Paper |
Mathematical Knowledge Management
Lecture Notes in Computer Science | 2007-02-12 | Paper |
Mathematical Knowledge Management
Lecture Notes in Computer Science | 2005-08-26 | Paper |
| scientific article; zbMATH DE number 2085168 (Why is no real title available?) | 2004-08-09 | Paper |
| scientific article; zbMATH DE number 2085169 (Why is no real title available?) | 2004-08-09 | Paper |
A constructive algebraic hierarchy in Coq.
Journal of Symbolic Computation | 2003-08-21 | Paper |
| scientific article; zbMATH DE number 1948185 (Why is no real title available?) | 2003-07-10 | Paper |
| scientific article; zbMATH DE number 1722653 (Why is no real title available?) | 2002-03-21 | Paper |
Proof by computation in the Coq system
Theoretical Computer Science | 2002-03-03 | Paper |
| Certified and portable mathematical documents from formal contexts | 2002-02-14 | Paper |
| Proof-assistants using dependent type systems | 2001-12-04 | Paper |
| scientific article; zbMATH DE number 1670742 (Why is no real title available?) | 2001-11-11 | Paper |
Some logical and syntactical observations concerning the first-order dependent type system λP
Mathematical Structures in Computer Science | 2000-06-29 | Paper |
| scientific article; zbMATH DE number 1424052 (Why is no real title available?) | 2000-06-07 | Paper |
| scientific article; zbMATH DE number 1400716 (Why is no real title available?) | 2000-02-09 | Paper |
| scientific article; zbMATH DE number 1377703 (Why is no real title available?) | 1999-12-14 | Paper |
Modularity of strong normalization in the algebraic-λ-cube
Journal of Functional Programming | 1999-03-16 | Paper |
Explicit substitution. On the edge of strong normalization
Theoretical Computer Science | 1999-01-12 | Paper |
| scientific article; zbMATH DE number 1086666 (Why is no real title available?) | 1997-11-13 | Paper |
