Edit Profile (opens in new tab) Abel, Andreas M. Co-Author Distance Author ID: abel.andreas-m Published as: Abel, Andreas; Abel, Andreas M. External Links: MGP · Wikidata Documents Indexed: 54 Publications since 1996, including 1 Additional arXiv Preprint 2 Contributions as Editor Software Indexed: 3 Packages Co-Authors: 32 Co-Authors with 35 Joint Publications 401 Co-Co-Authors all top 5 Co-Authors 20 single-authored 8 Coquand, Thierry 8 Pientka, Brigitte 4 Matthes, Ralph 3 Altenkirch, Thorsten 3 Dybjer, Peter 3 Setzer, Anton 3 Thibodeau, David 2 Cockx, Jesper 2 Pagano, Miguel 2 Uustalu, Tarmo 2 Vezzosi, Andrea 1 Adelsberger, Stephan 1 Aehlig, Klaus 1 Allais, Guillaume 1 Chapman, James T. E. 1 Chen, Xu 1 Devriese, Dominique 1 Ferreira, Francisco H. G. 1 Hameer, Aliya 1 Kaposi, Ambrus 1 Momigliano, Alberto 1 Mörtberg, Anders 1 Nordvall Forsberg, Fredrik 1 Norell, Ulf 1 Rodriguez, Dulma 1 Sattler, Christian 1 Schäfer, Steven 1 Scherer, Gabriel 1 Stark, Kathrin 1 Timany, Amin 1 Urban, Christian 1 Wadler, Philip Lee 1 Zucchini, Rebecca all top 5 Serials 8 Journal of Functional Programming 4 Logical Methods in Computer Science 1 Theoretical Computer Science 1 Science of Computer Programming 1 Mathematical Structures in Computer Science 1 Acta Mechanica Sinica. (English Edition) 1 RAIRO. Theoretical Informatics and Applications 1 Fundamenta Informaticae 1 Electronic Notes in Theoretical Computer Science 1 LIPIcs – Leibniz International Proceedings in Informatics all top 5 Fields 50 Computer science (68-XX) 24 Mathematical logic and foundations (03-XX) 2 General and overarching topics; collections (00-XX) 1 Category theory; homological algebra (18-XX) 1 Algebraic topology (55-XX) 1 Mechanics of deformable solids (74-XX) Publications by Year all cited Publications top 5 cited Publications Citations contained in zbMATH Open 52 Publications have been cited 294 times in 189 Documents Cited by ▼ Year ▼ Copatterns, programming infinite structures by observations. Zbl 1301.68080 Abel, Andreas; Pientka, Brigitte; Thibodeau, David; Setzer, Anton 29 2013 Cubical Agda: a dependently typed programming language with univalence and higher inductive types. Zbl 1512.68058 Vezzosi, Andrea; Mörtberg, Anders; Abel, Andreas 22 2021 Wellfounded recursion with copatterns: a unified approach to termination and productivity. Zbl 1323.68087 Abel, Andreas M.; Pientka, Brigitte 21 2013 Iteration and coiteration schemes for higher-order and nested datatypes. Zbl 1070.68093 Abel, Andreas; Matthes, Ralph; Uustalu, Tarmo 19 2005 Well-founded recursion with copatterns and sized types. Zbl 1420.68031 Abel, Andreas; Pientka, Brigitte 16 2016 On irrelevance and algorithmic equality in predicative type theory. Zbl 1238.03028 Abel, Andreas; Scherer, Gabriel 15 2012 A predicative analysis of structural recursion. Zbl 0998.68027 Abel, Andreas; Altenkirch, Thorsten 12 2002 Termination checking with types. Zbl 1089.68028 Abel, Andreas 10 2004 Type-based termination, inflationary fixed-points, and mixed inductive-coinductive types. Zbl 1457.68058 Abel, Andreas 10 2012 Semi-continuous sized types and termination. Zbl 1143.68013 Abel, Andreas 9 2008 POPLMark reloaded: mechanizing proofs by logical relations. Zbl 1442.68257 Abel, Andreas; Allais, Guillaume; Hameer, Aliya; Pientka, Brigitte; Momigliano, Alberto; Schäfer, Steven; Stark, Kathrin 9 2019 Mixed inductive/coinductive types and strong normalization. Zbl 1138.68023 Abel, Andreas 8 2007 Verifying a semantic \(\beta \eta \)-conversion test for Martin-Löf type theory. Zbl 1157.68025 Abel, Andreas; Coquand, Thierry; Dybjer, Peter 8 2008 Well-founded recursion over contextual objects. Zbl 1367.68073 Pientka, Brigitte; Abel, Andreas 8 2015 Fixed points of type constructors and primitive recursion. Zbl 1095.68059 Abel, Andreas; Matthes, Ralph 6 2004 Polarised subtyping for sized types. Zbl 1156.68014 Abel, Andreas 6 2008 On the algebraic foundation of proof assistants for intuitionistic type theory. Zbl 1137.68570 Abel, Andreas; Coquand, Thierry; Dybjer, Peter 5 2008 A formalized proof of strong normalization for guarded recursive types. Zbl 1453.68035 Abel, Andreas; Vezzosi, Andrea 5 2014 Normalization by evaluation in the delay monad: a case study for coinduction via copatterns and sized types. Zbl 1464.68050 Abel, Andreas; Chapman, James 5 2014 A modular type-checking algorithm for type theory with singleton types and proof irrelevance. Zbl 1246.03025 Abel, Andreas; Coquand, Thierry; Pagano, Miguel 4 2009 Specification and verification of a formal system for structurally recursive functions. Zbl 0988.68054 Abel, Andreas 4 2000 A two-surface model describing ratchetting behaviors and transient hardening under nonproportional loading. Zbl 0883.73024 Chen, Xu; Abel, A. 4 1996 A modular type-checking algorithm for type theory with singleton types and proof irrelevance. Zbl 1213.68199 Abel, Andreas; Coquand, Thierry; Pagano, Miguel 4 2011 Generalized iteration and coiteration for higher-order nested datatypes. Zbl 1029.68097 Abel, Andreas; Matthes, Ralph; Uustalu, Tarmo 4 2003 A predicative strong normalisation proof for a \(\lambda\)-calculus with interleaving inductive types. Zbl 0988.03029 Abel, Andreas; Altenkirch, Thorsten 3 2000 Termination and productivity checking with continuous types. Zbl 1039.68029 Abel, Andreas 3 2003 Higher-order dynamic pattern unification for dependent types and records. Zbl 1331.68040 Abel, Andreas; Pientka, Brigitte 3 2011 A third-order representation of the \(\lambda\mu\)-calculus. Zbl 1268.68045 Abel, Andreas 3 2001 Type-based termination of generic programs. Zbl 1192.68134 Abel, Andreas 3 2009 Typed applicative structures and normalization by evaluation for system \(\mathrm F^{\omega }\). Zbl 1257.03037 Abel, Andreas 3 2009 Polarized subtyping for sized types. Zbl 1142.68326 Abel, Andreas 3 2006 Implementing a normalizer using sized heterogeneous types. Zbl 1191.68152 Abel, Andreas 3 2009 (Co-)Iteration for higher-order nested datatypes. Zbl 1023.68066 Abel, Andreas; Matthes, Ralph 3 2003 Failure of normalization in impredicative type theory with proof-irrelevant propositional equality. Zbl 1528.03099 Abel, Andreas; Coquand, Thierry 3 2020 Weak \(\beta \eta \)-normalization and normalization by evaluation for System F. Zbl 1182.03100 Abel, Andreas 2 2008 Semi-continuous sized types and termination. Zbl 1225.68063 Abel, Andreas 2 2006 Towards generic programming with sized types. Zbl 1235.68045 Abel, Andreas 2 2006 Strong normalization and equi-(co)inductive types. Zbl 1215.03019 Abel, Andreas 2 2007 Normalization by evaluation for Martin-Löf type theory with one universe. Zbl 1316.68038 Abel, Andreas; Aehlig, Klaus; Dybjer, Peter 2 2007 Connecting a logical framework to a first-order logic prover. Zbl 1171.68712 Abel, Andreas; Coquand, Thierry; Norell, Ulf 2 2005 Normalization for the simply-typed lambda-calculus in Twelf. Zbl 1278.68245 Abel, Andreas 2 2007 Untyped algorithmic equality for Martin-Löf’s logical framework with surjective pairs. Zbl 1112.68346 Abel, Andreas; Coquand, Thierry 1 2005 Irrelevance in type theory with a heterogeneous equality judgement. Zbl 1326.68076 Abel, Andreas 1 2011 Compositional coinduction with sized types. Zbl 1475.68073 Abel, Andreas 1 2016 Syntactic metatheory of higher-order subtyping. Zbl 1156.03311 Abel, Andreas; Rodriguez, Dulma 1 2008 Interactive programming in Agda – objects and graphical user interfaces. Zbl 1418.68031 Abel, Andreas; Adelsberger, Stephan; Setzer, Anton 1 2017 Untyped algorithmic equality for Martin-Löf’s logical framework with surjective pairs. Zbl 1121.68026 Abel, Andreas; Coquand, Thierry 1 2007 A partial type checking algorithm for Type:Type. Zbl 1291.68106 Abel, Andreas; Altenkirch, Thorsten 1 2011 Towards normalization by evaluation for the \(\beta \eta \)-calculus of constructions. Zbl 1284.68120 Abel, Andreas 1 2010 Unnesting of copatterns. Zbl 1416.68048 Setzer, Anton; Abel, Andreas; Pientka, Brigitte; Thibodeau, David 1 2014 Elaborating dependent (co)pattern matching: no pattern left behind. Zbl 1442.68025 Cockx, Jesper; Abel, Andreas 1 2020 A type theory for defining logics and proofs. Zbl 07959701 Pientka, Brigitte; Thibodeau, David; Abel, Andreas; Ferreira, Francisco; Zucchini, Rebecca 1 2019 Cubical Agda: a dependently typed programming language with univalence and higher inductive types. Zbl 1512.68058 Vezzosi, Andrea; Mörtberg, Anders; Abel, Andreas 22 2021 Failure of normalization in impredicative type theory with proof-irrelevant propositional equality. Zbl 1528.03099 Abel, Andreas; Coquand, Thierry 3 2020 Elaborating dependent (co)pattern matching: no pattern left behind. Zbl 1442.68025 Cockx, Jesper; Abel, Andreas 1 2020 POPLMark reloaded: mechanizing proofs by logical relations. Zbl 1442.68257 Abel, Andreas; Allais, Guillaume; Hameer, Aliya; Pientka, Brigitte; Momigliano, Alberto; Schäfer, Steven; Stark, Kathrin 9 2019 A type theory for defining logics and proofs. Zbl 07959701 Pientka, Brigitte; Thibodeau, David; Abel, Andreas; Ferreira, Francisco; Zucchini, Rebecca 1 2019 Interactive programming in Agda – objects and graphical user interfaces. Zbl 1418.68031 Abel, Andreas; Adelsberger, Stephan; Setzer, Anton 1 2017 Well-founded recursion with copatterns and sized types. Zbl 1420.68031 Abel, Andreas; Pientka, Brigitte 16 2016 Compositional coinduction with sized types. Zbl 1475.68073 Abel, Andreas 1 2016 Well-founded recursion over contextual objects. Zbl 1367.68073 Pientka, Brigitte; Abel, Andreas 8 2015 A formalized proof of strong normalization for guarded recursive types. Zbl 1453.68035 Abel, Andreas; Vezzosi, Andrea 5 2014 Normalization by evaluation in the delay monad: a case study for coinduction via copatterns and sized types. Zbl 1464.68050 Abel, Andreas; Chapman, James 5 2014 Unnesting of copatterns. Zbl 1416.68048 Setzer, Anton; Abel, Andreas; Pientka, Brigitte; Thibodeau, David 1 2014 Copatterns, programming infinite structures by observations. Zbl 1301.68080 Abel, Andreas; Pientka, Brigitte; Thibodeau, David; Setzer, Anton 29 2013 Wellfounded recursion with copatterns: a unified approach to termination and productivity. Zbl 1323.68087 Abel, Andreas M.; Pientka, Brigitte 21 2013 On irrelevance and algorithmic equality in predicative type theory. Zbl 1238.03028 Abel, Andreas; Scherer, Gabriel 15 2012 Type-based termination, inflationary fixed-points, and mixed inductive-coinductive types. Zbl 1457.68058 Abel, Andreas 10 2012 A modular type-checking algorithm for type theory with singleton types and proof irrelevance. Zbl 1213.68199 Abel, Andreas; Coquand, Thierry; Pagano, Miguel 4 2011 Higher-order dynamic pattern unification for dependent types and records. Zbl 1331.68040 Abel, Andreas; Pientka, Brigitte 3 2011 Irrelevance in type theory with a heterogeneous equality judgement. Zbl 1326.68076 Abel, Andreas 1 2011 A partial type checking algorithm for Type:Type. Zbl 1291.68106 Abel, Andreas; Altenkirch, Thorsten 1 2011 Towards normalization by evaluation for the \(\beta \eta \)-calculus of constructions. Zbl 1284.68120 Abel, Andreas 1 2010 A modular type-checking algorithm for type theory with singleton types and proof irrelevance. Zbl 1246.03025 Abel, Andreas; Coquand, Thierry; Pagano, Miguel 4 2009 Type-based termination of generic programs. Zbl 1192.68134 Abel, Andreas 3 2009 Typed applicative structures and normalization by evaluation for system \(\mathrm F^{\omega }\). Zbl 1257.03037 Abel, Andreas 3 2009 Implementing a normalizer using sized heterogeneous types. Zbl 1191.68152 Abel, Andreas 3 2009 Semi-continuous sized types and termination. Zbl 1143.68013 Abel, Andreas 9 2008 Verifying a semantic \(\beta \eta \)-conversion test for Martin-Löf type theory. Zbl 1157.68025 Abel, Andreas; Coquand, Thierry; Dybjer, Peter 8 2008 Polarised subtyping for sized types. Zbl 1156.68014 Abel, Andreas 6 2008 On the algebraic foundation of proof assistants for intuitionistic type theory. Zbl 1137.68570 Abel, Andreas; Coquand, Thierry; Dybjer, Peter 5 2008 Weak \(\beta \eta \)-normalization and normalization by evaluation for System F. Zbl 1182.03100 Abel, Andreas 2 2008 Syntactic metatheory of higher-order subtyping. Zbl 1156.03311 Abel, Andreas; Rodriguez, Dulma 1 2008 Mixed inductive/coinductive types and strong normalization. Zbl 1138.68023 Abel, Andreas 8 2007 Strong normalization and equi-(co)inductive types. Zbl 1215.03019 Abel, Andreas 2 2007 Normalization by evaluation for Martin-Löf type theory with one universe. Zbl 1316.68038 Abel, Andreas; Aehlig, Klaus; Dybjer, Peter 2 2007 Normalization for the simply-typed lambda-calculus in Twelf. Zbl 1278.68245 Abel, Andreas 2 2007 Untyped algorithmic equality for Martin-Löf’s logical framework with surjective pairs. Zbl 1121.68026 Abel, Andreas; Coquand, Thierry 1 2007 Polarized subtyping for sized types. Zbl 1142.68326 Abel, Andreas 3 2006 Semi-continuous sized types and termination. Zbl 1225.68063 Abel, Andreas 2 2006 Towards generic programming with sized types. Zbl 1235.68045 Abel, Andreas 2 2006 Iteration and coiteration schemes for higher-order and nested datatypes. Zbl 1070.68093 Abel, Andreas; Matthes, Ralph; Uustalu, Tarmo 19 2005 Connecting a logical framework to a first-order logic prover. Zbl 1171.68712 Abel, Andreas; Coquand, Thierry; Norell, Ulf 2 2005 Untyped algorithmic equality for Martin-Löf’s logical framework with surjective pairs. Zbl 1112.68346 Abel, Andreas; Coquand, Thierry 1 2005 Termination checking with types. Zbl 1089.68028 Abel, Andreas 10 2004 Fixed points of type constructors and primitive recursion. Zbl 1095.68059 Abel, Andreas; Matthes, Ralph 6 2004 Generalized iteration and coiteration for higher-order nested datatypes. Zbl 1029.68097 Abel, Andreas; Matthes, Ralph; Uustalu, Tarmo 4 2003 Termination and productivity checking with continuous types. Zbl 1039.68029 Abel, Andreas 3 2003 (Co-)Iteration for higher-order nested datatypes. Zbl 1023.68066 Abel, Andreas; Matthes, Ralph 3 2003 A predicative analysis of structural recursion. Zbl 0998.68027 Abel, Andreas; Altenkirch, Thorsten 12 2002 A third-order representation of the \(\lambda\mu\)-calculus. Zbl 1268.68045 Abel, Andreas 3 2001 Specification and verification of a formal system for structurally recursive functions. Zbl 0988.68054 Abel, Andreas 4 2000 A predicative strong normalisation proof for a \(\lambda\)-calculus with interleaving inductive types. Zbl 0988.03029 Abel, Andreas; Altenkirch, Thorsten 3 2000 A two-surface model describing ratchetting behaviors and transient hardening under nonproportional loading. Zbl 0883.73024 Chen, Xu; Abel, A. 4 1996 all cited Publications top 5 cited Publications all top 5 Cited by 262 Authors 19 Abel, Andreas M. 15 Pientka, Brigitte 7 Stump, Aaron 6 Matthes, Ralph 6 McBride, Conor Thomas 5 Altenkirch, Thorsten 5 Berger, Ulrich 5 Birkedal, Lars 5 Bizjak, Aleš 5 Coquand, Thierry 5 Møgelberg, Rasmus Ejlers 5 Setzer, Anton 4 Blanqui, Frédéric 4 Cave, Andrew 4 Gratzer, Daniel 4 Nuyts, Andreas 4 Uustalu, Tarmo 4 Veltri, Niccolò 4 Vezzosi, Andrea 3 Angiuli, Carlo 3 Chapman, James T. E. 3 Clouston, Ranald A. 3 Czajka, Łukasz 3 Dybjer, Peter 3 Eades, Harley III 3 Ghani, Neil 3 Grathwohl, Hans Bugge 3 Jenkins, Christopher 3 Johann, Patricia 3 Momigliano, Alberto 3 Pfenning, Frank 3 Pitts, Andrew M. 3 Sterling, Jonathan 3 Thibodeau, David 3 van der Weide, Niels 2 Ahn, Ki Yung 2 Allais, Guillaume 2 Barthe, Gilles 2 Basold, Henning 2 Bauer, Andrej 2 Cohen, Liron 2 Dal Lago, Ugo 2 Demangeon, Romain 2 Devriese, Dominique 2 Fiore, Marcelo P. 2 Huber, Simon 2 Kaposi, Ambrus 2 Kavvos, G. A. 2 Lindley, Sam 2 Lochbihler, Andreas 2 McLaughlin, Craig A. 2 Miller, Dale Allen 2 Miranda Perea, Favio Ezequiel 2 Mörtberg, Anders 2 Pagano, Miguel 2 Riba, Colin 2 Rutten, Jan J. M. M. 2 Schöpp, Ulrich 2 Schröder, Lutz 2 Sestini, Filippo 2 Steenkamp, S. C. 2 Szasz, Nora 2 Tasistro, Alvaro 2 Tassi, Enrico 2 Torrini, Paolo 2 Traytel, Dmitry 2 Urciuoli, Sebastián 2 Weirich, Stephanie 2 Yoshida, Nobuko 1 Adelsberger, Stephan 1 Aehlig, Klaus 1 Aguirre, Alejandro 1 Ahrens, Benedikt 1 Akama, Yohji 1 Al Wardani, Farah 1 Altisen, Karine 1 Åman Pohjola, Johannes 1 Amaro, Maycon J. J. 1 Amin, Nada 1 Appel, Andrew W. 1 Ariola, Zena M. 1 Asperti, Andrea 1 Atkey, Robert 1 Aubert, Clément 1 Bach Poulsen, Casper 1 Baelde, David 1 Ballester-Bolinches, Adolfo 1 Baunsgaard Kristensen, Magnus 1 Benton, Nick 1 Bentzen, Bruno 1 Berardi, Stefano 1 Blanchette, Jasmin Christian 1 Bonsangue, Marcello Maria 1 Bos, Nathaniel 1 Botta, Nicola 1 Boulier, Simon 1 Bouzy, Aymeric 1 Bove, Ana 1 Bowman, William J. 1 Brede, Nuria ...and 162 more Authors all top 5 Cited in 18 Serials 20 Journal of Functional Programming 18 Logical Methods in Computer Science 11 Mathematical Structures in Computer Science 9 Theoretical Computer Science 8 Journal of Automated Reasoning 3 Higher-Order and Symbolic Computation 2 Science of Computer Programming 2 Annals of Pure and Applied Logic 2 RAIRO. Theoretical Informatics and Applications 2 Journal of Logical and Algebraic Methods in Programming 1 Communications in Mathematical Physics 1 Programming and Computer Software 1 Information and Computation 1 Indagationes Mathematicae. New Series 1 Annals of Mathematics and Artificial Intelligence 1 Theory of Computing Systems 1 Sādhanā 1 ACM Transactions on Computational Logic all top 5 Cited in 10 Fields 157 Computer science (68-XX) 105 Mathematical logic and foundations (03-XX) 24 Category theory; homological algebra (18-XX) 7 Algebraic topology (55-XX) 2 Order, lattices, ordered algebraic structures (06-XX) 1 History and biography (01-XX) 1 General algebraic systems (08-XX) 1 Group theory and generalizations (20-XX) 1 Quantum theory (81-XX) 1 Game theory, economics, finance, and other social and behavioral sciences (91-XX) Citations by Year Wikidata Timeline The data are displayed as stored in Wikidata under a Creative Commons CC0 License. Updates and corrections should be made in Wikidata.