|
Current Teaching (Summer 2012):
Funktionale Programmierung
Formale Sprachen und Komplexität
Seminar Codierung und Information
TCS Oberseminar
Office hour (Sprechstunde):
nach Vereinbarung
Research Interests
- Type Theory, Functional Programming, and Termination
- Type Checking, Unification, and Compiling Dependent Types
- Constructive Logic and Logical Frameworks
- Theorem Proving and Program Verification
Software
Events
- FoSSaCS 2013
- Foundations of Software Science and Computation Structures,
part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2013
16-24 March 2013, Rome, Italy
7 October 2012: Abstract Submission
14 October 2012: Paper Submission
- AIM XVI
- 16th Agda Implementor's Meeting
3 - 9 October 2012 in Copenhagen, Denmark.
- HOR 2012
- 6th International Workshop on Higher-Order Rewriting
2 June 2012, Nagoya, Japan
Colocated with RTA 2012
- ITP 2012
- Third Conference on Interactive Theorem Proving
13-16 August 2012, New Jersey, USA
- RTA 2012
- 23rd International Conference on Rewriting Techniques and Applications
28 May - 2 June 2012, Nagoya, Japan
- Past events and PC memberships...
Thesis
-
A Polymorphic Lambda-Calculus with Sized Higher-Order Types
-
Andreas Abel (2006)
PhD thesis
Appeared as book Type-Based Termination, ISBN 978-3-938363-04-1, © 2007 HARLAND media.
Draft:
.pdf
.ps.gz
.dvi
.bib
-
Type-Based Termination, Inflationary Fixed-Points,
and Mixed Inductive-Coinductive Types
-
Andreas Abel (2012)
Invited talk at the Workshop on Fixed-points in Computer Science (FICS 2012), March 24, 2012, Tallinn, Estonia. Satellite workshop to ETAPS 2012.
.pdf
.ps.gz
.dvi
.bib
-
On Irrelevance and Algorithmic Equality in
Predicative Type Theory
-
Andreas Abel and Gabriel Scherer (2011)
Superseds the FoSSaCS'11 conference paper.
Submitted to Logical Methods in Computer Science.
.pdf
.ps.gz
.dvi
-
A Lambda Term Representation Based on Linear Ordered Logic
-
Andreas Abel and Nicolai Kraus (2011)
6th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, LFMTP 2011, Nijmegen, the Netherlands, August 26, 2011.
.pdf
.ps.gz
.dvi
.bib
-
Higher-Order Dynamic Pattern Unification for
Dependent Types and Records
-
Andreas Abel and Brigitte Pientka (2011)
10th International Conference on Typed Lambda Calculi and Application, TLCA 2011, Novi Sad, Serbia, 1-3 June 2011, part of RDP'11.
LNCS 6690
© Springer.
.pdf
.ps.gz
.dvi
.bib
Extended version:
.pdf
.ps.gz
.dvi
-
A Modular Type Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance
-
Andreas Abel, Thierry Coquand, and Miguel Pagano (2009-11)
Superseds the TLCA'09 conference paper.
Logical Methods in Computer Science 7(2:4) 2011, pp. 1-57.
.pdf
.ps.gz
.dvi
.bib
A note on eta-conversion:
.pdf
-
Irrelevance in Type Theory with a Heterogeneous Equality Judgement
-
Andreas Abel (2010)
Foundations of Software Science and Computation Structures (FoSSaCS 2011),
part of ETAPS 2011, Saarbrücken, Germany, 26-28 March 2011.
LNCS 6009
© Springer.
.bib
-
MiniAgda: Integrating Sized and Dependent Types
-
Andreas Abel (2010)
Workshop on Partiality and Recursion in Interactive Theorem Provers (PAR 2010), 15 July 2010, Federated Logic Conference (FLoC 2010), Edinburgh, UK.
.pdf
.ps.gz
.dvi
.bib
-
Explicit Substitutions for Contextual Type Theory
-
Andreas Abel and Brigitte Pientka (2010)
Logical Frameworks and Metalanguages: Theory and Practice (LFMTP 2010), 14 July 2010, Federated Logic Conference (FLoC 2010), Edinburgh, UK.
.pdf
.ps.gz
.dvi
Extended version:
.pdf
.ps.gz
.dvi
-
Towards Normalization by Evaluation for the Calculus of Constructions
-
Andreas Abel (2009)
Tenth International Symposium on Functional and Logic Programming, FLOPS 2010,
19-21 April 2010,
Sendai, Japan © Springer.
.pdf
.ps.gz
.dvi
.bib
Extended version:
.pdf
.ps.gz
.dvi
-
Typed Applicative Structures and Normalization by Evaluation for System Fω
-
Andreas Abel (2009)
Computer Science Logic, Coimbra, Portugal, September 2009. (34/89)
LNCS 5771 © Springer.
.pdf
.ps.gz
.dvi
.bib
Full version:
.pdf
.ps.gz
.dvi
-
Extensional Normalization in the Logical Framework with Proof Irrelevant Equality
-
Andreas Abel (2009)
Workshop on Normalization by Evaluation, affiliated to LiCS 2009, Los Angeles, 15 August 2009.
.pdf
.ps.gz
.dvi
.bib
Selected Recent Publications
-
Weak βη-Normalization and Normalization by Evaluation for System F
-
Andreas Abel (2008)
Logic for Programming, Artificial Intelligence, and Reasoning, LPAR'08, 22-17 November 2008, Doha, Qatar. (45/153)
LNAI 5330 © Springer.
.pdf
.ps.gz
.dvi
.bib
-
Implementing a Normalizer Using Sized Heterogeneous Types
-
Andreas Abel (2008)
Journal of Functional Programming, MSFP'06 special issue.
.pdf
.ps.gz
.dvi
.bib
-
Semi-continuous Sized Types and Termination
-
Andreas Abel (2007)
Logical Methods in Computer Science, Volume 4, Issue 2, Paper 3. CSL'06 special issue.
LMCS online
.pdf
.ps.gz
.dvi
.bib
-
Type-Based Termination of Generic Programs
-
Andreas Abel (2007)
Science of Computer Programming 74 (2009), pp. 550-567, MPC'06 special issue.
© Elsevier.
EE
.pdf
.ps.gz
.dvi
.bib
-
Mixed Inductive/Coinductive Types and Strong Normalization
-
Andreas Abel (2007)
The Fifth ASIAN Symposium on Programming Languages and Systems (APLAS 2007), Singapore.
.pdf
.ps.gz
.dvi
.bib
-
Syntactical Normalization for Intersection Types with Term Rewriting Rules
-
Andreas Abel (2007)
4th International Workshop on Higher-Order Rewriting, HOR'07, Paris, France, 25 June 2007.
.pdf
.ps.gz
.dvi
.bib
-
Normalization by Evaluation for Martin-Löf Type Theory with Typed Equality Judgements
-
Andreas Abel, Thierry Coquand, Peter Dybjer (2007)
Logics in Computer Science, LICS 2007.
.pdf
.ps.gz
.dvi
.bib
Errata:
.pdf
.ps.gz
.dvi
- More publications...
Last update: 8 May 2012.
- Type-Based Termination,
Inflationary Fixed-Points, and
Mixed Inductive-Coinductive Types
- 24 March 2012, Invited talk at the
Workshop on Fixed Points in Computer Science,
FICS 2012,
part of ETAPS 2012, Tallinn, Estonia.
- On Shape Irrelevance and Polymorphism in Type Theory
- 9 September 2011,
Shonan Meeting Seminar 008, 14th Agda Implementor's Meeting (AIM XIV),
Shonan Village Center, near Tokyo, Japan.
- Higher-Order Pattern Unification for Dependently Typed Records
- 1 June 2011,
TLCA 2011, 10th International Conference on
Typed Lambda Calculi and Applications, RDP 2011,
Novi Sad, Serbia.
- Irrelevance in Type Theory
- 28 March 2011,
14th International Conference on
Foundations of Software Science and Computation Structures
FoSSaCS 2011,
part of European Joint Conferences on Theory and Practice of Software
ETAPS 2011.
- Algorithmic Equality for the Calculus of Constructions
- 14 February 2011,
Two days on Models of the Calculus of Constructions, INRIA pi.r2, Pairs, France.
- Integrating Sized and Dependent Types
- 15 July 2010, Workshop on Partiality and Recursion in Interactive Theorem Provers, PAR-10,
Federated Logic Conference,
FLoC 2010,
Edinburgh, UK.
- Explicit substitutions for contextual type theory
- 14 July 2010, Workshop on Logical Frameworks and Metalanguages: Theory and Practice,
LFMTP 2010,
Federated Logic Conference,
FLoC 2010,
Edinburgh, UK.
- Parametric Dependent Function Types
- 9 July 2010, Workshop on Dependently Typed Programming,
DTP 2010,
Federated Logic Conference,
FLoC 2010,
Edinburgh, UK.
- Normalization by Evaluation for the βη-Calculus of Constructions
- 19 April 2010, 10th Int. Symp. on Functional and Logic Programming, FLOPS 2010, Sendai, Japan.
- On Irrelevance and Extraction in Type Theory
- 2 Februar 2010. Coq-Day on Equality and Termination, La Ciotat, Marseille, France.
- Remarks on Typed Equality for the Calculus of Constructions
- 12 November 2009. Groupe de Travail Types and Semantics, INRIA PI.R2 and PPS, Paris, France.
- Normalization by Evaluation for
the Calculus of Constructions
- 15 October 2009. PPS Lab, Universite Paris VII, France.
13 May 2009. International Workshop on Types for Proofs and Programs, TYPES 2009, Aussois, France.
- Extensions to Definitional Equality in Agda. Or: Making Agda See More
- 15 September 2009. 10th Agda Implementors' Meeting, Gothenburg, Sweden.
- Type Structures and Normalization by Evaluation for
System Fω
- 8 September 2009. Computer Science Logic, CSL'09, Coimbra, Portugal.
- Extensional Normalization in the Logical Framework with Proof Irrelevant Equality
- 15 August 2009. LiCS-affiliated Workshop on Normalization by Evaluation, NBE 2009, Los Angeles, USA.
- More talks...
More teaching...
| Klaus Aehlig
| | colleague, coauthor
| | Thorsten Altenkirch
|
| advisor (Sep 1997 - Apr 2000), coauthor
| | Marcin Benke
| | colleague, coauthor
| | Frédéric Blanqui
| | project partner
| | Pierre Boutillier
| | student
| | Ana Bove
| | colleague, coauthor
| | Bor-Yuh Evan Chang
| | student, coauthor
| | James Chapman
| | visitor
| | Thierry Coquand
| | colleague, coauthor
| | Peter Dybjer
| | colleague, coauthor
| | Nils Anders Danielsson
| | colleague, coimplementor
| | Hugo Herbelin
| | colleague
| | Martin Hofmann
|
| advisor (Oct 2001 - July 2006)
| | John Hughes
| | colleague, coauthor
| | Nicolai Kraus
| | student, coauthor
| | Ralph Matthes
| | colleague, coauthor
| | Karl Mehltretter
| | student, coimplementor
| | Ulf Norell
| | colleague, coauthor, coimplementor
| | Julien Oster
| | student
| | Miguel Pagano
| | coauthor
| | Frank Pfenning
| | advisor (May 2000 - June 2001), coauthor
| | Brigitte Pientka
| | colleague, coauthor
| | Axel Rauschmayer
| | coauthor
| | Colin Riba
| | project partner
| | Dulma Rodriguez
| | student, coauthor
| | Cody Roux
| | student, visitor
| | Gabriel Scherer
| | student, coauthor
| | Carsten Schürmann
| | host
| | Tarmo Uustalu
| | coauthor
|
This is a non-exhaustive list of people with whom I collaborated over
a longer time to produce scientific results.
Bibliometrics
My Erdös Number
is at most 4:
Paul Erdös - E. Rodney Canfield - Guo-Qiang Zhang -
Thierry Coquand - Andreas Abel
My H-index is at least 7.
(Last update: 2010-11-26, hand-computed from Google Scholar citation data.)
Harzing's Publish or Perish tool
gives me a more favorable 13. So does Google Scholar.
[ Home
| CV
| Projects
| Publications
| Talks
| Teaching
| Sharing
]
|