@inproceedings{AltenkirchG05,
  title = {A Functional Quantum Programming Language},
  author = {Thorsten Altenkirch and Jonathan Grattage},
  year = {2005},
  doi = {10.1109/LICS.2005.1},
  url = {http://dx.doi.org/10.1109/LICS.2005.1},
  tags = {programming languages, functional programming, programming},
  researchr = {https://researchr.org/publication/AltenkirchG05},
  cites = {0},
  citedby = {0},
  pages = {249-258},
  booktitle = {20th IEEE Symposium on Logic in Computer Science (LICS 2005), 26-29 June 2005, Chicago, IL, USA, Proceedings},
  publisher = {IEEE Computer Society},
  isbn = {0-7695-2266-1},
}

@inproceedings{AltenkirchLS10,
  title = {Higher-Order Containers},
  author = {Thorsten Altenkirch and Paul Levy and Sam Staton},
  year = {2010},
  doi = {10.1007/978-3-642-13962-8_2},
  url = {http://dx.doi.org/10.1007/978-3-642-13962-8_2},
  researchr = {https://researchr.org/publication/AltenkirchLS10},
  cites = {0},
  citedby = {0},
  pages = {11-20},
  booktitle = {Programs, Proofs, Processes, 6th Conference on Computability in Europe, CiE 2010, Ponta Delgada, Azores, Portugal, June 30 - July 4, 2010. Proceedings},
  editor = {Fernando Ferreira and Benedikt Löwe and Elvira Mayordomo and Luís Mendes Gomes},
  volume = {6158},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-642-13961-1},
}

@article{AbbottAMG05,
  title = {for Data: Differentiating Data Structures},
  author = {Michael Abbott and Thorsten Altenkirch and Conor McBride and Neil Ghani},
  year = {2005},
  url = {http://iospress.metapress.com/openurl.asp?genre=article&issn=0169-2968&volume=65&issue=1&spage=1},
  tags = {data-flow},
  researchr = {https://researchr.org/publication/AbbottAMG05},
  cites = {0},
  citedby = {0},
  journal = {Fundamenta Informaticae},
  volume = {65},
  number = {1-2},
  pages = {1-28},
}

@inproceedings{AltenkirchC01,
  title = {A Finitary Subsystem of the Polymorphic lambda-Calculus},
  author = {Thorsten Altenkirch and Thierry Coquand},
  year = {2001},
  url = {http://link.springer.de/link/service/series/0558/bibs/2044/20440022.htm},
  researchr = {https://researchr.org/publication/AltenkirchC01},
  cites = {0},
  citedby = {0},
  pages = {22-28},
  booktitle = {Typed Lambda Calculi and Applications, 5th International Conference, TLCA 2001, Krakow, Poland, May 2-5, 2001, Proceedings},
  editor = {Samson Abramsky},
  volume = {2044},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {3-540-41960-8},
}

@article{GibbonsHA01,
  title = {When is a function a fold or an unfold?},
  author = {Jeremy Gibbons and Graham Hutton and Thorsten Altenkirch},
  year = {2001},
  url = {http://www.elsevier.com/gej-ng/31/29/23/73/23/show/Products/notes/index.htt#008},
  researchr = {https://researchr.org/publication/GibbonsHA01},
  cites = {0},
  citedby = {0},
  journal = {Electronic Notes in Theoretical Computer Science},
  volume = {44},
  number = {1},
  pages = {146-160},
}

@article{MorrisAG09,
  title = {A Universe of Strictly Positive Families},
  author = {Peter Morris and Thorsten Altenkirch and Neil Ghani},
  year = {2009},
  doi = {10.1142/S0129054109006462},
  url = {http://dx.doi.org/10.1142/S0129054109006462},
  researchr = {https://researchr.org/publication/MorrisAG09},
  cites = {0},
  citedby = {0},
  journal = {Int. J. Found. Comput. Sci.},
  volume = {20},
  number = {1},
  pages = {83-107},
}

@article{AbelA02,
  title = {A predicative analysis of structural recursion},
  author = {Andreas Abel and Thorsten Altenkirch},
  year = {2002},
  tags = {analysis},
  researchr = {https://researchr.org/publication/AbelA02},
  cites = {0},
  citedby = {0},
  journal = {Journal of Functional Programming},
  volume = {12},
  number = {1},
  pages = {1-41},
}

@inproceedings{DanielssonA10,
  title = {Subtyping, Declaratively},
  author = {Nils Anders Danielsson and Thorsten Altenkirch},
  year = {2010},
  doi = {10.1007/978-3-642-13321-3_8},
  url = {http://dx.doi.org/10.1007/978-3-642-13321-3_8},
  tags = {subtyping},
  researchr = {https://researchr.org/publication/DanielssonA10},
  cites = {0},
  citedby = {0},
  pages = {100-118},
  booktitle = {Mathematics of Program Construction, 10th International Conference, MPC 2010, Québec City, Canada, June 21-23, 2010. Proceedings},
  editor = {Claude Bolduc and Jules Desharnais and Béchir Ktari},
  volume = {6120},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-642-13320-6},
}

@inproceedings{SwierstraA07,
  title = {Beauty in the beast},
  author = {Wouter Swierstra and Thorsten Altenkirch},
  year = {2007},
  doi = {10.1145/1291201.1291206},
  url = {http://doi.acm.org/10.1145/1291201.1291206},
  tags = {Haskell},
  researchr = {https://researchr.org/publication/SwierstraA07},
  cites = {0},
  citedby = {0},
  pages = {25-36},
  booktitle = {Proceedings of the ACM SIGPLAN Workshop on Haskell, Haskell 2007, Freiburg, Germany, September 30, 2007},
  editor = {Gabriele Keller},
  publisher = {ACM},
  isbn = {978-1-59593-674-5},
}

@inproceedings{AltenkirchMS07,
  title = {Observational equality, now!},
  author = {Thorsten Altenkirch and Conor McBride and Wouter Swierstra},
  year = {2007},
  doi = {10.1145/1292597.1292608},
  url = {http://doi.acm.org/10.1145/1292597.1292608},
  researchr = {https://researchr.org/publication/AltenkirchMS07},
  cites = {0},
  citedby = {0},
  pages = {57-68},
  booktitle = {Proceedings of the ACM Workshop Programming Languages meets Program Verification, PLPV 2007, Freiburg, Germany, October 5, 2007},
  editor = {Aaron Stump and Hongwei Xi},
  publisher = {ACM},
  isbn = {978-1-59593-677-6},
}

@inproceedings{MorrisAM04,
  title = {Exploring the Regular Tree Types},
  author = {Peter Morris and Thorsten Altenkirch and Conor McBride},
  year = {2004},
  doi = {10.1007/11617990_16},
  url = {http://dx.doi.org/10.1007/11617990_16},
  researchr = {https://researchr.org/publication/MorrisAM04},
  cites = {0},
  citedby = {0},
  pages = {252-267},
  booktitle = {Types for Proofs and Programs, International Workshop, TYPES 2004, Jouy-en-Josas, France, December 15-18, 2004, Revised Selected Papers},
  editor = {Jean-Christophe Filliâtre and Christine Paulin-Mohring and Benjamin Werner},
  volume = {3839},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {3-540-31428-8},
}

@inproceedings{AltenkirchDLO10,
  title = {PiSigma: Dependent Types without the Sugar},
  author = {Thorsten Altenkirch and Nils Anders Danielsson and Andres Löh and Nicolas Oury},
  year = {2010},
  doi = {10.1007/978-3-642-12251-4_5},
  url = {http://dx.doi.org/10.1007/978-3-642-12251-4_5},
  researchr = {https://researchr.org/publication/AltenkirchDLO10},
  cites = {0},
  citedby = {0},
  pages = {40-55},
  booktitle = {Functional and Logic Programming, 10th International Symposium, FLOPS 2010, Sendai, Japan, April 19-21, 2010. Proceedings},
  editor = {Matthias Blume and Naoki Kobayashi and Germán Vidal},
  volume = {6009},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-642-12250-7},
}

@inproceedings{Altenkirch93,
  title = {Proving Strong Normalization of CC by Modifying Realizability Semantics},
  author = {Thorsten Altenkirch},
  year = {1993},
  tags = {semantics},
  researchr = {https://researchr.org/publication/Altenkirch93},
  cites = {0},
  citedby = {0},
  pages = {3-18},
  booktitle = {Types for Proofs and Programs, International Workshop TYPES 93, Nijmegen, The Netherlands, May 24-28, 1993, Selected Papers},
  editor = {Henk Barendregt and Tobias Nipkow},
  volume = {806},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {3-540-58085-9},
}

@inproceedings{Altenkirch93:0,
  title = {A Formalization of the Strong Normalization Proof for System F in LEGO},
  author = {Thorsten Altenkirch},
  year = {1993},
  researchr = {https://researchr.org/publication/Altenkirch93%3A0},
  cites = {0},
  citedby = {0},
  pages = {13-28},
  booktitle = {Typed Lambda Calculi and Applications, International Conference on Typed Lambda Calculi and Applications, TLCA  93, Utrecht, The Netherlands, March 16-18, 1993, Proceedings},
  editor = {Marc Bezem and Jan Friso Groote},
  volume = {664},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {3-540-56517-5},
}

@inproceedings{AbbottAGM03,
  title = {Derivatives of Containers},
  author = {Michael Abbott and Thorsten Altenkirch and Neil Ghani and Conor McBride},
  year = {2003},
  url = {http://link.springer.de/link/service/series/0558/bibs/2701/27010016.htm},
  researchr = {https://researchr.org/publication/AbbottAGM03},
  cites = {0},
  citedby = {0},
  pages = {16-30},
  booktitle = {Typed Lambda Calculi and Applications, 6th International Conference, TLCA 2003, Valencia, Spain, June 10-12, 2003, Proceedings},
  editor = {Martin Hofmann},
  volume = {2701},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {3-540-40332-9},
}

@article{AltenkirchU10,
  title = {Preface},
  author = {Thorsten Altenkirch and Tarmo Uustalu},
  year = {2010},
  doi = {10.3233/FI-2010-302},
  url = {http://dx.doi.org/10.3233/FI-2010-302},
  researchr = {https://researchr.org/publication/AltenkirchU10},
  cites = {0},
  citedby = {0},
  journal = {Fundamenta Informaticae},
  volume = {102},
  number = {2},
}

@inproceedings{AltenkirchDHS01,
  title = {Normalization by Evaluation for Typed Lambda Calculus with Coproducts},
  author = {Thorsten Altenkirch and Peter Dybjer and Martin Hofmann and Philip J. Scott},
  year = {2001},
  researchr = {https://researchr.org/publication/AltenkirchDHS01},
  cites = {0},
  citedby = {0},
  pages = {303-310},
  booktitle = {LICS},
}

@inproceedings{AltenkirchHS95,
  title = {Categorical Reconstruction of a Reduction Free Normalization Proof},
  author = {Thorsten Altenkirch and Martin Hofmann and Thomas Streicher},
  year = {1995},
  researchr = {https://researchr.org/publication/AltenkirchHS95},
  cites = {0},
  citedby = {0},
  pages = {182-199},
  booktitle = {Category Theory and Computer Science, 6th International Conference, CTCS  95, Cambridge, UK, August 7-11, 1995, Proceedings},
  editor = {David H. Pitt and David E. Rydeheard and Peter Johnstone},
  volume = {953},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {3-540-60164-3},
}

@inproceedings{AltenkirchCU10,
  title = {Monads Need Not Be Endofunctors},
  author = {Thorsten Altenkirch and James Chapman and Tarmo Uustalu},
  year = {2010},
  doi = {10.1007/978-3-642-12032-9_21},
  url = {http://dx.doi.org/10.1007/978-3-642-12032-9_21},
  researchr = {https://researchr.org/publication/AltenkirchCU10},
  cites = {0},
  citedby = {0},
  pages = {297-311},
  booktitle = {Foundations of Software Science and Computational Structures, 13th International Conference, FOSSACS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings},
  editor = {C.-H. Luke Ong},
  volume = {6014},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-642-12031-2},
}

@article{AltenkirchGVS07,
  title = {An Algebra of Pure Quantum Programming},
  author = {Thorsten Altenkirch and Jonathan Grattage and Juliana Kaizer Vizzotto and Amr Sabry},
  year = {2007},
  doi = {10.1016/j.entcs.2006.12.010},
  url = {http://dx.doi.org/10.1016/j.entcs.2006.12.010},
  tags = { algebra, programming},
  researchr = {https://researchr.org/publication/AltenkirchGVS07},
  cites = {0},
  citedby = {0},
  journal = {Electronic Notes in Theoretical Computer Science},
  volume = {170},
  pages = {23-47},
}

@inproceedings{ChapmanAM05,
  title = {Epigram reloaded: a standalone typechecker for ETT},
  author = {James Chapman and Thorsten Altenkirch and Conor McBride},
  year = {2005},
  researchr = {https://researchr.org/publication/ChapmanAM05},
  cites = {0},
  citedby = {0},
  pages = {79-94},
  booktitle = {Revised Selected Papers from the Sixth Symposium on Trends in Functional Programming, TFP 2005, Tallinn, Estonia, 23-24 September 2005},
  editor = {Marko C. J. D. van Eekelen},
  volume = {6},
  series = {Trends in Functional Programming},
  publisher = {Intellect},
  isbn = {978-1-84150-176-5},
}

@inproceedings{AbbottAG03,
  title = {Categories of Containers},
  author = {Michael Abbott and Thorsten Altenkirch and Neil Ghani},
  year = {2003},
  url = {http://link.springer.de/link/service/series/0558/bibs/2620/26200023.htm},
  researchr = {https://researchr.org/publication/AbbottAG03},
  cites = {0},
  citedby = {0},
  pages = {23-38},
  booktitle = {Foundations of Software Science and Computational Structures, 6th International Conference, FOSSACS 2003 Held as Part of the Joint European Conference on Theory and Practice of Software, ETAPS 2003, Warsaw, Poland, April 7-11, 2003, Proceedings},
  editor = {Andrew D. Gordon},
  volume = {2620},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {3-540-00897-7},
}

@article{VizzottoAS06,
  title = {Structuring quantum effects: superoperators as arrows},
  author = {Juliana Kaizer Vizzotto and Thorsten Altenkirch and Amr Sabry},
  year = {2006},
  doi = {10.1017/S0960129506005287},
  url = {http://dx.doi.org/10.1017/S0960129506005287},
  researchr = {https://researchr.org/publication/VizzottoAS06},
  cites = {0},
  citedby = {0},
  journal = {Mathematical Structures in Computer Science},
  volume = {16},
  number = {3},
  pages = {453-468},
}

@inproceedings{MorrisAG07,
  title = {Constructing Strictly Positive Families},
  author = {Peter Morris and Thorsten Altenkirch and Neil Ghani},
  year = {2007},
  url = {http://crpit.com/abstracts/CRPITV65Morris.html},
  researchr = {https://researchr.org/publication/MorrisAG07},
  cites = {0},
  citedby = {0},
  pages = {111-121},
  booktitle = {Theory of Computing 2007.  Proceedings of the Thirteenth Computing: The Australasian Theory Symposium (CATS2007). January 30 - Febuary 2, 2007, Ballarat, Victoria, Australia, Proceedings},
  editor = {Joachim Gudmundsson and C. Barry Jay},
  volume = {65},
  series = {CRPIT},
  publisher = {Australian Computer Society},
  isbn = {1-920-68246-5},
}

@inproceedings{AbelA99,
  title = {A Predicative Strong Normalisation Proof for a lambda-Calculus with Interleaving Inductive Types},
  author = {Andreas Abel and Thorsten Altenkirch},
  year = {1999},
  url = {http://link.springer.de/link/service/series/0558/bibs/1956/19560021.htm},
  researchr = {https://researchr.org/publication/AbelA99},
  cites = {0},
  citedby = {0},
  pages = {21-40},
  booktitle = {Types for Proofs and Programs, International Workshop TYPES 99, Lökeberg, Sweden, June 12-16, 1999, Selected Papers},
  editor = {Thierry Coquand and Peter Dybjer and Bengt Nordström and Jan M. Smith},
  volume = {1956},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {3-540-41517-3},
}

@inproceedings{AltenkirchU04,
  title = {Normalization by Evaluation for lambda:::-2:::},
  author = {Thorsten Altenkirch and Tarmo Uustalu},
  year = {2004},
  url = {http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=2998&spage=260},
  researchr = {https://researchr.org/publication/AltenkirchU04},
  cites = {0},
  citedby = {0},
  pages = {260-275},
  booktitle = {Functional and Logic Programming, 7th International Symposium, FLOPS 2004, Nara, Japan, April 7-9, 2004, Proceedings},
  editor = {Yukiyoshi Kameyama and Peter J. Stuckey},
  volume = {2998},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {3-540-21402-X},
}

@inproceedings{AltenkirchM02,
  title = {Generic Programming within Dependently Typed Programming},
  author = {Thorsten Altenkirch and Conor McBride},
  year = {2002},
  tags = {generic programming, programming},
  researchr = {https://researchr.org/publication/AltenkirchM02},
  cites = {0},
  citedby = {0},
  pages = {1-20},
  booktitle = {Generic Programming, IFIP TC2/WG2.1 Working Conference on Generic Programming, July 11-12, 2002, Dagstuhl, Germany},
  editor = {Jeremy Gibbons and Johan  Jeuring},
  volume = {243},
  series = {IFIP Conference Proceedings},
  publisher = {Kluwer},
  isbn = {1-4020-7374-7},
}

@inproceedings{AltenkirchM09,
  title = {Indexed Containers},
  author = {Thorsten Altenkirch and Peter Morris},
  year = {2009},
  doi = {10.1109/LICS.2009.33},
  url = {http://dx.doi.org/10.1109/LICS.2009.33},
  researchr = {https://researchr.org/publication/AltenkirchM09},
  cites = {0},
  citedby = {0},
  pages = {277-285},
  booktitle = {Proceedings of the 24th Annual IEEE Symposium on Logic in Computer Science, LICS 2009, 11-14 August 2009, Los Angeles, CA, USA},
  publisher = {IEEE Computer Society},
  isbn = {978-0-7695-3746-7},
}

@inproceedings{AltenkirchR99,
  title = {Monadic Presentations of Lambda Terms Using Generalized Inductive Types},
  author = {Thorsten Altenkirch and Bernhard Reus},
  year = {1999},
  researchr = {https://researchr.org/publication/AltenkirchR99},
  cites = {0},
  citedby = {0},
  pages = {453-468},
  booktitle = {Computer Science Logic, 13th International Workshop, CSL  99, 8th Annual Conference of the EACSL, Madrid, Spain, September 20-25, 1999, Proceedings},
  editor = {Jörg Flum and Mario Rodríguez-Artalejo},
  volume = {1683},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {3-540-66536-6},
}

@article{AbbottAG05,
  title = {Containers: Constructing strictly positive types},
  author = {Michael Abbott and Thorsten Altenkirch and Neil Ghani},
  year = {2005},
  doi = {10.1016/j.tcs.2005.06.002},
  url = {http://dx.doi.org/10.1016/j.tcs.2005.06.002},
  researchr = {https://researchr.org/publication/AbbottAG05},
  cites = {0},
  citedby = {0},
  journal = {Theoretical Computer Science},
  volume = {342},
  number = {1},
  pages = {3-27},
}

@inproceedings{AbbottAG04,
  title = {Representing Nested Inductive Types Using W-Types},
  author = {Michael Abbott and Thorsten Altenkirch and Neil Ghani},
  year = {2004},
  url = {http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=3142&spage=59},
  researchr = {https://researchr.org/publication/AbbottAG04},
  cites = {0},
  citedby = {0},
  pages = {59-71},
  booktitle = {Automata, Languages and Programming: 31st International Colloquium, ICALP 2004, Turku, Finland, July 12-16, 2004. Proceedings},
  editor = {Josep Díaz and Juhani Karhumäki and Arto Lepistö and Donald Sannella},
  volume = {3142},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {3-540-22849-7},
}

@article{GreenA08,
  title = {From Reversible to Irreversible Computations},
  author = {Alexander S. Green and Thorsten Altenkirch},
  year = {2008},
  doi = {10.1016/j.entcs.2008.04.018},
  url = {http://dx.doi.org/10.1016/j.entcs.2008.04.018},
  researchr = {https://researchr.org/publication/GreenA08},
  cites = {0},
  citedby = {0},
  journal = {Electronic Notes in Theoretical Computer Science},
  volume = {210},
  pages = {65-74},
}

@inproceedings{AltenkirchHS96:0,
  title = {Reduction-Free Normalisation for a Polymorphic System},
  author = {Thorsten Altenkirch and Martin Hofmann and Thomas Streicher},
  year = {1996},
  researchr = {https://researchr.org/publication/AltenkirchHS96%3A0},
  cites = {0},
  citedby = {0},
  pages = {98-106},
  booktitle = {LICS},
}

@inproceedings{Altenkirch01,
  title = {Representations of First Order Function Types as Terminal Coalgebras},
  author = {Thorsten Altenkirch},
  year = {2001},
  url = {http://link.springer.de/link/service/series/0558/bibs/2044/20440008.htm},
  researchr = {https://researchr.org/publication/Altenkirch01},
  cites = {0},
  citedby = {0},
  pages = {8-21},
  booktitle = {Typed Lambda Calculi and Applications, 5th International Conference, TLCA 2001, Krakow, Poland, May 2-5, 2001, Proceedings},
  editor = {Samson Abramsky},
  volume = {2044},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {3-540-41960-8},
}

@inproceedings{AbbottAGM04,
  title = {Constructing Polymorphic Programs with Quotient Types},
  author = {Michael Abbott and Thorsten Altenkirch and Neil Ghani and Conor McBride},
  year = {2004},
  url = {http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=3125&spage=2},
  researchr = {https://researchr.org/publication/AbbottAGM04},
  cites = {0},
  citedby = {0},
  pages = {2-15},
  booktitle = {Mathematics of Program Construction, 7th International Conference, MPC 2004, Stirling, Scotland, UK, July 12-14, 2004, Proceedings},
  editor = {Dexter Kozen and Carron Shankland},
  volume = {3125},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {3-540-22380-0},
}

@article{AltenkirchC09,
  title = {Big-step normalisation},
  author = {Thorsten Altenkirch and James Chapman and   and  },
  year = {2009},
  doi = {10.1017/S0956796809007278},
  url = {http://dx.doi.org/10.1017/S0956796809007278},
  researchr = {https://researchr.org/publication/AltenkirchC09},
  cites = {0},
  citedby = {0},
  journal = {Journal of Functional Programming},
  volume = {19},
  number = {3-4},
  pages = {311-333},
}

@inproceedings{AltenkirchHS96,
  title = {Reduction-Free Normalisation for a Polymorphic System},
  author = {Thorsten Altenkirch and Martin Hofmann and Thomas Streicher},
  year = {1996},
  researchr = {https://researchr.org/publication/AltenkirchHS96},
  cites = {0},
  citedby = {0},
  pages = {146},
  booktitle = {ISTCS},
}

@inproceedings{Altenkirch99,
  title = {Extensional Equality in Intensional Type Theory},
  author = {Thorsten Altenkirch},
  year = {1999},
  url = {http://computer.org/conferen/proceed/lics/0158/01580412abs.htm},
  tags = {type theory},
  researchr = {https://researchr.org/publication/Altenkirch99},
  cites = {0},
  citedby = {0},
  pages = {412-420},
  booktitle = {Proceedings, 14th Annual IEEE Symposium on Logic in Computer Science, 2-5 July, 1999, Trento, Italy},
  publisher = {IEEE Computer Society},
}

@inproceedings{Altenkirch98,
  title = {Logical Relations and Inductive/Coinductive Types},
  author = {Thorsten Altenkirch},
  year = {1998},
  researchr = {https://researchr.org/publication/Altenkirch98},
  cites = {0},
  citedby = {0},
  pages = {343-354},
  booktitle = {Computer Science Logic, 12th International Workshop, CSL  98, Annual Conference of the EACSL, Brno, Czech Republic, August 24-28, 1998, Proceedings},
  editor = {Georg Gottlob and Etienne Grandjean and Katrin Seyr},
  volume = {1584},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {3-540-65922-6},
}
@proceedings{types:2006,
  title = {Types for Proofs and Programs, International Workshop, TYPES 2006, Nottingham, UK, April 18-21, 2006, Revised Selected Papers},
  year = {2007},
  researchr = {https://researchr.org/publication/types%3A2006},
  cites = {0},
  citedby = {0},
  booktitle = {Types for Proofs and Programs, International Workshop, TYPES 2006, Nottingham, UK, April 18-21, 2006, Revised Selected Papers},
  conference = {TYPES},
  editor = {Thorsten Altenkirch and Conor McBride},
  volume = {4502},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-540-74463-4},
}

@proceedings{types:1998,
  title = {Types for Proofs and Programs, International Workshop TYPES  98, Kloster Irsee, Germany, March 27-31, 1998, Selected Papers},
  year = {1999},
  researchr = {https://researchr.org/publication/types%3A1998},
  cites = {0},
  citedby = {0},
  booktitle = {Types for Proofs and Programs, International Workshop TYPES  98, Kloster Irsee, Germany, March 27-31, 1998, Selected Papers},
  conference = {TYPES},
  editor = {Thorsten Altenkirch and Wolfgang Naraschewski and Bernhard Reus},
  volume = {1657},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {3-540-66537-4},
}

@proceedings{plpv-2009,
  title = {Proceedings of the 3rd ACM Workshop Programming Languages meets Program Verification, PLPV 2009, Savannah, GA, USA, January 20, 2009},
  year = {2009},
  tags = {programming languages, program verification, programming},
  researchr = {https://researchr.org/publication/plpv-2009},
  cites = {0},
  citedby = {0},
  booktitle = {Proceedings of the 3rd ACM Workshop Programming Languages meets Program Verification, PLPV 2009, Savannah, GA, USA, January 20, 2009},
  conference = {plpv},
  editor = {Thorsten Altenkirch and Todd D. Millstein},
  publisher = {ACM},
  isbn = {978-1-60558-330-3},
}