Andreas Abel

Assistant Professor (Akademischer Rat auf Zeit, A13)		アンドレアス　アーベル

LFE Theoretische Informatik	e-mail:	andreas.abel@ifi.lmu.de
Ludwig-Maximilians-Universität München	Office:	E111
Oettingenstr. 67	Phone:	+49 89 2180-9315
80538 München, GERMANY	Fax:	+49 89 2180-9338
Wer nach schweren Dingen forscht, dem bringt's Ehre. --- Lutherbibel, Sprüche 25,27b

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

New Publications and Drafts

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...

Selected Recent Talks

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, Inﬂationary 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...

Recent Teaching

Computer-Aided Formal Reasoning (Rechnergestütztes Beweisen)
Semantics of programming languages (Semantik von Programmiersprachen)
Seminar on distributed algorithms (Blockseminar Verteilte Algorithmen)
Advanced Functional Programming (Funktionale Programmierung)
Lambda-Calculus (Lambda-Kalkül)
Python Tutorial (Python-Kompaktkurs)
Type Systems (Typsysteme)
Compiler Construction Lab (Übersetzerbaupraktikum)

More teaching...

Scientific Collaboration

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.

Andreas Abel, http://www.tcs.ifi.lmu.de/~abel