- Home
- About
- Find staff
- Andreas Martin Abel
Andreas Martin Abel
Senior Lecturer
Logic and Types-
A Graded Modal Dependent Type Theory with a Universe and Erasure,
Formalized
Andreas Abel, Nils Anders Danielsson, Oskar Eriksson
Proceedings of the ACM on Programming Languages - 2023 -
Cubical Agda: A dependently typed programming language with univalence and higher inductive
types
Andrea Vezzosi, A. Mortberg, Andreas Abel
Journal of Functional Programming - 2021 -
On model-theoretic strong normalization for truth-table natural
deduction
Andreas Abel
Leibniz International Proceedings in Informatics, LIPIcs - 2021 -
Elaborating dependent (co)pattern matching: No pattern left
behind
Jesper Cockx, Andreas Abel
Journal of Functional Programming - 2020 -
Leibniz equality is isomorphic to Martin-Lof identity,
parametrically
Andreas Abel, J. Cockx, D. Devriese, A. Timany, P. Wadler
Journal of Functional Programming - 2020 -
A Unified View of Modalities in Type
Systems
Andreas Abel, Jean-Philippe Bernardy
Proceedings of the ACM on Programming Languages - 2020 -
FAILURE OF NORMALIZATION IN IMPREDICATIVE TYPE THEORY WITH PROOF-IRRELEVANT PROPOSITIONAL
EQUALITY
Andreas Abel, Thierry Coquand
Logical Methods in Computer Science - 2020 -
POPLMark reloaded: Mechanizing proofs by logical
relations
Andreas Abel, G. Allais, A. Hameer, B. Pientka, A. Momigliano, S. Schafer, K. Stark
Journal of Functional Programming - 2019 -
Cubical Agda: A dependently typed programming language with univalence and higher inductive
types
Andrea Vezzosi, Anders Mörtberg, Andreas Abel
Proceedings of the ACM on Programming Languages (PACMPL). Article no. 87 - 2019 -
Normalization by Evaluation for Call-By-Push-Value and Polarized Lambda
Calculus
Andreas Abel, C. Sattler
PPDP '19: Proceedings of the 21st International Symposium on Principles and Practice of Programming Languages 2019 - 2019 -
A Type Theory for Defining Logics and
Proofs
B. Pientka, D. Thibodeau, Andreas Abel, F. Ferreira, R. Zucchini, Ieee, Ieee,
2019 34TH ANNUAL ACM/IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS) - 2019 -
Decidability of conversion for type theory in type
theory
Andreas Abel, Joakim Öhman, Andrea Vezzosi
Proceedings of the ACM on Programming Languages - 2018 -
23rd International Conference on Types for Proofs and Programs, TYPES 2017, May 29-June 1, 2017, Budapest,
Hungary.
Andreas Abel, Fredrik Nordvall Forsberg, Ambrus Kaposi
2018 -
Resourceful Dependent
Types
Andreas Abel
24th International Conference on Types for Proofs and Programs (TYPES 2018), Braga, Portugal, 18-21 June 2018. - 2018 -
Elaborating dependent (co)pattern
matching
Andreas Abel, Jesper Cockx
Proceedings of the ACM on Programming Languages - 2018 -
Interactive programming in Agda - Objects and graphical user
interfaces
Andreas Abel, S. Adelsberger, A. Setzer
Journal of Functional Programming - 2017 -
Normalization by evaluation for sized dependent
types
Andreas Abel, Andrea Vezzosi, Theo Winterhalter
PACMPL - 2017 -
Normalization by Evaluation for Sized Dependent
Types
Andreas Abel, Andrea Vezzosi, Theo Winterhalter
23nd International Conference on Types for Proofs and Programs (TYPES 2017), Budapest, Hungary, 29 May - 1 June 2017 - 2017 -
Well-founded recursion with copatterns and sized
types
Andreas Abel, B. Pientka
Journal of Functional Programming - 2016 -
Sprinkles of Extensionality for Your Vanilla Type
Theory
Andreas Abel, Jesper Cockx
22nd International Conference on Types for Proofs and Programs (TYPES 2016) - 2016 -
Compositional coinduction with sized
types
Andreas Abel
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) - 2016 -
Normalization by Evaluation in the Delay
Monad
Andreas Abel, James Chapman
22nd International Conference on Types for Proofs and Programs - 2016 -
On Decidability of Conversion in Type
Theory
Andreas Abel, Thierry Coquand, Bassel Mannaa
22nd International Conference on Types for Proofs and Programs (TYPES 2016) - 2016 -
An Extension of Martin-Löf Type Theory with Sized
Types
Andreas Abel, Theo Winterhalter
22nd International Conference on Types for Proofs and Programs (TYPES 2016) - 2016 -
Well-founded recursion over contextual
objects
Brigitte Pientka, Andreas Abel
Leibniz International Proceedings in Informatics, LIPIcs - 2015 -
Normalization by evaluation in the delay monad: A case study for coinduction via copatterns and sized
types
Andreas Abel, James Chapman
Electronic Proceedings in Theoretical Computer Science, EPTCS - 2014 -
Unnesting of
copatterns
A. Setzer, Andreas Abel, B. Pientka, D. Thibodeau
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) - 2014 -
A formalized proof of strong normalization for guarded recursive
types
Andreas Abel, Andrea Vezzosi
Lecture Notes in Computer Science: 12th Asian Symposium on Programming Languages and Systems, APLAS 2014 Singapore, 17-19 November 2014 - 2014 -
Copatterns: Programming infinite structures by
observations
Andreas Abel, Brigitte Pientka, David Thibodeau, Anton Setzer
ACM SIGPLAN Notices - 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, ICFP - 2013 -
A modular type-checking algorithm for type theory with singleton
types
Miguel Pagano, Andreas Abel, Thierry Coquand
Logical Methods in Computer Science - 2011 -
Verifying a Semantic beta-eta-Conversion Test for Martin-Löf Type
Theory
Andreas Abel, Thierry Coquand, Peter Dybjer
Mathematics of Program Construction 2008 - 2008 -
On the Algebraic Foundation of Proof Assistants for Intuitionistic Type
Theory
Andreas Abel, Thierry Coquand, Peter Dybjer
FLOPS 2008 - 2008 -
Normalization by evaluation for Martin-Löf type theory with one
universe
Andreas Abel, Klaus Aehlig, Peter Dybjer
Mathematical Foundations of Programming Semantics, New Orleans, LA, USA, April 2007. Ed. M. Fiore. Electronic Notes in Theoretical Computer Science, Elsevier. - 2007 -
Normalization by Evaluation for Martin-Löf Type Theory with Equality
Judgements
Andreas Abel, Thierry Coquand, Peter Dybjer
Proceedings of 22nd IEEE Annual Symposium on Logic in ComputerScience, Wroclaw, Poland, July 2007. - 2007 -
Untyped algorithmic equality for Martin-Löf's logical framework with surjective
pairs
Andreas Abel, Thierry Coquand
Fundamenta Informaticae - 2007 -
Connecting a Logical Framework to a First-Order Logic
Prover.
Thierry Coquand, Andreas Abel, Ulf Norell
FroCos 2005 - 2005 -
Iteration and coiteration schemes for higher-order and nested
datatypes
Andreas Abel, R. Matthes, T. Uustalu
Theoretical Computer Science - 2005 -
Untyped Algorithmic Equality for Martin-Löf's Logical Framework with Surjective
Pairs.
Thierry Coquand, Andreas Abel
Proceedings of the 7th International Conference on Typed Lambda Calculi and Applications (TLCA 2005); in: LECTURE NOTES IN COMPUTER SCIENCE , Volume: 3461) - 2005 -
Verifying Haskell Programs Using Constructive Type
Theory
Andreas Abel, Marcin Benke, Ana Bove, John Hughes, Ulf Norell
Proceedings of the 2005 ACM SIGPLAN Workshop on Haskell - 2005 -
Termination checking with
types
Andreas Abel
RAIRO - Theoretical Informatics and Applications - 2004 -
Fixed Points of Type Constructors and Primitive
Recursion
Andreas Abel, Ralph Matthes
Lecture Notes in Computer Science - 2004