Overview

(* = hot!, highly recommended read).

Journal Articles

Implementing a Normalizer Using Sized Heterogeneous Types	JFP	To appear	*
Semi-continuous Sized Types and Termination	LMCS	2008	*
Type-Based Termination of Generic Programs	SCP	To appear
Untyped Algorithmic Equality for Martin-Löf's Logical Framework with Surjective Pairs	Fund.Inf.	2007
Polarized Subtyping for Sized Types	MSCS	To appear	*
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

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 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	To appear
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

Primitive Recursion for Rank-2 Inductive Types	FICS	2003
A Semantical Analysis of Structural Recursion	WST	1999

Theses

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)

Connecting a Logical Framework to a First-Order Prover (Extended Version)	CS, Chalmers	2005
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

Syntactic Metatheory of Higher-Order Subtyping: Andreas Abel and Dulma Rodriguez (2008)
Computer Science Logic, CSL'08. To appear.
.pdf .ps.gz .dvi .bib
A Partial Type Checking Algorithm for Type:Type: Andreas Abel and Thorsten Altenkirch (2008)
Mathematically Structured Functional Programming, MSFP'08. To appear.
.pdf .ps.gz .dvi .bib
Verifying a Semantic βη-Conversion Test for Martin-Löf Type Theory: Andreas Abel, Thierry Coquand, Peter Dybjer (2008)
Mathematics of Program Construction, MPC'08. To appear.
.pdf .ps.gz .dvi .bib Extended version: .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
Implementing a Normalizer Using Sized Heterogeneous Types: Andreas Abel (2008)
Superseds MSFP'06 workshop paper.
Journal of Functional Programming, MSFP'06 special issue. To appear.
.pdf .ps.gz .dvi .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
Type-Based Termination of Generic Programs: Andreas Abel (2007)
Superseds MPC'06 conference paper.
Science of Computer Programming, MPC'06 special issue. Submitted.
.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
Polarized Subtyping for Sized Types: Andreas Abel (2006)
Superseds CSR'06 conference paper.
Accepted for publication in MSCS special issue on subtyping.
.pdf .ps.gz .dvi .bib

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 © 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 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
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
.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
International Computer Science Symposium in Russia, CSR'06, St. Petersburg, June 8-12, 2006 © 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
Connecting a Logical Framework to a First-Order 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 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,
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
(New!) 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 .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. ©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: Wed Jun 18 15:04:16 CEST 2008