| Publication | Date of Publication | Type |
|---|
Effective applicative structures
Category Theory and Computer Science | 2022-12-16 | Paper |
Paths, computations and labels in the λ-calculus
Rewriting Techniques and Applications | 2022-12-09 | Paper |
δο!∈=1 Optimizing optimal λ-calculus implementations
Rewriting Techniques and Applications | 2022-12-09 | Paper |
Optimal reductions in interaction systems
Lecture Notes in Computer Science | 2022-11-02 | Paper |
| Superposition as a logical glue | 2021-03-03 | Paper |
Superposition as a logical glue
(available as arXiv preprint) | 2021-03-03 | Paper |
| Matita Tutorial | 2019-09-18 | Paper |
| scientific article; zbMATH DE number 7106484 (Why is no real title available?) | 2019-09-18 | Paper |
On the dynamics of sharing graphs
Automata, Languages and Programming | 2018-07-04 | Paper |
The cost of usage in the \(\lambda\)-calculus
2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science | 2017-07-03 | Paper |
Intuitionistic light affine logic
ACM Transactions on Computational Logic | 2017-06-13 | Paper |
Reverse complexity
Journal of Automated Reasoning | 2016-05-26 | Paper |
A formalization of multi-tape Turing machines
Theoretical Computer Science | 2015-10-12 | Paper |
Computational Complexity Via Finite Types
ACM Transactions on Computational Logic | 2015-09-17 | Paper |
(Optimal) duplication is not elementary recursive
Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages | 2015-03-17 | Paper |
A formal proof of Borodin-Trakhtenbrot's gap theorem
Certified Programs and Proofs | 2015-01-13 | Paper |
The intensional content of Rice's theorem
Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages | 2014-09-12 | Paper |
An Interactive Driver for Goal-directed Proof Strategies
Electronic Notes in Theoretical Computer Science | 2014-06-27 | Paper |
| The optimal implementation of functional programming languages | 2014-02-21 | Paper |
A machine-checked proof of the odd order theorem
Interactive Theorem Proving | 2013-08-07 | Paper |
Rating Disambiguation Errors
Certified Programs and Proofs | 2013-04-19 | Paper |
Formal metatheory of programming languages in the Matita interactive theorem prover
Journal of Automated Reasoning | 2013-04-17 | Paper |
Formalizing Turing Machines
Logic, Language, Information and Computation | 2012-09-21 | Paper |
A Compact Proof of Decidability for Regular Expression Equivalence
Interactive Theorem Proving | 2012-09-20 | Paper |
A Web Interface for Matita
Lecture Notes in Computer Science | 2012-09-07 | Paper |
Proof, message and certificate
Lecture Notes in Computer Science | 2012-09-07 | Paper |
A bi-directional refinement algorithm for the calculus of (co)inductive constructions
Logical Methods in Computer Science | 2012-04-03 | Paper |
Zen and the art of formalisation
Mathematical Structures in Computer Science | 2011-10-21 | Paper |
The Matita interactive theorem prover
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 |
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 |
Social processes, program verification and all that
Mathematical Structures in Computer Science | 2009-11-11 | Paper |
Hints in Unification
Lecture Notes in Computer Science | 2009-10-20 | Paper |
| scientific article; zbMATH DE number 5587007 (Why is no real title available?) | 2009-07-27 | Paper |
About the Formalization of Some Results by Chebyshev in Number Theory
Lecture Notes in Computer Science | 2009-07-02 | Paper |
Crafting a Proof Assistant
Lecture Notes in Computer Science | 2009-03-10 | Paper |
| Searching mathematics on the web: state of the art and future developments | 2008-05-05 | 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 |
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 |
Mathematical Knowledge Management
Lecture Notes in Computer Science | 2005-08-26 | Paper |
| scientific article; zbMATH DE number 2185649 (Why is no real title available?) | 2005-07-04 | Paper |
(Optimal) duplication is not elementary recursive
Information and Computation | 2004-10-04 | Paper |
| scientific article; zbMATH DE number 2078371 (Why is no real title available?) | 2004-07-09 | 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 |
Parallel beta reduction is not elementary recursive
Information and Computation | 2003-01-14 | Paper |
| Mathematical knowledge management in HELM | 2002-02-14 | Paper |
| scientific article; zbMATH DE number 1499082 (Why is no real title available?) | 2000-09-03 | Paper |
| scientific article; zbMATH DE number 1479624 (Why is no real title available?) | 2000-07-20 | Paper |
A sufficient condition for completability of partial combinatory algebras
Journal of Symbolic Logic | 1999-08-17 | Paper |
Safe operators: Brackets closed forever. Optimizing optimal \(\lambda\)-calculus implementations
Applicable Algebra in Engineering, Communication and Computing | 1998-11-26 | Paper |
The bologna optimal higher-order machine
Journal of Functional Programming | 1997-06-04 | Paper |
Paths, computations and labels in the \(\lambda\)-calculus
Theoretical Computer Science | 1997-02-28 | Paper |
Interaction systems II: The practice of optimal reductions
Theoretical Computer Science | 1997-02-27 | Paper |
Causal dependencies in multiplicative linear logic with MIX
Mathematical Structures in Computer Science | 1996-12-05 | Paper |
| scientific article; zbMATH DE number 742718 (Why is no real title available?) | 1995-08-10 | Paper |
A categorical understanding of environment machines
Journal of Functional Programming | 1995-05-01 | Paper |
Interaction Systems I: The theory of optimal reductions
Mathematical Structures in Computer Science | 1995-04-06 | Paper |
| scientific article; zbMATH DE number 139605 (Why is no real title available?) | 1993-03-28 | Paper |
| scientific article; zbMATH DE number 49833 (Why is no real title available?) | 1993-01-23 | Paper |
Categorical models of polymorphism
Information and Computation | 1992-09-27 | Paper |
Stability and computability in coherent domains
Information and Computation | 1990-01-01 | Paper |
| scientific article; zbMATH DE number 4014020 (Why is no real title available?) | 1986-01-01 | Paper |
