×
Author ID: abel.andreas-m Recent zbMATH articles by "Abel, Andreas M."
Published as: Abel, Andreas; Abel, Andreas M.
External Links: MGP

Publications by Year

Citations contained in zbMATH Open

49 Publications have been cited 234 times in 151 Documents Cited by Year
Copatterns, programming infinite structures by observations. Zbl 1301.68080
Abel, Andreas; Pientka, Brigitte; Thibodeau, David; Setzer, Anton
23
2013
Iteration and coiteration schemes for higher-order and nested datatypes. Zbl 1070.68093
Abel, Andreas; Matthes, Ralph; Uustalu, Tarmo
18
2005
Wellfounded recursion with copatterns: a unified approach to termination and productivity. Zbl 1323.68087
Abel, Andreas M.; Pientka, Brigitte
17
2013
Cubical Agda: a dependently typed programming language with univalence and higher inductive types. Zbl 1512.68058
Vezzosi, Andrea; Mörtberg, Anders; Abel, Andreas
16
2021
On irrelevance and algorithmic equality in predicative type theory. Zbl 1238.03028
Abel, Andreas; Scherer, Gabriel
13
2012
A predicative analysis of structural recursion. Zbl 0998.68027
Abel, Andreas; Altenkirch, Thorsten
11
2002
Well-founded recursion with copatterns and sized types. Zbl 1420.68031
Abel, Andreas; Pientka, Brigitte
11
2016
Termination checking with types. Zbl 1089.68028
Abel, Andreas
10
2004
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
Well-founded recursion over contextual objects. Zbl 1367.68073
Pientka, Brigitte; Abel, Andreas
7
2015
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
7
2019
A formalized proof of strong normalization for guarded recursive types. Zbl 1453.68035
Abel, Andreas; Vezzosi, Andrea
5
2014
On the algebraic foundation of proof assistants for intuitionistic type theory. Zbl 1137.68570
Abel, Andreas; Coquand, Thierry; Dybjer, Peter
5
2008
Fixed points of type constructors and primitive recursion. Zbl 1095.68059
Abel, Andreas; Matthes, Ralph
4
2004
A two-surface model describing ratchetting behaviors and transient hardening under nonproportional loading. Zbl 0883.73024
Chen, Xu; Abel, A.
4
1996
Mixed inductive/coinductive types and strong normalization. Zbl 1138.68023
Abel, Andreas
4
2007
Normalization by evaluation in the delay monad: a case study for coinduction via copatterns and sized types. Zbl 1464.68050
Abel, Andreas; Chapman, James
4
2014
Polarized subtyping for sized types. Zbl 1142.68326
Abel, Andreas
3
2006
Generalized iteration and coiteration for higher-order nested datatypes. Zbl 1029.68097
Abel, Andreas; Matthes, Ralph; Uustalu, Tarmo
3
2003
Specification and verification of a formal system for structurally recursive functions. Zbl 0988.68054
Abel, Andreas
3
2000
Type-based termination of generic programs. Zbl 1192.68134
Abel, Andreas
3
2009
Implementing a normalizer using sized heterogeneous types. Zbl 1191.68152
Abel, Andreas
3
2009
Typed applicative structures and normalization by evaluation for system \(\mathrm F^{\omega }\). Zbl 1257.03037
Abel, Andreas
3
2009
A third-order representation of the \(\lambda\mu\)-calculus. Zbl 1268.68045
Abel, Andreas
3
2001
Termination and productivity checking with continuous types. Zbl 1039.68029
Abel, Andreas
3
2003
A modular type-checking algorithm for type theory with singleton types and proof irrelevance. Zbl 1213.68199
Abel, Andreas; Coquand, Thierry; Pagano, Miguel
3
2011
Type-based termination, inflationary fixed-points, and mixed inductive-coinductive types. Zbl 1457.68058
Abel, Andreas
3
2012
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
(Co-)Iteration for higher-order nested datatypes. Zbl 1023.68066
Abel, Andreas; Matthes, Ralph
2
2003
A predicative strong normalisation proof for a \(\lambda\)-calculus with interleaving inductive types. Zbl 0988.03029
Abel, Andreas; Altenkirch, Thorsten
2
2000
Polarised subtyping for sized types. Zbl 1156.68014
Abel, Andreas
2
2008
A modular type-checking algorithm for type theory with singleton types and proof irrelevance. Zbl 1246.03025
Abel, Andreas; Coquand, Thierry; Pagano, Miguel
2
2009
Weak \(\beta \eta \)-normalization and normalization by evaluation for System F. Zbl 1182.03100
Abel, Andreas
2
2008
Strong normalization and equi-(co)inductive types. Zbl 1215.03019
Abel, Andreas
2
2007
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
Failure of normalization in impredicative type theory with proof-irrelevant propositional equality. Zbl 07225974
Abel, Andreas; Coquand, Thierry
2
2020
Normalization for the simply-typed lambda-calculus in Twelf. Zbl 1278.68245
Abel, Andreas
1
2007
Unnesting of copatterns. Zbl 1416.68048
Setzer, Anton; Abel, Andreas; Pientka, Brigitte; Thibodeau, David
1
2014
Compositional coinduction with sized types. Zbl 1475.68073
Abel, Andreas
1
2016
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
Syntactic metatheory of higher-order subtyping. Zbl 1156.03311
Abel, Andreas; Rodriguez, Dulma
1
2008
Higher-order dynamic pattern unification for dependent types and records. Zbl 1331.68040
Abel, Andreas; Pientka, Brigitte
1
2011
Towards normalization by evaluation for the \(\beta \eta \)-calculus of constructions. Zbl 1284.68120
Abel, Andreas
1
2010
Elaborating dependent (co)pattern matching: no pattern left behind. Zbl 1442.68025
Cockx, Jesper; Abel, Andreas
1
2020
Interactive programming in Agda – objects and graphical user interfaces. Zbl 1418.68031
Abel, Andreas; Adelsberger, Stephan; Setzer, Anton
1
2017
Cubical Agda: a dependently typed programming language with univalence and higher inductive types. Zbl 1512.68058
Vezzosi, Andrea; Mörtberg, Anders; Abel, Andreas
16
2021
Failure of normalization in impredicative type theory with proof-irrelevant propositional equality. Zbl 07225974
Abel, Andreas; Coquand, Thierry
2
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
7
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
11
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
7
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
4
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
23
2013
Wellfounded recursion with copatterns: a unified approach to termination and productivity. Zbl 1323.68087
Abel, Andreas M.; Pientka, Brigitte
17
2013
On irrelevance and algorithmic equality in predicative type theory. Zbl 1238.03028
Abel, Andreas; Scherer, Gabriel
13
2012
Type-based termination, inflationary fixed-points, and mixed inductive-coinductive types. Zbl 1457.68058
Abel, Andreas
3
2012
A modular type-checking algorithm for type theory with singleton types and proof irrelevance. Zbl 1213.68199
Abel, Andreas; Coquand, Thierry; Pagano, Miguel
3
2011
A partial type checking algorithm for Type:Type. Zbl 1291.68106
Abel, Andreas; Altenkirch, Thorsten
1
2011
Higher-order dynamic pattern unification for dependent types and records. Zbl 1331.68040
Abel, Andreas; Pientka, Brigitte
1
2011
Towards normalization by evaluation for the \(\beta \eta \)-calculus of constructions. Zbl 1284.68120
Abel, Andreas
1
2010
Type-based termination of generic programs. Zbl 1192.68134
Abel, Andreas
3
2009
Implementing a normalizer using sized heterogeneous types. Zbl 1191.68152
Abel, Andreas
3
2009
Typed applicative structures and normalization by evaluation for system \(\mathrm F^{\omega }\). Zbl 1257.03037
Abel, Andreas
3
2009
A modular type-checking algorithm for type theory with singleton types and proof irrelevance. Zbl 1246.03025
Abel, Andreas; Coquand, Thierry; Pagano, Miguel
2
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
On the algebraic foundation of proof assistants for intuitionistic type theory. Zbl 1137.68570
Abel, Andreas; Coquand, Thierry; Dybjer, Peter
5
2008
Polarised subtyping for sized types. Zbl 1156.68014
Abel, Andreas
2
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
4
2007
Normalization by evaluation for Martin-Löf type theory with one universe. Zbl 1316.68038
Abel, Andreas; Aehlig, Klaus; Dybjer, Peter
2
2007
Strong normalization and equi-(co)inductive types. Zbl 1215.03019
Abel, Andreas
2
2007
Normalization for the simply-typed lambda-calculus in Twelf. Zbl 1278.68245
Abel, Andreas
1
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
18
2005
Connecting a logical framework to a first-order logic prover. Zbl 1171.68712
Abel, Andreas; Coquand, Thierry; Norell, Ulf
2
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
4
2004
Generalized iteration and coiteration for higher-order nested datatypes. Zbl 1029.68097
Abel, Andreas; Matthes, Ralph; Uustalu, Tarmo
3
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
2
2003
A predicative analysis of structural recursion. Zbl 0998.68027
Abel, Andreas; Altenkirch, Thorsten
11
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
3
2000
A predicative strong normalisation proof for a \(\lambda\)-calculus with interleaving inductive types. Zbl 0988.03029
Abel, Andreas; Altenkirch, Thorsten
2
2000
A two-surface model describing ratchetting behaviors and transient hardening under nonproportional loading. Zbl 0883.73024
Chen, Xu; Abel, A.
4
1996
all top 5

Cited by 214 Authors

18 Abel, Andreas M.
11 Pientka, Brigitte
7 Stump, Aaron
5 Bizjak, Aleš
5 Coquand, Thierry
5 Matthes, Ralph
4 Altenkirch, Thorsten
4 Berger, Ulrich
4 Birkedal, Lars
4 Blanqui, Frédéric
4 McBride, Conor Thomas
4 Møgelberg, Rasmus Ejlers
4 Uustalu, Tarmo
3 Angiuli, Carlo
3 Clouston, Ranald A.
3 Czajka, Łukasz
3 Dybjer, Peter
3 Eades, Harley III
3 Ghani, Neil
3 Grathwohl, Hans Bugge
3 Gratzer, Daniel
3 Jenkins, Christopher
3 Johann, Patricia
3 Momigliano, Alberto
3 Pfenning, Frank
3 Setzer, Anton
3 Sterling, Jonathan
3 Vezzosi, Andrea
2 Allais, Guillaume
2 Bauer, Andrej
2 Cave, Andrew
2 Chapman, James T. E.
2 Cohen, Liron
2 Fiore, Marcelo P.
2 Huber, Simon
2 Lochbihler, Andreas
2 Miranda Perea, Favio Ezequiel
2 Mörtberg, Anders
2 Nuyts, Andreas
2 Pagano, Miguel
2 Riba, Colin
2 Rutten, Jan J. M. M.
2 Schöpp, Ulrich
2 Schröder, Lutz
2 Sestini, Filippo
2 Szasz, Nora
2 Tasistro, Alvaro
2 Tassi, Enrico
2 Torrini, Paolo
2 Traytel, Dmitry
2 Veltri, Niccolò
2 Weirich, Stephanie
1 Adelsberger, Stephan
1 Aehlig, Klaus
1 Ahn, Ki Yung
1 Ahrens, Benedikt
1 Akama, Yohji
1 Amaro, Maycon J. J.
1 Ariola, Zena M.
1 Asperti, Andrea
1 Atkey, Robert
1 Aubert, Clément
1 Bach Poulsen, Casper
1 Ballester-Bolinches, Adolfo
1 Barthe, Gilles
1 Basold, Henning
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
1 Breuvart, Flavien
1 Brunerie, Guillaume
1 Buisse, Alexandre
1 Caires, Luís
1 Ceulemans, Joris
1 Chan, Jonathan Cheung-Wai
1 Cheney, James
1 Choudhury, Pritam
1 Claessen, Koen
1 Clairambault, Pierre
1 Cockx, Jesper
1 Convent, Lukas
1 Copello, Ernesto
1 Cosme-Llópez, Enric
1 Dagnino, Francesco
1 Dal Lago, Ugo
1 Das, Ankush
1 Demangeon, Romain
1 Derakhshan, Farzaneh
1 Devesas Campos, Marco
1 Devries, Edsko
1 Devriese, Dominique
1 DeYoung, Henry
...and 114 more Authors

Citations by Year