@InProceedings{alti:tlca93,
author = "Thorsten Altenkirch",
title = "A Formalization of the Strong Normalization Proof for
{System F} in {LEGO}",
booktitle = "Typed Lambda Calculi and Applications",
year = "1993",
editor = "M. Bezem, J.F. Groote",
series = "LNCS 664",
pages = "13 - 28",
}
@PhdThesis{alti:phd93,
author = "Thorsten Altenkirch",
title = "Constructions, Inductive Types and Strong Normalization",
school = "University of Edinburgh",
year = "1993",
month = "November",
}
@InProceedings{alti:types94,
author = "Thorsten Altenkirch",
title = "Proving Strong Normalization of {CC} by Modifying
Realizability Semantics",
editor = "Henk Barendregt and Tobias Nipkow",
series = "LNCS 806",
pages = "3 - 18",
booktitle = "Types for Proofs and Programs",
year = "1994",
}
@Misc{alti:alf94,
author = "Thorsten Altenkirch and Veronica Gaspes and Bengt
{Nordstr\"om} and {Bj\"orn} von Sydow",
title = "A user's guide to {ALF}",
year = "1994",
month = "May",
howpublished = "available from http://www.cs.nott.ac.uk/\~{}txa/publ/alf94.pdf",
note = "{Department of Computing Science,
University of G\"{o}teborg/Chalmers}",
url = "http://www.cs.nott.ac.uk/~txa/publ/alf94.pdf"
}
@InProceedings{alti:ctcs95,
author = "Thorsten Altenkirch and Martin Hofmann and Thomas Streicher",
title = "Categorical reconstruction of a reduction free
normalization proof",
year = "1995",
booktitle = "Category Theory and Computer Science",
editor = {David Pitt and David E. Rydeheard and Peter Johnstone},
series = {LNCS 953},
pages = {182-199},
}
@Misc{alti:esslli96,
author = "Thorsten Altenkirch",
title = "Integrated Verification in {Type} {Theory}",
howpublished = "Lecture notes for a course at ESSLLI 96, Prague",
note = "available from {\tt http://www.cs.nott.ac.uk/\~{}txa/publ/esslli96.pdf}",
year = "1996",
}
@InProceedings{alti:lics96,
author = "Thorsten Altenkirch and Martin Hofmann and Thomas Streicher",
title = "Reduction-free normalisation for a polymorphic system",
pages = "98-106",
booktitle = "11th Annual IEEE Symposium on Logic in Computer
Science",
year = "1996",
}
@Unpublished{alti:f97,
author = {Thorsten Altenkirch and Martin Hofmann and Thomas Streicher},
title = {Reduction-free normalisation for system {$F$}},
note = {available from {\tt http://www.cs.nott.ac.uk/\~{}txa/publ/f97.pdf}},
year = {1997},
www = {http://www.cs.nott.ac.uk/~txa/publ/f97.pdf},
}
@Proceedings{alti:types98,
title = {Types for Proofs and Programs (TYPES '98)},
year = {1999},
editor = {Thorsten Altenkirch and Wolfgang Naraschewski and Bernhard Reus},
volume = {1657},
series = {Lecture Notes in Computer Science},
}
@InProceedings{alti:csl98,
author = {Thorsten Altenkirch},
title = {Logical relations and inductive/coinductive types},
booktitle = {Computer Science Logic, 12th International Workshop, CSL '98},
pages = {343-354},
year = {1998},
series = {LNCS 1584}
}
@InProceedings{alti:csl99,
author = {Thorsten Altenkirch and Bernhard Reus},
title = {Monadic presentations of lambda terms using generalized inductive types},
booktitle = {Computer Science Logic, 13th International Workshop, CSL '99},
year = {1999},
pages = {453-468}
}
@InProceedings{alti:lics99,
author = {Thorsten Altenkirch},
title = {Extensional Equality in Intensional Type Theory},
booktitle = {14th Symposium on Logic in Computer Science},
year = {1999},
pages = { 412 -- 420 }
}
@InProceedings{alti:types99,
author = {Andreas Abel and Thorsten Altenkirch},
title = {A Predicative Strong Normalisation Proof for a
$\lambda$-calculus with Interleaving Inductive Types},
booktitle = {{Types for Proof and Programs, International Workshop, TYPES '99, Selected Papers}},
year = {2000},
series = {Lecture Notes in Computer Science},
volume = {1956},
pages = "1--18"
}
@InProceedings{alti:cmcs01,
author = {Jeremy Gibbons and Graham Hutton and Thorsten Altenkirch},
title = {When is a function a fold or an unfold? },
booktitle = {Proceedings of the 4th International Workshop on Coalgebraic Methods in Computer Science},
year = {2001},
volume = {44.1},
series = {Electronic Notes in Theoretical Computer Science},
}
@InProceedings{alti:tlca01a,
author = {Thorsten Altenkirch},
title = {Representations of first order function types as
terminal coalgebras},
booktitle = {Typed Lambda Calculi and Applications, TLCA 2001},
pages = {8 - 21},
year = {2001},
number = {2044},
series = {Lecture Notes in Computer Science}
}
@InProceedings{alti:tlca01b,
author = {Thorsten Altenkirch and Thierry Coquand},
title = {A Finitary Subsystem of the Polymorphic $\lambda$-calculus},
booktitle = {Typed Lambda Calculi and Applications, TLCA 2001},
pages = {22 - 28},
year = {2001},
number = {2044},
series = {Lecture Notes in Computer Science}
}
@InProceedings{alti:lics01,
author = "Thorsten Altenkirch and Peter Dybjer and Martin Hofmann and Phil Scott",
title = "Normalization by evaluation for typed lambda calculus with
coproducts",
pages = "303-310",
booktitle = "16th Annual IEEE Symposium on Logic in Computer
Science",
year = "2001"
}
@Article{alti:jfp02,
author = {Andreas Abel and Thorsten Altenkirch},
title = {A Predicative Analysis of Structural Recursion},
journal = {Journal of Functional Programming},
year = 2002,
volume = 12,
number = 1,
pages = {1--41},
month = {January}
}
@InProceedings{alti:wcgp02,
author = {Thorsten Altenkirch and Conor McBride},
title = {Generic Programming Within Dependently Typed Programming},
booktitle = {Generic Programming},
year = {2003},
note = {Proceedings of the IFIP TC2 Working Conference on Generic Programming, Schloss Dagstuhl, July 2002}
}
@InProceedings{alti:fossacs03,
author = {Michael Abott and Thorsten Altenkirch and Neil Ghani },
title = {Categories of Containers},
booktitle = {Proceedings of Foundations of Software Science and Computation Structures},
year = {2003}
}
@InProceedings{alti:tlca03,
author = {Michael Abott and Thorsten Altenkirch and Neil Ghani
and Conor McBride},
title = {Derivatives of Containers},
booktitle = {Typed Lambda Calculi and Applications, TLCA},
year = {2003},
}
@InProceedings{alti:flops04,
author = {Thorsten Altenkirch and Tarmo Uustalu},
title = {Normalization by evaluation for $\lambda^{\to 2}$},
booktitle = {Functional and Logic Programming},
isbn = {3-540-21402-X},
year = {2004},
number = {2998},
series = {LNCS},
pages = {260 - 275},
}
@InProceedings{alti:icalp04,
author = {Michael Abbott and Thorsten Altenkirch and Neil Ghani},
title = {Representing Nested Inductive Types using {W-types}},
booktitle = {Automata, Languages and Programming, 31st International Colloqium (ICALP)},
pages = {59 -- 71},
year = {2004}
}
@Article{alti:jpartial,
author = {Michael Abott and Thorsten Altenkirch and Neil Ghani
and Conor McBride},
title = {$\partial$ for Data},
journal = {Fundamentae Informatica},
year = {2005},
volume = {65},
number = {1,2},
pages = {1 -- 28},
month = {March},
note = {Special Issue on Typed Lambda Calculi and Applications 2003}
}
@InProceedings{alti:mpc04,
author = {Michael Abott and Thorsten Altenkirch and Neil Ghani
and Conor McBride},
title = {Constructing Polymorphic Programs with Quotient Types},
booktitle = {7th International Conference on Mathematics of Program Construction (MPC 2004)},
year = {2004}
}
@Article{alti:cont-tcs,
author = {Michael Abott and Thorsten Altenkirch and Neil Ghani},
title = {Containers - Constructing Strictly Positive Types},
journal = {Theoretical Computer Science},
year = {2005},
volume = {342},
pages = {3--27},
month = {September},
note = {Applied Semantics: Selected Topics},
}
@InProceedings{alti:qml,
author = {Thorsten Altenkirch and Jonathan Grattage},
title = {A functional quantum programming language},
booktitle = "20th Annual IEEE Symposium on Logic in Computer
Science",
year = "2005",
}
@Article{alti:qarrows,
author = {Juliana K. Vizzotto and Thorsten Altenkirch and Amr Sabry},
title = {Structuring Quantum Effects: Superoperators as Arrows},
journal={Mathematical Structures in Computer Science},
volume={16},
number={03},
pages={453--468},
year={2006},
publisher={Cambridge University Press}
}
@inproceedings{alti:regular,
author = "Peter Morris and Thorsten Altenkirch and Conor McBride",
title = "Exploring the Regular Tree Types",
booktitle = "Types for Proofs and Programs ({TYPES} 2004)",
editor = "Jean-Christophe Filliatre, Christine Paulin-Mohring and Benjamin Werner",
series = "Lecture Notes in Computer Science",
year = 2006
}
@article{alti:qpl05,
title={{An Algebra of Pure Quantum Programming}},
author={Thorsten Altenkirch and Jonathan Grattage and Juliana K. Vizzotto and Amr Sabry },
journal={Electronic Notes in Theoretical Computer Science},
volume={170},
pages={23--47},
year={2007},
publisher={Elsevier},
note = {3rd International Workshop on Quantum Programming Languages},
}
@Misc{alti:ydtm,
author = {Thorsten Altenkirch and Conor McBride and James McKinna},
title = {Why Dependent Types Matter},
howpublished = {Manuscript, available online},
month = {April},
year = {2005},
}
@InCollection{alti:checking,
author = {James Chapman and Thorsten Altenkirch and Conor McBride},
title = {Epigram Reloaded: A Standalone Typechecker for {ETT}},
year = {2006},
booktitle = {Trends in Functional Programming Volume 6},
publisher = {Intellect},
editor = {Marko van Eekelen}
}
@inproceedings{alti:tait06,
author = "Thorsten Altenkirch and James Chapman",
title = "{Tait in one big step}",
booktitle = "{Workshop on Mathematically
Structured Functional Programming, MSFP 2006, Kuressaare, Estonia, July 2, 2006}",
address = "Kuressaare, Estonia",
year = 2006,
series = "{electronic Workshop in Computing (eWiC)}",
publisher = "{The British Computer Society (BCS)}",
url = {http://ewic.bcs.org/conferences/2006/msfp/}
}
@Misc{alti:qpl06,
author = {Alexander Green and Thorsten Altenkirch},
title = {From reversible to irreversible computations},
howpublished = {Proceedings of QPL 2006},
month = {June},
year = {2006},
}
@InCollection{txa:ssgp06,
author = {Thorsten Altenkirch and Conor Mcbride and Peter Morris},
title = {Generic Programming with Dependent Types},
booktitle = {Spring School on Datatype-Generic Programming},
OPTpages = {},
publisher = {Springer-Verlag},
year = {2007},
editor = {Roland Backhouse and Jeremy Gibbons and Ralf Hinze and Johan Jeuring},
volume = {4719},
series = {LNCS},
}
@InProceedings{alti:cats07,
author = {Peter Morris and Thorsten Altenkirch and Neil Ghani},
title = {Constructing Strictly Positive Families},
year = {2007},
booktitle = {The Australasian Theory Symposium (CATS2007)},
month = {January}
}
@proceedings{alti:types06,
editor = {Thorsten Altenkirch and
Conor McBride},
title = {Types for Proofs and Programs, International Workshop, TYPES
2006, Nottingham, UK, April 18-21, 2006, Revised Selected
Papers},
booktitle = {TYPES},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {4502},
year = {2007},
}
@Article{alti:jcats07,
author = {Peter Morris and Thorsten Altenkirch and Neil Ghani},
title = {A Universe of Strictly Positive Families},
journal={International Journal of Foundations of Computer Science},
volume={20},
number={1},
pages={83--107},
year={2009},
}
@InProceedings{alti:beast,
author = {Wouter Swierstra and Thorsten Altenkirch},
title = {Beauty in the Beast},
year = {2007},
OPTcrossref = {},
OPTkey = {},
booktitle = {Haskell workshop},
OPTpages = {},
OPTyear = {},
OPTeditor = {},
OPTvolume = {},
OPTnumber = {},
OPTseries = {},
OPTaddress = {},
OPTmonth = {},
OPTorganization = {},
OPTpublisher = {},
OPTnote = {},
OPTannote = {}
}
@inproceedings{alti:ott-conf,
author = {Thorsten Altenkirch and Conor McBride and Wouter Swierstra},
title = {Observational equality, now!},
booktitle = {PLPV '07: Proceedings of the 2007 workshop on Programming languages meets program verification},
year = {2007},
isbn = {978-1-59593-677-6},
pages = {57--68},
location = {Freiburg, Germany},
doi = {http://doi.acm.org/10.1145/1292597.1292608},
publisher = {ACM},
address = {New York, NY, USA},
}
@inproceedings{alti:tfp08,
Author = {Wouter Swierstra and Thorsten Altenkirch},
Booktitle = {Trends in Functional Programming},
Title = {Dependent Types for Distributed Arrays},
Volume = {9},
Year = {2008}}@inproceedings{alti:msfp08,
author = {Andreas Abel and Thorsten Altenkirch},
title = {A Partial Type Checking Algorithm for {Type:Type}},
booktitle = "{Workshop on Mathematically
Structured Functional Programming, MSFP 2008}",
address = "Kuressaare, Estonia",
year = 2008,
}
@Article{txa:jtait,
title={{Big-step normalisation}},
author={Thorsten Altenkirch and James Chapman},
journal={Journal of Functional Programming},
volume={19},
number={3-4},
pages={311--333},
year={2009},
publisher={Cambridge University Press}
}@InProceedings{alti:lics09,
author = {Peter Morris and Thorsten Altenkirch},
title = {Indexed Containers},
year = {2009},
booktitle = {Twenty-Fourth IEEE Symposium in Logic in Computer Science (LICS 2009)},
}
@InCollection{alti:qio,
author = {Thorsten Altenkirch and Alexander Green},
title = {The {Quantum} {IO} {Monad}},
booktitle = {Semantic Techniques in Quantum Computation},
pages={173--205},
publisher = {Cambridge University Press},
year = {2010},
editor = {Simon Gay and Ian McKie},
note = {to appear},
}
@article{alti:fossacs10,
author = {Thorsten Altenkirch and James Chapman and Tarmo Uustalu},
title = {Monads Need Not Be Endofunctors},
journal={Foundations of Software Science and Computational Structures},
pages={297--311},
year={2010},
publisher={Springer}
}
@article{alti:pisigma-new,
author = {Thorsten Altenkirch and Nils Anders Danielsson and Andres L\"oh and Nicolas Oury},
title = {{$\Pi$}{$\Sigma$}: Dependent Types Without the Sugar},
journal={Functional and Logic Programming},
pages={40--55},
year={2010},
publisher={Springer}
}
@conference{txa:mpc2010g,
title={{Subtyping, declaratively; an exercise in mixed induction and coinduction}},
author={Danielsson, Nils Anders and Altenkirch, Thorsten},
booktitle={proceedings of the Tenth International Conference on Mathematics of Program Construction (MPC 10)},
year={2010}
}@article{txa:cie10,
title={{Higher Order Containers}},
author={Altenkirch, Thorsten and Levy, Paul and Staton, Sam},
journal = {Computability in Europe},
year = {2010},
}
@InProceedings{txa:catind2,
author = {Thorsten Altenkirch and Fredrik Nordvall Forsberg and Peter Morris and Anton Setzer},
title = {A categorical semantics for inductive-inductive definitions},
OPTcrossref = {},
OPTkey = {},
booktitle = {CALCO 2011: Fourth International Conference on Algebra and Coalgebra in Computer Science},
OPTpages = {},
year = {2011},
OPTeditor = {},
OPTvolume = {},
OPTnumber = {},
OPTseries = {},
OPTaddress = {},
OPTmonth = {},
OPTorganization = {},
OPTpublisher = {},
note = {to appear},
OPTannote = {}
}
@inproceedings{alti:csl12,
author = {Thorsten Altenkirch and
Ondrej Rypacek},
title = {A Syntactical Approach to Weak omega-Groupoids},
booktitle = Computer Science Logic (CSL'12)},
year = {2012},
pages = {16-30},
ee = {http://dx.doi.org/10.4230/LIPIcs.CSL.2012.16},
}
@inproceedings{alti:tlca13-hedberg,
author = {Nicolai Kraus and
Mart\'{\i}n H{\"o}tzel Escard{\'o} and
Thierry Coquand and
Thorsten Altenkirch},
title = {Generalizations of Hedberg's Theorem},
booktitle = {Typed Lambda Calculi and Applications, 11th International
Conference, TLCA 2013},
year = {2013},
pages = {173-188},
ee = {http://dx.doi.org/10.1007/978-3-642-38946-7_14},
}
@inproceedings{DBLP:conf/tlca/HancockMGMA13,
author = {Peter Hancock and
Conor McBride and
Neil Ghani and
Lorenzo Malatesta and
Thorsten Altenkirch},
title = {Small Induction Recursion},
booktitle = {Typed Lambda Calculi and Applications, 11th International
Conference, TLCA 2013},
year = {2013},
pages = {156-172},
ee = {http://dx.doi.org/10.1007/978-3-642-38946-7_13},
crossref = {DBLP:conf/tlca/2013},
bibsource = {DBLP, http://dblp.uni-trier.de}
}