Thorsten Altenkirch's drafts and publications

See alti.bib for a collection of most of my bibtex entries.

Naive Type Theory

to appear as a chapter in Reflections on the Foundations of Mathematics

Partiality, Revisited (The Partiality Monad as a Quotient Inductive-Inductive Type)

with Nils Anders Danielsson and Nicolaai Kraus
FOSSACS 2017

Extending Homotopy Type Theory with Strict Equality

with Palo Capriotti and Nicolaai Kraus
CSL, August 2016
Bibtex entry

Normalisation by Evaluation for Dependent Types

with Ambrus Kaposi
FSCD, May 2016
Bibtex entry

Type Theory in Type Theory using Quotient Inductive Types

with Ambrus Kaposi
POPL, January 2016
Bibtex entry

Monads need not be endofunctors (Journal version)

with James Chapman and Tarmo Uustalu
March 2015, LMCS
Bibtex entry

A syntax for cubical type theory

with Ambrus Kaposi
(Draft, August 2014)

Relative Monads Formalised

with James Chapman and Tarmo Uustalu
Journal for Formalized Reasoning
Bibtex entry

Some constructions on ω-groupoids

with Li Nuo and Ondrej Rypacek
(appeared in LFMTP 2014)
Bibtex entry

Notions of anonympous existence in Martin-Löf Type Theory (Journal version of Generalizations of Hedberg's Theorem)

with Nicolai Kraus, Martin Escardo and Thierry Coquand
(submitted for publication, March 2014)

Small Induction Recursion

with Peter Hancock, Conor McBride, Neil Ghani and Lorenzo Malatesta
TLCA 2013
Bibtex entry

Generalizations of Hedberg's Theorem

with Nicolai Kraus, Martin Escardo and Thierry Coquand
TLCA 2013
Bibtex entry

Indexed Container (Journal version)

with Neil Ghani, Peter Hancock, Conor McBride and Peter Morris
July 2013, submitted for publication
Bibtex entry

A Syntactical Approach to Weak ω-Groupoids

with Ondrej Rypacek
CSL 2012
Bibtex entry

A categorical semantics for inductive-inductive definitions

with Frederik Forsberg, Peter Morris and Anton Setzer
CALCO 2011
Bibtex entry

Normalisation by Heredetary Substitutions

with Chantal Keller
MSFP 2010

Termination Checking Nested Inductive and Coinductive Types

with Nils Anders Danielsson
short note, June 2010

Higher Order Containers

with Paul Levy and Sam Staton
CIE 2010, invited paper
Bibtex entry

Subtyping, Declaratively - An Exercise in Mixed Induction and Coinduction

with Nils Anders Danielsson
to appear in the proceedings of MPC 2010
Bibtex entry

PiSigma: Dependent Types Without the Sugar

with Nils Anders Danielsson, Andres Löh and Nicolas Oury
FLOPS 2010
Bibtex entry

Monads Need Not Be Endofunctors

with James Chapman and Tarmo Uustalu
FOSSACS 2010
Bibtex entry

Mixing Induction and Coinduction

with Nils Anders Danielsson
under revision, October 2009

The Quantum IO Monad

with Alexander Green
chapter in Semantic Techniques in Quantum Computation, January 2009, appeared in 2010
Bibtex entry

Indexed Containers

with Peter Morris
LICS 09, August 2009
Bibtex entry

A Universe of Strictly Positive Families

with Peter Morris and Neil Ghani
International Journal of Foundations of Computer Science, 2009
Bibtex entry

Big step normalisation

with James Chapman
Journal for Functional Programming, 2009
Bibtex entry

From High School to University Algebra

Unfinished Draft, June 2008.

A Partial Type Checking Algorithm for System U

with Andreas Abel
MSFP 2008, May 2008
Bibtex entry

PiSigma: A Core Language for Dependently Typed Programming

with Nicolas Oury
under revision, April 2008,

Shor in Haskell (The Quantum IO Monad)

with Alexander Green
TFP 08, March 2008

Dependent Types for Distributed Arrays

with Wouter Swierstra
TFP 08, March 2008
Bibtex entry

Types for Proofs and Programs (TYPES '06) (Editor)

with Conor McBride
Lecture Notes in Computer Science 4502, 2007
Bibtex entry

Observational Equality, Now!

with Conor McBride and Wouter Swierstra
PLPV 2007
Bibtex entry

Beauty in the beast

with Wouter Swierstra
Haskell workshop 2007
Bibtex entry

Constructing Strictly Positive Families

with Peter Morris and Neil Ghani
Proceedings of CATS 07, January 2007
Bibtex entry

Generic Programming with Dependent Types

with Conor McBride and Peter Morris
Lecture notes for the Spring School on Datatype-Generic Programming in Nottingham, August 2006
Bibtex entry

From reversible to irreversible computations

with Alexander Green
QPL 2006, June 2006
Bibtex entry

Generic programming for dependent types

with Peter Morris
Draft, June 2006
Bibtex entry

Constructing strictly positive families

with Peter Morris
Draft, April 2006
Bibtex entry

Tait in one big step

with James Chapman
Proceedings of MSFP, April 2006
Bibtex entry

Indexed Containers

with Neil Ghani, Peter Hancock, Conor McBride and Peter Morris
Draft, February 2006
Bibtex entry

Towards Observational Type Theory

with Conor McBride
Draft, February 2006
Bibtex entry

Epigram Reloaded: A Standalone Typechecker for ETT

with James Chapman and Conor McBride
TFP 2005, July 2005
Bibtex entry

An Algebra of Pure Quantum Programming

with Jonathan Grattage, Juliana K. Vizzotto and Amr Sabry
3rd International Workshop on Quantum Programming Languages, May 2005
Bibtex entry

Exploring the Regular Tree Types

with Peter Morris and Conor McBride
Proceedings of TYPES 04, February 2006
Bibtex entry

Why Dependent Types Matter

with Conor McBride and James McKinna
Draft, April 2005,
Bibtex entry

QML: Quantum data and control

with Jonathan Grattage
Draft, February 2005,
Bibtex entry

A Compiler for a Functional Quantum Programming Language

with Jonathan Grattage
Draft, January 2005,
Bibtex entry

Structuring Quantum Effects: Superoperators as Arrows

with Juliana K. Vizzotto and Amr Sabry
Mathematical Structures in Computer Science, special issue on Quantum Programming Languages, 2006
Bibtex entry

A functional quantum programming language

with Jonathan Grattage
20th Symposium on Logic in Computer Science (LICS), 2005
see also quant-ph/0409065
Bibtex entry

Containers - Constructing Strictly Positive Types

with Michael Abbott and Neil Ghani,
Theoretical Computer Science, September 2005,
Bibtex entry

Lambda calculus and types

Lecture notes for MGS/APPSEM Spring School 2004, March 2004
Bibtex entry

Constructing Polymorphic Programs with Quotient Types

with Michael Abbott, Neil Ghani and Conor McBride
Mathematics of Program Construction (MPC 2004)
Bibtex entry

for Data --- Differentiating Data Structures

with Michael Abbott, Neil Ghani and Conor McBride
Fundamentae Informatica, March 2005
Bibtex entry

Representing Nested Inductive Types using W-types

with Michael Abbott and Neil Ghani
ICALP 2004
Bibtex entry

Normalization by evaluation for

with Tarmo Uustalu
Functional and Logic Programming (FLOPS) 2004
Bibtex entry, Literate Haskell script

Derivatives of Containers

with Michael Abbott, Neil Ghani and Conor McBride
Typed Lambda Calculi and Applications (TLCA), 2003
Bibtex entry

Categories of Containers

with Michael Abbott and Neil Ghani
Foundations of Software Science and Computation Structures (FOSSACS), 2003
Bibtex entry

alpha-conversion is easy

(under revision)
September 2002
Bibtex entry

Generic Programming Within Dependently Typed Programming

with Conor McBride
Working Conference on Generic Programming (WCGP), 2002
Bibtex entry, OLEG code

A Predicative Analysis of Structural Recursion

with Andreas Abel
Journal for Functional Programming (JFP), 2002
Bibtex entry

Normalization by evaluation for typed lambda calculus with coproducts

with Peter Dybjer,Martin Hofmann and Phil Scott
16th Symposium on Logic in Computer Science (LICS), 2001
Bibtex entry

When is a function a fold or an unfold?

with Jeremy Gibbons and Graham Hutton
Coalgebraic Methods in Computer Science (CMCS), 2001
Bibtex entry

A Finitary Subsystem of the Polymorphic lambda-calculus

with Thierry Coquand
Typed Lambda Calculi and Applications (TLCA), 2001
Bibtex entry

Representations of first order function types as terminal coalgebras

Typed Lambda Calculi and Applications (TLCA), 2001
Bibtex entry

Notes on definability and Kripke Logical Relations

Unpublished note, 2000
Bibtex entry

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

with Andreas Abel
Types for Proofs and Programs (TYPES), 1999
Bibtex entry

Extensional Equality in Intensional Type Theory

14th Symposium on Logic in Computer Science (LICS), 1999
Bibtex entry

Monadic presentations of lambda terms using generalized inductive types

with Bernhard Reus
Computer Science Logic (CSL), 1999
Bibtex entry

Types for Proofs and Programs (TYPES '98) (Editor)

with Wolfgang Naraschewski and Bernhard Reus
Lecture Notes in Computer Science 1656, 1998
Bibtex entry

Logical relations and inductive/coinductive types

Computer Science Logic (CSL), 1998
Bibtex entry

Reduction-free normalisation for system F

with Martin Hofmann and Thomas Streicher
Unpublished note, 1997
Bibtex entry

Integrated Verification in Type Theory

Lecture Notes, ESSLLI, 1996
Bibtex entry

Reduction-free normalisation for a polymorphic system

with Martin Hofmann and Thomas Streicher
11th Symposium on Logic in Computer Science (LICS), 1996
Bibtex entry, SML code

Categorical reconstruction of a reduction free normalization proof

with Martin Hofmann and Thomas Streicher
Category Theory and Computer Science (CTCS), 1995
Bibtex entry, SML code

Programming + Verification = Progification

unpublished note, September 1994
Bibtex entry

A user's guide to ALF

with Veronica Gaspes,Bengt Nordström and Björn von Sydow
Internal note, Chalmers University of Technology, 1994
Bibtex entry

Proving Strong Normalization of CC by Modifying Realizability Semantics

Types for Proofs and Programs (TYPES), 1994
Bibtex entry

Constructions, Inductive Types and Strong Normalization

PhD thesis, University of Edinburgh, 1993
Bibtex entry, LEGO code (.zip)

A formalization of the strong normalization proof for System F in LEGO

Typed Lambda Calculi and Applications (TLCA), 1993
Bibtex entry, LEGO code (.zip)