Andreas Abel
Andreas Abel
Senior Lecturer at the Department of Computer Science and Engineering, Gothenburg University
Verified email at - Homepage
Cited by
Cited by
Copatterns: programming infinite structures by observations
A Abel, B Pientka, D Thibodeau, A Setzer
ACM SIGPLAN Notices 48 (1), 27-38, 2013
Wellfounded recursion with copatterns: A unified approach to termination and productivity
AM Abel, B Pientka
ACM SIGPLAN Notices 48 (9), 185-196, 2013
A polymorphic lambda-calculus with sized higher-order types
A Abel
Doktorarbeit (PhD thesis), LMU München, 2006
Termination checking with types
A Abel
RAIRO-Theoretical Informatics and Applications 38 (04), 277-319, 2004
MiniAgda: Integrating sized and dependent types
A Abel
arXiv preprint arXiv:1012.4896, 2010
A predicative analysis of structural recursion
A Abel, T Altenkirch
Journal of functional programming 12 (1), 1-41, 2002
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
Normalization by evaluation for Martin-Löf Type Theory with typed equality judgements
A Abel, T Coquand, P Dybjer
22nd Annual IEEE Symposium on Logic in Computer Science (LICS 2007), 3-12, 2007
On irrelevance and algorithmic equality in predicative type theory
A Abel, G Scherer
arXiv preprint arXiv:1203.4716, 2012
Semi-continuous sized types and termination
A Abel
International Workshop on Computer Science Logic, 72-88, 2006
Cubical Agda: a dependently typed programming language with univalence and higher inductive types
A Vezzosi, A Mörtberg, A Abel
Proceedings of the ACM on Programming Languages 3 (ICFP), 1-29, 2019
Human-Readable Machine-Verifiable Proofs for Teaching Constructive Logic
A Abel, BYE Chang, F Pfenning
Verifying Haskell programs using constructive type theory
A Abel, M Benke, A Bove, J Hughes, U Norell
Proceedings of the 2005 ACM SIGPLAN workshop on Haskell, 62-73, 2005
Higher-order dynamic pattern unification for dependent types and records
A Abel, B Pientka
International Conference on Typed Lambda Calculi and Applications, 10-26, 2011
Well-founded recursion with copatterns and sized types
A Abel, B Pientka
Journal of Functional Programming 26, 2016
Verifying a semantic βη-conversion test for Martin-Löf type theory
A Abel, T Coquand, P Dybjer
Mathematics of Program Construction, 29-56, 2008
Normalization by evaluation for Martin-Löf type theory with one universe
A Abel, K Aehlig, P Dybjer
Electronic Notes in Theoretical Computer Science 173, 17-39, 2007
A predicative strong normalisation proof for a λcalculus with interleaving inductive types
A Abel, T Altenkirch
International Workshop on Types for Proofs and Programs, 21-40, 1999
Type-based termination, inflationary fixed-points, and mixed inductive-coinductive types
A Abel
arXiv preprint arXiv:1202.3496, 2012
Normalization by Evaluation: Dependent Types and Impredicativity
A Abel
Unpublished. http://www. tcs. ifi. lmu. de/~ abel/habil. pdf, 2013
The system can't perform the operation now. Try again later.
Articles 1–20