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 |