2009 |
22 | EE | José Espírito Santo,
Ralph Matthes,
Luis Pinto:
Continuation-Passing Style and Strong Normalisation for Intuitionistic Sequent Calculi
CoRR abs/0903.1822: (2009) |
2008 |
21 | EE | Ralph Matthes:
Recursion on Nested Datatypes in Dependent Type Theory.
CiE 2008: 431-446 |
20 | EE | Ralph Matthes:
Nested Datatypes with Generalized Mendler Iteration: Map Fusion and the Example of the Representation of Untyped Lambda Calculus with Explicit Flattening.
MPC 2008: 220-242 |
19 | EE | Ralph Matthes,
Sergei Soloviev:
Preface to the special issue: isomorphisms of types and invertibility of lambda terms.
Mathematical Structures in Computer Science 18(4): 645-646 (2008) |
2007 |
18 | EE | José Espírito Santo,
Ralph Matthes,
Luis Pinto:
Continuation-Passing Style and Strong Normalisation for Intuitionistic Sequent Calculi.
TLCA 2007: 133-147 |
17 | EE | Ralph Matthes,
Martin Strecker:
Verification of the Redecoration Algorithm for Triangular Matrices.
TYPES 2007: 125-141 |
2006 |
16 | EE | Ralph Matthes:
A Datastructure for Iterated Powers.
MPC 2006: 299-315 |
2005 |
15 | EE | Ralph Matthes:
Non-strictly positive fixed points for classical natural deduction.
Ann. Pure Appl. Logic 133(1-3): 205-230 (2005) |
14 | EE | Andreas Abel,
Ralph Matthes,
Tarmo Uustalu:
Iteration and coiteration schemes for higher-order and nested datatypes.
Theor. Comput. Sci. 333(1-2): 3-66 (2005) |
2004 |
13 | EE | Andreas Abel,
Ralph Matthes:
Fixed Points of Type Constructors and Primitive Recursion.
CSL 2004: 190-204 |
12 | EE | Ralph Matthes,
Tarmo Uustalu:
Substitution in non-wellfounded syntax with variable binding.
Theor. Comput. Sci. 327(1-2): 155-174 (2004) |
2003 |
11 | EE | Andreas Abel,
Ralph Matthes,
Tarmo Uustalu:
Generalized Iteration and Coiteration for Higher-Order Nested Datatypes.
FoSSaCS 2003: 54-69 |
10 | EE | Felix Joachimski,
Ralph Matthes:
Short proofs of normalization for the simply- typed lambda-calculus, permutative conversions and Go"del's T.
Arch. Math. Log. 42(1): 59-87 (2003) |
9 | EE | Ralph Matthes,
Tarmo Uustalu:
Substitution in Non-wellfounded Syntax with Variable Binding.
Electr. Notes Theor. Comput. Sci. 82(1): (2003) |
2002 |
8 | EE | Andreas Abel,
Ralph Matthes:
(Co-)Iteration for Higher-Order Nested Datatypes.
TYPES 2002: 1-20 |
2001 |
7 | EE | Ralph Matthes:
Monotone Inductive and Coinductive Constructors of Rank 2.
CSL 2001: 600-614 |
6 | EE | Ralph Matthes:
Interpolation for Natural Deduction with Generalized Eliminations.
Proof Theory in Computer Science 2001: 153-169 |
5 | EE | Ralph Matthes:
Parigot's Second Order lambda-mu-Calculus and Inductive Types.
TLCA 2001: 329-343 |
2000 |
4 | | Ralph Matthes:
Characterizing Strongly Normalizing Terms of a Calculus with Generalized Applications via Intersection Types.
ICALP Satellite Workshops 2000: 339-354 |
3 | | Felix Joachimski,
Ralph Matthes:
Standardization and Confluence for a Lambda Calculus with Generalized Applications.
RTA 2000: 141-155 |
1999 |
2 | | Ralph Matthes:
Monotone (co)inductive types and positive fixed-point types.
ITA 33(4/5): 309-328 (1999) |
1998 |
1 | | Ralph Matthes:
Monotone Fixed-Point Types and Strong Normalization.
CSL 1998: 298-312 |