Specification and Verification of a Formal System for Structurally Recursive Functions. - Andreas Abel 001 (TYPES, 1999)

A Predicative Strong Normalisation Proof for a lambda-Calculus with Interleaving Inductive Types. - Andreas Abel 001; Thorsten Altenkirch (TYPES, 1999)

A Third-Order Representation of the lambda-mu-Calculus. - Andreas Abel 001 (MERLIN, 2001)

(Co-)Iteration for Higher-Order Nested Datatypes. - Andreas Abel 001; Ralph Matthes (TYPES, 2002)

A predicative analysis of structural recursion. - Andreas Abel 001; Thorsten Altenkirch (J. Funct. Program., 2002)

Primitive Recursion for Rank-2 Inductive Types. - Andreas Abel 001; Ralph Matthes (FICS, 2003)

Generalized Iteration and Coiteration for Higher-Order Nested Datatypes. - Andreas Abel 001; Ralph Matthes; Tarmo Uustalu (FoSSaCS, 2003)

Termination and Productivity Checking with Continuous Types. - Andreas Abel 001 (TLCA, 2003)

Private Währungen im Internet - Fachkonzept und Einsatzpotenziale. - Andreas Abel 001; Claus Rautenstrauch (Wirtschaftsinformatik (1), 2003)

Fixed Points of Type Constructors and Primitive Recursion. - Andreas Abel 001; Ralph Matthes (CSL, 2004)

Normalization for the Simply-Typed Lambda-Calculus in Twelf. - Andreas Abel 001 (LFM@IJCAR, 2004)

Termination checking with types. - Andreas Abel 001 (RAIRO Theor. Informatics Appl., 2004)

Connecting a Logical Framework to a First-Order Logic Prover. - Andreas Abel 001; Thierry Coquand; Ulf Norell (FroCoS, 2005)

Verifying haskell programs using constructive type theory. - Andreas Abel 001; Marcin Benke; Ana Bove; John Hughes 001; Ulf Norell (Haskell, 2005)

Iteration and coiteration schemes for higher-order and nested datatypes. - Andreas Abel 001; Ralph Matthes; Tarmo Uustalu (Theor. Comput. Sci., 2005)

Polarized Subtyping for Sized Types. - Andreas Abel 001 (CSR, 2006)

Towards Generic Programming with Sized Types. - Andreas Abel 001 (MPC, 2006)

Mixed Inductive/Coinductive Types and Strong Normalization. - Andreas Abel 001 (APLAS, 2007)

Normalization by Evaluation for Martin-Lof Type Theory with Typed Equality Judgements. - Andreas Abel 001; Thierry Coquand; Peter Dybjer (LICS, 2007)

Strong Normalization and Equi-(Co)Inductive Types. - Andreas Abel 001 (TLCA, 2007)

Normalization by Evaluation for Martin-Löf Type Theory with One Universe. - Andreas Abel 001; Klaus Aehlig; Peter Dybjer (MFPS, 2007)

Untyped Algorithmic Equality for Martin-Löf's Logical Framework with Surjective Pairs. - Andreas Abel 001; Thierry Coquand (Fundam. Informaticae, 2007)

Type-based termination: a polymorphic lambda-calculus with sized higher-order types. - Andreas Abel 001 (2007)

Syntactic Metatheory of Higher-Order Subtyping. - Andreas Abel 001; Dulma Rodriguez (CSL, 2008)

On the Algebraic Foundation of Proof Assistants for Intuitionistic Type Theory. - Andreas Abel 001; Thierry Coquand; Peter Dybjer (FLOPS, 2008)

Weak beta-theta-Normalization and Normalization by Evaluation for System F. - Andreas Abel 001 (LPAR, 2008)

Verifying a Semantic beta-eta-Conversion Test for Martin-Löf Type Theory. - Andreas Abel 001; Thierry Coquand; Peter Dybjer (MPC, 2008)

A Partial Type Checking Algorithm for Type: Type. - Andreas Abel 001; Thorsten Altenkirch (MSFP@ICALP, 2008)

Preface. - Andreas Abel 001; Christian Urban (LFMTP@LICS, 2008)

Semi-Continuous Sized Types and Termination. - Andreas Abel 001 (Log. Methods Comput. Sci., 2008)

Polarised subtyping for sized types. - Andreas Abel 001 (Math. Struct. Comput. Sci., 2008)

Typed Applicative Structures and Normalization by Evaluation for System Fomega. - Andreas Abel 001 (CSL, 2009)

Implementing a normalizer using sized heterogeneous types. - Andreas Abel 001 (J. Funct. Program., 2009)

Type-based termination of generic programs. - Andreas Abel 001 (Sci. Comput. Program., 2009)

Towards Normalization by Evaluation for the betaeta-Calculus of Constructions. - Andreas Abel 001 (FLOPS, 2010)

Explicit Substitutions for Contextual Type Theory - Andreas Abel 001; Brigitte Pientka (LFMTP, 2010)

MiniAgda: Integrating Sized and Dependent Types - Andreas Abel 001 (PAR, 2010)

Irrelevance in Type Theory with a Heterogeneous Equality Judgement. - Andreas Abel 001 (FoSSaCS, 2011)

Higher-Order Dynamic Pattern Unification for Dependent Types and Records. - Andreas Abel 001; Brigitte Pientka (TLCA, 2011)

A Modular Type-checking algorithm for Type Theory with Singleton Types and Proof Irrelevance - Andreas Abel 001; Thierry Coquand; Miguel Pagano (Log. Methods Comput. Sci., 2011)

A Lambda Term Representation Inspired by Linear Ordered Logic - Andreas Abel 001; Nicolai Kraus (LFMTP, 2011)

Type-Based Termination, Inflationary Fixed-Points, and Mixed Inductive-Coinductive Types - Andreas Abel 001 (FICS, 2012)

On Irrelevance and Algorithmic Equality in Predicative Type Theory - Andreas Abel 001; Gabriel Scherer (Log. Methods Comput. Sci., 2012)

Wellfounded recursion with copatterns: a unified approach to termination and productivity. - Andreas Abel 001; Brigitte Pientka (ICFP, 2013)

Copatterns: programming infinite structures by observations. - Andreas Abel 001; Brigitte Pientka; David Thibodeau 001; Anton Setzer (POPL, 2013)

A Formalized Proof of Strong Normalization for Guarded Recursive Types. - Andreas Abel 001; Andrea Vezzosi (APLAS, 2014)

Unnesting of Copatterns. - Anton Setzer; Andreas Abel 001; Brigitte Pientka; David Thibodeau 001 (RTA-TLCA, 2014)

Programming and Reasoning with Infinite Structures Using Copatterns and Sized Types. - Andreas Abel 001 (Software Engineering (Workshops), 2014)

A Categorical Perspective on Pattern Unification (Extended Abstract). - Andrea Vezzosi; Andreas Abel 001 (UNIF, 2014)

Normalization by Evaluation in the Delay Monad: A Case Study for Coinduction via Copatterns and Sized Types. - Andreas Abel 001; James Chapman 001 (MSFP, 2014)

Well-Founded Recursion over Contextual Objects. - Brigitte Pientka; Andreas Abel 001 (TLCA, 2015)

Compositional Coinduction with Sized Types. - Andreas Abel 001 (CMCS, 2016)

Type checking through unification. - Francesco Mazzoli; Andreas Abel 001 (CoRR, 2016)

Well-founded recursion with copatterns and sized types. - Andreas Abel 001; Brigitte Pientka (J. Funct. Program., 2016)

Interactive programming in Agda - Objects and graphical user interfaces. - Andreas Abel 001; Stephan Adelsberger; Anton Setzer (J. Funct. Program., 2017)

Normalization by evaluation for sized dependent types. - Andreas Abel 001; Andrea Vezzosi; Théo Winterhalter (Proc. ACM Program. Lang., 2017)

Decidability of conversion for type theory in type theory. - Andreas Abel 001; Joakim Öhman; Andrea Vezzosi (Proc. ACM Program. Lang., 2018)

Elaborating dependent (co)pattern matching. - Jesper Cockx; Andreas Abel 001 (Proc. ACM Program. Lang., 2018)

A Type Theory for Defining Logics and Proofs. - Brigitte Pientka; David Thibodeau 001; Andreas Abel 001; Francisco Ferreira 001; Rébecca Zucchini (LICS, 2019)

Normalization by Evaluation for Call-By-Push-Value and Polarized Lambda Calculus. - Andreas Abel 001; Christian Sattler (PPDP, 2019)

Cocon: Computation in Contextual Type Theory. - Brigitte Pientka; Andreas Abel 001; Francisco Ferreira 001; David Thibodeau 001; Rébecca Zucchini (CoRR, 2019)

POPLMark reloaded: Mechanizing proofs by logical relations. - Andreas Abel 001; Guillaume Allais; Aliya Hameer; Brigitte Pientka; Alberto Momigliano; Steven Schäfer; Kathrin Stark (J. Funct. Program., 2019)

Cubical agda: a dependently typed programming language with univalence and higher inductive types. - Andrea Vezzosi; Anders Mörtberg; Andreas Abel 001 (Proc. ACM Program. Lang., 2019)

On Model-Theoretic Strong Normalization for Truth-Table Natural Deduction. - Andreas Abel 001 (TYPES, 2020)

Leibniz equality is isomorphic to Martin-Löf identity, parametrically. - Andreas Abel 001; Jesper Cockx; Dominique Devriese; Amin Timany; Philip Wadler (J. Funct. Program., 2020)

Elaborating dependent (co)pattern matching: No pattern left behind. - Jesper Cockx; Andreas Abel 001 (J. Funct. Program., 2020)

Failure of Normalization in Impredicative Type Theory with Proof-Irrelevant Propositional Equality. - Andreas Abel 001; Thierry Coquand (Log. Methods Comput. Sci., 2020)

A unified view of modalities in type systems. - Andreas Abel 001; Jean-Philippe Bernardy (Proc. ACM Program. Lang., 2020)

Birkhoff's Completeness Theorem for Multi-Sorted Algebras Formalized in Agda. - Andreas Abel 001 (CoRR, 2021)

A Graded Modal Dependent Type Theory with a Universe and Erasure, Formalized. - Andreas Abel 001; Nils Anders Danielsson; Oskar Eriksson (Proc. ACM Program. Lang., 2023)

Equivalence of Applicative Functors and Multifunctors. - Andreas Abel 001 (CoRR, 2024)

foetus - Termination Checker for Simple Functional Programs. - Andreas Abel 001 (CoRR, 2024)