| Publication | Date of Publication | Type |
|---|
| Causal reversibility implies time reversibility | 2024-05-29 | Paper |
| Reversible debugging of concurrent Erlang programs: supporting imperative primitives | 2024-03-20 | Paper |
| Reversibility in Erlang: imperative constructs | 2022-11-11 | Paper |
| Logic-independent proof search in logical frameworks (short paper) | 2022-11-09 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4964708 | 2021-03-03 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5111895 | 2020-05-27 | Paper |
| Relational data across mathematical libraries | 2020-01-22 | Paper |
| The Coq library as a theory graph | 2020-01-22 | Paper |
| A plugin to export Coq libraries to XML | 2020-01-22 | Paper |
| Implementing type theory in higher order constraint logic programming | 2019-10-09 | Paper |
| Matita Tutorial | 2019-09-18 | Paper |
| On the Relative Usefulness of Fireballs | 2018-04-23 | Paper |
| On the value of variables | 2017-09-04 | Paper |
| A survey on retrieval of mathematical knowledge | 2017-07-25 | Paper |
| ELPI: Fast, Embeddable, $$\lambda $$ Prolog Interpreter | 2016-01-12 | Paper |
| Certified Complexity (CerCo) | 2016-01-07 | Paper |
| A survey on retrieval of mathematical knowledge | 2015-11-20 | Paper |
| On the Value of Variables | 2015-01-13 | Paper |
| A User Interface for a Mathematical System that Allows Ambiguous Formulae | 2014-06-27 | Paper |
| Tinycals: step by step tacticals | 2013-12-20 | Paper |
| Reduction and conversion strategies for the calculus of (co)inductive constructions. I | 2013-12-06 | Paper |
| Formal metatheory of programming languages in the Matita interactive theorem prover | 2013-04-17 | Paper |
| A bi-directional refinement algorithm for the calculus of (co)inductive constructions | 2012-04-03 | Paper |
| Lebesgue's dominated convergence theorem in Bishop's style | 2011-12-12 | Paper |
| Formalising Overlap Algebras in Matita | 2011-10-21 | Paper |
| The Matita Interactive Theorem Prover | 2011-07-29 | Paper |
| A Foundational View on Integration Problems | 2011-07-29 | Paper |
| Formalization of Formal Topology by Means of the Interactive Theorem Prover Matita | 2011-07-29 | Paper |
| Some Considerations on the Usability of Interactive Provers | 2010-08-24 | Paper |
| Theoretical Computer Science | 2010-02-23 | Paper |
| Declarative representation of proof terms | 2010-01-25 | Paper |
| A compact kernel for the calculus of inductive constructions | 2009-11-23 | Paper |
| Hints in Unification | 2009-10-20 | Paper |
| Spurious disambiguation errors and how to get rid of them | 2009-09-18 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3497625 | 2009-07-27 | Paper |
| Natural Deduction Environment for Matita | 2009-07-09 | Paper |
| Crafting a Proof Assistant | 2009-03-10 | Paper |
| Working with Mathematical Structures in Type Theory | 2008-06-03 | Paper |
| User interaction with the Matita proof assistant | 2007-12-03 | Paper |
| Spurious Disambiguation Error Detection | 2007-11-28 | Paper |
| A Formal Correspondence Between OMDoc with Alternative Proofs and the ${\overline{\lambda}\mu\tilde{\mu}}$ -Calculus | 2007-09-05 | Paper |
| Mathematical Knowledge Management | 2007-02-12 | Paper |
| Mathematical Knowledge Management | 2007-02-12 | Paper |
| Types for Proofs and Programs | 2006-11-13 | Paper |
| Types for Proofs and Programs | 2006-11-13 | Paper |
| Mathematical Knowledge Management | 2005-08-26 | Paper |
| Mathematical Knowledge Management | 2005-08-26 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4413879 | 2003-07-21 | Paper |
| Mathematical knowledge management in HELM | 2003-06-09 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4790651 | 2003-02-04 | Paper |
| Mathematical knowledge management in HELM | 2002-02-14 | Paper |
