Edit Profile (opens in new tab) Matthes, Ralph Co-Author Distance Author ID: matthes.ralph Published as: Matthes, Ralph Documents Indexed: 41 Publications since 1998, including 1 Book 4 Contributions as Editor Co-Authors: 21 Co-Authors with 29 Joint Publications 332 Co-Co-Authors all top 5 Co-Authors 15 single-authored 9 Espírito Santo, José Carlos 9 Pinto, Luís F. 4 Abel, Andreas M. 4 Uustalu, Tarmo 2 Ahrens, Benedikt 2 Joachimski, Felix 2 Nakazawa, Koji 2 Picard, Celia 2 Strecker, Martin 1 Baelde, David 1 Berger, Ulrich 1 Carayol, Arnaud 1 Doebner, Heinz-Dietrich 1 Giorgino, Mathieu 1 Larchey-Wendling, Dominique 1 Mio, Matteo 1 Mörtberg, Anders 1 Pantel, Marc 1 Schubert, Aleksy 1 Setzer, Anton 1 Solov’ëv, Sergeĭ Vladimirovich 1 Walukiewicz, Igor all top 5 Serials 3 MSCS. Mathematical Structures in Computer Science 2 Theoretical Computer Science 2 Annals of Pure and Applied Logic 2 Fundamenta Informaticae 1 Synthese 1 Science of Computer Programming 1 Bulgarian Journal of Physics 1 Journal of Automated Reasoning 1 Archive for Mathematical Logic 1 Journal of Functional Programming 1 RAIRO. Theoretical Informatics and Applications 1 Logical Methods in Computer Science 1 LIPIcs – Leibniz International Proceedings in Informatics 1 Electronic Proceedings in Theoretical Computer Science (EPTCS) all top 5 Fields 35 Computer science (68-XX) 23 Mathematical logic and foundations (03-XX) 5 Category theory; homological algebra (18-XX) 4 General and overarching topics; collections (00-XX) 2 Combinatorics (05-XX) 2 Global analysis, analysis on manifolds (58-XX) 2 Quantum theory (81-XX) 1 Associative rings and algebras (16-XX) 1 Difference and functional equations (39-XX) 1 Functional analysis (46-XX) 1 Operator theory (47-XX) 1 Algebraic topology (55-XX) Publications by Year all cited Publications top 5 cited Publications Citations contained in zbMATH Open 31 Publications have been cited 145 times in 92 Documents Cited by ▼ Year ▼ Short proofs of normalization for the simply-typed \(\lambda\)-calculus, permutative conversions and Gödel’s \(\mathbf T\). Zbl 1025.03010Joachimski, Felix; Matthes, Ralph 29 2003 Iteration and coiteration schemes for higher-order and nested datatypes. Zbl 1070.68093Abel, Andreas; Matthes, Ralph; Uustalu, Tarmo 18 2005 Substitution in non-wellfounded syntax with variable binding. Zbl 1071.68063Matthes, Ralph; Uustalu, Tarmo 12 2004 Extensions of system F by iteration and primitive recursion on monotone inductive types. Zbl 0943.68086Matthes, Ralph 10 1998 Non-strictly positive fixed points for classical natural deduction. Zbl 1066.03057Matthes, Ralph 8 2005 Standardization and confluence for a lambda calculus with generalized applications. Zbl 0964.03014Joachimski, Felix; Matthes, Ralph 7 2000 Monotone fixed-point types and strong normalization. Zbl 0933.03027Matthes, Ralph 6 1999 An induction principle for nested datatypes in intensional type theory. Zbl 1191.68164Matthes, Ralph 5 2009 Map fusion for nested datatypes in intensional type theory. Zbl 1210.68048Matthes, Ralph 4 2011 Tarski’s fixed-point theorem and lambda calculi with monotone inductive types. Zbl 1069.03009Matthes, Ralph 4 2002 Fixed points of type constructors and primitive recursion. Zbl 1095.68059Abel, Andreas; Matthes, Ralph 4 2004 Verification of the Schorr-Waite algorithm – from trees to graphs. Zbl 1326.68095Giorgino, Mathieu; Strecker, Martin; Matthes, Ralph; Pantel, Marc 3 2011 Generalized iteration and coiteration for higher-order nested datatypes. Zbl 1029.68097Abel, Andreas; Matthes, Ralph; Uustalu, Tarmo 3 2003 Monotone (co)inductive types and positive fixed-point types. Zbl 0940.03018Matthes, Ralph 3 1999 Substitution in non-wellfounded syntax with variable binding. Zbl 1270.68089Matthes, Ralph; Uustalu, Tarmo 3 2003 Stabilization – an alternative to double-negation translation for classical natural deduction. Zbl 1102.03008Matthes, Ralph 3 2006 From signatures to monads in UniMath. Zbl 1468.03007Ahrens, Benedikt; Matthes, Ralph; Mörtberg, Anders 3 2019 Recursion on nested datatypes in dependent type theory. Zbl 1142.68441Matthes, Ralph 2 2008 Nested datatypes with generalized Mendler iteration: Map fusion and the example of the representation of untyped lambda calculus with explicit flattening. Zbl 1156.68483Matthes, Ralph 2 2008 (Co-)Iteration for higher-order nested datatypes. Zbl 1023.68066Abel, Andreas; Matthes, Ralph 2 2003 Monotone inductive and coinductive constructors of rank 2. Zbl 0999.68037Matthes, Ralph 2 2001 Continuation-passing style and strong normalisation for intuitionistic sequent calculi. Zbl 1167.03012Espírito Santo, José; Matthes, Ralph; Pinto, Luís 2 2007 Heterogeneous substitution systems revisited. Zbl 1433.68220Ahrens, Benedikt; Matthes, Ralph 2 2018 A coinductive approach to proof search. Zbl 1469.03041Espírito Santo, José; Matthes, Ralph; Pinto, Luís 1 2013 Certification of breadth-first algorithms by extraction. Zbl 1434.68090Larchey-Wendling, Dominique; Matthes, Ralph 1 2019 Permutations in coinductive graph representation. Zbl 1327.68205Picard, Celia; Matthes, Ralph 1 2012 Parigot’s second order \(\lambda\mu\)-calculus and inductive types. Zbl 0981.03024Matthes, Ralph 1 2001 Continuation-passing style and strong normalisation for intuitionistic sequent calculi. Zbl 1168.03008Espírito Santo, José; Matthes, Ralph; Pinto, Luís 1 2009 Monadic translation of intuitionistic sequent calculus. Zbl 1246.03027Espírito Santo, José; Matthes, Ralph; Pinto, Luís 1 2009 Decidability of several concepts of finiteness for simple types. Zbl 1446.03036Espírito Santo, José; Matthes, Ralph; Pinto, Luís 1 2019 Inhabitation in simply typed lambda-calculus through a lambda-calculus for proof search. Zbl 1456.03024Espírito Santo, José; Matthes, Ralph; Pinto, Luís 1 2019 From signatures to monads in UniMath. Zbl 1468.03007Ahrens, Benedikt; Matthes, Ralph; Mörtberg, Anders 3 2019 Certification of breadth-first algorithms by extraction. Zbl 1434.68090Larchey-Wendling, Dominique; Matthes, Ralph 1 2019 Decidability of several concepts of finiteness for simple types. Zbl 1446.03036Espírito Santo, José; Matthes, Ralph; Pinto, Luís 1 2019 Inhabitation in simply typed lambda-calculus through a lambda-calculus for proof search. Zbl 1456.03024Espírito Santo, José; Matthes, Ralph; Pinto, Luís 1 2019 Heterogeneous substitution systems revisited. Zbl 1433.68220Ahrens, Benedikt; Matthes, Ralph 2 2018 A coinductive approach to proof search. Zbl 1469.03041Espírito Santo, José; Matthes, Ralph; Pinto, Luís 1 2013 Permutations in coinductive graph representation. Zbl 1327.68205Picard, Celia; Matthes, Ralph 1 2012 Map fusion for nested datatypes in intensional type theory. Zbl 1210.68048Matthes, Ralph 4 2011 Verification of the Schorr-Waite algorithm – from trees to graphs. Zbl 1326.68095Giorgino, Mathieu; Strecker, Martin; Matthes, Ralph; Pantel, Marc 3 2011 An induction principle for nested datatypes in intensional type theory. Zbl 1191.68164Matthes, Ralph 5 2009 Continuation-passing style and strong normalisation for intuitionistic sequent calculi. Zbl 1168.03008Espírito Santo, José; Matthes, Ralph; Pinto, Luís 1 2009 Monadic translation of intuitionistic sequent calculus. Zbl 1246.03027Espírito Santo, José; Matthes, Ralph; Pinto, Luís 1 2009 Recursion on nested datatypes in dependent type theory. Zbl 1142.68441Matthes, Ralph 2 2008 Nested datatypes with generalized Mendler iteration: Map fusion and the example of the representation of untyped lambda calculus with explicit flattening. Zbl 1156.68483Matthes, Ralph 2 2008 Continuation-passing style and strong normalisation for intuitionistic sequent calculi. Zbl 1167.03012Espírito Santo, José; Matthes, Ralph; Pinto, Luís 2 2007 Stabilization – an alternative to double-negation translation for classical natural deduction. Zbl 1102.03008Matthes, Ralph 3 2006 Iteration and coiteration schemes for higher-order and nested datatypes. Zbl 1070.68093Abel, Andreas; Matthes, Ralph; Uustalu, Tarmo 18 2005 Non-strictly positive fixed points for classical natural deduction. Zbl 1066.03057Matthes, Ralph 8 2005 Substitution in non-wellfounded syntax with variable binding. Zbl 1071.68063Matthes, Ralph; Uustalu, Tarmo 12 2004 Fixed points of type constructors and primitive recursion. Zbl 1095.68059Abel, Andreas; Matthes, Ralph 4 2004 Short proofs of normalization for the simply-typed \(\lambda\)-calculus, permutative conversions and Gödel’s \(\mathbf T\). Zbl 1025.03010Joachimski, Felix; Matthes, Ralph 29 2003 Generalized iteration and coiteration for higher-order nested datatypes. Zbl 1029.68097Abel, Andreas; Matthes, Ralph; Uustalu, Tarmo 3 2003 Substitution in non-wellfounded syntax with variable binding. Zbl 1270.68089Matthes, Ralph; Uustalu, Tarmo 3 2003 (Co-)Iteration for higher-order nested datatypes. Zbl 1023.68066Abel, Andreas; Matthes, Ralph 2 2003 Tarski’s fixed-point theorem and lambda calculi with monotone inductive types. Zbl 1069.03009Matthes, Ralph 4 2002 Monotone inductive and coinductive constructors of rank 2. Zbl 0999.68037Matthes, Ralph 2 2001 Parigot’s second order \(\lambda\mu\)-calculus and inductive types. Zbl 0981.03024Matthes, Ralph 1 2001 Standardization and confluence for a lambda calculus with generalized applications. Zbl 0964.03014Joachimski, Felix; Matthes, Ralph 7 2000 Monotone fixed-point types and strong normalization. Zbl 0933.03027Matthes, Ralph 6 1999 Monotone (co)inductive types and positive fixed-point types. Zbl 0940.03018Matthes, Ralph 3 1999 Extensions of system F by iteration and primitive recursion on monotone inductive types. Zbl 0943.68086Matthes, Ralph 10 1998 all cited Publications top 5 cited Publications all top 5 Cited by 100 Authors 13 Matthes, Ralph 9 Abel, Andreas M. 7 Uustalu, Tarmo 6 Berger, Ulrich 6 Espírito Santo, José Carlos 5 Ahrens, Benedikt 4 Hirschowitz, André 4 Johann, Patricia 4 Maggesi, Marco 4 Nour, Karim 4 Pinto, Luís F. 4 Stump, Aaron 3 Aehlig, Klaus 3 Ghani, Neil 3 Joachimski, Felix 3 Lafont, Ambroise 3 Nakazawa, Koji 3 Tatsuta, Makoto 2 David, Rene 2 Ferreira, Fernando 2 Ferreira, Gilda 2 Geuvers, Jan Herman 2 Ghiorzi, Enrico 2 Jenkins, Christopher 2 Milius, Stefan 2 Miranda Perea, Favio Ezequiel 2 Mörtberg, Anders 2 Saber, Khelifa 2 Schroeder-Heister, Peter Joseph 2 Schwichtenberg, Helmut 2 Setzer, Anton 2 Szasz, Nora 2 Tasistro, Alvaro 2 Torrini, Paolo 2 Vene, Varmo 2 Wu, Nicolas 1 Abou-Saleh, Faris 1 Adámek, Jiří 1 Adelsberger, Stephan 1 Affeldt, Reynald 1 Ahn, Ki Yung 1 Allais, Guillaume 1 Bellantoni, Stephen J. 1 Blanqui, Frédéric 1 Brotherston, James 1 Copello, Ernesto 1 Crespo, Juan Manuel 1 Devesas Campos, Marco 1 Diehl, Larry 1 Dyckhoff, Roy 1 Fiore, Marcelo P. 1 Frade, Maria João 1 Fu, Peng 1 Fujita, Ken-etsu 1 Garrigue, Jacques 1 Gast, Holger 1 Ghilezan, Silvia 1 Giorgino, Mathieu 1 Hamana, Makoto 1 Hameer, Aliya 1 Hasegawa, Ryu 1 Hinze, Ralf 1 Hofmann, Martin 1 Hou, Tie 1 Hurkens, Tonny 1 Ikeda, Satoshi 1 Ivetić, Jelena 1 Jeffries, Daniel 1 Kaposi, Ambrus 1 Kovács, András 1 Kunz, César 1 Mints, Grigoriĭ Efroimovich 1 Momigliano, Alberto 1 Moss, Lawrence S. 1 Mossakowski, Till 1 Nakano, Hiroshi 1 Negri, Sara 1 Niggl, Karl-Heinz 1 Niqui, Milad 1 Pantel, Marc 1 Pattinson, Dirk 1 Pientka, Brigitte 1 Polonsky, Andrew 1 Qi, Xuanrui 1 Schäfer, Steven 1 Schrijvers, Tom 1 Schröder, Lutz 1 Stark, Kathrin 1 Strecker, Martin 1 Tanaka, Kazunari 1 Tsuiki, Hideki 1 Urciuoli, Sebastián 1 Velebil, Jiří 1 Vestergaard, René 1 Vezzosi, Andrea 1 Voevodskiĭ, Vladimir Aleksandrovich 1 von Plato, Jan 1 Wansing, Heinrich Theodor 1 Yang, Zhixuan 1 Zach, Richard all top 5 Cited in 21 Serials 11 Annals of Pure and Applied Logic 8 Theoretical Computer Science 7 Journal of Functional Programming 5 MSCS. Mathematical Structures in Computer Science 5 RAIRO. Theoretical Informatics and Applications 2 The Journal of Symbolic Logic 2 Science of Computer Programming 2 Information and Computation 2 Journal of Automated Reasoning 2 Higher-Order and Symbolic Computation 2 Logical Methods in Computer Science 1 Information Processing Letters 1 Journal of Pure and Applied Algebra 1 Synthese 1 Bulletin of the Section of Logic 1 Archive for Mathematical Logic 1 Formal Methods in System Design 1 Journal of Applied Non-Classical Logics 1 Theory of Computing Systems 1 The Review of Symbolic Logic 1 Journal of Logical and Algebraic Methods in Programming all top 5 Cited in 8 Fields 66 Computer science (68-XX) 59 Mathematical logic and foundations (03-XX) 11 Category theory; homological algebra (18-XX) 1 History and biography (01-XX) 1 Combinatorics (05-XX) 1 Order, lattices, ordered algebraic structures (06-XX) 1 General algebraic systems (08-XX) 1 Algebraic topology (55-XX) Citations by Year