| Publication | Date of Publication | Type |
|---|
Causal reversibility implies time reversibility
| 2024-05-29 | Paper |
Reversible debugging of concurrent Erlang programs: supporting imperative primitives
Journal of Logical and Algebraic Methods in Programming | 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
Mathematical Structures in Computer Science | 2019-10-09 | Paper |
Matita Tutorial
| 2019-09-18 | Paper |
On the Relative Usefulness of Fireballs
2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science | 2018-04-23 | Paper |
On the value of variables
Information and Computation | 2017-09-04 | Paper |
A survey on retrieval of mathematical knowledge
Mathematics in Computer Science | 2017-07-25 | Paper |
ELPI: fast, embeddable, \(\lambda \)Prolog interpreter
Logic for Programming, Artificial Intelligence, and Reasoning | 2016-01-12 | Paper |
Certified complexity (CerCo)
Foundational and Practical Aspects of Resource Analysis | 2016-01-07 | Paper |
A survey on retrieval of mathematical knowledge
Lecture Notes in Computer Science | 2015-11-20 | Paper |
On the value of variables
Logic, Language, Information, and Computation | 2015-01-13 | Paper |
A user interface for a mathematical system that allows ambiguous formulae
Electronic Notes in Theoretical Computer Science | 2014-06-27 | Paper |
Tinycals: step by step tacticals
Electronic Notes in Theoretical Computer Science | 2013-12-20 | Paper |
Reduction and conversion strategies for the calculus of (co)inductive constructions. I
Electronic Notes in Theoretical Computer Science | 2013-12-06 | Paper |
Formal metatheory of programming languages in the Matita interactive theorem prover
Journal of Automated Reasoning | 2013-04-17 | Paper |
A bi-directional refinement algorithm for the calculus of (co)inductive constructions
Logical Methods in Computer Science | 2012-04-03 | Paper |
Lebesgue's dominated convergence theorem in Bishop's style
Annals of Pure and Applied Logic | 2011-12-12 | Paper |
Formalising overlap algebras in Matita
Mathematical Structures in Computer Science | 2011-10-21 | Paper |
The Matita interactive theorem prover
Lecture Notes in Computer Science | 2011-07-29 | Paper |
A foundational view on integration problems
Lecture Notes in Computer Science | 2011-07-29 | Paper |
Formalization of formal topology by means of the interactive theorem prover Matita
Lecture Notes in Computer Science | 2011-07-29 | Paper |
Some considerations on the usability of interactive provers
Lecture Notes in Computer Science | 2010-08-24 | Paper |
A constructive proof of the soundness of the encoding of random access machines in a Linda calculus with ordered semantics.
Lecture Notes in Computer Science | 2010-02-23 | Paper |
Declarative representation of proof terms
Journal of Automated Reasoning | 2010-01-25 | Paper |
A compact kernel for the calculus of inductive constructions
Sādhanā | 2009-11-23 | Paper |
Hints in Unification
Lecture Notes in Computer Science | 2009-10-20 | Paper |
Spurious disambiguation errors and how to get rid of them
Mathematics in Computer Science | 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
Lecture Notes in Computer Science | 2009-07-09 | Paper |
Crafting a Proof Assistant
Lecture Notes in Computer Science | 2009-03-10 | Paper |
Working with Mathematical Structures in Type Theory
Lecture Notes in Computer Science | 2008-06-03 | Paper |
User interaction with the Matita proof assistant
Journal of Automated Reasoning | 2007-12-03 | Paper |
Spurious Disambiguation Error Detection
Towards Mechanized Mathematical Assistants | 2007-11-28 | Paper |
A Formal Correspondence Between OMDoc with Alternative Proofs and the ${\overline{\lambda}\mu\tilde{\mu}}$ -Calculus
Lecture Notes in Computer Science | 2007-09-05 | Paper |
Mathematical Knowledge Management
Lecture Notes in Computer Science | 2007-02-12 | Paper |
Mathematical Knowledge Management
Lecture Notes in Computer Science | 2007-02-12 | Paper |
Types for Proofs and Programs
Lecture Notes in Computer Science | 2006-11-13 | Paper |
Types for Proofs and Programs
Lecture Notes in Computer Science | 2006-11-13 | Paper |
Mathematical Knowledge Management
Lecture Notes in Computer Science | 2005-08-26 | Paper |
Mathematical Knowledge Management
Lecture Notes in Computer Science | 2005-08-26 | Paper |
scientific article; zbMATH DE number 1951627 (Why is no real title available?)
| 2003-07-21 | Paper |
Mathematical knowledge management in HELM
Annals of Mathematics and Artificial Intelligence | 2003-06-09 | Paper |
scientific article; zbMATH DE number 1863377 (Why is no real title available?)
| 2003-02-04 | Paper |
Mathematical knowledge management in HELM
| 2002-02-14 | Paper |
