@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{alti:catind2,
  author    = {Thorsten Altenkirch and
               Peter Morris and
               Fredrik Nordvall Forsberg and
               Anton Setzer},
  title     = {A Categorical Semantics for Inductive-Inductive Definitions},
  booktitle = {CALCO},
  year      = {2011},
  pages     = {70-84},
  ee        = {http://dx.doi.org/10.1007/978-3-642-22944-2_6},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@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{alti:tlca13-small-ir,
  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}
}