Andreas Abel


Senior Lecturer orcid:   0000-0003-0420-4492
 
Programming Logic Group, Divison of Computing Science   e-mail:   andreas abel gu se
Department of Computer Science and Engineering       abela chalmers se
Gothenburg University / Chalmers   Office:   EDIT 6111
[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 Modal Dependent Type Theory, grant by Vetenskapsrådet 2020-2023.
  • Coinvestigator in project Syntax and Semantics of Univalent Type Theory (2018-2021), VR Grant 2017-04064.
  • Editor of the Theoretical Pearls column of the Journal of Functional Programming.
  • Member of steering committee of the conference series International Conference on Types for Proofs and Programs (TYPES).
  • Member 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.

ghc-8.10.5-x86_64-apple-darwin.tar.xz (157M).
Binary distribution of GHC 8.10.5 for macOS, built under Mojave 10.14.6 with XCode 11.3.
Works around GHC issue 19950.

ghc-8.10.6-x86_64-apple-darwin.tar.xz (ditto).

Events / PC Memberships

JFP Theoretical Pearls
Contact me or submit directly a theoretical pearl article to the Journal of Functional Programming.
ITP:
- Paper submission deadline: February 20, 2023
- PC review deadline: April 10, 2023
- Authors notification: April 24, 2023
PADL 2023
PADL 2023: The 25th International Symposium on Practical Aspects of Declarative Languages

15 Nov 2022: author notification
16-17 Jan 2023: conference (colocated with POPL)

POPL 2023
POPL 2023: The 50th ACM SIGPLAN Symposium on Principles of Programming Languages
LFMTP 2022
Logical Frameworks and Meta-Languages: Theory and Practice,
Affiliated with FSCD 2022, part of FLoC 2022, August 1, 2022, Haifa, Israel.
Past events and PC memberships...
Advice on scientific writing

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

Equivalence of Applicative Functors and Multifunctors
Andreas Abel (2024)
arXiv: 2401.14286 GitHub: andreasabel/applicative
Birkhoff's Completeness Theorem for Multi-Sorted Algebras Formalized in Agda
Andreas Abel (2021)
Proof document: .pdf arXiv Code: .agda
On Model-Theoretic Strong Normalization for Truth-Table Natural Deduction
Andreas Abel (2021)
Accepted for the post-proceedings of the 26th International Conference on Types for Proofs and Programs (TYPES 2020), Torino, Italy, 2-5 March 2020.
Final version: .pdf DOI: 10.4230/LIPIcs.TYPES.2020.1
Strong normalization for simply-typed combinatory algebra using Girard's reducibility candidates formalized in Agda
Andreas Abel (2020)
Proof document: .pdf Code: .agda
Extension to non-determinism: .pdf Code: .agda
A Unified View of Modalities in Type Systems
Andreas Abel and Jean-Philippe Bernardy (2020)
25th ACM SIGPLAN International Conference on Functional Programming, ICFP 2020, August 24-26, 2020 (virtual conference).
Proceedings of the ACM on Programming Languages, Volume 4(ICFP).
Final draft: .pdf Extended version: .pdf Errata: .md
Failure of Normalization in Impredicative Type Theory with Proof-Irrelevant Propositional Equality
Andreas Abel and Thierry Coquand (2020)
Logical Methods in Computer Science, June 30, 2020, Volume 16, Issue 2.
A counter example against the normalization conjecture in Benjamin Werner, On the strength of proof-irrelevant type theories, LMCS 2008.
LMCS Draft: .pdf arXiv: 1911.08174
Type-preserving compilation via dependently typed syntax
Andreas Abel (2020)
Abstract for the 26th International Conference on Types for Proofs and Programs (TYPES 2020), Torino, Italy, 2-5 March 2020. (Cancelled due to COVID-19.)
2-page abstract: .pdf slides: .pdf
Normalization by Evaluation for Call-by-Push-Value and Polarized Lambda-Calculus
Andreas Abel and Christian Sattler (2019).
In 21st International Symposium on Principles and Practice of Declarative Programming, PPDP'19, 7–9 October 2019, Porto, Portugal.
Colocated with The 3rd World Congress on Formal Methods, FM'19.
Final draft: .pdf arXiv: 1902.06097 Agda code: github:andreasabel/ipl
Cubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive Types
Andrea Vezzosi and Anders Mörtberg and Andreas Abel (2019)
24th ACM SIGPLAN International Conference on Functional Programming, ICFP 2019, August 19-21, 2019, Berlin, Germany. (39/119)
Received the Distinguished Paper Award (4 out of 39 accepted papers).
Proceedings of the ACM on Programming Languages, Volume 5(ICFP).
Final draft: .pdf
A Type Theory for Defining Logics and Proofs
Brigitte Pientka, David Thibodeau, Andreas Abel, Francisco Ferreira, Rebecca Zucchini (2019)
34th Annual ACM/IEEE Symposium on Logics in Computer Science, LICS 2019, 24–27 June 2019, Vancouver, Canada.
Final draft: .pdf
Cubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive Types
Andrea Vezzosi and Anders Mörtberg and Andreas Abel (2019)
25th International Conference on Types for Proofs and Programs (TYPES 2019), Oslo, Norway, 11-14 June 2019.
2-page abstract: .pdf
Normalization by Evaluation for Call-By-Push-Value
Andreas Abel and Christian Sattler (2019)
25th International Conference on Types for Proofs and Programs (TYPES 2019), Oslo, Norway, 11-14 June 2019.
2-page abstract: .pdf
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

Selected Recent Publications

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
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 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: 21 June 2022. See also full talk list.
Modalities and Erasure in a Dependently Typed Language
21 June 2022, 28th International Conference on Types for Proofs and Programs, Nantes, France.
Agda Tutorial in Advanced Functional Programming course
28 February 2022, Chalmers, Gothenburg
Agda sources (.zip): start finish
On Model-Theoretic Strong Normalization for Truth-Table Natural Deduction
7 June 2021, 27th International Conference on Types for Proofs and Programs, online.
Agda Tutorial in Advanced Functional Programming course
22 February 2021, Chalmers, Gothenburg
Agda sources (.zip): start finish

7 June 2021, VU 183.653, TU Wien
Agda sources (.zip): start finish

Agda Tutorial in Advanced Functional Programming course
17 February 2020, Chalmers, Gothenburg
Agda sources (.zip): start finish
Type-preserving compilation via dependently typed syntax in Agda
16 January 2020, IFIP 1.3 Meeting, Massa Marittima, Italy.
Similar talk planned for TYPES 2020, Torino, Italy, 2-5 March 2020. (Cancelled due to COVID-19.)
Normalization by Evaluation for Call-By-Push-Value
13 June 2019, 25th International Conference on Types for Proofs and Programs, TYPES 2019, Oslo, Norway.
Similar talk given 28 June 2019 in the TCS Oberseminar, LMU München, DE.
Informal talk given 22 May 2019 in the Programming Logic seminar, Chalmers.
How to Represent It in Agda
13 March 2019, 29th Agda Implementors' Meeting, AIM XXIX, Ochanomizu University, Tokyo, Japan
slides Agda code (stub)
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
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
Christian Sattler   colleague, coauthor
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 | Software ]

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