Current Teaching
Programming Language Technology (DIT231GU, DAT151 replacing DAT150): Parsing, typechecking, interpretation, compilation to stack machines.
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
 ESSLLI 2016
1526 August 2016
 FSCD 2016
 1st International Conference on Formal Structures for Computation and Deduction,
2226 June 2016, Porto, Portugal
Abstract Submission: 29 January 2016
Paper Submission: 5 February 2016
Rebuttal: 21  23 March 2016
Notification: 6 April 2016
 CMCS 2016
 13th International Workshop on Coalgebraic Methods in Computer Science,
part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2016
23 April 2016, Eindhoven, The Netherlands
 ESOP 2016
 25th European Symposium on Programming,
part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2016
28 April 2016, Eindhoven, The Netherlands
Abstract Submission: 9 October 2015
Paper Submission: 16 October 2015
Author Rebuttal: 24 December 2015
 FLOPS 2016
 13th International Symposium on Functional and Logic Programming
36 March 2016, Kochi, Japan
 Past events and PC memberships...
Habilitation Thesis

Normalization by Evaluation: Dependent Types and Impredicativity

Andreas Abel (2013)
Habilitation thesis, Institut für Informatik, LudwigMaximiliansUniversität München, 2013
Date of habilitation: 31 May 2013.
Last update of thesis: 9 May 2015.

Wellfounded Recursion with Copatterns and Sized Types

Andreas Abel and Brigitte Pientka (2015)
Journal version of the ICFP'13 conference paper, to appear in the Journal of Functional Programming.
Draft: .pdf

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, 1821 May 2015.
2page abstract: .pdf

Wellfounded Recursion over Contextual Objects

Brigitte Pientka and Andreas Abel (2015)
13th International Conference on
Typed Lambda Calculi and Applications
(TLCA 2015),
13 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, 1719 November 2014, Singapore.
Short version:
.pdf
Sources (.tex/.lagda):
.zip
Agda code:
.html
Long version:
.pdf

Normalization by Evaluation in the Delay Monad:
An Extended Case Study for Coinduction via Copatterns and Sized Types

Andreas Abel and James Chapman (2014)
25th Nordic Workshop on Programming Theory, NWPT 2014, Halmstad, Sweden, 2931 October 2014.

A Categorical Perspective on Pattern Unification

Andrea Vezzosi and Andreas Abel (2014)
The 28th Workshop on Unification, UNIF 2014,
FLoC workshop, hosted by RTATLCA and IJCAR, Vienna Summer of Logic (VSL 2014),
13 July 2014, Vienna, Austria.
.pdf

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 1417, 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

Productive Infinite Objects via Copatterns

Andreas Abel
25th Nordic Workshop on Programming Theory, NWPT 2013, Tallinn, Estonia, 2022 November 2013.

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, 2527 September 2013.
.pdf
.bib
Long version:
.pdf
.bib
Version 20130329:
.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, 2325 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}

TypeBased Termination, Inflationary FixedPoints,
and Mixed InductiveCoinductive Types

Andreas Abel (2012)
Invited talk at the Workshop on Fixedpoints in Computer Science (FICS 2012), March 24, 2012, Tallinn, Estonia. Satellite workshop to ETAPS 2012.
.pdf
.ps.gz
.dvi
.bib

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):136, 2012.
.pdf
.ps.gz
.dvi
.bib

A Lambda Term Representation Based on Linear Ordered Logic

Andreas Abel and Nicolai Kraus (2011)
6th International Workshop on Logical Frameworks and Metalanguages: Theory and Practice, LFMTP 2011, Nijmegen, the Netherlands, August 26, 2011.
.pdf
.ps.gz
.dvi
.bib

HigherOrder 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, 13 June 2011, part of RDP'11.
LNCS 6690
© Springer.
.pdf
.ps.gz
.dvi
.bib
Extended version:
.pdf
.ps.gz
.dvi
Errata:
.txt

A Modular Type Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance

Andreas Abel, Thierry Coquand, and Miguel Pagano (200911)
Superseds the TLCA'09 conference paper.
Logical Methods in Computer Science 7(2:4) 2011, pp. 157.
.pdf
.ps.gz
.dvi
.bib
A note on etaconversion:
.pdf
Selected Recent Publications

Towards Normalization by Evaluation for the Calculus of Constructions

Andreas Abel (2009)
Tenth International Symposium on Functional and Logic Programming, FLOPS 2010,
1921 April 2010,
Sendai, Japan © Springer.
.pdf
.ps.gz
.dvi
.bib
Extended version:
.pdf
.ps.gz
.dvi

Weak βηNormalization and Normalization by Evaluation for System F

Andreas Abel (2008)
Logic for Programming, Artificial Intelligence, and Reasoning, LPAR'08, 2217 November 2008, Doha, Qatar. (45/153)
LNAI 5330 © Springer.
.pdf
.ps.gz
.dvi
.bib

Implementing a Normalizer Using Sized Heterogeneous Types

Andreas Abel (2008)
Journal of Functional Programming, MSFP'06 special issue.
.pdf
.ps.gz
.dvi
.bib

Semicontinuous Sized Types and Termination

Andreas Abel (2007)
Logical Methods in Computer Science, 2008, Volume 4, Issue 2, Paper 3. CSL'06 special issue.
LMCS online
.pdf
.ps.gz
.dvi
.bib

Mixed Inductive/Coinductive Types and Strong Normalization

Andreas Abel (2007)
The Fifth ASIAN Symposium on Programming Languages and Systems (APLAS 2007), Singapore.
.pdf
.ps.gz
.dvi
.bib

Normalization by Evaluation for MartinLöf Type Theory with Typed Equality Judgements

Andreas Abel, Thierry Coquand, Peter Dybjer (2007)
Logics in Computer Science, LICS 2007.
.pdf
.ps.gz
.dvi
.bib
Errata:
.pdf
.ps.gz
.dvi
 More publications...
Last update: 3 June 2015.
 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 HighLevel and LowLevel 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.
 Copatterns: Programming Infinite
Structures by Observations
 4 July 2013,
Theory Seminar,
Institute of Cybernetics,
Tallinn Technical University,
Tallinn, Estonia.
 Normalization by Evaluation: Dependent Types and Impredicativity
 31 May 2013, Department of Computer Science, LudwigMaximiliansUniversity Munich.
Habilitation talk.
 Copatterns: Programming Infinite
Structures by Observations
 23 Jan 2013, 40th ACM Symp. on Principles of Programming Languages,
POPL 2013,
Rome, Italy.
 TypeBased Termination,
Inﬂationary FixedPoints, and
Mixed InductiveCoinductive Types
 24 March 2012, Invited talk at the
Workshop on Fixed Points in Computer Science,
FICS 2012,
part of ETAPS 2012, Tallinn, Estonia.
 On Shape Irrelevance and Polymorphism in Type Theory
 9 September 2011,
Shonan Meeting Seminar 008, 14th Agda Implementor's Meeting (AIM XIV),
Shonan Village Center, near Tokyo, Japan.
 HigherOrder Pattern Unification for Dependently Typed Records
 1 June 2011,
TLCA 2011, 10th International Conference on
Typed Lambda Calculi and Applications, RDP 2011,
Novi Sad, Serbia.
 Irrelevance in Type Theory
 28 March 2011,
14th International Conference on
Foundations of Software Science and Computation Structures
FoSSaCS 2011,
part of European Joint Conferences on Theory and Practice of Software
ETAPS 2011.
 Algorithmic Equality for the Calculus of Constructions
 14 February 2011,
Two days on Models of the Calculus of Constructions, INRIA pi.r2, Pairs, France.
 Integrating Sized and Dependent Types
 15 July 2010, Workshop on Partiality and Recursion in Interactive Theorem Provers, PAR10,
Federated Logic Conference,
FLoC 2010,
Edinburgh, UK.
 Explicit substitutions for contextual type theory
 14 July 2010, Workshop on Logical Frameworks and Metalanguages: Theory and Practice,
LFMTP 2010,
Federated Logic Conference,
FLoC 2010,
Edinburgh, UK.
 Parametric Dependent Function Types
 9 July 2010, Workshop on Dependently Typed Programming,
DTP 2010,
Federated Logic Conference,
FLoC 2010,
Edinburgh, UK.
 Normalization by Evaluation for the βηCalculus of Constructions
 19 April 2010, 10th Int. Symp. on Functional and Logic Programming, FLOPS 2010, Sendai, Japan.
 On Irrelevance and Extraction in Type Theory
 2 Februar 2010. CoqDay on Equality and Termination, La Ciotat, Marseille, France.
 Remarks on Typed Equality for the Calculus of Constructions
 12 November 2009. Groupe de Travail Types and Semantics, INRIA PI.R2 and PPS, Paris, France.
 Normalization by Evaluation for
the Calculus of Constructions
 15 October 2009. PPS Lab, Universite Paris VII, France.
13 May 2009. International Workshop on Types for Proofs and Programs, TYPES 2009, Aussois, France.
 Extensions to Definitional Equality in Agda. Or: Making Agda See More
 15 September 2009. 10th Agda Implementors' Meeting, Gothenburg, Sweden.
 Type Structures and Normalization by Evaluation for
System F^{ω}
 8 September 2009. Computer Science Logic, CSL'09, Coimbra, Portugal.
 Extensional Normalization in the Logical Framework with Proof Irrelevant Equality
 15 August 2009. LiCSaffiliated Workshop on Normalization by Evaluation, NBE 2009, Los Angeles, USA.
 More talks...
More teaching...
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
 BorYuh Evan Chang
  student, coauthor
 James Chapman
  coauthor
 Thierry Coquand
  colleague, coauthor
 Peter Dybjer
  colleague, coauthor
 Nils Anders Danielsson
  colleague, coimplementor
 Hugo Herbelin
  colleague
 Martin Hofmann

 advisor (Oct 2001  July 2006)
 John Hughes
  colleague, coauthor
 Nicolai Kraus
  student, coauthor
 Ralph Matthes
  colleague, coauthor
 Karl Mehltretter
  student, coimplementor
 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

This is a nonexhaustive 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  GuoQiang Zhang 
Thierry Coquand  Andreas Abel
Google Scholar
gives me an Hindex of 16 and an i10 index of 30. (Retrieved 20150428.)
[ Home
 CV
 Projects
 Publications
 Talks
 Teaching
 Sharing
]
