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

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

Thorsten Altenkirch Last modified: Fri Sep 29 14:24:42 BST 2017