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
$\partial$ 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 $\lambda^{\to{}2}$
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: Thu Mar 28 10:07:05 GMT 2019