Andreas Abel

Visiting Researcher (on leave from Assistant Professorship at LMU Munich)

Laboratoire PPS (Preuves, Programmes et Systèmes)	e-mail:	abel@informatik.uni-muenchen.de
INRIA PI.R2 Project	Office:	IT-5.37
23, avenue d'Italie	Phone:	+33.1.39.63.59.41
F-75013 Paris, France	Fax:	(ATTN: Abel) +33.1.39.63.79.88

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

A Modular Type Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance (New.): Andreas Abel, Thierry Coquand, and Miguel Pagano (2009)
Long version of TLCA'09 conference paper. Submitted.
.pdf .ps.gz .dvi .bib
Towards Normalization by Evaluation for the Calculus of Constructions (New.): Andreas Abel (2009)
Tenth International Symposium on Functional and Logic Programming, FLOPS 2010, 19-21 April 2010, Sendai, Japan
.pdf .ps.gz .dvi .bib Extended version: .pdf .ps.gz .dvi
Typed Applicative Structures and Normalization by Evaluation for System F^ω (New.): 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 (New.): Andreas Abel (2009)
Workshop on Normalization by Evaluation, affiliated to LiCS 2009, Los Angeles, 15 August 2009.
.pdf .ps.gz .dvi .bib
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. 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

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

Advanced Functional Programming (Funktionale Programmierung)
Lambda-Calculus (Lambda-Kalkül)
Python Tutorial (Python-Kompaktkurs)
Type Systems (Typsysteme)
Computer-Aided Formal Reasoning (Rechnergestütztes Beweisen)
Compiler Construction Lab (Übersetzerbaupraktikum)

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

My Erdös Number is at most 4: Paul Erdös - E. Rodney Canfield - Guo-Qiang Zhang - Thierry Coquand - Andreas Abel

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