Type Theory Papers

Recursive Types

• authors: Marco Kuhlmann
• date: 2003
• online @ www.ps.uni-saarland.de
• format: lecture-notes

It's an extended abstract of a talk given in a seminar on Types and Programming Languages at Saarland University.

On Universes in Type Theory

• authors: Erik Palmgren
• date: 1998
• publication: Twenty-five years of Constructive Type Theory (Oxford Logic Guides: Volume 36), Oxford, New York: Oxford University Press, 191-204
• online @ www2.math.uu.se
• online @ media.githubusercontent.com

.

The Gentle Art of Levitation

• authors: James Chapman, Pierre-Évariste Dagand, Conor McBride, Peter Morris
• date: 2010
• online @ personal.cis.strath.ac.uk

.

Breaking Through the Normalization Barrier: A Self-Interpreter for F-omega

• authors: Matt Brown, Jens Palsberg
• date: 2016
• online @ web.cs.ucla.edu

.

A lean specification for GADTs: system F with first-class equality proofs

• authors: Arie Middelkoop, Atze Dijkstra, S. Doaitse Swierstra
• date: 2011
• online @ link.springer.com

.

Observational Equality, Now!

• authors: Thorsten Altenkirch, Conor McBride, Wouter Swierstra
• date: 2007
• online @ strictlypositive.org
• topics: Type Theory, Equational Logic

.