2009 |
30 | EE | Andreas Abel,
Christian Urban:
Preface.
Electr. Notes Theor. Comput. Sci. 228: 1 (2009) |
2008 |
29 | EE | Andreas Abel,
Dulma Rodriguez:
Syntactic Metatheory of Higher-Order Subtyping.
CSL 2008: 446-460 |
28 | EE | Andreas Abel,
Thierry Coquand,
Peter Dybjer:
On the Algebraic Foundation of Proof Assistants for Intuitionistic Type Theory.
FLOPS 2008: 3-13 |
27 | EE | Andreas Abel:
Weak beta-theta-Normalization and Normalization by Evaluation for System F.
LPAR 2008: 497-511 |
26 | EE | Andreas Abel,
Thierry Coquand,
Peter Dybjer:
Verifying a Semantic beta-eta-Conversion Test for Martin-Löf Type Theory.
MPC 2008: 29-56 |
25 | EE | Andreas Abel:
Semi-continuous Sized Types and Termination
CoRR abs/0804.0876: (2008) |
24 | EE | Andreas Abel:
Normalization for the Simply-Typed Lambda-Calculus in Twelf.
Electr. Notes Theor. Comput. Sci. 199: 3-16 (2008) |
23 | EE | Andreas Abel:
Polarised subtyping for sized types.
Mathematical Structures in Computer Science 18(5): 797-822 (2008) |
2007 |
22 | EE | Andreas Abel:
Mixed Inductive/Coinductive Types and Strong Normalization.
APLAS 2007: 286-301 |
21 | EE | Andreas Abel,
Thierry Coquand,
Peter Dybjer:
Normalization by Evaluation for Martin-Lof Type Theory with Typed Equality Judgements.
LICS 2007: 3-12 |
20 | EE | Andreas Abel:
Strong Normalization and Equi-(Co)Inductive Types.
TLCA 2007: 8-22 |
19 | EE | 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) |
18 | EE | Andreas Abel,
Thierry Coquand:
Untyped Algorithmic Equality for Martin-Löf's Logical Framework with Surjective Pairs.
Fundam. Inform. 77(4): 345-395 (2007) |
2006 |
17 | EE | Andreas Abel:
Semi-continuous Sized Types and Termination.
CSL 2006: 72-88 |
16 | EE | Andreas Abel:
Polarized Subtyping for Sized Types.
CSR 2006: 381-392 |
15 | EE | Andreas Abel:
Towards Generic Programming with Sized Types.
MPC 2006: 10-28 |
2005 |
14 | EE | Andreas Abel,
Thierry Coquand,
Ulf Norell:
Connecting a Logical Framework to a First-Order Logic Prover.
FroCos 2005: 285-301 |
13 | EE | Andreas Abel,
Marcin Benke,
Ana Bove,
John Hughes,
Ulf Norell:
Verifying haskell programs using constructive type theory.
Haskell 2005: 62-73 |
12 | EE | Andreas Abel,
Thierry Coquand:
Untyped Algorithmic Equality for Martin-Löf's Logical Framework with Surjective Pairs.
TLCA 2005: 23-38 |
11 | EE | 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 |
10 | EE | Andreas Abel,
Ralph Matthes:
Fixed Points of Type Constructors and Primitive Recursion.
CSL 2004: 190-204 |
2003 |
9 | EE | Andreas Abel,
Ralph Matthes,
Tarmo Uustalu:
Generalized Iteration and Coiteration for Higher-Order Nested Datatypes.
FoSSaCS 2003: 54-69 |
8 | EE | 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 | EE | 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 | EE | Andreas Abel:
A Third-Order Representation of the lambda-mu-Calculus.
Electr. Notes Theor. Comput. Sci. 58(1): (2001) |
1999 |
2 | EE | Andreas Abel:
Specification and Verification of a Formal System for Structurally Recursive Functions.
TYPES 1999: 1-20 |
1 | EE | Andreas Abel,
Thorsten Altenkirch:
A Predicative Strong Normalisation Proof for a lambda-Calculus with Interleaving Inductive Types.
TYPES 1999: 21-40 |