 | 2012 |
|---|
| 47 |       | Andreas Abel:
Type-Based Termination, Inflationary Fixed-Points, and Mixed Inductive-Coinductive Types
FICS 2012: 1-11 |
| 46 | | Andreas Abel,
Gabriel Scherer:
On Irrelevance and Algorithmic Equality in Predicative Type Theory
Logical Methods in Computer Science 8(1): (2012) |
| 2011 |
|---|
| 45 | | Andreas Abel:
Irrelevance in Type Theory with a Heterogeneous Equality Judgement.
FOSSACS 2011: 57-71 |
| 44 | | Andreas Abel,
Nicolai Kraus:
A Lambda Term Representation Inspired by Linear Ordered Logic
LFMTP 2011: 1-13 |
| 43 | | Andreas Abel,
Brigitte Pientka:
Higher-Order Dynamic Pattern Unification for Dependent Types and Records.
TLCA 2011: 10-26 |
| 42 | | Andreas Abel,
Thorsten Altenkirch:
A Partial Type Checking Algorithm for Type: Type.
Electr. Notes Theor. Comput. Sci. 229(5): 3-17 (2011) |
| 41 | | 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) |
| 2010 |
|---|
| 40 | | Andreas Abel:
Towards Normalization by Evaluation for the betaeta-Calculus of Constructions.
FLOPS 2010: 224-239 |
| 39 | | Andreas Abel,
Brigitte Pientka:
Explicit Substitutions for Contextual Type Theory
LFMTP 2010: 5-20 |
| 38 | | Andreas Abel:
MiniAgda: Integrating Sized and Dependent Types
PAR 2010: 14-28 |
| 2009 |
|---|
| 37 | | Andreas Abel:
Typed Applicative Structures and Normalization by Evaluation for System Fomega.
CSL 2009: 40-54 |
| 36 | | Andreas Abel,
Thierry Coquand,
Miguel Pagano:
A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance.
TLCA 2009: 5-19 |
| 35 | | Andreas Abel,
Christian Urban:
Preface.
Electr. Notes Theor. Comput. Sci. 228: 1 (2009) |
| 34 | | Andreas Abel:
Implementing a normalizer using sized heterogeneous types.
J. Funct. Program. 19(3-4): 287-310 (2009) |
| 33 | | Andreas Abel:
Type-based termination of generic programs.
Sci. Comput. Program. 74(8): 550-567 (2009) |
| 2008 |
|---|
| 32 | | Andreas Abel,
Dulma Rodriguez:
Syntactic Metatheory of Higher-Order Subtyping.
CSL 2008: 446-460 |
| 31 | | Andreas Abel,
Thierry Coquand,
Peter Dybjer:
On the Algebraic Foundation of Proof Assistants for Intuitionistic Type Theory.
FLOPS 2008: 3-13 |
| 30 | | Andreas Abel:
Weak beta-theta-Normalization and Normalization by Evaluation for System F.
LPAR 2008: 497-511 |
| 29 | | Andreas Abel,
Thierry Coquand,
Peter Dybjer:
Verifying a Semantic beta-eta-Conversion Test for Martin-Löf Type Theory.
MPC 2008: 29-56 |
| 28 | | Andreas Abel:
Semi-continuous Sized Types and Termination
CoRR abs/0804.0876: (2008) |
| 27 | | Andreas Abel:
Normalization for the Simply-Typed Lambda-Calculus in Twelf.
Electr. Notes Theor. Comput. Sci. 199: 3-16 (2008) |
| 26 | | Andreas Abel:
Semi-Continuous Sized Types and Termination.
Logical Methods in Computer Science 4(2): (2008) |
| 25 | | Andreas Abel:
Polarised subtyping for sized types.
Mathematical Structures in Computer Science 18(5): 797-822 (2008) |
| 2007 |
|---|
| 24 | | Andreas Abel:
Mixed Inductive/Coinductive Types and Strong Normalization.
APLAS 2007: 286-301 |
| 23 | | Andreas Abel,
Thierry Coquand,
Peter Dybjer:
Normalization by Evaluation for Martin-Lof Type Theory with Typed Equality Judgements.
LICS 2007: 3-12 |
| 22 | | Andreas Abel:
Strong Normalization and Equi-(Co)Inductive Types.
TLCA 2007: 8-22 |
| 21 | | 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) |
| 20 | | Andreas Abel,
Thierry Coquand:
Untyped Algorithmic Equality for Martin-Löf's Logical Framework with Surjective Pairs.
Fundam. Inform. 77(4): 345-395 (2007) |
| 19 |  | Andreas Abel:
Type-based termination: a polymorphic lambda-calculus with sized higher-order types.
Ludwig Maximilians University Munich 2007: 1-203 |
| 2006 |
|---|
| 18 | | Andreas Abel:
Semi-continuous Sized Types and Termination.
CSL 2006: 72-88 |
| 17 | | Andreas Abel:
Polarized Subtyping for Sized Types.
CSR 2006: 381-392 |
| 16 | | Andreas Abel:
Towards Generic Programming with Sized Types.
MPC 2006: 10-28 |
| 2005 |
|---|
| 15 | | Andreas Abel,
Thierry Coquand,
Ulf Norell:
Connecting a Logical Framework to a First-Order Logic Prover.
FroCos 2005: 285-301 |
| 14 | | Andreas Abel,
Marcin Benke,
Ana Bove,
John Hughes,
Ulf Norell:
Verifying haskell programs using constructive type theory.
Haskell 2005: 62-73 |
| 13 | | Andreas Abel,
Thierry Coquand:
Untyped Algorithmic Equality for Martin-Löf's Logical Framework with Surjective Pairs.
TLCA 2005: 23-38 |
| 12 | | 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) |
| 2004 |
|---|
| 11 | | Andreas Abel,
Ralph Matthes:
Fixed Points of Type Constructors and Primitive Recursion.
CSL 2004: 190-204 |
| 10 | | Andreas Abel:
Termination checking with types.
ITA 38(4): 277-319 (2004) |
| 2003 |
|---|
| 9 | | Andreas Abel,
Ralph Matthes,
Tarmo Uustalu:
Generalized Iteration and Coiteration for Higher-Order Nested Datatypes.
FoSSaCS 2003: 54-69 |
| 8 | | Andreas Abel:
Termination and Productivity Checking with Continuous Types.
TLCA 2003: 1-15 |
| 7 | | Andreas Abel,
Claus Rautenstrauch:
Private Währungen im Internet - Fachkonzept und Einsatzpotenziale.
Wirtschaftsinformatik (1) 2003: 325-344 |
| 2002 |
|---|
| 6 | | Andreas Abel,
Ralph Matthes:
(Co-)Iteration for Higher-Order Nested Datatypes.
TYPES 2002: 1-20 |
| 5 | | Andreas Abel,
Thorsten Altenkirch:
A predicative analysis of structural recursion.
J. Funct. Program. 12(1): 1-41 (2002) |
| 2001 |
|---|
| 4 | | Andreas Abel,
Frank Wolff:
Betrachtungen zur "Schaffung" oder "Abbildung" von Realitäten beispielhaft anhand eines E-Commerce-Projektes.
GI Jahrestagung (2) 2001: 770-775 |
| 3 | | Andreas Abel:
A Third-Order Representation of the lambda-mu-Calculus.
Electr. Notes Theor. Comput. Sci. 58(1): 97-114 (2001) |
| 1999 |
|---|
| 2 | | Andreas Abel:
Specification and Verification of a Formal System for Structurally Recursive Functions.
TYPES 1999: 1-20 |
| 1 | | Andreas Abel,
Thorsten Altenkirch:
A Predicative Strong Normalisation Proof for a lambda-Calculus with Interleaving Inductive Types.
TYPES 1999: 21-40 |
Data released under the ODC-BY 1.0 license — See also our legal information page