|
| Home Email |
| Curriculum Vitæ |
| Professional Service |
| Projects |
| Publications |
| Talks |
| Teaching |
| Supervision |
|
|
| Friends |
Andreas Abel
| |||||||||||||||||||||||||||||||||||||
Current Teaching
- 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)
- Master theses: proposals more proposals presentation slots
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
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.)
|
Andreas Abel,
http://www.cse.chalmers.se/~abela
Last modified: 2019-01-22 17:51 |
|