Publications: Overview

(* = hot!, highly recommended read).

Journal Articles

Cubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive Types	JFP	2021	*
A Unified View of Modalities in Type Systems	PACMPL	2020	*
Failure of Normalization in Impredicative Type Theory with Proof-Irrelevant Propositional Equality	LMCS	2020
Cubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive Types	PACMPL	2019	*
Elaborating dependent (co)pattern matching	PACMPL	2018	*
Decidability of Conversion for Type Theory in Type Theory	PACMPL	2018	*
Normalization by Evaluation for Sized Dependent Types	PACMPL	2017	*
Interactive Programming in Agda -- Objects and Graphical User Interfaces	JFP	2016	*
Well-founded Recursion with Copatterns and Sized Types	JFP	2016	*
On Irrelevance and Algorithmic Equality in Predicative Type Theory	LMCS	2012	*
A Modular Type Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance	LMCS	2011
Implementing a Normalizer Using Sized Heterogeneous Types	JFP	2009
Type-Based Termination of Generic Programs	SCP	2009
Semi-continuous Sized Types and Termination	LMCS	2008
Polarized Subtyping for Sized Types	MSCS	2008
Untyped Algorithmic Equality for Martin-Löf's Logical Framework with Surjective Pairs	Fund.Inf.	2007
Iteration and Coiteration Schemes for Higher-Order and Nested Datatypes	TCS	2005
Termination Checking with Types	ITA (RAIRO)	2004
A Predicative Analysis of Structural Recursion	JFP	2002

Refereed Conference Proceedings

A Unified View of Modalities in Type Systems	ICFP	2020	*
Normalization by Evalution for Call-By-Push-Value and Polarized Lambda Calculus	PPDP	2019	*
Cubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive Types	ICFP	2019	distinction
A Type Theory for Defining Logics and Proofs	LICS	2019
Elaborating Dependent (Co)pattern Matching	ICFP	2018	*
Decidability of Conversion for Type Theory in Type Theory	POPL	2018	*
Normalization by Evaluation for Sized Dependent Types	ICFP	2017	*
Well-founded Recursion over Contextual Objects	TLCA	2015
A Formalized Proof of Strong Normalization for Guarded Recursive Types	APLAS	2014
Unnesting of Copatterns	RTA-TLCA	2014
Wellfounded Recursion with Copatterns	ICFP	2013	*
Copatterns -- Programming Infinite Structures by Observations	POPL	2013	*
Higher-Order Dynamic Pattern Unification for Dependent Types and Records	TLCA	2011	*
Irrelevance in Type Theory with a Heterogeneous Equality Judgement	FoSSaCS	2011
Towards Normalization by Evaluation for the Calculus of Constructions	FLOPS	2010	*
Typed Applicative Structures and Normalization by Evaluation for System F^ω	CSL	2009
A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance	TLCA	2009
Weak βη-Normalization and Normalization by Evaluation for System F	LPAR	2008	*
Syntactic Metatheory of Higher-Order Subtyping	CSL	2008
Verifying a Semantic βη-Conversion Test for Martin-Löf Type Theory	MPC	2008
On the Algebraic Foundation of Proof Assistants for Intuitionistic Type Theory	FLOPS	2008
Mixed Inductive/Coinductive Types and Strong Normalization	APLAS	2007	*
Normalization by Evaluation for Martin-Löf Type Theory with Typed Equality Judgements	LICS	2007	*
Strong Normalization and Equi-(co)inductive Types	TLCA	2007
Normalization by Evaluation for Martin-Löf Type Theory with One Universe	MFPS	2007
Semi-continuous Sized Types and Termination	CSL	2006
Towards Generic Programming with Sized Types	MPC	2006
Polarized Subtyping for Sized Types	CSR	2006
Untyped Algorithmic Equality for Martin-Löf's Logical Framework with Surjective Pairs	TLCA	2005
Fixed Points of Type Constructors and Primitive Recursion	CSL	2004
Termination and Guardedness Checking with Continuous Types	TLCA	2003
Generalized Iteration and Coiteration for Higher-Order Nested Datatypes	FoSSaCS	2003

Refereed Workshop Proceedings

A Categorical Perspective on Pattern Unification	UNIF	2014
Normalization by Evaluation in the Delay Monad: A Case Study for Coinduction via Copatterns and Sized Types	MSFP	2014	*
Type-Based Termination, Inflationary Fixed-Points, and Mixed Inductive-Coinductive Types	FICS	2012
A Lambda Term Representation Based on Linear Ordered Logic	LFMTP	2011
MiniAgda: Integrating Sized and Dependent Types	PAR	2010
Explicit Substitutions for Contextual Type Theory	LFMTP	2010
Extensional Normalization in the Logical Framework with Proof Irrelevant Equality	NBE	2009
A Partial Type Checking Algorithm for Type:Type	MSFP	2008
Syntactical Normalization for Intersection Types with Term Rewriting Rules	HOR	2007
Normalization for the Simply-Typed Lambda-Calculus in Twelf	LFM'04	2008
Implementing a Normalizer Using Sized Heterogeneous Types	MSFP	2006
Verifying Haskell Programs Using Constructive Type Theory	Haskell	2005
Connecting a Logical Framework to a First-Order Prover	FroCoS	2005
(Co-)Iteration for Higher-Order Nested Datatypes	TYPES'02	2003
A Third-Order Representation of the λμ-Calculus	MERLIN	2001
Human-Readable Machine-Verifiable Proofs for Teaching Constructive Logic	PTP	2001
A Predicative Strong Normalisation Proof for a λ-calculus with Interleaving Inductive Types	TYPES'99	2000
Specification and Verification of a Formal System for Structural Recursion	TYPES'99	2000

Refereed Workshop Abstracts

Type-preserving compilation via dependently typed syntax	TYPES	2020
Cubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive Types	TYPES	2019
Normalization by Evaluation for Call-By-Push-Value	TYPES	2019
Resourceful Dependent Types	TYPES	2018
Normalization by Evaluation for Sized Dependent Types	TYPES	2017
Normalization by Evaluation in the Delay Monad	TYPES	2016
An Extension of Martin-Löf Type Theory with Sized Types	TYPES	2016
On Decidability of Conversion in Type Theory	TYPES	2016
Sprinkles of Extensionality for Your Vanilla Type Theory	TYPES	2016
Compositional Coinduction with Sized Types	CMCS	2016
The Next 700 Modal Type Assignment Systems	TYPES	2015
Normalization by Evaluation in the Delay Monad: An Extended Case Study for Coinduction via Copatterns and Sized Types	NWPT	2014
Programming and Reasoning with Infinite Structures Using Copatterns and Sized Types	ATPS	2014
Productive Infinite Objects via Copatterns	NWPT	2013
Primitive Recursion for Rank-2 Inductive Types	FICS	2003
A Semantical Analysis of Structural Recursion	WST	1999

Theses

Normalization by Evaluation: Dependent Types and Impredicativity	IFI, LMU	2013	*
A Polymorphic Lambda-Calculus With Sized Higher-Order Types	IFI, LMU	2006
A Semantic Analysis of Structural Recursion	IFI, LMU	1999

Technical Reports and Manuscripts (unrefereed or rejected)

On Parametric Polymorphism and Irrelevance in Martin-Löf Type Theory	PI.R2, INRIA	2010
Weak Normalization for the Simply-Typed Lambda-Calculus in Twelf	LFM (IJCAR)	2004
Constructing Type-Safe Operators for Software Composition	IFI, LMU	2003
Termination Checking with Types	IFI, LMU	2002
foetus - Termination Checker for Simple Functional Programs	IFI, LMU	1998

Publications and Preprints

Cubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive Types: Andrea Vezzosi and Anders Mörtberg and Andreas Abel (2020)
Journal of Functional Programming, volume 31, 2021.
Final draft: .pdf

2020

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

2019

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 3(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)
Abstract for the 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)
Abstract for the 25th International Conference on Types for Proofs and Programs (TYPES 2019), Oslo, Norway, 11-14 June 2019.
2-page abstract: .pdf
POPLMark Reloaded: Mechanizing Proofs by Logical Relations: Andreas Abel, Guillaume Allais, Aliya Hameer, Brigitte Pientka, Alberto Momigliano, Steven Schäfer and Kathrin Stark (2018).
Draft, submitted to the Journal of Functional Programming.

2018

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.
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 2(ICFP).
Long version: .pdf
Resourceful Dependent Types: Andreas Abel (2018)
Abstract for 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

2017

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 27: e8, 2017, DTP 2016 special issue.
Author's version: .pdf

2016

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

2015

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 doi:10.4230/LIPIcs.TLCA.2015.273 Long version (draft): .pdf

2014

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 Long version: .pdf Maintained repository: github Original sources (.tex/.lagda): .zip Rendered Agda code: .html
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, 29-31 October 2014.
Programming and Reasoning with Infinite Structures Using Copatterns and Sized Types: Andreas Abel (2014)
Arbeitstagung Programmiersprachen (ATPS 2014), veranstaltet von der GI-Fachgruppe Programmiersprachen und Rechenkonzepte im Rahmen der Software Engineering 2014, 26 February 2014, Kiel, Germany
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
A Categorical Perspective on Pattern Unification: Andrea Vezzosi and Andreas Abel (2014)
The 28th Workshop on Unification, UNIF 2014, FLoC workshop, hosted by RTA-TLCA and IJCAR, Vienna Summer of Logic (VSL 2014), 13 July 2014, Vienna, Austria.
.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

2013

Productive Infinite Objects via Copatterns: Andreas Abel
25th Nordic Workshop on Programming Theory, NWPT 2013, Tallinn, Estonia, 20-22 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, 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.
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.
Copatterns -- Programming Infinite Structures by Observations: Andreas Abel, Brigitte Pientka, David Thibodeau, Anton Setzer (2012)
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.

2012

Type-Based Termination, Inflationary Fixed-Points, and Mixed Inductive-Coinductive 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. 1-11. 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):1-36, 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 Meta-languages: Theory and Practice, LFMTP 2011, Nijmegen, the Netherlands, August 26, 2011.
EPTCS 71 , 2011, pp. 1-13. DOI: 10.4204/EPTCS.71.1
.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
A Modular Type Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance: Andreas Abel, Thierry Coquand, and Miguel Pagano (2009-11)
Superseds the TLCA'09 conference paper.
Logical Methods in Computer Science 7(2:4) 2011, pp. 1-57.
.pdf .ps.gz .dvi .bib A note on eta-conversion: .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, 26-28 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
On Parametric Polymorphism and Irrelevance in Martin-Löf Type Theory: Andreas Abel (2010)
Rejected from Logics in Computer Science, LICS 2010.
MLTT with ``Curry-style'' definitional equality. While a proof of consistency is given, decidability of equality is unclear.
Still, the substitution calculus is interesting and seems to work for irrelevance.
Draft: .pdf Reviews: .txt (Reviewer 2 has a point.)
Towards Normalization by Evaluation for the Calculus of Constructions: Andreas Abel (2009)
Tenth International Symposium on Functional and Logic Programming, FLOPS 2010, 19-21 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, 1-3 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 3-4, MSFP'06 special issue. © Cambridge University Press.
.pdf .ps.gz .dvi .bib
Type-Based Termination of Generic Programs: Andreas Abel (2007)
Superseds MPC'06 conference paper.
Science of Computer Programming 74 (2009), pp. 550-567, 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. 797-822, 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, 22-17 November 2008, Doha, Qatar. (45/153)
LNAI 5330 © Springer.
.pdf .ps.gz .dvi .bib
Syntactic Metatheory of Higher-Order Subtyping: Andreas Abel and Dulma Rodriguez (2008)
Computer Science Logic, 22nd International Workshop, CSL 2008, 17th Annual Conference of the EACSL, Bertinoro, Italy, September 16-19, 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 Martin-Löf Type Theory: Andreas Abel, Thierry Coquand, Peter Dybjer (2008)
9th International Conference on Mathematics of Program Construction, MPC'08, Marseille, France, 15-18 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
Semi-continuous 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 Simply-Typed λ-calculus in Twelf: Andreas Abel (2007)
Superseds LFM'04 informal proceedings version.
Post-proceedings 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 Higher-Order Rewriting, HOR'07, Paris, France.
.pdf .ps.gz .dvi .bib
Normalization by Evaluation for Martin-Lö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 Martin-Lö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: 17-39 (2007)
.pdf .ps.gz .dvi .bib Amendment (subset instead of PER model) .pdf .ps.gz .dvi
Untyped Algorithmic Equality for Martin-Löf's Logical Framework with Surjective Pairs: Andreas Abel and Thierry Coquand (2007)
Superseds TLCA'05 conference paper.
Fundamenta Informaticae 77(4):345-395, TLCA'05 special issue.
.pdf .ps.gz .dvi .bib Haskell implementation: MLFSigma.lhs

2006

A Polymorphic Lambda-Calculus with Sized Higher-Order Types: Andreas Abel (2006)
PhD thesis
Appeared as book Type-Based Termination, ISBN 978-3-938363-04-1, © 2007 HARLAND media.
Draft: .pdf .ps.gz .dvi .bib
Semi-continuous Sized Types and Termination: Andreas Abel (2006)
Computer Science Logic (CSL 2006), Szeged, Hungary, September 25-29, 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 3-5, 2006. © Springer
.bib doi
Polarized Subtyping for Sized Types: Andreas Abel (2005)
International Computer Science Symposium in Russia, CSR'06, St. Petersburg, June 8-12, 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 First-Order Prover: Andreas Abel, Thierry Coquand, Ulf Norell (2005)
5th International Workshop on Frontiers of Combining Systems FroCoS'05, Vienna, Austria, September 19-21, 2005 © Springer
.pdf .ps.gz .dvi .bib Extended version: .pdf .ps.gz .dvi .bib
Untyped Algorithmic Equality for Martin-Löf's Logical Framework with Surjective Pairs: Andreas Abel and Thierry Coquand (2005)
TLCA'05, Nara, Japan. LNCS 3461, pp. 23-38 © Springer
Superseded by long version.
Iteration and Coiteration Schemes for Higher-Order and Nested Datatypes: Andreas Abel, Ralph Matthes, and Tarmo Uustalu (2004)
FoSSaCS 03 special issue, Theoretical Computer Science 333(1-2):3-66, 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 Simply-Typed λ-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 Chung-chieh 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):277-319, 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 Type-Safe Operators for Software Composition: Axel Rauschmayer, Andreas Abel, Alexander Knapp and Martin Wirsing.
Technical Report, Institut für Informatik, Ludwig-Maximilians-Universität München, June 2003.
.pdf .ps.gz .dvi .bib
Generalized Iteration and Coiteration for Higher-Order 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 Rank-2 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 Higher-Order 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, Ludwig-Maximilians-Universitä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):1-41. ©Cambridge University Press
.pdf .ps.gz .dvi .bib AMS Review by C. Raffalli
Comparison with Pierce's algorithmic least-fixed point construction: .pdf .ps.gz .dvi .bib

2001

A Third-Order Representation of the λμ-Calculus: Andreas Abel (2001)
S. J. Ambler, R. L. Crole and A. Momigliano (eds.), Electronic Notes in Theoretical Computer Science, vol. 58-1, © 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
Human-Readable Machine-Verifiable Proofs for Teaching Constructive Logic: Andreas Abel, Bor-Yuh Evan Chang and Frank Pfenning (2001)
Proof Transformation, Proof Presentation and Complexity of Proofs (PTP-01). 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. ©Springer-Verlag
.pdf .ps.gz .dvi .bib Errata: .pdf
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. ©Springer-Verlag
.pdf .ps.gz .dvi .bib

1999 and before

A Semantic Analysis of Structural Recursion: Andreas Abel (1999)
Diploma Thesis, Ludwig-Maximilians-University, 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 mini-tutorial on coinduction. June 2000.
Pattern Matching vs. Elimination Rules: A Case Study in LEGO. September 1999.

Andreas Abel, http://www.tcs.informatik.uni-muenchen.de/~abel
Last modified: 2019-01-22 17:51