Overview

(* = hot!, highly recommended read).

Journal Articles

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

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

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)

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

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
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)
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, 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 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, 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, {VOL##, ISS##, (DATE)} http://doi.acm.org/10.1145/{nnnnnn.nnnnnn}

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.
.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 (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
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
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 (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 .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.


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

Valid HTML 4.01! Andreas Abel, http://www.tcs.informatik.uni-muenchen.de/~abel
Last modified: Tue Jun 9 14:00:55 CEST 2009
Valid CSS!