Andreas Abel

Research and Teaching Assistant (wissenschaftlicher Mitarbeiter, A13)

LFE Theoretische Informatik	e-mail:	abel@informatik.uni-muenchen.de
Ludwig-Maximilians-Universität München	Office:	D1.09
Oettingenstr. 67	Phone:	+49 89 2180-9315
80538 München, GERMANY	Fax:	+49 89 2180-9338

Current Teaching:

Algorithms and data structures (Algorithmen und Datenstrukturen)
Functional programming (Funktionale Programmierung)

Office hour (Sprechstunde): nach Vereinbarung

Research Interests

Type Theory, Functional Programming, and Termination
Constructive Logic and Logical Frameworks
Theorem Proving and Program Verification

Events

FoSSaCS 2010: Foundations of Software Science and Computation Structures (PC member)
PLPV'09: Programming Languages meet Program Verification, International Workshop (PC member)
20 January 2009, Savannah, Georgia, USA. Affiliated with POPL 2009.
LFMTP'08: International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (Organizer and PC co-chair)
23 June 2008, Pittsburgh, PA, USA, colocated with LiCS'08
LFMTP'07: International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice(PC member)
16 July 2007, Bremen, Germany, colocated with CADE-21.

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

Recent Publications and Drafts

Typed Applicative Structures and Normalization by Evaluation for System F^ω (New.): Andreas Abel (2009)
To appear at CSL 2009.
.pdf .ps.gz .dvi Full version: .pdf .ps.gz .dvi
A Modular Type Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance (New.): Andreas Abel, Thierry Coquand, and Miguel Pagano (2009)
9th International Conference on Typed Lambda Calculi and Applications, TLCA'09, 1-3 July 2009, Brasilia, Brazil.
LNCS 5608 © Springer.
.pdf .ps.gz .dvi .bib Full version: .pdf .ps.gz .dvi
Polarized Subtyping for Sized Types (Appeared.): Andreas Abel (2006)
Superseds CSR'06 conference paper.
Mathematical Structures in Computer Science, vol. 18, pp. 797-822, special issue on subtyping. © Cambridge University Press.
.pdf .ps.gz .dvi .bib
Weak βη-Normalization and Normalization by Evaluation for System F (New.): 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
Syntactic Metatheory of Higher-Order Subtyping (New.): Andreas Abel and Dulma Rodriguez (2008)
Computer Science Logic, CSL'08. To appear.
.pdf .ps.gz .dvi .bib
A Partial Type Checking Algorithm for Type:Type (New.): Andreas Abel and Thorsten Altenkirch (2008)
Mathematically Structured Functional Programming, MSFP'08. To appear.
.pdf .ps.gz .dvi .bib
Verifying a Semantic βη-Conversion Test for Martin-Löf Type Theory: Andreas Abel, Thierry Coquand, Peter Dybjer (2008)
9th International Conference on Mathematics of Program Construction, MPC'08, Marseille, France, 15-18 July 2008. (18/38)
LNCS 5133 © Springer.
.pdf .ps.gz .dvi .bib Extended version: .pdf .ps.gz .dvi
On the Algebraic Foundation of Proof Assistants for Intuitionistic Type Theory: Andreas Abel, Thierry Coquand, Peter Dybjer (2008)
9th International Symposium on Functional and Logic Programming, FLOPS'08, Invited paper. © Springer
.pdf .bib
Implementing a Normalizer Using Sized Heterogeneous Types: Andreas Abel (2008)
Journal of Functional Programming, MSFP'06 special issue. To appear.
.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 (Appeared.): 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

Selected Recent Talks

Normalization by Evaluation for the Calculus of Constructions: 13 May 2009. International Workshop on Types for Proofs and Programs, TYPES 2009, Aussois, France.
Sized Types in Agda: 28 November 2008. Agda Intensive Meeting (AIM 9), Sendai, Japan.
Normalization by Evaluation for System F: 26 November 2008. 15th International Conference on Logics for Programming, Artificial Intelligence, and Reasoning LPAR'08, Doha, Qatar.
Verifying a Semantic βη-Conversion Test for Martin-Löf Type Theory: 18 July 2008, Mathematics of Program Construction, Marseille, France.
Normalization by Evaluation for Martin-Löf Type Theory: 27 March 2008. International Workshop on Types for Proofs and Programs, TYPES 2008, Torino, Italy.
Type-Based Termination of Functional Programs: 11 October 2007. Kolloquium Programmiersprachen und Grundlagen der Programmierung, KPS'07, Timmendorfer Strand, Germany.
Normalization by Evaluation for Martin-Löf Type Theory with Typed Equality Judgements: 10 July 2007. Logic in Computer Science, LiCS 2007, Wroclaw, Poland.
Strong Normalization for Equi-(Co)inductive Types: 27 June 2007. International Conference on Typed Lambda Calculi and Applications, TLCA 2007, Paris, France.
Similar talk given at TYPES'07.
Syntactical Strong Normalization for Intersection Types with Term Rewriting Rules: 25 June 2007. International Workshop on Higher-Order Rewriting, HOR 2007, Paris, France.
Type-Based Termination: 9 March 2007. Copenhagen Programming Language Seminar, ITU, Copenhagen, Denmark.
More talks...

Recent Teaching

Lambda-Calculus (Lambda-Kalkül), Winter 2008/09, LMU, Munich.

concept and lecture (3 hours * 14 weeks)
tutorial section (1 hour * 14 weeks)
design and grading of assignments
oral exam

Python Tutorial (Python-Kompaktkurs), Winter 2008/09, LMU, Munich.

concept and lecture (4 hours * 5 days)
final projects for students

Functional Programming in SML (Programmierung und Modellierung (Info II) by Francois Bry, Summer 2008, LMU, Munich.

organization
adaptation of Plone EduComponents to SML handins
design and grading of assignments
tutorial section (2 hour * 14 weeks)

Computer-Aided Formal Reasoning (Rechnergestütztes Beweisen) with Martin Hofmann, Winter 2007/08, LMU, Munich.

lecture with Martin (each 2 hours * 14 weeks)
tutorial section (2 hours * 14 weeks)
design and grading of assignments

Compiler Construction Lab (Übersetzerbaupraktikum) with Hans-Wolfgang Loidl, Winter 2007/08, LMU, Munich.

lecture with Hans-Wolfgang (each 2 hours * 7 weeks)
implementation of a compiler for Mini-Java in Haskell
student supervision (2 hours * 14 weeks)

Type Systems (Typsysteme), with Martin Hofmann, Summer 2007, LMU, Munich.

concept and lecture with Martin (each 2 hours * 14 weeks)
tutorial section (2 hour * 14 weeks)
design and grading of assignments

Programming Language Theory, seminar, (Hauptseminar Programmiersprachentheorie) with Lennart Beringer and Hans-Wolfgang Loidl, Summer 2007, LMU, Munich.

concept and seminar (2 hours * 8 weeks)

More teaching...

Coauthors and Coworkers

Klaus Aehlig		colleague, coauthor
Thorsten Altenkirch		advisor (Sep 1997 - Apr 2000), coauthor
Marcin Benke		colleague, coauthor
Frédéric Blanqui		visit
Ana Bove		colleague, coauthor
Bor-Yuh Evan Chang		student, coauthor
Thierry Coquand		colleague, coauthor
Peter Dybjer		colleague, coauthor
Martin Hofmann		advisor (Oct 2001 - July 2006)
John Hughes		colleague, coauthor
Ralph Matthes		colleague, coauthor
Karl Mehltretter		student
Ulf Norell		colleague, coauthor
Frank Pfenning		advisor (May 2000 - June 2001), coauthor
Brigitte Pientka		colleague
Axel Rauschmayer		coauthor
Dulma Rodriguez		student
Colin Riba		visit
Carsten Schürmann		visit
Tarmo Uustalu		coauthor

Erdös Number

March 2000: 6. My Erdös Number is at most 6. Jan Johannsen found the following path: Paul Erdös - E. Rodney Canfield - Guo-Qiang Zhang - Thierry Coquand - Martin Hofmann - Thorsten Altenkirch - Andreas Abel

March 2001: 5. Due to a joint paper of Thierry Coquand and Thorsten Altenkirch (TLCA 2001) the upper bound for my Erdös number went down to 5.

December 2004: 4. A paper (TLCA 2005) with Thierry Coquand brings my Erdös Number down to at most 4.

Quotes

Computer science is no more about computers than astronomy is about telescopes. —Dijkstra

Technical skill is mastery of complexity, while creativity is mastery of simplicity. — Christopher Zeeman, mathematician

Ich fühl mich wie eine Turingmaschine ohne Band. —Steffen Jost (25.11.2002)

Weil der Computer nicht mehr ging, habe ich dann theoretisch gearbeitet. —Ralph Matthes (16.12.2003)

Andreas Abel, http://www.tcs.ifi.lmu.de/~abel
Last modified: Tue Jun 23 00:45:35 CEST 2009