| A coinductive approach to proof search through typed lambda-calculi | 0 | 0.34 | 2021 |
| Inhabitation in simply typed lambda-calculus through a lambda-calculus for proof search | 0 | 0.34 | 2019 |
| Decidability of Several Concepts of Finiteness for Simple Types. | 0 | 0.34 | 2019 |
| From Signatures to Monads in <Emphasis FontCategory="SansSerif">UniMath</Emphasis> | 0 | 0.34 | 2019 |
| Inhabitation in Simply-Typed Lambda-Calculus through a Lambda-Calculus for Proof Search. | 0 | 0.34 | 2016 |
| A Calculus for a Coinductive Analysis of Proof Search. | 1 | 0.37 | 2016 |
| Heterogeneous substitution systems revisited. | 0 | 0.34 | 2015 |
| Confluence For Classical Logic Through The Distinction Between Values And Computations | 0 | 0.34 | 2014 |
| Monadic translation of classical sequent calculus. | 1 | 0.36 | 2013 |
| On a Dynamic Logic for Graph Rewriting. | 0 | 0.34 | 2013 |
| A Coinductive Approach To Proof Search | 2 | 0.47 | 2013 |
| Permutations in Coinductive Graph Representation. | 2 | 0.40 | 2012 |
| Preface to the special issue: Commutativity of algebraic diagrams | 0 | 0.34 | 2012 |
| Map fusion for nested datatypes in intensional type theory | 3 | 0.42 | 2011 |
| Coinductive Graph Representation: the Problem of Embedded Lists. | 6 | 0.54 | 2011 |
| Verification of redecoration for infinite triangular matrices using coinduction. | 1 | 0.41 | 2011 |
| Verification of the Schorr-Waite algorithm - from trees to graphs | 8 | 0.56 | 2010 |
| An induction principle for nested datatypes in intensional type theory | 9 | 0.66 | 2009 |
| Continuation-Passing Style and Strong Normalisation for Intuitionistic Sequent Calculi | 0 | 0.34 | 2009 |
| Coinductive Predicates as Final Coalgebras | 1 | 0.36 | 2009 |
| Preface to the special issue: Isomorphisms of types and invertibility of lambda terms | 0 | 0.34 | 2008 |
| Nested Datatypes with Generalized Mendler Iteration: Map Fusion and the Example of the Representation of Untyped Lambda Calculus with Explicit Flattening | 3 | 0.41 | 2008 |
| Monadic Translation of Intuitionistic Sequent Calculus | 2 | 0.40 | 2008 |
| Recursion on Nested Datatypes in Dependent Type Theory | 5 | 0.50 | 2008 |
| Verification of the redecoration algorithm for triangular matrices | 1 | 0.43 | 2007 |
| Continuation-passing style and strong normalisation for intuitionistic sequent calculi | 6 | 0.52 | 2007 |
| Verification of programs on truly nested datatypes in intensional type theory | 2 | 0.41 | 2006 |
| A datastructure for iterated powers | 1 | 0.38 | 2006 |
| Non-strictly positive fixed points for classical natural deduction | 13 | 0.89 | 2005 |
| Iteration and coiteration schemes for higher-order and nested datatypes | 30 | 1.16 | 2005 |
| Substitution in non-wellfounded syntax with variable binding | 13 | 0.75 | 2004 |
| Generalized iteration and coiteration for higher-order nested datatypes | 6 | 0.48 | 2003 |
| Short Proofs Of Normalization For The Simply-Typed Lambda-Calculus, Permutative Conversions And Godel'S T | 28 | 1.45 | 2003 |
| Primitive Recursion for Rank-2 Inductive Types | 0 | 0.34 | 2003 |
| (Co-) iteration for higher-order nested datatypes | 6 | 0.47 | 2002 |
| Tarski's Fixed-Point Theorem and Lambda Calculi With Monotone Inductive Types | 4 | 0.49 | 2002 |
| Interpolation for Natural Deduction with Generalized Eliminations | 0 | 0.34 | 2001 |
| Parigot's Second Order lambda-mu-Calculus and Inductive Types | 0 | 0.34 | 2001 |
| Monotone Inductive and Coinductive Constructors of Rank 2 | 7 | 0.55 | 2001 |
| Characterizing Strongly Normalizing Terms of a Calculus with Generalized Applications via Intersection Types | 8 | 0.57 | 2000 |
| Standardization and Confluence for a Lambda Calculus with Generalized Applications | 14 | 0.93 | 2000 |
| Monotone (co)inductive types and positive fixed-point types | 8 | 0.64 | 1999 |
| Monotone Fixed-Point Types and Strong Normalization | 10 | 0.96 | 1998 |
