| 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 |
| Nonuniform coercions via unification hints | 2021-03-03 | Paper |
| A term rewriting system for Kuratowski's closure-complement problem | 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 |
| A constructive proof of the soundness of the encoding of random access machines in a Linda calculus with ordered semantics. | 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 |
| A constructive and formal proof of Lebesgue's dominated convergence theorem in the interactive theorem prover Matita | 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 |
