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

Current Teaching (Summer 2012):

Funktionale Programmierung
Formale Sprachen und Komplexität
Seminar Codierung und Information
TCS Oberseminar

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

Agda (sample: ParallelSubstitution.agda)
MiniAgda
Tutch

Events

FoSSaCS 2013: Foundations of Software Science and Computation Structures, part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2013
16-24 March 2013, Rome, Italy
7 October 2012: Abstract Submission
14 October 2012: Paper Submission
AIM XVI: 16th Agda Implementor's Meeting
3 - 9 October 2012 in Copenhagen, Denmark.
HOR 2012: 6th International Workshop on Higher-Order Rewriting
2 June 2012, Nagoya, Japan
Colocated with RTA 2012
ITP 2012: Third Conference on Interactive Theorem Proving
13-16 August 2012, New Jersey, USA
RTA 2012: 23rd International Conference on Rewriting Techniques and Applications
28 May - 2 June 2012, Nagoya, Japan
Past events and PC memberships...

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

New Publications and Drafts

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.
Submitted to Logical Methods in Computer Science.
.pdf .ps.gz .dvi
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
Irrelevance in Type Theory with a Heterogeneous Equality Judgement: Andreas Abel (2010)
Foundations of Software Science and Computation Structures (FoSSaCS 2011), part of ETAPS 2011, Saarbrücken, Germany, 26-28 March 2011.
LNCS 6009 © Springer.
.bib
MiniAgda: Integrating Sized and Dependent Types: Andreas Abel (2010)
Workshop on Partiality and Recursion in Interactive Theorem Provers (PAR 2010), 15 July 2010, Federated Logic Conference (FLoC 2010), Edinburgh, UK.
.pdf .ps.gz .dvi .bib
Explicit Substitutions for Contextual Type Theory: Andreas Abel and Brigitte Pientka (2010)
Logical Frameworks and Metalanguages: Theory and Practice (LFMTP 2010), 14 July 2010, Federated Logic Conference (FLoC 2010), Edinburgh, UK.
.pdf .ps.gz .dvi Extended version: .pdf .ps.gz .dvi
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
Typed Applicative Structures and Normalization by Evaluation for System F^ω: Andreas Abel (2009)
Computer Science Logic, Coimbra, Portugal, September 2009. (34/89)
LNCS 5771 © Springer.
.pdf .ps.gz .dvi .bib Full version: .pdf .ps.gz .dvi
Extensional Normalization in the Logical Framework with Proof Irrelevant Equality: Andreas Abel (2009)
Workshop on Normalization by Evaluation, affiliated to LiCS 2009, Los Angeles, 15 August 2009.
.pdf .ps.gz .dvi .bib

Selected Recent Publications

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, Volume 4, Issue 2, Paper 3. CSL'06 special issue.
LMCS online .pdf .ps.gz .dvi .bib
Type-Based Termination of Generic Programs: 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
More publications...

Selected Recent Talks

Last update: 8 May 2012.

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
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
Carsten Schürmann		host
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