| Publication | Date of Publication | Type |
|---|
| scientific article; zbMATH DE number 7649978 (Why is no real title available?) | 2023-02-03 | Paper |
| Superposition as a logical glue | 2021-03-03 | Paper |
Superposition as a logical glue
(available as arXiv preprint) | 2021-03-03 | Paper |
| Nonuniform coercions via unification hints | 2021-03-03 | Paper |
Nonuniform coercions via unification hints
(available as arXiv preprint) | 2021-03-03 | Paper |
Implementing type theory in higher order constraint logic programming
Mathematical Structures in Computer Science | 2019-10-09 | Paper |
Hamiltonian fluid reductions of electromagnetic drift-kinetic equations for an arbitrary number of moments
Annals of Physics | 2016-09-02 | Paper |
ELPI: fast, embeddable, \(\lambda \)Prolog interpreter
Logic for Programming, Artificial Intelligence, and Reasoning | 2016-01-12 | Paper |
Asynchronous processing of Coq documents: from the kernel up to the user interface
Interactive Theorem Proving | 2015-09-14 | Paper |
A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3)
Interactive Theorem Proving | 2014-09-08 | Paper |
An Interactive Driver for Goal-directed Proof Strategies
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 |
Pervasive parallelism in highly-trustable interactive theorem proving systems
Lecture Notes in Computer Science | 2013-08-09 | Paper |
A machine-checked proof of the odd order theorem
Interactive Theorem Proving | 2013-08-07 | Paper |
Canonical structures for the working Coq user
Interactive Theorem Proving | 2013-08-07 | Paper |
Formal metatheory of programming languages in the Matita interactive theorem prover
Journal of Automated Reasoning | 2013-04-17 | Paper |
A Language of Patterns for Subterm Selection
Interactive Theorem Proving | 2012-09-20 | Paper |
A bi-directional refinement algorithm for the calculus of (co)inductive constructions
Logical Methods in Computer Science | 2012-04-03 | 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 |
Smart matching
Lecture Notes in Computer Science | 2010-08-24 | 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 |
| 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 |
A Modular Formalisation of Finite Group Theory
Lecture Notes in Computer Science | 2008-09-02 | 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 |
Higher order Proof Reconstruction from Paramodulation-Based Refutations: The Unit Equality Case
Towards Mechanized Mathematical Assistants | 2007-11-28 | Paper |
Types for Proofs and Programs
Lecture Notes in Computer Science | 2006-11-13 | Paper |
Event indexing systems for efficient selection and analysis of HERA data
Computer Physics Communications | 2001-10-10 | Paper |
