| Publication | Date of Publication | Type |
|---|
| Effective applicative structures | 2022-12-16 | Paper |
| Paths, computations and labels in the λ-calculus | 2022-12-09 | Paper |
| δο!∈=1 Optimizing optimal λ-calculus implementations | 2022-12-09 | Paper |
| Optimal reductions in interaction systems | 2022-11-02 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4964707 | 2021-03-03 | Paper |
| Matita Tutorial | 2019-09-18 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5195248 | 2019-09-18 | Paper |
| On the dynamics of sharing graphs | 2018-07-04 | Paper |
| The cost of usage in the \(\lambda\)-calculus | 2017-07-03 | Paper |
| Intuitionistic light affine logic | 2017-06-13 | Paper |
| Reverse complexity | 2016-05-26 | Paper |
| A formalization of multi-tape Turing machines | 2015-10-12 | Paper |
| Computational Complexity Via Finite Types | 2015-09-17 | Paper |
| (Optimal) duplication is not elementary recursive | 2015-03-17 | Paper |
| A formal proof of Borodin-Trakhtenbrot's gap theorem | 2015-01-13 | Paper |
| The intensional content of Rice's theorem | 2014-09-12 | Paper |
| An Interactive Driver for Goal-directed Proof Strategies | 2014-06-27 | Paper |
| The optimal implementation of functional programming languages | 2014-02-21 | Paper |
| A machine-checked proof of the odd order theorem | 2013-08-07 | Paper |
| Rating Disambiguation Errors | 2013-04-19 | Paper |
| Formal metatheory of programming languages in the Matita interactive theorem prover | 2013-04-17 | Paper |
| Formalizing Turing Machines | 2012-09-21 | Paper |
| A Compact Proof of Decidability for Regular Expression Equivalence | 2012-09-20 | Paper |
| A Web Interface for Matita | 2012-09-07 | Paper |
| Proof, message and certificate | 2012-09-07 | Paper |
| A bi-directional refinement algorithm for the calculus of (co)inductive constructions | 2012-04-03 | Paper |
| Zen and the art of formalisation | 2011-10-21 | Paper |
| The Matita interactive theorem prover | 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 |
| Smart matching | 2010-08-24 | Paper |
| A compact kernel for the calculus of inductive constructions | 2009-11-23 | Paper |
| Social processes, program verification and all that | 2009-11-11 | Paper |
| Hints in Unification | 2009-10-20 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3497621 | 2009-07-27 | Paper |
| About the Formalization of Some Results by Chebyshev in Number Theory | 2009-07-02 | Paper |
| Crafting a Proof Assistant | 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 | 2007-12-03 | Paper |
| Higher order Proof Reconstruction from Paramodulation-Based Refutations: The Unit Equality Case | 2007-11-28 | Paper |
| Mathematical Knowledge Management | 2007-02-12 | Paper |
| Types for Proofs and Programs | 2006-11-13 | Paper |
| Mathematical Knowledge Management | 2005-08-26 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3024818 | 2005-07-04 | Paper |
| (Optimal) duplication is not elementary recursive | 2004-10-04 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4474349 | 2004-07-09 | Paper |
| Mathematical knowledge management in HELM | 2003-06-09 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4790651 | 2003-02-04 | Paper |
| Parallel beta reduction is not elementary recursive | 2003-01-14 | Paper |
| Mathematical knowledge management in HELM | 2002-02-14 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4501135 | 2000-09-03 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4490737 | 2000-07-20 | Paper |
| A sufficient condition for completability of partial combinatory algebras | 1999-08-17 | Paper |
| Safe operators: Brackets closed forever. Optimizing optimal \(\lambda\)-calculus implementations | 1998-11-26 | Paper |
| The bologna optimal higher-order machine | 1997-06-04 | Paper |
| Paths, computations and labels in the \(\lambda\)-calculus | 1997-02-28 | Paper |
| Interaction systems II: The practice of optimal reductions | 1997-02-27 | Paper |
| Causal dependencies in multiplicative linear logic with MIX | 1996-12-05 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4327828 | 1995-08-10 | Paper |
| A categorical understanding of environment machines | 1995-05-01 | Paper |
| Interaction Systems I: The theory of optimal reductions | 1995-04-06 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4029583 | 1993-03-28 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3999603 | 1993-01-23 | Paper |
| Categorical models of polymorphism | 1992-09-27 | Paper |
| Stability and computability in coherent domains | 1990-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3026332 | 1986-01-01 | Paper |
