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 |
https://portal.mardi4nfdi.de/entity/Q5195248 | 2019-09-18 | Paper |
Matita Tutorial | 2019-09-18 | Paper |
On the dynamics of sharing graphs | 2018-07-04 | Paper |
The Cost of Usage in the ?-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 |
https://portal.mardi4nfdi.de/entity/Q5397484 | 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 |
Proof, Message and Certificate | 2012-09-07 | Paper |
A Web Interface for Matita | 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 |
https://portal.mardi4nfdi.de/entity/Q5460254 | 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 |
https://portal.mardi4nfdi.de/entity/Q2767919 | 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 |