Andreas Abel


Senior Lecturer
 
Department of Computer Science and Engineering   e-mail:   abela chalmers se
Chalmers and Gothenburg University   Office:   4679
Rännvägen 6   Phone:   +46 31 772 1731
41296 Göteborg, SWEDEN   Fax:   +46 31 772 ????
     
 

 

Current Teaching

DIT725: Logic, Algorithms, and Data Structures in lecture hall Alfa in building Saga.

DATX02 DIT560: Kandidatarbete inom Data och Informationsteknik (Bachelor thesis supervision)

Some chalmers programs and course lists: CS master PhD courses

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

Events

FoSSaCS 2015
Foundations of Software Science and Computation Structures,
part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2015
11-19 April 2015, London, UK
10 October 2014: Abstract Submission
17 October 2014: Paper Submission
3-5 December 2014: Author Rebuttal
19 December 2014: Author Notification
16 January 2015: Camera-ready version
LFMTP 2014
Workshop on Logical Framework and Meta-languages: Theory and Practice, 17 July 2014
affiliated with CSL-LICS 2014 and IJCAR 2014, part of FLoC 2014, held as part of the Vienna Summer of Logic (VSL 2014), Vienna, Austria

Paper submission: 2 May 2014
Author notification: 3 June 2014
Workshop: 17 July 2014

DTP 2014
Workshop on Dependently Typed Programming, 13 July 2014
affiliated with CSL-LICS 2014, part of FLoC 2014, held as part of the Vienna Summer of Logic (VSL 2014), Vienna, Austria

Abstract submission: 2 May 2014
Author notification: 9 May 2014
Workshop: 13 July 2014

RTlcA 2014
Joint Conference on Rewriting Theory and Applications (RTA) and Typed Lambda Calculi and Applications (TLCA)
14-17 July, 2014, Vienna, Austria; part of FLoC 2014, part of The Vienna Summer of Logic (VSL 2014),
Workshop on Certification of High-Level and Low-Level Programs
07 - 11 July 2014, Paris, part of Institut Henri Poincaré Trimester
TYPES 2014
TYPES Meeting 2014 in Paris, 12-15 May 2014, in conjunction with the Institut Henri Poincaré Trimester on Semantics of proofs and certified mathematics
Past events and PC memberships...

Habilitation Thesis

Normalization by Evaluation: Dependent Types and Impredicativity
Andreas Abel (2013)
Habilitation thesis, Institut für Informatik, Ludwig-Maximilians-Universität München, 2013
Date of habilitation: 31 May 2013.

New Publications and Drafts

Normalization by Evaluation in the Delay Monad: A Case Study for Coinduction via Copatterns and Sized Types
Andreas Abel and James Chapman (2014)
Accepted for presentation at MSFP 2014.
To appear in EPTCS.
Proceedings version: .pdf Literate Agda code: .lagda
Preliminary version: .pdf Literate Agda code: .lagda
Structural Recursion over Contextual Objects
Brigitte Pientka, Sherry Shanshan Ruan, Andreas Abel (2014)
Draft.
Short version: .pdf Long version: .pdf
Productive Infinite Objects via Copatterns
Andreas Abel
25th Nordic Workshop on Programming Theory, NWPT 2013, Tallinn, Estonia, 20-22 November 2013.
Wellfounded Recursion with Copatterns: A Unified Approach to Termination and Productivity
Andreas Abel, Brigitte Pientka (2013)
The 18th ACM SIGPLAN International Conference on Functional Programming (ICFP 2013), Boston, MA, USA, 25-27 September 2013.
.pdf .bib Long version: .pdf .bib Version 2013-03-29: .pdf

© ACM, (2013). This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution.
The definitive version was published in PUBLICATION, {VOL##, ISS##, (DATE)} http://dx.doi.org/10.1145/2500365.2500591

Copatterns -- Programming Infinite Structures by Observations
Andreas Abel, Brigitte Pientka, David Thibodeau, Anton Setzer (2012)
Accepted for presentation at POPL 2013, Rome, Italy, 23-25 January 2013. (43/233)
© ACM, (2012). This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution.
The definitive version was published in PUBLICATION, {VOL##, ISS##, (DATE)} http://doi.acm.org/10.1145/{nnnnnn.nnnnnn}
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.
In Logical Methods in Computer Science, 8(1):1-36, 2012.
.pdf .ps.gz .dvi .bib
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 Errata: .txt
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

Selected Recent Publications

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
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, 2008, Volume 4, Issue 2, Paper 3. CSL'06 special issue.
LMCS online .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
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: 7 July 2013.
Copatterns: Programming Infinite Structures by Observations
4 July 2013, Institute of Cybernetics, Theory Seminar, Tallinn, Estonia.
Normalization by Evaluation: Dependent Types and Impredicativity
31 May 2013, Department of Computer Science, Ludwig-Maximilians-University Munich. Habilitation talk.
Copatterns: Programming Infinite Structures by Observations
23 Jan 2013, 40th ACM Symp. on Principles of Programming Languages, POPL 2013, Rome, Italy.
Type-Based Termination, Inflationary 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

More teaching...

Scientific Collaboration

Klaus Aehlig   colleague, coauthor
Thorsten Altenkirch    advisor (Sep 1997 - Apr 2000), coauthor
Matthias Benkard   student
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   coauthor
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
Anton Setzer   coauthor
Carsten Schürmann   host
David Thibodeau   student, coauthor
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.


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

Valid HTML 4.01! Andreas Abel, http://www.tcs.ifi.lmu.de/~abel
Valid CSS!