Seguir
Ralph Matthes
Ralph Matthes
CNRS, IRIT, Toulouse, France
Dirección de correo verificada de irit.fr - Página principal
Título
Citado por
Citado por
Año
Short proofs of normalization for the simply-typed λ-calculus, permutative conversions and Gödel's T
F Joachimski, R Matthes
Archive for Mathematical Logic 42 (1), 59-87, 2003
1562003
Extensions of system F by iteration and primitive recursion on monotone inductive types
R Matthes
Herbert Utz Verlag, 1999
921999
Iteration and coiteration schemes for higher-order and nested datatypes
A Abel, R Matthes, T Uustalu
Theoretical Computer Science 333 (1-2), 3-66, 2005
732005
Standardization and confluence for a lambda calculus with generalized applications
F Joachimski, R Matthes
International Conference on Rewriting Techniques and Applications, 141-155, 2000
542000
Substitution in non-wellfounded syntax with variable binding
R Matthes, T Uustalu
Theoretical Computer Science 327 (1-2), 155-174, 2004
432004
Monotone fixed-point types and strong normalization
R Matthes
Computer Science Logic: 12th International Workshop, CSL’98, Annual …, 1999
371999
Non-strictly positive fixed points for classical natural deduction
R Matthes
Annals of pure and Applied logic 133 (1-3), 205-230, 2005
312005
Fixed points of type constructors and primitive recursion
A Abel, R Matthes
Computer Science Logic: 18th International Workshop, CSL 2004, 13th Annual …, 2004
282004
Characterizing strongly normalizing terms of a λ-calculus with generalized applications via intersection types
R Matthes
ICALP Workshops, 339-353, 2000
272000
An induction principle for nested datatypes in intensional type theory
R Matthes
Journal of Functional Programming 19 (3-4), 439-468, 2009
242009
Monotone (co) inductive types and positive fixed-point types
R Matthes
RAIRO-Theoretical Informatics and Applications 33 (4-5), 309-328, 1999
221999
Verification of the Schorr-Waite algorithm–From trees to graphs
M Giorgino, M Strecker, R Matthes, M Pantel
Logic-Based Program Synthesis and Transformation: 20th International …, 2011
182011
Generalized iteration and coiteration for higher-order nested datatypes
A Abel, R Matthes, T Uustalu
Foundations of Software Science and Computation Structures: 6th …, 2003
172003
Coinductive graph representation: the problem of embedded lists
C Picard, R Matthes
Electronic Communications of the EASST 39, 2011
162011
An inductive proof of the wellfoundedness of the multiset order
T Nipkow, R Matthes, W Part
161998
Tarski's fixed-point theorem and lambda calculi with monotone inductive types
R Matthes
Synthese 133 (1-2), 107-129, 2002
152002
Monotone inductive and coinductive constructors of rank 2
R Matthes
Computer Science Logic: 15th International Workshop, CSL 2001 10th Annual …, 2001
152001
Continuation-passing style and strong normalisation for intuitionistic sequent calculi
JE Santo, R Matthes, L Pinto
International Conference on Typed Lambda Calculi and Applications, 133-147, 2007
142007
From Signatures to Monads in UniMath
B Ahrens, R Matthes, A Mörtberg
Journal of Automated Reasoning 63 (2), 285-318, 2019
132019
Implementing a category-theoretic framework for typed abstract syntax
B Ahrens, R Matthes, A Mörtberg
Proceedings of the 11th ACM SIGPLAN International Conference on Certified …, 2022
122022
El sistema no puede realizar la operación en estos momentos. Inténtalo de nuevo más tarde.
Artículos 1–20