Current Teaching:

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

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 (New.)

Andreas Abel, Thierry Coquand, Peter Dybjer (2008)
Mathematics of Program Construction, MPC'08. (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 (New.)

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)
Superseds CSL'06 conference paper.
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 (New.)

Andreas Abel (2007)
Superseds MPC'06 conference paper.
Science of Computer Programming, MPC'06 special issue. Submitted.
.pdf .ps.gz .dvi .bib

Mixed Inductive/Coinductive Types and Strong Normalization (New.)

Andreas Abel (2007)
Improves on TLCA'07 conference paper.
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 (New.)

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

Strong Normalization and Equi-(co)inductive Types

Andreas Abel (2007)
Typed Lambda Calculi and Application, TLCA'07, Paris, France.
.pdf .ps.gz .dvi .bib

Normalization by Evaluation for Martin-Löf Type Theory with One Universe

Andreas Abel, Klaus Aehlig, Peter Dybjer (2007)
23rd Conference on the Mathematical Foundations of Programming Semantics, MFPS XXIII.
.pdf .ps.gz .dvi .bib

Normalization for the Simply-Typed λ-calculus in Twelf

Andreas Abel (2007)
Superseds LFM'04 informal proceedings version.
Post-proceedings of Logical Frameworks and Metalanguages (LFM 04), IJCAR, Cork, Ireland, 2004.
.pdf .ps.gz .dvi .bib Twelf code: wn.tar.gz, weak normalization sn.tar.gz, strong normalization

Untyped Algorithmic Equality for Martin-Löf's Logical Framework with Surjective Pairs

Andreas Abel and Thierry Coquand (2006)
Superseds TLCA'05 conference paper.
Fundamenta Informaticae 77(4):345-395, TLCA'05 special issue.
.pdf .ps.gz .dvi .bib Haskell implementation: MLFSigma.lhs

Selected Recent Talks

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.

Normalization by Evaluation and Dependent Types

February 27, 2007. Protheo Seminar, LORIA, Nancy, France.

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

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)

[ Home | CV | Projects | Publications | Talks | Teaching | Sharing | Personal page ]

Andreas Abel, http://www.tcs.ifi.lmu.de/~abel Last modified: Tue Dec 16 14:35:01 CET 2008