Andreas Abel


Senior Lecturer アンドレアス アーベル
 
Department of Computer Science and Engineering   e-mail:   abela chalmers se
Chalmers and Gothenburg University   Office:   6479
Rännvägen 6b   Phone:   +46 31 772 1731
41296 Göteborg, SWEDEN  
     
 

 

Current Teaching

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

More teaching...

Some chalmers programs and course lists: CS master 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

Software

Events

SOFSEM-FOCS 2017
43nd International Conference on Current Trends in Theory and Practice of Computer Science
Foundations of Computer Science track
January 2017, CZ/SK

Abstract deadline: 1 July 2016 CEST
Paper deadline: 8 July 2016 CEST

APLAS 2016
14th Asian Symposium on Programming Languages and Systems
21-23 November 2016, Hanoi, Vietnam

Abstract deadline: 12 June 2016
Paper deadline: 17 June 2016
Notification: August 15, 2016
Final version: August 31, 2016

HaL 2016
Haskell in Leizig 2016 (11th Workshop)
Colocated with the Workshop on Functional and (Constraint) Logic Programming (WFLP) and the Workshop on (Constraint) Logic Programming (WLP)
Forming the Leipzig Week of Declarative Programming (L-DEC)
12-16 September 2016, Leizig, Germany

Abstract deadline: 1 July 2016 (tentative)

ESSLLI 2016
28th European Summer School in Logic, Language and Information
Bolzano-Bozen, South Tyrol, Italy, 15-26 August 2016
Course Type Theory. A Constructive Foundation for Logics and Computer Science in the first week (15-19 August)

Early registration until 31 May 2016
Late registration until 31 July 2016

FSCD 2016
1st International Conference on Formal Structures for Computation and Deduction,
22-26 June 2016, Porto, Portugal

Notification: 6 April 2016

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.
Last update of thesis: 9 May 2015.

New Publications and Drafts

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
Sprinkles of extensionality for your vanilla 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
Interactive Programming in Agda - Objects and Graphical User Interfaces
Andreas Abel, Stephan Adelsberger, and Anton Setzer (2016)
Draft: .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   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.
.pdf .ps.gz .dvi .bib Extended version: .pdf .ps.gz .dvi Errata: .txt
More publications...

Selected Recent Talks

Last update: 22 April 2016.
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
Agda Tutorial in Advanced Functional Programming course
24 February 2016, Chalmers, Gothenburg
Agda sources: .zip
Coinduction in Agda Using Copatterns and Sized Types
15 December 2015, Workshop on Advances in Programming Languages and Systems (APLS 2015), Frankfurt a.M., Germany.
Agda code
10 Years of Agda2
3 June 2015, 21st Agda Implementor's Meeting (AIM XXI), Chalmers, Gothenburg, Sweden.
Logic and Language, Proposition and Types, Proofs and Computation
21 April 2015, Introduction to Programming Logic research for 1st year students, Seminarier i Data och IT Chalmers, Gothenburg, Sweden.
Strong Normalization for Guarded Recursive Types
18 December 2014, Theory Seminar, Institute of Cybernetics, Tallinn Technical University, Tallinn, Estonia. ITU, Copenhagen, Denmark.
Strong Normalization for Guarded Types
20 August 2014, Programming Logics and Semantics Group, ITU, Copenhagen, Denmark.
Coinduction in Agda Using Copatterns and Sized Types
7 July 2014, Workshop on Certification of High-Level and Low-Level Programs, part of the Institut Henri Poincaré thematic trimester Semantics of proofs and certified mathematics, Paris, France.
Coinduction in Agda Using Copatterns and Sized Types
15 May 2014, Types for Proofs and Programs ( TYPES 2014), part of the Institut Henri Poincaré thematic trimester Semantics of proofs and certified mathematics, Paris, France.
Wellfounded Recursion with Copatterns
26 September 2013, The 18th ACM SIGPLAN International Conference on Functional Programming (ICFP 2013), Hilton Logan Airport, Boston, MA, USA.
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
Thierry Coquand   colleague, coauthor
Peter Dybjer   colleague, coauthor
Nils Anders Danielsson   colleague, coimplementor
Hugo Herbelin   colleague, host
Martin Hofmann    advisor (Oct 2001 - July 2006)
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
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
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 16 and an i10 index of 30. (Retrieved 2015-04-28.)


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

Valid HTML 4.01! Andreas Abel, http://www.cse.chalmers.se/~abela
Last modified: 2016-04-22 09:54>
Valid CSS!