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

PLPV'09

Programming Languages meet Program Verification, International Workshop

LFMTP'08

International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice
23 June 2008, Pittsburgh, PA, USA, colocated with LiCS'08
Abstract deadline: 14 April 2008
Paper deadline: 21 April 2008

LFMTP'07

International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice
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

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) To appear.
.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)
.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

Polarized Subtyping for Sized Types

Andreas Abel (2006)
Superseds CSR'06 conference paper.
Accepted for publication in MSCS special issue on subtyping. To appear in MSCS issue 18.6 or 19.1.
.pdf .ps.gz .dvi .bib

Selected Recent Talks

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.

Semantical Type-Checking Normalization by Evaluation Techniques and Abstract Values

December 19, 2006. TYPES Workshop Curry-Howard Implementation Techniques - Connecting Humans And Theorem provers CHIT-CHAT, Radboud University, Nijmegen, The Netherlands.
.pdf .ps.gz .dvi

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

December 7, 2006. Arbeitstreffen Bern-München, Department of Mathematics, University of Munich.
.pdf .ps.gz .dvi

Semi-continuous Sized Types and Termination

September 26, 2006. 15th Annual Conference of the EACSL, Computer Science Logic, CSL '06, Szeged, Hungary, September 25-29, 2006.
.pdf .ps.gz .dvi

A Polymorphic Lambda-Calculus with Sized Higher-Order Types

July 14, 2006. Thesis Defense. Department of Computer Science, University of Munich.

Towards Generic Programming with Sized Types

July 3, 2006. 8th International Conference on Mathematics of Program Construction, MPC '06, Kuressaare, Estonia, July 3-5, 2006.
.pdf .ps.gz .dvi

Implementing a Normalizer Using Sized Heterogeneous Types

July 2, 2006. Workshop on Mathematically Structured Functional Programming, MSFP 06, Kuressaare, Estonia.
.pdf .ps.gz .dvi

Polarized Subtyping for Sized Types

June 10, 2006. First International Computer Science Symposium in Russia (CSR 06), St. Petersburg, Russia, June 8-12, 2006
.pdf .ps.gz .dvi

Higher-Order Subtyping, Revisited Syntactic Completeness Proofs for Algorithmic Judgements

April 21, 2006. TYPES Workshop, Nottingham, UK.
.pdf .ps.gz .dvi

More talks...

Recent Teaching

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)

Lambda-Calculus (Lambda-Kalkül), Winter 2006/07, LMU, Munich.

• concept and lecture
• tutorial section
• design and grading of assignments
• oral exam

Efficient Algorithms (Effiziente Algorithmen), Summer 2006, LMU, Munich.

• design of assignments
• tutorial section
• grading of assignments

Computer-Aided Formal Reasoning (Rechnergestütztes Beweisen), Winter 2005/06, LMU, Munich.

• design of assignments
• tutorial section
• grading of assignments

Compiler Construction Lab (Übersetzerbaupraktikum) , Winter 2005/06, LMU, Munich.

• tutorial section

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: Mon Sep 8 21:13:10 CEST 2008