Andreas Abel

Andreas Abel, Brigitte Pientka, David Thibodeau, Anton Setzer: Copatterns: programming infinite structures by observations. POPL 2013: 27-38

Matthew Might, David Van Horn, Andreas Abel, Tim Sheard (Eds.): Proceedings of the 7th Workshop on Programming languages meets program verification, PLPV 2013, Rome, Italy, January 22, 2013. ACM 2013, isbn 978-1-4503-1860-0

Andreas Abel, Gabriel Scherer: On Irrelevance and Algorithmic Equality in Predicative Type Theory. Logical Methods in Computer Science 8(1) (2012)

Andreas Abel: Type-Based Termination, Inflationary Fixed-Points, and Mixed Inductive-Coinductive Types. FICS 2012: 1-11

Andreas Abel, Thierry Coquand, Miguel Pagano: A Modular Type-checking algorithm for Type Theory with Singleton Types and Proof Irrelevance. Logical Methods in Computer Science 7(2) (2011)

Andreas Abel, Thorsten Altenkirch: A Partial Type Checking Algorithm for Type: Type. Electr. Notes Theor. Comput. Sci. 229(5): 3-17 (2011)

Andreas Abel: Irrelevance in Type Theory with a Heterogeneous Equality Judgement. FOSSACS 2011: 57-71

Andreas Abel, Brigitte Pientka: Higher-Order Dynamic Pattern Unification for Dependent Types and Records. TLCA 2011: 10-26

Andreas Abel, Nicolai Kraus: A Lambda Term Representation Inspired by Linear Ordered Logic. LFMTP 2011: 1-13

Andreas Abel: Towards Normalization by Evaluation for the betaeta-Calculus of Constructions. FLOPS 2010: 224-239

Andreas Abel, Brigitte Pientka: Explicit Substitutions for Contextual Type Theory. LFMTP 2010: 5-20

Andreas Abel: MiniAgda: Integrating Sized and Dependent Types. PAR 2010: 14-28

Andreas Abel, Christian Urban: Preface. Electr. Notes Theor. Comput. Sci. 228: 1 (2009)

Andreas Abel: Implementing a normalizer using sized heterogeneous types. J. Funct. Program. 19(3-4): 287-310 (2009)

Andreas Abel: Type-based termination of generic programs. Sci. Comput. Program. 74(8): 550-567 (2009)

Andreas Abel: Typed Applicative Structures and Normalization by Evaluation for System F^omega. CSL 2009: 40-54

Andreas Abel, Thierry Coquand, Miguel Pagano: A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance. TLCA 2009: 5-19

Andreas Abel: Normalization for the Simply-Typed Lambda-Calculus in Twelf. Electr. Notes Theor. Comput. Sci. 199: 3-16 (2008)

Andreas Abel: Semi-Continuous Sized Types and Termination. Logical Methods in Computer Science 4(2) (2008)

Andreas Abel: Polarised subtyping for sized types. Mathematical Structures in Computer Science 18(5): 797-822 (2008)

Andreas Abel, Dulma Rodriguez: Syntactic Metatheory of Higher-Order Subtyping. CSL 2008: 446-460

Andreas Abel, Thierry Coquand, Peter Dybjer: On the Algebraic Foundation of Proof Assistants for Intuitionistic Type Theory. FLOPS 2008: 3-13

Andreas Abel: Weak beta-theta-Normalization and Normalization by Evaluation for System F. LPAR 2008: 497-511

Andreas Abel, Thierry Coquand, Peter Dybjer: Verifying a Semantic beta-eta-Conversion Test for Martin-Löf Type Theory. MPC 2008: 29-56

Andreas Abel: Semi-continuous Sized Types and Termination. CoRR abs/0804.0876 (2008)

Andreas Abel: Type-based termination: a polymorphic lambda-calculus with sized higher-order types. Ludwig Maximilians University Munich 2007, isbn 978-3-938363-04-1, pp. 1-203

Andreas Abel, Klaus Aehlig, Peter Dybjer: Normalization by Evaluation for Martin-Löf Type Theory with One Universe. Electr. Notes Theor. Comput. Sci. 173: 17-39 (2007)

Andreas Abel, Thierry Coquand: Untyped Algorithmic Equality for Martin-Löf's Logical Framework with Surjective Pairs. Fundam. Inform. 77(4): 345-395 (2007)

Andreas Abel: Mixed Inductive/Coinductive Types and Strong Normalization. APLAS 2007: 286-301

Andreas Abel, Thierry Coquand, Peter Dybjer: Normalization by Evaluation for Martin-Lof Type Theory with Typed Equality Judgements. LICS 2007: 3-12

Andreas Abel: Strong Normalization and Equi-(Co)Inductive Types. TLCA 2007: 8-22

Andreas Abel: Semi-continuous Sized Types and Termination. CSL 2006: 72-88

Andreas Abel: Polarized Subtyping for Sized Types. CSR 2006: 381-392

Andreas Abel: Towards Generic Programming with Sized Types. MPC 2006: 10-28

Andreas Abel, Ralph Matthes, Tarmo Uustalu: Iteration and coiteration schemes for higher-order and nested datatypes. Theor. Comput. Sci. 333(1-2): 3-66 (2005)

Andreas Abel, Thierry Coquand, Ulf Norell: Connecting a Logical Framework to a First-Order Logic Prover. FroCoS 2005: 285-301

Andreas Abel, Marcin Benke, Ana Bove, John Hughes, Ulf Norell: Verifying haskell programs using constructive type theory. Haskell 2005: 62-73

Andreas Abel, Thierry Coquand: Untyped Algorithmic Equality for Martin-Löf's Logical Framework with Surjective Pairs. TLCA 2005: 23-38

Andreas Abel: Termination checking with types. ITA 38(4): 277-319 (2004)

Andreas Abel, Ralph Matthes: Fixed Points of Type Constructors and Primitive Recursion. CSL 2004: 190-204

Andreas Abel, Ralph Matthes, Tarmo Uustalu: Generalized Iteration and Coiteration for Higher-Order Nested Datatypes. FoSSaCS 2003: 54-69

Andreas Abel: Termination and Productivity Checking with Continuous Types. TLCA 2003: 1-15

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

Andreas Abel, Thorsten Altenkirch: A predicative analysis of structural recursion. J. Funct. Program. 12(1): 1-41 (2002)

Andreas Abel, Ralph Matthes: (Co-)Iteration for Higher-Order Nested Datatypes. TYPES 2002: 1-20

Andreas Abel: A Third-Order Representation of the lambda-mu-Calculus. Electr. Notes Theor. Comput. Sci. 58(1): 97-114 (2001)

Andreas Abel, Frank Wolff: Betrachtungen zur "Schaffung" oder "Abbildung" von Realitäten beispielhaft anhand eines E-Commerce-Projektes. GI Jahrestagung (2) 2001: 770-775

Andreas Abel: Specification and Verification of a Formal System for Structurally Recursive Functions. TYPES 1999: 1-20

Andreas Abel, Thorsten Altenkirch: A Predicative Strong Normalisation Proof for a lambda-Calculus with Interleaving Inductive Types. TYPES 1999: 21-40