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

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, Rewriting, and Termination
  • Type Checking, Unification, and Compiling Dependent Types
  • Linear and Modal Typing and Coeffects
  • Constructive Logic and Logical Frameworks
  • Theorem Proving and Program Verification

Current Projects and Roles

  • Principal investigator of project Termination Certificates for Dependently-Typed Programs and Proofs via Refinement Types, VR Grant 2014-04864.
  • Coinvestigator in project Syntax and Semantics of Univalent Type Theory, VR Grant 2017-04064.
  • Editor of the Theoretical Pearls column of the Journal of Functional Programming.
  • Member of core group and managing committee of EU Coordination Action CA15123 EUTYPESTypes for programming and verification. Impact brochure.
  • Member of steering committee of the conference series International Conference on Types for Proofs and Programs (TYPES).
  • Observer in the IFIP WG 1.3 on Foundations of System Specification.
  • Senior developer of the dependently-typed language Agda.
  • Maintainer of the Backus Naur Form Compiler (BNFC).

Software

  Agda   A dependently-typed functional programming language and proof assistant.
  BNFC   The Backus Naur Form Compiler: A front-end to parser generators.
  MiniAgda   Agda-like toy language for researching dependent typing and subtyping.
  Tutch   The tutorial proof checker: Educational language for reasoning in natural deduction.
  java-adt   Tool: Algebraic data type generator for JAVA.

Events / PC Memberships

JFP Theoretical Pearls
Contact me or submit directly a theoretical pearl article to the Journal of Functional Programming.
LiCS 2020
34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)

6 January 2020 (tentative): abstract submission
10 January 2020 (tentative): paper submission
16-20 March 2020 (tentative): rebuttal
10 April 2020 (tentative): notification
late June or July 2020 (tentative): conference

ITP 2019
10th conference on Interactive Theorem Proving, 8-13 September 2019, Portland, OR, USA

31 March 2019: paper submission
31 May 2019: author notification
1 July 2019: camera-ready paper

TYPES 2019
25th International Conference on Types for Proofs and Programs, 11-14 June 2019, Oslo, Norway

4 March 2019: submission of 2 pp abstract
15 April 2019: notification
6 May 2019: camera-ready version
September 2019 (tentative): post-proceedings submission

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, Ludwig-Maximilians-Universität München, 2013
Date of habilitation: 31 May 2013.
Last update of thesis: 9 May 2015.

New Publications and Drafts

Lifting linear laws: On the preservation of linear equational laws under the pointwise lifting to sets
A rediscovery of a universal algebra law for power algebras (aka complex algebras).
Presented in the Chalmers ProgLog Seminar on 21 November 2018.
POPLMark Reloaded: Mechanizing Proofs by Logical Relations
Andreas Abel, Guillaume Allais, Aliya Hameer, Brigitte Pientka, Alberto Momigliano, Steven Schäfer and Kathrin Stark (2018).
Draft, submitted to the Journal of Functional Programming.
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 ACM SIGPLAN Notices - ICFP '13, Volume 48, Issue 9, September 2013, DOI 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, ACM SIGPLAN Notices - POPL '13, Volume 48 Issue 1, January 2013, DOI 10.1145/2429069.2429075.

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: 22 January 2019. See also full talk list.
Correct-By-Construction Programming in Agda
14 January 2019, Tutorial at the 46th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2019), Hotel Cascais Miragem, Lisbon, Portugal
On Proof-Relevant Relations and Evidence-Aware Programming
11 January 2019, TCS Oberseminar, LMU München, DE
Lifting linear laws: On the preservation of linear equational laws under the pointwise lifting to sets
21 November 2018, Programming Logic seminar, Chalmers, Gothenburg, Sweden
Handout: .pdf
Normalization by Evaluation for Intuitionistic Propositional Logic
19 July 2018, Initial Types Club, Chalmers, Gothenburg, Sweden
PDF Handout: local github Agda code: html github
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 2005 - Sep 2013), colecturer
John Hughes   colleague, coauthor
Steffen Jost   colleague, colecturer
Ekatarina Komendantskaya   host, coapplicant
Nicolai Kraus   student, coauthor
Hans-Wolfgang Loidl   colleague, colecturer
Ralph Matthes   colleague, coauthor
Karl Mehltretter   student, coimplementor
Bassel Mannaa   coauthor
Francesco Mazzoli   student, coimplementor
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
Ulrich Schöpp   colleague, colecturer
Carsten Schürmann   host
Anton Setzer   coauthor
Christoph-Simon Senjak  student
Sandro Stucki   colleague, colecturer
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 20 and an i10 index of 42. (Retrieved 2019-01-22.)


[ Home | CV | Professional Service | Projects | Publications | Talks | Teaching | Supervision ]

Valid HTML 4.01! Andreas Abel, http://www.cse.chalmers.se/~abela
Last modified: 2019-01-22 17:51
Valid CSS!