Andreas Abel

ORCID

Publication Activity (10 Years)

Years Active: 1999-2024
Publications (10 Years): 25

Top Venues

CoRR

Proc. ACM Program. Lang.

J. Funct. Program.

TYPES

Ludwig Maximilians University Munich (PHD)

Education History

Ludwig Maximilians University Munich

PHD

Publications

Andreas Abel
Equivalence of Applicative Functors and Multifunctors. CoRR (2024)
Andreas Abel, Nils Anders Danielsson, Oskar Eriksson
A Graded Modal Dependent Type Theory with a Universe and Erasure, Formalized. Proc. ACM Program. Lang. 7 (ICFP) (2023)
Andreas Abel
Birkhoff's Completeness Theorem for Multi-Sorted Algebras Formalized in Agda. CoRR (2021)
Andrea Vezzosi, Anders Mörtberg, Andreas Abel
Cubical Agda: A dependently typed programming language with univalence and higher inductive types. J. Funct. Program. 31 (2021)
Andreas Abel
On Model-Theoretic Strong Normalization for Truth-Table Natural Deduction. TYPES (2020)
Andreas Abel, Jean-Philippe Bernardy
A unified view of modalities in type systems. Proc. ACM Program. Lang. 4 (ICFP) (2020)
Andreas Abel, Thierry Coquand
Failure of Normalization in Impredicative Type Theory with Proof-Irrelevant Propositional Equality. Log. Methods Comput. Sci. 16 (2) (2020)
Andreas Abel, Jesper Cockx, Dominique Devriese, Amin Timany, Philip Wadler
Leibniz equality is isomorphic to Martin-Löf identity, parametrically. J. Funct. Program. 30 (2020)
Jesper Cockx, Andreas Abel
Elaborating dependent (co)pattern matching: No pattern left behind. J. Funct. Program. 30 (2020)
Brigitte Pientka, Andreas Abel, Francisco Ferreira, David Thibodeau, Rébecca Zucchini
Cocon: Computation in Contextual Type Theory. CoRR (2019)
Andreas Abel, Thierry Coquand
Failure of Normalization in Impredicative Type Theory with Proof-Irrelevant Propositional Equality. CoRR (2019)
Brigitte Pientka, David Thibodeau, Andreas Abel, Francisco Ferreira, Rébecca Zucchini
A Type Theory for Defining Logics and Proofs. CoRR (2019)
Andreas Abel, Guillaume Allais, Aliya Hameer, Brigitte Pientka, Alberto Momigliano, Steven Schäfer, Kathrin Stark
POPLMark reloaded: Mechanizing proofs by logical relations. J. Funct. Program. 29 (2019)
Andreas Abel, Christian Sattler
Normalization by Evaluation for Call-by-Push-Value and Polarized Lambda-Calculus. CoRR (2019)
Andrea Vezzosi, Anders Mörtberg, Andreas Abel
Cubical agda: a dependently typed programming language with univalence and higher inductive types. Proc. ACM Program. Lang. 3 (ICFP) (2019)
Brigitte Pientka, David Thibodeau, Andreas Abel, Francisco Ferreira, Rébecca Zucchini
A Type Theory for Defining Logics and Proofs. LICS (2019)
Andreas Abel, Christian Sattler
Normalization by Evaluation for Call-By-Push-Value and Polarized Lambda Calculus. PPDP (2019)
Andreas Abel, Joakim Öhman, Andrea Vezzosi
Decidability of conversion for type theory in type theory. Proc. ACM Program. Lang. 2 (POPL) (2018)
Jesper Cockx, Andreas Abel
Elaborating dependent (co)pattern matching. Proc. ACM Program. Lang. 2 (ICFP) (2018)
Andreas Abel, Andrea Vezzosi, Théo Winterhalter
Normalization by evaluation for sized dependent types. Proc. ACM Program. Lang. 1 (ICFP) (2017)
Andreas Abel, Stephan Adelsberger, Anton Setzer
Interactive programming in Agda - Objects and graphical user interfaces. J. Funct. Program. 27 (2017)
Andreas Abel
Compositional Coinduction with Sized Types. CMCS (2016)
Francesco Mazzoli, Andreas Abel
Type checking through unification. CoRR (2016)
Andreas Abel, Brigitte Pientka
Well-founded recursion with copatterns and sized types. J. Funct. Program. 26 (2016)
Brigitte Pientka, Andreas Abel
Well-Founded Recursion over Contextual Objects. TLCA (2015)
Anton Setzer, Andreas Abel, Brigitte Pientka, David Thibodeau
Unnesting of Copatterns. RTA-TLCA (2014)
Andreas Abel, Andrea Vezzosi
A Formalized Proof of Strong Normalization for Guarded Recursive Types. APLAS (2014)
Andrea Vezzosi, Andreas Abel
A Categorical Perspective on Pattern Unification (Extended Abstract). UNIF (2014)
Andreas Abel
Programming and Reasoning with Infinite Structures Using Copatterns and Sized Types. Software Engineering (Workshops) (2014)
Andreas Abel, James Chapman
Normalization by Evaluation in the Delay Monad: A Case Study for Coinduction via Copatterns and Sized Types. MSFP (2014)
Andreas Abel, Brigitte Pientka, David Thibodeau, Anton Setzer
Copatterns: programming infinite structures by observations. POPL (2013)
Andreas Abel, Brigitte Pientka
Wellfounded recursion with copatterns: a unified approach to termination and productivity. ICFP (2013)
Andreas Abel
Type-Based Termination, Inflationary Fixed-Points, and Mixed Inductive-Coinductive Types FICS (2012)
Andreas Abel, Gabriel Scherer
On Irrelevance and Algorithmic Equality in Predicative Type Theory Log. Methods Comput. Sci. 8 (1) (2012)
Andreas Abel, Nicolai Kraus
A Lambda Term Representation Inspired by Linear Ordered Logic LFMTP (2011)
Andreas Abel
Irrelevance in Type Theory with a Heterogeneous Equality Judgement. FoSSaCS (2011)
Andreas Abel, Brigitte Pientka
Higher-Order Dynamic Pattern Unification for Dependent Types and Records. TLCA (2011)
Andreas Abel, Thierry Coquand, Miguel Pagano
A Modular Type-checking algorithm for Type Theory with Singleton Types and Proof Irrelevance Log. Methods Comput. Sci. 7 (2) (2011)
Andreas Abel, Thorsten Altenkirch
A Partial Type Checking Algorithm for Type: Type. Electron. Notes Theor. Comput. Sci. 229 (5) (2011)
Andreas Abel, Brigitte Pientka
Explicit Substitutions for Contextual Type Theory LFMTP (2010)
Andreas Abel
MiniAgda: Integrating Sized and Dependent Types PAR (2010)
Andreas Abel
-Calculus of Constructions. FLOPS (2010)
Andreas Abel
MiniAgda: Integrating Sized and Dependent Types. PAR@ITP (2010)
Andreas Abel, Christian Urban
Preface. Electron. Notes Theor. Comput. Sci. 228 (2009)
Andreas Abel
Implementing a normalizer using sized heterogeneous types. J. Funct. Program. 19 (3-4) (2009)
Andreas Abel
Type-based termination of generic programs. Sci. Comput. Program. 74 (8) (2009)
Andreas Abel
. CSL (2009)
Andreas Abel, Thierry Coquand, Miguel Pagano
A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance. TLCA (2009)
Andreas Abel, Dulma Rodriguez
Syntactic Metatheory of Higher-Order Subtyping. CSL (2008)
Andreas Abel, Thierry Coquand, Peter Dybjer
Verifying a Semantic beta-eta-Conversion Test for Martin-Löf Type Theory. MPC (2008)
Andreas Abel
Semi-continuous Sized Types and Termination CoRR (2008)
Andreas Abel
Weak beta-theta-Normalization and Normalization by Evaluation for System F. LPAR (2008)
Andreas Abel, Thierry Coquand, Peter Dybjer
On the Algebraic Foundation of Proof Assistants for Intuitionistic Type Theory. FLOPS (2008)
Andreas Abel
Semi-Continuous Sized Types and Termination. Log. Methods Comput. Sci. 4 (2) (2008)
Andreas Abel
Polarised subtyping for sized types. Math. Struct. Comput. Sci. 18 (5) (2008)
Andreas Abel
Normalization for the Simply-Typed Lambda-Calculus in Twelf. Electron. Notes Theor. Comput. Sci. 199 (2008)
Andreas Abel
Mixed Inductive/Coinductive Types and Strong Normalization. APLAS (2007)
Andreas Abel, Thierry Coquand, Peter Dybjer
Normalization by Evaluation for Martin-Lof Type Theory with Typed Equality Judgements. LICS (2007)
Andreas Abel, Klaus Aehlig, Peter Dybjer
Normalization by Evaluation for Martin-Löf Type Theory with One Universe. MFPS (2007)
Andreas Abel
Strong Normalization and Equi-(Co)Inductive Types. TLCA (2007)
Andreas Abel, Thierry Coquand
Untyped Algorithmic Equality for Martin-Löf's Logical Framework with Surjective Pairs. Fundam. Informaticae 77 (4) (2007)
Andreas Abel
Towards Generic Programming with Sized Types. MPC (2006)
Andreas Abel
Polarized Subtyping for Sized Types. CSR (2006)
Andreas Abel
Implementing a Normalizer Using Sized Heterogeneous Types. MSFP@MPC (2006)
Andreas Abel
Semi-continuous Sized Types and Termination. CSL (2006)
Andreas Abel, Ralph Matthes, Tarmo Uustalu
Iteration and coiteration schemes for higher-order and nested datatypes. Theor. Comput. Sci. 333 (1-2) (2005)
Andreas Abel, Thierry Coquand
Untyped Algorithmic Equality for Martin-Löf's Logical Framework with Surjective Pairs. TLCA (2005)
Andreas Abel, Marcin Benke, Ana Bove, John Hughes, Ulf Norell
Verifying haskell programs using constructive type theory. Haskell (2005)
Andreas Abel, Thierry Coquand, Ulf Norell
Connecting a Logical Framework to a First-Order Logic Prover. FroCoS (2005)
Andreas Abel, Ralph Matthes
Fixed Points of Type Constructors and Primitive Recursion. CSL (2004)
Andreas Abel
Termination checking with types. RAIRO Theor. Informatics Appl. 38 (4) (2004)
Andreas Abel, Ralph Matthes
Primitive Recursion for Rank-2 Inductive Types. FICS (2003)
Andreas Abel
Termination and Productivity Checking with Continuous Types. TLCA (2003)
Andreas Abel, Ralph Matthes, Tarmo Uustalu
Generalized Iteration and Coiteration for Higher-Order Nested Datatypes. FoSSaCS (2003)
Andreas Abel, Claus Rautenstrauch
Private Währungen im Internet - Fachkonzept und Einsatzpotenziale. Wirtschaftsinformatik (1) (2003)
Andreas Abel, Ralph Matthes
(Co-)Iteration for Higher-Order Nested Datatypes. TYPES (2002)
Andreas Abel, Thorsten Altenkirch
A predicative analysis of structural recursion. J. Funct. Program. 12 (1) (2002)
Andreas Abel
A Third-Order Representation of the lambda-mu-Calculus. Electron. Notes Theor. Comput. Sci. 58 (1) (2001)
Andreas Abel, Thorsten Altenkirch
A Predicative Strong Normalisation Proof for a lambda-Calculus with Interleaving Inductive Types. TYPES (1999)
Andreas Abel
Specification and Verification of a Formal System for Structurally Recursive Functions. TYPES (1999)

Andreas Abel.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Andreas Abel