| LF+ in Coq for "fast and loose" reasoning | 0 | 0.34 | 2019 |
| A Definitional Implementation of the Lax Logical Framework LLFP in Coq, for Supporting Fast and Loose Reasoning. | 0 | 0.34 | 2019 |
| lambda!-calculus, Intersection Types, and Involutions. | 0 | 0.34 | 2019 |
| The involutions-as-principal types/application-as-unification Analogy. | 0 | 0.34 | 2018 |
| A prototype-based approach to object reclassification. | 0 | 0.34 | 2018 |
| Linear lambda-calculus and Reversible Automatic Combinators. | 0 | 0.34 | 2018 |
| Towards Turing computability via coinduction. | 2 | 0.40 | 2016 |
| Mechanizing type environments in weak HOAS | 0 | 0.34 | 2015 |
| Internal Adequacy of Bookkeeping in Coq | 1 | 0.35 | 2014 |
| A Coinductive Animation of Turing Machines. | 1 | 0.39 | 2014 |
| A Weak Hoas Approach To The Poplmark Challenge | 2 | 0.37 | 2012 |
| A Coinductive Semantics Of The Unlimited Register Machine | 2 | 0.43 | 2011 |
| Reasoning about Object-based Calculi in (Co)Inductive Type Theory and the Theory of Contexts | 7 | 0.48 | 2007 |
| A certified, corecursive implementation of exact real numbers | 18 | 1.01 | 2006 |
| Proof methodologies for behavioural equivalence in DPI | 2 | 0.37 | 2005 |
| Plug and Play the Theory of Contexts in Higher-Order Abstract Syntax | 1 | 0.35 | 2004 |
| Imperative Object-Based Calculi in Co-inductive Type Theories | 7 | 0.46 | 2003 |
| Reasoning on an imperative object-based calculus in Higher Order Abstract Syntax | 4 | 0.42 | 2003 |
| A Tour with Constructive Real Numbers | 2 | 0.89 | 2000 |
| A Co-inductive Approach to Real Numbers | 9 | 1.68 | 1999 |
