Andreas Abel


Senior Lecturer orcid:   0000-0003-0420-4492
 
Programming Logic Group, Divison of Computer Science   e-mail:   andreas abel gu se
Department of Computer Science and Engineering       abela chalmers se
Gothenburg University / Chalmers   Office:   EDIT 6117
[Postal address]   Phone:   +46 31 772 1731
     
 

 

Current Teaching

Master thesis topics (Presentation slots)

Programming Language Technology (DIT231, DAT151): Parsing, type-checking, interpretation, compilation to stack machines.

Programming Logic Seminar (research level; 2006-2009 2010-2015)

Initial Types Club (Master/PhD level)

Previous teaching...

Some Chalmers programs and course lists: CSALL/MPALG master (algorithms, languages, logic) PhD courses

Research Interests

  • Verified Software Development and Dependently Typed Programming
  • Type Theory, Functional Programming, and Termination
  • Type Checking, Unification, and Compiling Dependent Types
  • Theorem Proving and Program Verification
Current projects:
  • Termination Certificates for Dependently-Typed Programs and Proofs via Refinement Types, VR Grant 2014-4864
  • Types for programming and verification, EU Coordination Action CA15123 EUTYPES   [Impact brochure]

Software

Events / PC Memberships

POPL 2019
The 46th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Lisbon, Portugal, January 2019

11 July 2019: paper submission
17-20 Sep 2019: rebuttal

PARIS 2018
Workshop Programming And Reasoning on Infinite Structures, affiliated to FSCD 2018, part of FLoC, Oxford, UK, 7/8 July 2018

7/8 July 2018: workshop

MSFP 2018
Seventh Workshop on Mathematically Structured Functional Programming (MSFP 2018), affiliated to FSCD 2018, part of FLoC, Oxford, UK, 8 July 2018
Both full papers (15 pages) and talk abstracts (2 pages) are welcome!

14 June 2018: camera-ready paper
8 July 2018: workshop

ITP 2018
9th conference on Interactive Theorem Proving, 9-12 July 2018, Oxford, UK
part of the Federated Logic Conference, FLoC 2018

TYPES 2018
24th International Conference on Types for Proofs and Programs, TYPES 2018, Braga, Portugal, 18-21 June 2018
Past events and PC memberships...

Habilitation Thesis

Normalization by Evaluation: Dependent Types and Impredicativity
Andreas Abel (2013)
Habilitation thesis, Fakultät für Mathematik, Informatik, und Statistik (MIST), Ludwig-Maximilians-Universität München, 2013
Date of habilitation: 31 May 2013.
Last update of thesis: 9 May 2015.

New Publications and Drafts

Elaborating dependent (co)pattern matching
Jesper Cockx and Andreas Abel (2018)
23nd ACM SIGPLAN International Conference on Functional Programming, ICFP 2018, September 23–29, 2018, St. Louis, Missouri, US.
Proceedings of the ACM on Programming Languages, Volume 3(ICFP).
Long version: .pdf
Resourceful Dependent Types
Andreas Abel (2018)
Abstract submitted to the 24th International Conference on Types for Proofs and Programs (TYPES 2018), Braga, Portugal, 18-21 June 2018.
2-page abstract: .pdf
Decidability of Conversion for Type Theory in Type Theory
Andreas Abel, Joakim Öhman, and Andrea Vezzosi (2017)
Proceedings of the ACM on Programming Languages, Volume 2(POPL), January 8–13, 2018, Los Angeles, CA, USA
Final version: .pdf Agda code: html github DOI: 10.1145/3158111
Normalization by Evaluation for Sized Dependent Types
Andreas Abel, Andrea Vezzosi, and Theo Winterhalter (2017)
Proceedings of the ACM on Programming Languages, Volume 1(ICFP), September 3–9, 2017, Oxford, UK
22nd ACM SIGPLAN International Conference on Functional Programming, ICFP 2017. (44/126)
Long version: .pdf Artifact: Sit (protoypical type checker)
Normalization by Evaluation for Sized Dependent Types
Andreas Abel, Andrea Vezzosi, and Theo Winterhalter (2017)
Abstract for the 23nd International Conference on Types for Proofs and Programs (TYPES 2017), Budapest, Hungary, 29 May - 1 June 2017.
2-page abstract: .pdf
Equational Reasoning about Formal Languages in Coalgebraic Style
Andreas Abel (2016)
Submitted to the CMCS 2016 special issue.
Draft: .pdf
Interactive Programming in Agda -- Objects and Graphical User Interfaces
Andreas Abel, Stephan Adelsberger, and Anton Setzer (2016)
Journal of Functional Programming, volume 27, January 2017, DTP 2016 special issue.
Published version: JFP, 6 Feb 2017 Author's version: .pdf
Normalization by Evaluation in the Delay Monad
Andreas Abel and James Chapman (2016)
Abstract for the 22nd International Conference on Types for Proofs and Programs (TYPES 2016), Novi Sad, Serbia, 23-26 May 2016.
2-page abstract: .pdf
An Extension of Martin-Löf Type Theory with Sized Types
Andreas Abel and Theo Winterhalter (2016)
Abstract for the 22nd International Conference on Types for Proofs and Programs (TYPES 2016), Novi Sad, Serbia, 23-26 May 2016.
2-page abstract: .pdf
On Decidability of Conversion in Type Theory
Andreas Abel, Thierry Coquand, and Bassel Mannaa (2016)
Abstract for the 22nd International Conference on Types for Proofs and Programs (TYPES 2016), Novi Sad, Serbia, 23-26 May 2016.
2-page abstract: .pdf
Sprinkles of Extensionality for Your Vanilla Type Theory
Jesper Cockx and Andreas Abel (2016)
Abstract for the 22nd International Conference on Types for Proofs and Programs (TYPES 2016), Novi Sad, Serbia, 23-26 May 2016.
2-page abstract: .pdf
Compositional Coinduction with Sized Types
Andreas Abel (2016)
Abstract for the invited talk at the 13th IFIP WG 1.3 International Workshop on Coalgebraic Methods in Computer Science (CMCS 2016), Eindhoven, the Netherlands, 2-3 April 2016.
6-page abstract: .pdf
Wellfounded Recursion with Copatterns and Sized Types
Andreas Abel and Brigitte Pientka (2015)
Journal version of the ICFP'13 conference paper, Journal of Functional Programming, 2016, vol. 26, Copyright © Cambridge University Press 2016.
Author's version: .pdf   Agda code: html .tgz   Final version: .bib http://dx.doi.org/10.1017/S0956796816000022
The Next 700 Modal Type Assignment Systems
Andreas Abel (2015)
Abstract for the 21st International Conference on Types for Proofs and Programs (TYPES 2015), Tallinn, Estonia, 18-21 May 2015.
2-page abstract: .pdf
Well-founded Recursion over Contextual Objects
Brigitte Pientka and Andreas Abel (2015)
13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015), 1-3 July 2015, Warsaw, Poland.
Short version: .pdf Long version (draft): .pdf
A Formalized Proof of Strong Normalization for Guarded Recursive Types
Andreas Abel and Andrea Vezzosi (2014)
12th Asian Symposium on Programming Languages and Systems, APLAS 2014, 17-19 November 2014, Singapore.
Short version: .pdf Sources (.tex/.lagda): .zip Agda code: .html Long version: .pdf

Selected Recent Publications

Unnesting of Copatterns
Anton Setzer, Andreas Abel, Brigitte Pientka, and David Thibodeau (2014)
Joint 25th International Conference on Rewriting Techniques and Applications and
12th International Conference on Typed Lambda Calculi and Applications
(RTATLCA 2014), July 14-17, 2014, Vienna, Austria
Final draft: .pdf
Normalization by Evaluation in the Delay Monad: A Case Study for Coinduction via Copatterns and Sized Types
Andreas Abel and James Chapman (2014)
5th Workshop on Mathematically Structured Functional Programming (MSFP 2014), 12 April 2015, Grenoble, France.
Published in EPTCS 153.
Proceedings version: .pdf Literate Agda code: .lagda Preliminary version: .pdf Literate Agda code: .lagda
Wellfounded Recursion with Copatterns: A Unified Approach to Termination and Productivity
Andreas Abel and 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}
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
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.
Final draft: .pdf .bib   Extended version (revised July 2017): .pdf   Errata (fixed in extended version): .txt
More publications...

Selected Recent Talks

Last update: 3 July 2018. See also full talk list.
Resourceful Dependent Types
20 June 2018, 24th International Conference on Types for Proofs and Programs, TYPES 2018, Braga, Portugal
On Typed Lambda Definability and Normalization By Evaluation
7 June 2018, 27th Agda Implementors' Meeting (AIM XXVII), Chalmers Teknikparken, Gothenburg, Sweden
Agda code: listing github
On the Syntax and Semantics of Quantitative Type Theory
19 April 2018, Workshop on Mixed Inductive-Coinductive Reasoning, Institute for Computing and Information Sciences, Radboud University, Nijmegen, The Netherlands
Compositional Coinduction with Sized Types
16 February 2018, Functional Programming Seminar, School of Computer Science, University of St Andrews, Scotland, UK
What is a monotone dependently typed function?
9 January 2018, Winter Meeting 2018 of the Division of Functional Programming, Salt & Sill, Tjörn, Sweden
Normalization by Evaluation for Sized Dependent Types
6 September 2017, 22nd ACM SIGPLAN International Conference on Functional Programming, ICFP 2017, Oxford, UK
Formal Languages, Coinductively Formalized
Invited talk, 19 July 2017, Workshop on Termination and Circular Proofs, Department of Mathematics (LAMA), Université Savoie Mont Blanc, Chambery, France
Agda Tutorial at Big Proof 2017
30 June 2017, Issac Newton Institute, Cambridge, UK

Tutorial material for live coding: Tutorial.zip Individual files: Tutorial.agda Prelude.agda TreeSortOrd.agda Copatterns.agda Rewriting.agda Cubical.agda
Normalization by Evaluation for Sized Dependent Types
30 May 2017, 23nd International Conference on Types for Proofs and Programs TYPES 2017, Budapest, Hungary
Formal Languages, Coinductively Formalized
Seminar on the occasion of Jesper Cockx' non-public defense, Department of Computer Science, KU Leuven, Belgium, 17 May 2017
Programming Language Technology: Putting Formal Languages to Work
11 May 2017, guest lecture in class Finite Automata Theory and Formal Languages TMV027/DIT321, Chalmers and Gothenburg University, Sweden.
Slides: .pdf Code: .zip
Translating between Agda and Dedukti
Universality of Proofs (Dagstuhl seminar 16421)
18 October 2016, Schloss Dagstuhl, Wadern, Germany
Type Theory. A Constructive Foundation for Logics and Computer Science
Introductory course (5 × 90 min)
28th European Summer School in Logic, Language and Information (ESSLLI 2016)
Bolzano-Bozen, South Tyrol, Italy, 15-26 August 2016
How to Keep Your Neighbors in Order
An Agda tutorial using Conor McBride's beautiful representation of binary search trees
30 June 2016, guest lecture in Computer Aided Formal Reasoning, class by Gordon Cichon and Martin Hofmann, Institut für Informatik, Ludwig-Maximilians-Universität München
Agda code: .html .zip
Normalization by Evaluation in the Delay Monad
24 May 2016, 22nd International Conference on Types for Proofs and Programs TYPES 2016, Novi Sad, Serbia
Formal Languages, Coinductively Formalized
19 April 2016, Departmental Seminar CISeminar, Computer and Information Sciences, Strathclyde University, Glasgow, Scotland, UK.
Compositional Coinduction with Sized Types
13th IFIP WG 1.3 International Workshop on Coalgebraic Methods in Computer Science (CMCS 2016)
Part of ETAPS 2016
3 April 2016, Eindhoven, the Netherlands
Slides: .pdf Agda code: .zip Agda code pretty: unsized sized
Coinduction in Agda via Copatterns and Sized Types
Language Based Verification Tools for Functional Programs (Dagstuhl seminar 16131)
30 March 2016, Schloss Dagstuhl, Wadern, Germany
Slides: .pdf Agda code: .zip Agda code pretty: unsized sized
Agda Tutorial at FLOPS 2016
13th International Symposium of Functional and Logic Programming (FLOPS 2016)
6 March 2016, Kochi, Japan
Slides: .pdf Start: .agda Solution: .agda Solution pretty: .html
Interactive Programs and Objects, Functionally -- Via Coinduction with Copatterns and Sized Types in Agda
2 March 2016, Dept. of Communications and Computer Engineering, Graduate School of Informatics, Kyoto University, Japan
Agda code: .zip   Agda code pretty: .html
More talks...

Scientific Collaboration

Stephan Adelsberger   visitor, coauthor
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
Jesper Cockx   coimplementor, coauthor, postdoc
Youyou Cong   student
Thierry Coquand   colleague, coauthor
Nils Anders Danielsson   colleague, coimplementor
Dominique Devriese   host, coauthor
Peter Dybjer   colleague, coauthor, boss (Sep 2013 -)
Hugo Herbelin   colleague, host
Martin Hofmann   advisor (Oct 2001 - July 2006), boss (Oct 2015 - Sep 2013)
John Hughes   colleague, coauthor
Nicolai Kraus   student, coauthor
Ralph Matthes   colleague, coauthor
Karl Mehltretter   student, coimplementor
Bassel Mannaa   coauthor
Francesco Mazzoli   student
Keiko Nakata   host
Ulf Norell   colleague, coauthor, coimplementor
Andreas Nuyts   visitor
Joakim Öhman   student, coauthor
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
Andrea Vezzosi   student, coauthor
Phil Wadler   coauthor
Theo Winterhalter   student, coauthor

This is a non-exhaustive list of people with whom I collaborated over a longer time to produce scientific results.

For students, see also Supervision...

Bibliometrics

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

Google Scholar gives me an H-index of 19 and an i10 index of 40. (Retrieved 2018-04-30.)


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

Valid HTML 4.01! Andreas Abel, http://www.cse.chalmers.se/~abela
Last modified: 2018-07-10 16:04>
Valid CSS!