Travelled to:1 × Austria
1 × Brazil
1 × Serbia
1 × USA
2 × Italy
3 × Japan
4 × Poland
Collaborated with:B.Pientka T.Coquand R.Matthes P.Dybjer A.Setzer D.Thibodeau ∅ D.Rodriguez M.Pagano T.Uustalu
Talks about:type (8) copattern (3) theori (3) recurs (3) higher (3) order (3) algorithm (2) normal (2) martin (2) proof (2)
Person: Andreas Abel
DBLP: Abel_0001:Andreas
Contributed to:
2015
2014
2013
20132011
20102009
20082008
200720052004
2003Wrote 13 papers:
- TLCA-2015-Pientka0 #recursion
- Well-Founded Recursion over Contextual Objects (BP, AA), pp. 273–287.
- RTA-TLCA-2014-Setzer0PT #pattern matching
- Unnesting of Copatterns (AS, AA, BP, DT), pp. 31–45.
- ICFP-2013-AbelP #approach #pattern matching #recursion #termination
- Wellfounded recursion with copatterns: a unified approach to termination and productivity (AA, BP), pp. 185–196.
- POPL-2013-AbelPTS #infinity #named #pattern matching #programming
- Copatterns: programming infinite structures by observations (AA, BP, DT, AS), pp. 27–38.
- TLCA-2011-AbelP #dependent type #higher-order #unification
- Higher-Order Dynamic Pattern Unification for Dependent Types and Records (AA, BP), pp. 10–26.
- FLOPS-2010-Abel #calculus #evaluation #normalisation #towards
- Towards Normalization by Evaluation for the βη-Calculus of Constructions (AA), pp. 224–239.
- TLCA-2009-AbelCP #algorithm #composition #proving #type system
- A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance (AA, TC, MP), pp. 5–19.
- CSL-2008-AbelR #higher-order #type system
- Syntactic Metatheory of Higher-Order Subtyping (AA, DR), pp. 446–460.
- FLOPS-2008-AbelCD #algebra #on the #proving #type system
- On the Algebraic Foundation of Proof Assistants for Intuitionistic Type Theory (AA, TC, PD), pp. 3–13.
- LICS-2007-AbelCD #evaluation #normalisation #similarity #type system
- Normalization by Evaluation for Martin-Lof Type Theory with Typed Equality Judgements (AA, TC, PD), pp. 3–12.
- TLCA-2005-AbelC #algorithm #framework #logic #similarity
- Untyped Algorithmic Equality for Martin-Löf’s Logical Framework with Surjective Pairs (AA, TC), pp. 23–38.
- CSL-2004-AbelM #fixpoint #recursion
- Fixed Points of Type Constructors and Primitive Recursion (AA, RM), pp. 190–204.
- FoSSaCS-2003-AbelMU #data type #higher-order
- Generalized Iteration and Coiteration for Higher-Order Nested Datatypes (AA, RM, TU), pp. 54–69.