Andreas Abel

According to our database, Andreas Abel authored at least 71 papers between 1999 and 2024.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of four.

2024

Equivalence of Applicative Functors and Multifunctors.

Andreas Abel

CoRR, 2024

2023

A Graded Modal Dependent Type Theory with a Universe and Erasure, Formalized.

Andreas Abel, Nils Anders Danielsson, Oskar Eriksson

Proc. ACM Program. Lang., August, 2023

2021

Birkhoff's Completeness Theorem for Multi-Sorted Algebras Formalized in Agda.

Andreas Abel

CoRR, 2021

2020

A unified view of modalities in type systems.

Andreas Abel, Jean-Philippe Bernardy

Proc. ACM Program. Lang., 2020

Failure of Normalization in Impredicative Type Theory with Proof-Irrelevant Propositional Equality.

Andreas Abel, Thierry Coquand

Log. Methods Comput. Sci., 2020

Elaborating dependent (co)pattern matching: No pattern left behind.

Jesper Cockx, Andreas Abel

J. Funct. Program., 2020

Leibniz equality is isomorphic to Martin-Löf identity, parametrically.

Andreas Abel, Jesper Cockx, Dominique Devriese, Amin Timany, Philip Wadler

J. Funct. Program., 2020

On Model-Theoretic Strong Normalization for Truth-Table Natural Deduction.

Andreas Abel

Proceedings of the 26th International Conference on Types for Proofs and Programs, 2020

2019

Cubical agda: a dependently typed programming language with univalence and higher inductive types.

Andrea Vezzosi, Anders Mörtberg, Andreas Abel

Proc. ACM Program. Lang., 2019

POPLMark reloaded: Mechanizing proofs by logical relations.

Andreas Abel, Guillaume Allais, Aliya Hameer, Brigitte Pientka, Alberto Momigliano, Steven Schäfer, Kathrin Stark

J. Funct. Program., 2019

Cocon: Computation in Contextual Type Theory.

Brigitte Pientka, Andreas Abel, Francisco Ferreira, David Thibodeau, Rébecca Zucchini

CoRR, 2019

Normalization by Evaluation for Call-By-Push-Value and Polarized Lambda Calculus.

Andreas Abel, Christian Sattler

Proceedings of the 21st International Symposium on Principles and Practice of Programming Languages, 2019

A Type Theory for Defining Logics and Proofs.

Brigitte Pientka, David Thibodeau, Andreas Abel, Francisco Ferreira, Rébecca Zucchini

Proceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science, 2019

2018

Elaborating dependent (co)pattern matching.

Jesper Cockx, Andreas Abel

Proc. ACM Program. Lang., 2018

Decidability of conversion for type theory in type theory.

Andreas Abel, Joakim Öhman, Andrea Vezzosi

Proc. ACM Program. Lang., 2018

2017

Normalization by evaluation for sized dependent types.

Andreas Abel, Andrea Vezzosi, Théo Winterhalter

Proc. ACM Program. Lang., 2017

Interactive programming in Agda - Objects and graphical user interfaces.

Andreas Abel, Stephan Adelsberger, Anton Setzer

J. Funct. Program., 2017

2016

Well-founded recursion with copatterns and sized types.

Andreas Abel, Brigitte Pientka

J. Funct. Program., 2016

Type checking through unification.

Francesco Mazzoli, Andreas Abel

CoRR, 2016

Compositional Coinduction with Sized Types.

Andreas Abel

Proceedings of the Coalgebraic Methods in Computer Science, 2016

2015

Well-Founded Recursion over Contextual Objects.

Brigitte Pientka, Andreas Abel

Proceedings of the 13th International Conference on Typed Lambda Calculi and Applications, 2015

2014

Normalization by Evaluation in the Delay Monad: A Case Study for Coinduction via Copatterns and Sized Types.

Andreas Abel, James Chapman

Proceedings of the Proceedings 5th Workshop on Mathematically Structured Functional Programming, 2014

A Categorical Perspective on Pattern Unification (Extended Abstract).

Andrea Vezzosi, Andreas Abel

Proceedings of the 28th International Workshop on Unification, 2014

Programming and Reasoning with Infinite Structures Using Copatterns and Sized Types.

Andreas Abel

Proceedings of the Gemeinsamer Tagungsband der Workshops der Tagung Software Engineering 2014, 2014

Unnesting of Copatterns.

Anton Setzer, Andreas Abel, Brigitte Pientka, David Thibodeau

Proceedings of the Rewriting and Typed Lambda Calculi - Joint International Conference, 2014

A Formalized Proof of Strong Normalization for Guarded Recursive Types.

Andreas Abel, Andrea Vezzosi

Proceedings of the Programming Languages and Systems - 12th Asian Symposium, 2014

2013

Copatterns: programming infinite structures by observations.

Andreas Abel, Brigitte Pientka, David Thibodeau, Anton Setzer

Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2013

Wellfounded recursion with copatterns: a unified approach to termination and productivity.

Andreas Abel, Brigitte Pientka

Proceedings of the ACM SIGPLAN International Conference on Functional Programming, 2013

2012

On Irrelevance and Algorithmic Equality in Predicative Type Theory

Andreas Abel, Gabriel Scherer

Log. Methods Comput. Sci., 2012

Type-Based Termination, Inflationary Fixed-Points, and Mixed Inductive-Coinductive Types

Andreas Abel

Proceedings of the Proceedings 8th Workshop on Fixed Points in Computer Science, 2012

2011

A Lambda Term Representation Inspired by Linear Ordered Logic

Andreas Abel, Nicolai Kraus

Proceedings of the Proceedings Sixth International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, 2011

A Modular Type-checking algorithm for Type Theory with Singleton Types and Proof Irrelevance

Andreas Abel, Thierry Coquand, Miguel Pagano

Log. Methods Comput. Sci., 2011

Higher-Order Dynamic Pattern Unification for Dependent Types and Records.

Andreas Abel, Brigitte Pientka

Proceedings of the Typed Lambda Calculi and Applications - 10th International Conference, 2011

Irrelevance in Type Theory with a Heterogeneous Equality Judgement.

Andreas Abel

Proceedings of the Foundations of Software Science and Computational Structures, 2011

2010

MiniAgda: Integrating Sized and Dependent Types

Andreas Abel

Proceedings of the Proceedings Workshop on Partiality and Recursion in Interactive Theorem Provers, 2010

Explicit Substitutions for Contextual Type Theory

Andreas Abel, Brigitte Pientka

Proceedings of the Proceedings 5th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, 2010

Towards Normalization by Evaluation for the <i>betaeta</i>-Calculus of Constructions.

Andreas Abel

Proceedings of the Functional and Logic Programming, 10th International Symposium, 2010

2009

Type-based termination of generic programs.

Andreas Abel

Sci. Comput. Program., 2009

Implementing a normalizer using sized heterogeneous types.

Andreas Abel

J. Funct. Program., 2009

Typed Applicative Structures and Normalization by Evaluation for System F^<i>omega</i>.

Andreas Abel

Proceedings of the Computer Science Logic, 23rd international Workshop, 2009

2008

Polarised subtyping for sized types.

Andreas Abel

Math. Struct. Comput. Sci., 2008

Semi-Continuous Sized Types and Termination.

Andreas Abel

Log. Methods Comput. Sci., 2008

Preface.

Andreas Abel, Christian Urban

Proceedings of the International Workshop on Logical Frameworks and Metalanguages: Theory and Practice, 2008

A Partial Type Checking Algorithm for Type: Type.

Andreas Abel, Thorsten Altenkirch

Proceedings of the Second Workshop on Mathematically Structured Functional Programming, 2008

Verifying a Semantic beta-eta-Conversion Test for Martin-Löf Type Theory.

Andreas Abel, Thierry Coquand, Peter Dybjer

Proceedings of the Mathematics of Program Construction, 9th International Conference, 2008

Weak beta-theta-Normalization and Normalization by Evaluation for System F.

Andreas Abel

Proceedings of the Logic for Programming, 2008

On the Algebraic Foundation of Proof Assistants for Intuitionistic Type Theory.

Andreas Abel, Thierry Coquand, Peter Dybjer

Proceedings of the Functional and Logic Programming, 9th International Symposium, 2008

Syntactic Metatheory of Higher-Order Subtyping.

Andreas Abel, Dulma Rodriguez

Proceedings of the Computer Science Logic, 22nd International Workshop, 2008

2007

Type-based termination: a polymorphic lambda-calculus with sized higher-order types.

Andreas Abel

PhD thesis, 2007

Untyped Algorithmic Equality for Martin-Löf's Logical Framework with Surjective Pairs.

Andreas Abel, Thierry Coquand

Fundam. Informaticae, 2007

Normalization by Evaluation for Martin-Löf Type Theory with One Universe.

Andreas Abel, Klaus Aehlig, Peter Dybjer

Proceedings of the 23rd Conference on the Mathematical Foundations of Programming Semantics, 2007

Strong Normalization and Equi-(Co)Inductive Types.

Andreas Abel

Proceedings of the Typed Lambda Calculi and Applications, 8th International Conference, 2007

Normalization by Evaluation for Martin-Lof Type Theory with Typed Equality Judgements.

Andreas Abel, Thierry Coquand, Peter Dybjer

Proceedings of the 22nd IEEE Symposium on Logic in Computer Science (LICS 2007), 2007

Mixed Inductive/Coinductive Types and Strong Normalization.

Andreas Abel

Proceedings of the Programming Languages and Systems, 5th Asian Symposium, 2007

2006

Towards Generic Programming with Sized Types.

Andreas Abel

Proceedings of the Mathematics of Program Construction, 8th International Conference, 2006

Polarized Subtyping for Sized Types.

Andreas Abel

Proceedings of the Computer Science, 2006

2005

Iteration and coiteration schemes for higher-order and nested datatypes.

Andreas Abel, Ralph Matthes, Tarmo Uustalu

Theor. Comput. Sci., 2005

Verifying haskell programs using constructive type theory.

Andreas Abel, Marcin Benke, Ana Bove, John Hughes, Ulf Norell

Proceedings of the ACM SIGPLAN Workshop on Haskell, 2005

Connecting a Logical Framework to a First-Order Logic Prover.

Andreas Abel, Thierry Coquand, Ulf Norell

Proceedings of the Frontiers of Combining Systems, 5th International Workshop, 2005

2004

Termination checking with types.

Andreas Abel

RAIRO Theor. Informatics Appl., 2004

Normalization for the Simply-Typed Lambda-Calculus in Twelf.

Andreas Abel

Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages, 2004

Fixed Points of Type Constructors and Primitive Recursion.

Andreas Abel, Ralph Matthes

Proceedings of the Computer Science Logic, 18th International Workshop, 2004

2003

Private Währungen im Internet - Fachkonzept und Einsatzpotenziale.

Andreas Abel, Claus Rautenstrauch

Proceedings of the Wirtschaftsinformatik 2003, Medien - Märkte - Mobilität, Band I, 2003

Termination and Productivity Checking with Continuous Types.

Andreas Abel

Proceedings of the Typed Lambda Calculi and Applications, 6th International Conference, 2003

Generalized Iteration and Coiteration for Higher-Order Nested Datatypes.

Andreas Abel, Ralph Matthes, Tarmo Uustalu

Proceedings of the Foundations of Software Science and Computational Structures, 2003

Primitive Recursion for Rank-2 Inductive Types.

Andreas Abel, Ralph Matthes

Proceedings of the FICS '03, 2003

2002

A predicative analysis of structural recursion.

Andreas Abel, Thorsten Altenkirch

J. Funct. Program., 2002

(Co-)Iteration for Higher-Order Nested Datatypes.

Andreas Abel, Ralph Matthes

Proceedings of the Types for Proofs and Programs, Second International Workshop, 2002

2001

A Third-Order Representation of the lambda-mu-Calculus.

Andreas Abel

Proceedings of the Mechanized Reasoning about Languages with Variable Binding, 2001

1999

A Predicative Strong Normalisation Proof for a lambda-Calculus with Interleaving Inductive Types.

Andreas Abel, Thorsten Altenkirch

Proceedings of the Types for Proofs and Programs, 1999

Specification and Verification of a Formal System for Structurally Recursive Functions.

Andreas Abel

Proceedings of the Types for Proofs and Programs, 1999