Overview
(* = hot!, highly recommended read).
Journal Articles
Refereed Conference Proceedings
Refereed Workshop Proceedings
Refereed Workshop Abstracts
Theses
Technical Reports and Manuscripts (unrefereed)
Publications and Preprints

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

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)
Accepted for presentation at MSFP 2014.
To appear in EPTCS.
Proceedings version:
.pdf
Literate Agda code:
.lagda
Preliminary version:
.pdf
Literate Agda code:
.lagda
2013

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

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.

Copatterns  Programming Infinite Structures by Observations

Andreas Abel, Brigitte Pientka, David Thibodeau, Anton Setzer (2012)
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}
2012

TypeBased Termination, Inflationary FixedPoints,
and Mixed InductiveCoinductive Types

Andreas Abel (2012)
Invited talk at the
8th Workshop on Fixed Points in Computer Science
(FICS 2012),
March 24, 2012, Tallinn, Estonia. Satellite workshop to ETAPS 2012.
Appeared in Electronic Proceedings in Theoretical Computer Science,
EPTCS 77,
2012, pp. 111. DOI: 10.4204/EPTCS.77.1
.pdf
.ps.gz
.dvi
.bib

On Irrelevance and Algorithmic Equality in
Predicative Type Theory

Andreas Abel and Gabriel Scherer (2011/12)
Superseds the FoSSaCS'11 conference paper.
In
Logical Methods in Computer Science, 8(1):136, 2012.
.pdf
.ps.gz
.dvi
.bib
2011

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.
EPTCS 71, 2011, pp. 113.
DOI: 10.4204/EPTCS.71.1
.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

Irrelevance in Type Theory with a Heterogeneous Equality Judgement

Andreas Abel (2010)
Foundations of Software Science and Computation Structures (FoSSaCS 2011),
part of ETAPS 2011, Saarbrücken, Germany, 2628 March 2011.
LNCS 6009
© Springer.
.bib
Erratum:
.pdf
2010

MiniAgda: Integrating Sized and Dependent Types

Andreas Abel (2010)
Workshop on Partiality and Recursion in Interactive Theorem Provers (PAR 2010), 15 July 2010, Federated Logic Conference (FLoC 2010), Edinburgh, UK.
.pdf
.ps.gz
.dvi
.bib

Explicit Substitutions for Contextual Type Theory

Andreas Abel and Brigitte Pientka (2010)
Logical Frameworks and Metalanguages: Theory and Practice (LFMTP 2010), 14 July 2010, Federated Logic Conference (FLoC 2010), Edinburgh, UK.
.pdf
.ps.gz
.dvi
Extended version:
.pdf
.ps.gz
.dvi

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
2009

Typed Applicative Structures and Normalization by Evaluation for System F^{ω}

Andreas Abel (2009)
Computer Science Logic, Coimbra, Portugal, September 2009. (34/89)
LNCS 5771 © Springer.
.pdf
.ps.gz
.dvi
.bib
Full version:
.pdf
.ps.gz
.dvi

Extensional Normalization in the Logical Framework with Proof Irrelevant Equality

Andreas Abel (2009)
Workshop on Normalization by Evaluation, affiliated to LiCS 2009, Los Angeles, 15 August 2009.
.pdf
.ps.gz
.dvi
.bib

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

Andreas Abel, Thierry Coquand, and Miguel Pagano (2009)
9th International Conference on Typed Lambda Calculi and Applications, TLCA'09, 13 July 2009, Brasilia, Brazil.
LNCS 5608 © Springer.
.pdf
.ps.gz
.dvi
.bib
Full version:
.pdf
.ps.gz
.dvi

Implementing a Normalizer Using Sized Heterogeneous Types

Andreas Abel (2008)
Superseds MSFP'06 workshop paper.
Journal of Functional Programming 2009, Issue 34, MSFP'06 special issue. © Cambridge University Press.
.pdf
.ps.gz
.dvi
.bib

TypeBased Termination of Generic Programs

Andreas Abel (2007)
Superseds MPC'06 conference paper.
Science of Computer Programming 74 (2009), pp. 550567, MPC'06 special issue.
© Elsevier.
EE
.pdf
.ps.gz
.dvi
.bib
2008

Polarized Subtyping for Sized Types

Andreas Abel (2006)
Superseds CSR'06 conference paper.
Mathematical Structures in Computer Science, vol. 18, pp. 797822, special issue on subtyping. © Cambridge University Press.
.pdf
.ps.gz
.dvi
.bib

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

Syntactic Metatheory of HigherOrder Subtyping

Andreas Abel and Dulma Rodriguez (2008)
Computer Science Logic, 22nd International Workshop, CSL
2008, 17th Annual Conference of the EACSL, Bertinoro, Italy,
September 1619, 2008.
LNCS 5213 © Springer.
.pdf
.ps.gz
.dvi
.bib

A Partial Type Checking Algorithm for Type:Type

Andreas Abel and Thorsten Altenkirch (2008)
International Workshop on Mathematically Structured Functional Programming, MSFP'08, Reykjavik University, Iceland, July 6, 2008.
.pdf
.ps.gz
.dvi
.bib

Verifying a Semantic βηConversion Test for MartinLöf Type Theory

Andreas Abel, Thierry Coquand, Peter Dybjer (2008)
9th International Conference on Mathematics of Program Construction, MPC'08, Marseille, France, 1518 July 2008. (18/38)
LNCS 5133 © Springer.
.pdf
.ps.gz
.dvi
.bib
Extended version:
.pdf
.ps.gz
.dvi
Erratum:
.pdf
.ps.gz
.dvi

On the Algebraic Foundation of Proof Assistants for Intuitionistic Type Theory

Andreas Abel, Thierry Coquand, Peter Dybjer (2008)
9th International Symposium on Functional and Logic Programming, FLOPS'08, Invited paper.
© Springer
.pdf
.bib

Semicontinuous Sized Types and Termination

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

Normalization for the SimplyTyped λcalculus in Twelf

Andreas Abel (2007)
Superseds LFM'04 informal proceedings version.
Postproceedings of Logical Frameworks and Metalanguages (LFM 04), IJCAR, Cork, Ireland, 2004.
.pdf
.ps.gz
.dvi
.bib
Twelf code:
wn.tar.gz, weak normalization
sn.tar.gz, strong normalization
2007

Mixed Inductive/Coinductive Types and Strong Normalization

Andreas Abel (2007)
Improves on TLCA'07 conference paper.
The Fifth ASIAN Symposium on Programming Languages and Systems (APLAS 2007), Singapore (25/84)
© Springer
.pdf
.ps.gz
.dvi
.bib

Syntactical Normalization for Intersection Types with Term Rewriting Rules

Andreas Abel (2007)
4th International Workshop on HigherOrder Rewriting, HOR'07, Paris, France.
.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
Longer version:
.pdf
.ps.gz
.dvi
Errata:
.pdf
.ps.gz
.dvi

Strong Normalization and Equi(co)inductive Types

Andreas Abel (2007)
Typed Lambda Calculi and Application, TLCA'07, Paris, France.
© Springer
.pdf
.ps.gz
.dvi
.bib

Normalization by Evaluation for MartinLöf Type Theory with One Universe

Andreas Abel, Klaus Aehlig, Peter Dybjer (2007)
23rd Conference on the Mathematical Foundations of Programming Semantics, MFPS XXIII, New Orleans, USA.
Electr. Notes Theor. Comput. Sci. 173: 1739 (2007)
.pdf
.ps.gz
.dvi
.bib
Amendment (subset instead of PER model)
.pdf
.ps.gz
.dvi

Untyped Algorithmic Equality for MartinLöf's Logical Framework with Surjective Pairs

Andreas Abel and Thierry Coquand (2007)
Superseds TLCA'05 conference paper.
Fundamenta Informaticae 77(4):345395, TLCA'05 special issue.
.pdf
.ps.gz
.dvi
.bib
Haskell implementation:
MLFSigma.lhs
2006

A Polymorphic LambdaCalculus with Sized HigherOrder Types

Andreas Abel (2006)
PhD thesis
Appeared as book TypeBased Termination, ISBN 9783938363041, © 2007 HARLAND media.
Draft:
.pdf
.ps.gz
.dvi
.bib

Semicontinuous Sized Types and Termination

Andreas Abel (2006)
Computer Science Logic (CSL 2006), Szeged, Hungary, September 2529, 2006
© Springer
.bib

Implementing a Normalizer Using Sized Heterogeneous Types

Andreas Abel (2006)
Workshop on Mathematically Structured Functional Programming, MSFP 2006, Kuressaare, Estonia, July 2, 2006
eWiC proceedings, The British Computer Society.
.pdf
.ps.gz
.dvi
.bib

Towards Generic Programming with Sized Types

Andreas Abel (2006)
Mathematics of Program Construction, MPC '06, Kuressaare, Estonia, July 35, 2006. © Springer
.bib
doi

Polarized Subtyping for Sized Types

Andreas Abel (2005)
International Computer Science Symposium in Russia,
CSR'06,
St. Petersburg, June 812, 2006 (30/159)
© Springer
.bib
doi
2005

Verifying Haskell Programs Using Constructive Type Theory

Andreas Abel, Marcin Benke, Ana Bove, John Hughes, Ulf Norell (2005)
Haskell'05, Tallinn, Estonia,
September 30, 2005
© ACM
.pdf
.ps.gz
.dvi
.bib

Connecting a Logical Framework to a FirstOrder Prover

Andreas Abel, Thierry Coquand, Ulf Norell (2005)
5th International Workshop on Frontiers of Combining Systems
FroCoS'05,
Vienna, Austria, September 1921, 2005
© Springer
.pdf
.ps.gz
.dvi
.bib

Connecting a Logical Framework to a FirstOrder Prover (Extended Version)

Andreas Abel, Thierry Coquand, Ulf Norell (2005)
Technical report, Department of Computer Science, Chalmers University of Technology, Göteborg, Sweden.
.pdf
.ps.gz
.dvi
.bib

Untyped Algorithmic Equality for MartinLöf's Logical Framework with Surjective Pairs

Andreas Abel and Thierry Coquand (2005)
TLCA'05, Nara, Japan.
LNCS 3461, pp. 2338
© Springer
Superseded by long version.

Iteration and Coiteration Schemes for HigherOrder and Nested Datatypes

Andreas Abel, Ralph Matthes, and Tarmo Uustalu (2004)
FoSSaCS 03 special issue, Theoretical Computer Science
333(12):366, 2005.
© Elsevier.
.pdf
.ps.gz
.dvi
.bib
2004

Fixed Points of Type Constructors and Primitive Recursion

Andreas Abel and Ralph Matthes
Computer Science Logic, 18th International Workshop, CSL 2004, 13th Annual Conference of the EACSL
Karpacz, Poland, September 2004.
LNCS 3210, © Springer.
.pdf
.ps.gz
.dvi
.bib
Errata:
.pdf
.ps.gz
.dvi

Weak Normalization for the SimplyTyped λcalculus in Twelf

Andreas Abel
Logical Frameworks and Metalanguages (LFM 04), IJCAR, Cork, Ireland, 2004.
.pdf
.ps.gz
.dvi
.bib
Twelf code:
wn.tar.gz (updated Oct 2006, thanks to
Chungchieh Shan (Rutgers), who made it check coverage)

Termination Checking with Types

Andreas Abel
Special Issue: Fixed Points in Computer Science (FICS'03)
RAIRO  Theoretical Informatics and Applications
38(4):277319, 2004.
©RDP Sciences
.pdf
.ps.gz
.dvi
.bib
Soundness of typing algorithm in Twelf:
rairo04twelf.tar.gz
Enhanced Twelf proof also ensuring wellformedness of types:
rairo04twelf_no_itype.tar.gz
Referenced on Lambda the Ultimate.
2003

Termination and Guardedness Checking with Continuous Types

Andreas Abel.
Typed Lambda Calculi and Applications, 6th International Conference, TLCA 2003 (21/40),
Valencia, Spain, June 2003.
LNCS 2701, © Springer.
.pdf
.ps.gz
.dvi
.bib
Errata:
.pdf
.ps.gz
.dvi

Constructing TypeSafe Operators for Software Composition

Axel Rauschmayer, Andreas Abel, Alexander Knapp and Martin Wirsing.
Technical Report, Institut für Informatik,
LudwigMaximiliansUniversität München, June 2003.
.pdf
.ps.gz
.dvi
.bib

Generalized Iteration and Coiteration for HigherOrder Nested Datatypes

Andreas Abel, Ralph Matthes and Tarmo Uustalu.
Foundations of Software Science and Computation Structures (FoSSaCS 2003),
Warsaw, Poland, April 2003.
LNCS 2620, © Springer.
.pdf
.ps.gz
.dvi
.bib

Primitive Recursion for Rank2 Inductive Types

Andreas Abel and Ralph Matthes.
Abstract for FICS03, Satellite Workshop to ETAPS 03, Warsaw, Poland, April 2003.
.pdf
.ps.gz
.dvi
.bib

(Co)Iteration for HigherOrder Nested Datatypes

Andreas Abel and Ralph Matthes.
Types for Proofs and Programs, International Workshop, TYPES 2002,
Berg en Dal, The Netherlands, April 2002.
LNCS 2646, © Springer.
.pdf
.ps.gz
.dvi
.bib
Haskell sources
Haskell listing:
.pdf
.ps.gz
.dvi
2002

Termination Checking with Types

Andreas Abel (2002)
Technical Report 0201, Institut für
Informatik, LudwigMaximiliansUniversität München.
Superseeded by journal article.

A Predicative Analysis of Structural Recursion

Andreas Abel and Thorsten Altenkirch (2002)
Journal of Functional Programming 12(1):141.
©Cambridge University
Press
.pdf
.ps.gz
.dvi
.bib
AMS Review by C. Raffalli
Comparison with Pierce's algorithmic leastfixed point construction:
.pdf
.ps.gz
.dvi
.bib
2001

A ThirdOrder Representation of the λμCalculus

Andreas Abel (2001)
S. J. Ambler, R. L. Crole and A. Momigliano (eds.),
Electronic Notes in Theoretical Computer Science,
vol. 581,
© Elsevier Science Publishers.
Also appeared in:
MEchanized Reasoning about Languages with variable bINnding
(MERLIN 2001),
University of Leicester, Technical Report 2001/26.
.pdf
.ps.gz
.dvi
.bib
Twelf sources

HumanReadable MachineVerifiable Proofs for
Teaching Constructive Logic

Andreas Abel, BorYuh Evan Chang and Frank Pfenning (2001)
Proof Transformation, Proof Presentation and Complexity of Proofs
(PTP01). Workshop
Proceedings.
.pdf
.ps.gz
.dvi
.bib
2000

A Predicative Strong Normalisation Proof for a
λcalculus with Interleaving Inductive Types

Thorsten Altenkirch and Andreas Abel (2000)
Types for Proofs and Programs, International Workshop, TYPES '99
Lökeberg, Sweden, June 1999.
LNCS 1956.
©SpringerVerlag
.pdf
.ps.gz
.dvi
.bib
Errata:
.pdf
.ps.gz
.dvi

Specification and Verification of a
Formal System for Structurally Recursive Functions

Andreas Abel (2000)
Types for Proofs and Programs, International Workshop, TYPES '99
Lökeberg, Sweden, June 1999.
LNCS 1956.
©SpringerVerlag
.pdf
.ps.gz
.dvi
.bib
1999 and before

A Semantic Analysis of Structural Recursion

Andreas Abel (1999)
Diploma Thesis, LudwigMaximiliansUniversity, Munich.
.pdf
.ps.gz
.dvi
.bib
Extended abstract for WST'99:
.pdf
.ps.gz
.dvi
Errata:
.pdf
.ps.gz
.dvi

foetus  Termination Checker for Simple
Functional Programs

Andreas Abel (1998)
Implementation and Documentation.
.pdf
.ps.gz
.dvi
.bib
Executable web version
Notes

Introduction to Parigot's λμCalculus
 A motivation and explanation of Parigot's original formulation. March 2001.
 A Coinductive Formulation of
the "Coinduction Theorem" by Michael and Appel
 Including a minitutorial on coinduction. June 2000.
 Pattern Matching vs. Elimination Rules
 A Case Study in LEGO. September 1999.
[ Home
 CV
 Projects
 Publications
 Talks
 Teaching
 Sharing
]
