|
Current Teaching (Summer 2013):
Compilerbau-Praktikum Mo 14-18 CIP
Logik und diskrete Strukturen Mi 16-18 A022 Hgb
Seminar Typbasierte Programmanalayse
TCS Oberseminar Fr 14-16 L109
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
- My Habilitation
- 31st May 2013, 2pm, Room BU 101, Oettingenstr. 67, Munich
- TLCA 2013
- Typed Lambda Calculi and Applications,
part of RDP 2013
26-28 June 2013, Eindhoven, The Netherlands
- Past events and PC memberships...
Habilitation Thesis
-
Normalization by Evaluation: Dependent Types and Impredicativity
-
Andreas Abel (2013)
Habilitation thesis
Draft:
.pdf
-
Wellfounded Recursion with Copatterns:
A Unified Approach to Termination and Productivity
-
Andreas Abel, Brigitte Pientka (2013)
Submitted.
.pdf
.bib
Version 2013-03-29:
.pdf
-
Copatterns -- Programming Infinite Structures by Observations
-
Andreas Abel, Brigitte Pientka, David Thibodeau, Anton Setzer (2012)
Accepted for presentation at POPL 2013, Rome, Italy, 23-25 January 2013. (43/233)
© ACM, (2012). This is the author's version of the work.
It is posted here by permission of ACM for your personal use.
Not for redistribution.
The definitive version was published in PUBLICATION,
{VOL##, ISS##, (DATE)} http://doi.acm.org/10.1145/{nnnnnn.nnnnnn}
-
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.
In
Logical Methods in Computer Science, 8(1):1-36, 2012.
.pdf
.ps.gz
.dvi
.bib
-
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
Selected Recent Publications
-
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
-
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, 2008, Volume 4, Issue 2, Paper 3. CSL'06 special issue.
LMCS online
.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
-
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: 1 Mar 2013.
- Copatterns: Programming Infinite
Structures by Observations
- 23 Jan 2013, 40th ACM Symp. on Principles of Programming Languages,
POPL 2013,
Rome, Italy.
- 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
| | Matthias Benkard
| | student
| | 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
| | Anton Setzer
| | coauthor
| | Carsten Schürmann
| | host
| | David Thibodeau
| | student, coauthor
| | 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
]
|