Andreas Abel - RankMe

87 papers A* 3A 1B 12C 3Misc 3Journal 34Unranked 27

Year	Rank	Type	Title / Venue / Authors
2026	J	`jnl`	A Graded Modal Dependent Type Theory with Erasure, Formalized. CoRR Andreas Abel, Nils Anders Danielsson, Oskar Eriksson
2025	J	`jnl`	The Agda standard library: version 2.0. J. Open Source Softw. Matthew L. Daggitt, Guillaume Allais, James McKinna, Andreas Abel, Van Doorn, Nathan, James Wood, Ulf Norell, Donnacha Oisín Kidney, Sergei Meshveliani, Sandro Stucki, Jacques Carette, Alex Rice, Jason Z. S. Hu, Li-yao Xia, Shu-Hung You, Reed Mullanix, Wen Kokke
2024	J	`jnl`	Equivalence of Applicative Functors and Multifunctors. CoRR Andreas Abel
2024	J	`jnl`	foetus - Termination Checker for Simple Functional Programs. CoRR Andreas Abel
2023	J	`jnl`	A Graded Modal Dependent Type Theory with a Universe and Erasure, Formalized. Proc. ACM Program. Lang. Andreas Abel, Nils Anders Danielsson, Oskar Eriksson
2021	J	`jnl`	Birkhoff's Completeness Theorem for Multi-Sorted Algebras Formalized in Agda. CoRR Andreas Abel
2021	J	`jnl`	Cubical Agda: A dependently typed programming language with univalence and higher inductive types. J. Funct. Program. Andrea Vezzosi, Anders Mörtberg, Andreas Abel
2020	J	`jnl`	A unified view of modalities in type systems. Proc. ACM Program. Lang. Andreas Abel, Jean-Philippe Bernardy
2020	J	`jnl`	Elaborating dependent (co)pattern matching: No pattern left behind. J. Funct. Program. Jesper Cockx, Andreas Abel
2020	J	`jnl`	Failure of Normalization in Impredicative Type Theory with Proof-Irrelevant Propositional Equality. Log. Methods Comput. Sci. Andreas Abel, Thierry Coquand
2020	J	`jnl`	Leibniz equality is isomorphic to Martin-Löf identity, parametrically. J. Funct. Program. Andreas Abel, Jesper Cockx, Dominique Devriese, Amin Timany, Philip Wadler
2020	—	`conf`	On Model-Theoretic Strong Normalization for Truth-Table Natural Deduction. TYPES Andreas Abel
2019	A*	`conf`	A Type Theory for Defining Logics and Proofs. LICS Brigitte Pientka, David Thibodeau, Andreas Abel, Francisco Ferreira, Rébecca Zucchini
2019	J	`jnl`	A Type Theory for Defining Logics and Proofs. CoRR Brigitte Pientka, David Thibodeau, Andreas Abel, Francisco Ferreira, Rébecca Zucchini
2019	J	`jnl`	Cocon: Computation in Contextual Type Theory. CoRR Brigitte Pientka, Andreas Abel, Francisco Ferreira, David Thibodeau, Rébecca Zucchini
2019	J	`jnl`	Cubical agda: a dependently typed programming language with univalence and higher inductive types. Proc. ACM Program. Lang. Andrea Vezzosi, Anders Mörtberg, Andreas Abel
2019	J	`jnl`	Failure of Normalization in Impredicative Type Theory with Proof-Irrelevant Propositional Equality. CoRR Andreas Abel, Thierry Coquand
2019	C	`conf`	Normalization by Evaluation for Call-By-Push-Value and Polarized Lambda Calculus. PPDP Andreas Abel, Christian Sattler
2019	J	`jnl`	Normalization by Evaluation for Call-by-Push-Value and Polarized Lambda-Calculus. CoRR Andreas Abel, Christian Sattler
2019	J	`jnl`	POPLMark reloaded: Mechanizing proofs by logical relations. J. Funct. Program. Andreas Abel, Guillaume Allais, Aliya Hameer, Brigitte Pientka, Alberto Momigliano, Steven Schäfer, Kathrin Stark
2018	—	`ed.`	23rd International Conference on Types for Proofs and Programs, TYPES 2017, Budapest, Hungary, May 29 - June 1, 2017 TYPES Andreas Abel, Fredrik Nordvall Forsberg, Ambrus Kaposi
2018	J	`jnl`	Decidability of conversion for type theory in type theory. Proc. ACM Program. Lang. Andreas Abel, Joakim Öhman, Andrea Vezzosi
2018	J	`jnl`	Elaborating dependent (co)pattern matching. Proc. ACM Program. Lang. Jesper Cockx, Andreas Abel
2017	J	`jnl`	Interactive programming in Agda - Objects and graphical user interfaces. J. Funct. Program. Andreas Abel, Stephan Adelsberger, Anton Setzer
2017	J	`jnl`	Normalization by evaluation for sized dependent types. Proc. ACM Program. Lang. Andreas Abel, Andrea Vezzosi, Théo Winterhalter
2016	—	`conf`	Compositional Coinduction with Sized Types. CMCS Andreas Abel
2016	J	`jnl`	Type checking through unification. CoRR Francesco Mazzoli, Andreas Abel
2016	J	`jnl`	Well-founded recursion with copatterns and sized types. J. Funct. Program. Andreas Abel, Brigitte Pientka
2015	—	`conf`	Well-Founded Recursion over Contextual Objects. TLCA Brigitte Pientka, Andreas Abel
2014	—	`conf`	A Categorical Perspective on Pattern Unification (Extended Abstract). UNIF Andrea Vezzosi, Andreas Abel
2014	B	`conf`	A Formalized Proof of Strong Normalization for Guarded Recursive Types. APLAS Andreas Abel, Andrea Vezzosi
2014	—	`conf`	Normalization by Evaluation in the Delay Monad: A Case Study for Coinduction via Copatterns and Sized Types. MSFP Andreas Abel, James Chapman
2014	C	`conf`	Programming and Reasoning with Infinite Structures Using Copatterns and Sized Types. Software Engineering (Workshops) Andreas Abel
2014	—	`conf`	Unnesting of Copatterns. RTA-TLCA Anton Setzer, Andreas Abel, Brigitte Pientka, David Thibodeau
2013	A*	`conf`	Copatterns: programming infinite structures by observations. POPL Andreas Abel, Brigitte Pientka, David Thibodeau, Anton Setzer
2013	—	`ed.`	Proceedings of the 7th Workshop on Programming languages meets program verification, PLPV 2013, Rome, Italy, January 22, 2013 PLPV Matthew Might, David Van Horn, Andreas Abel, Tim Sheard
2013	A	`conf`	Wellfounded recursion with copatterns: a unified approach to termination and productivity. ICFP Andreas Abel, Brigitte Pientka
2012	J	`jnl`	On Irrelevance and Algorithmic Equality in Predicative Type Theory Log. Methods Comput. Sci. Andreas Abel, Gabriel Scherer
2012	—	`conf`	Type-Based Termination, Inflationary Fixed-Points, and Mixed Inductive-Coinductive Types FICS Andreas Abel
2011	—	`conf`	A Lambda Term Representation Inspired by Linear Ordered Logic LFMTP Andreas Abel, Nicolai Kraus
2011	J	`jnl`	A Modular Type-checking algorithm for Type Theory with Singleton Types and Proof Irrelevance Log. Methods Comput. Sci. Andreas Abel, Thierry Coquand, Miguel Pagano
2011	—	`conf`	Higher-Order Dynamic Pattern Unification for Dependent Types and Records. TLCA Andreas Abel, Brigitte Pientka
2011	B	`conf`	Irrelevance in Type Theory with a Heterogeneous Equality Judgement. FoSSaCS Andreas Abel
2010	—	`conf`	Explicit Substitutions for Contextual Type Theory LFMTP Andreas Abel, Brigitte Pientka
2010	—	`conf`	MiniAgda: Integrating Sized and Dependent Types PAR Andreas Abel
2010	—	`conf`	MiniAgda: Integrating Sized and Dependent Types. PAR@ITP Andreas Abel
2010	Misc	`conf`	Towards Normalization by Evaluation for the FLOPS Andreas Abel
2009	—	`conf`	A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance. TLCA Andreas Abel, Thierry Coquand, Miguel Pagano
2009	J	`jnl`	Implementing a normalizer using sized heterogeneous types. J. Funct. Program. Andreas Abel
2009	—	`ed.`	Proceedings of the International Workshop on Logical Frameworks and Metalanguages: Theory and Practice, LFMTP@LICS 2008, Pittsburgh, PA, USA, June 23, 2008 LFMTP@LICS Andreas Abel, Christian Urban
2009	J	`jnl`	Type-based termination of generic programs. Sci. Comput. Program. Andreas Abel
2009	B	`conf`	Typed Applicative Structures and Normalization by Evaluation for System F CSL Andreas Abel
2008	—	`conf`	A Partial Type Checking Algorithm for Type: Type. MSFP@ICALP Andreas Abel, Thorsten Altenkirch
2008	Misc	`conf`	On the Algebraic Foundation of Proof Assistants for Intuitionistic Type Theory. FLOPS Andreas Abel, Thierry Coquand, Peter Dybjer
2008	J	`jnl`	Polarised subtyping for sized types. Math. Struct. Comput. Sci. Andreas Abel
2008	—	`conf`	Preface. LFMTP@LICS Andreas Abel, Christian Urban
2008	J	`jnl`	Semi-Continuous Sized Types and Termination. Log. Methods Comput. Sci. Andreas Abel
2008	J	`jnl`	Semi-continuous Sized Types and Termination CoRR Andreas Abel
2008	B	`conf`	Syntactic Metatheory of Higher-Order Subtyping. CSL Andreas Abel, Dulma Rodriguez
2008	B	`conf`	Verifying a Semantic beta-eta-Conversion Test for Martin-Löf Type Theory. MPC Andreas Abel, Thierry Coquand, Peter Dybjer
2008	B	`conf`	Weak beta-theta-Normalization and Normalization by Evaluation for System F. LPAR Andreas Abel
2007	B	`conf`	Mixed Inductive/Coinductive Types and Strong Normalization. APLAS Andreas Abel
2007	A*	`conf`	Normalization by Evaluation for Martin-Lof Type Theory with Typed Equality Judgements. LICS Andreas Abel, Thierry Coquand, Peter Dybjer
2007	B	`conf`	Normalization by Evaluation for Martin-Löf Type Theory with One Universe. MFPS Andreas Abel, Klaus Aehlig, Peter Dybjer
2007	—	`conf`	Strong Normalization and Equi-(Co)Inductive Types. TLCA Andreas Abel
2007	—	`—`	Type-based termination: a polymorphic lambda-calculus with sized higher-order types. Andreas Abel
2007	J	`jnl`	Untyped Algorithmic Equality for Martin-Löf's Logical Framework with Surjective Pairs. Fundam. Informaticae Andreas Abel, Thierry Coquand
2006	—	`conf`	Implementing a Normalizer Using Sized Heterogeneous Types. MSFP@MPC Andreas Abel
2006	Misc	`conf`	Polarized Subtyping for Sized Types. CSR Andreas Abel
2006	B	`conf`	Semi-continuous Sized Types and Termination. CSL Andreas Abel
2006	B	`conf`	Towards Generic Programming with Sized Types. MPC Andreas Abel
2005	—	`conf`	Connecting a Logical Framework to a First-Order Logic Prover. FroCoS Andreas Abel, Thierry Coquand, Ulf Norell
2005	J	`jnl`	Iteration and coiteration schemes for higher-order and nested datatypes. Theor. Comput. Sci. Andreas Abel, Ralph Matthes, Tarmo Uustalu
2005	—	`conf`	Untyped Algorithmic Equality for Martin-Löf's Logical Framework with Surjective Pairs. TLCA Andreas Abel, Thierry Coquand
2005	C	`conf`	Verifying haskell programs using constructive type theory. Haskell Andreas Abel, Marcin Benke, Ana Bove, John Hughes, Ulf Norell
2004	B	`conf`	Fixed Points of Type Constructors and Primitive Recursion. CSL Andreas Abel, Ralph Matthes
2004	—	`conf`	Normalization for the Simply-Typed Lambda-Calculus in Twelf. LFM@IJCAR Andreas Abel
2004	J	`jnl`	Termination checking with types. RAIRO Theor. Informatics Appl. Andreas Abel
2003	B	`conf`	Generalized Iteration and Coiteration for Higher-Order Nested Datatypes. FoSSaCS Andreas Abel, Ralph Matthes, Tarmo Uustalu
2003	—	`conf`	Primitive Recursion for Rank-2 Inductive Types. FICS Andreas Abel, Ralph Matthes
2003	—	`conf`	Private Währungen im Internet - Fachkonzept und Einsatzpotenziale. Wirtschaftsinformatik (1) Andreas Abel, Claus Rautenstrauch
2003	—	`conf`	Termination and Productivity Checking with Continuous Types. TLCA Andreas Abel
2002	—	`conf`	(Co-)Iteration for Higher-Order Nested Datatypes. TYPES Andreas Abel, Ralph Matthes
2002	J	`jnl`	A predicative analysis of structural recursion. J. Funct. Program. Andreas Abel, Thorsten Altenkirch
2001	—	`conf`	A Third-Order Representation of the lambda-mu-Calculus. MERLIN Andreas Abel
1999	—	`conf`	A Predicative Strong Normalisation Proof for a lambda-Calculus with Interleaving Inductive Types. TYPES Andreas Abel, Thorsten Altenkirch
1999	—	`conf`	Specification and Verification of a Formal System for Structurally Recursive Functions. TYPES Andreas Abel