| 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 | 155 | 2003 |
| Extensions of system F by iteration and primitive recursion on monotone inductive types R Matthes Herbert Utz Verlag, 1999 | 92 | 1999 |
| 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 | 73 | 2005 |
| Standardization and confluence for a lambda calculus with generalized applications F Joachimski, R Matthes International Conference on Rewriting Techniques and Applications, 141-155, 2000 | 53 | 2000 |
| Substitution in non-wellfounded syntax with variable binding R Matthes, T Uustalu Theoretical Computer Science 327 (1-2), 155-174, 2004 | 43 | 2004 |
| Monotone fixed-point types and strong normalization R Matthes Computer Science Logic: 12th International Workshop, CSL’98, Annual …, 1999 | 37 | 1999 |
| Non-strictly positive fixed points for classical natural deduction R Matthes Annals of pure and Applied logic 133 (1-3), 205-230, 2005 | 31 | 2005 |
| Fixed points of type constructors and primitive recursion A Abel, R Matthes Computer Science Logic: 18th International Workshop, CSL 2004, 13th Annual …, 2004 | 28 | 2004 |
| Characterizing strongly normalizing terms of a λ-calculus with generalized applications via intersection types R Matthes ICALP Workshops, 339-353, 2000 | 27 | 2000 |
| An induction principle for nested datatypes in intensional type theory R Matthes Journal of Functional Programming 19 (3-4), 439-468, 2009 | 24 | 2009 |
| Monotone (co) inductive types and positive fixed-point types R Matthes RAIRO-Theoretical Informatics and Applications 33 (4-5), 309-328, 1999 | 22 | 1999 |
| 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 | 18 | 2011 |
| Generalized iteration and coiteration for higher-order nested datatypes A Abel, R Matthes, T Uustalu Foundations of Software Science and Computation Structures: 6th …, 2003 | 17 | 2003 |
| Coinductive graph representation: the problem of embedded lists C Picard, R Matthes Electronic Communications of the EASST 39, 2011 | 16 | 2011 |
| An inductive proof of the wellfoundedness of the multiset order T Nipkow, R Matthes, W Part | 16 | 1998 |
| Tarski's fixed-point theorem and lambda calculi with monotone inductive types R Matthes Synthese 133 (1-2), 107-129, 2002 | 15 | 2002 |
| Monotone inductive and coinductive constructors of rank 2 R Matthes Computer Science Logic: 15th International Workshop, CSL 2001 10th Annual …, 2001 | 15 | 2001 |
| 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 | 14 | 2007 |
| From Signatures to Monads in UniMath B Ahrens, R Matthes, A Mörtberg Journal of Automated Reasoning 63 (2), 285-318, 2019 | 13 | 2019 |
| 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 | 12 | 2022 |
Luís PintoCentro de Matemática and Departamento de Matemática e Aplicações, Universidade do MinhoVerified email at math.uminho.pt
