weirich.bib

@phdthesis{abel_2013,
  title  = {{Normalization by Evaluation: Dependent Types and Impredicativity}},
  author = {Abel, Andreas},
  year   = {2013},
  type   = {Habilitation thesis},
  school = {Ludwig-Maximilians-Universität München},
  url    = {http://www.cse.chalmers.se/~abela/habil.pdf}
}

@article{abel-scherer,
  title     = {{On Irrelevance and Algorithmic Equality in Predicative Type Theory}},
  author    = {Andreas Abel and Gabriel Scherer},
  year      = 2012,
  journal   = {Logical Methods in Computer Science},
  editor    = {Pawel Urzyczyn},
  publisher = {Logical Methods in Computer Science e.V.},
  volume    = {8},
  number    = {1},
  doi       = {10.2168/lmcs-8(1:29)2012}
}

@inproceedings{atkey,
  title     = {{Syntax and Semantics of Quantitative Type Theory}},
  author    = {Atkey, Robert},
  year      = {2018},
  booktitle = {Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science},
  publisher = {Association for Computing Machinery},
  address   = {New York, NY, USA},
  location  = {Oxford, United Kingdom},
  series    = {LICS '18},
  pages     = {56--65},
  numpages  = {10},
  doi       = {10.1145/3209108.3209189},
  keywords  = {Linear Logic, Type Theory},
  isbn      = {9781450355834}
}

@misc{augustsson:tutorial,
  title  = {{Simpler, Easier!}},
  author = {Lennart Augustsson},
  year   = 2007,
  note   = {Available from \url{https://augustss.blogspot.com/2007/10/simpler-easier-in-recent-paper-simply.html}}
}

@inbook{barendregt:lambda-calculi-with-types,
  title     = {{Lambda Calculi with Types}},
  author    = {Barendregt, H. P.},
  year      = {1993},
  booktitle = {Handbook of Logic in Computer Science (Vol. 2): Background: Computational Structures},
  publisher = {Oxford University Press, Inc.},
  address   = {USA},
  pages     = {117--309},
  numpages  = {193},
  isbn      = {0198537611}
}

@misc{bauer:tutorial,
  title  = {{How to implement dependent type theory}},
  author = {Andrej Bauer},
  year   = 2012,
  note   = {Available from {\url{http://math.andrej.com/2012/11/08/how-to-implement-dependent-type-theory-i/}}}
}

@techreport{cardelli:1986,
  title       = {{A Polymorphic $\lambda$ Calculus with Type:Type}},
  author      = {Luca Cardelli},
  year        = {1986},
  institution = {Digital Equipment Corporation, SRC},
  number      = {10},
  url         = {http://www.hpl.hp.com/techreports/Compaq-DEC/SRC-RR-10.pdf}
}

@inproceedings{choudhury:ddc,
  title     = {{A Dependent Dependency Calculus}},
  author    = {Choudhury, Pritam and Eades III, Harley and Weirich, Stephanie},
  year      = {2022},
  booktitle = {Programming Languages and Systems, ESOP 2022},
  editor    = {Sergey, Ilya},
  publisher = {Springer International Publishing},
  address   = {Cham},
  series    = {Lecture Notes in Computer Science},
  volume    = 13240,
  pages     = {403--430},
  doi       = {10.1007/978-3-030-99336-8_15},
  url       = {https://github.com/sweirich/graded-haskell},
  isbn      = {978-3-030-99336-8},
  plclub    = yes
}

@misc{christiansen:tutorial-bidirectional,
  title        = {{Bidirectional Typing Rules: A Tutorial}},
  author       = {David Raymond Christiansen},
  year         = 2013,
  howpublished = {Tutorial},
  url          = {http://davidchristiansen.dk/tutorials/bidirectional.pdf}
}

@techreport{Coc,
  title       = {{The calculus of constructions}},
  author      = {Coquand, T. and Huet, G{\'e}rard},
  year        = {1986},
  institution = {{INRIA}},
  number      = {RR-0530},
  url         = {https://hal.inria.fr/inria-00076024},
  pdf         = {https://hal.inria.fr/inria-00076024/file/RR-0530.pdf},
  hal_id      = {inria-00076024},
  hal_version = {v1}
}

@incollection{coquand:tutorial,
  title     = {{A simple type-theoretic language: Mini-TT}},
  author    = {Coquand, Thierry and Kinoshita, Yoshiki and Nordström, Bengt and Takeyama, Makoto},
  year      = 2009,
  booktitle = {From Semantics to Computer Science: Essays in Honour of Gilles Kahn},
  editor    = {Bertot, Yves and Huet, Gérard and Lévy, Jean-Jacques and Plotkin, Gordon},
  publisher = {Cambridge University Press},
  pages     = {139--164},
  doi       = {10.1017/CBO9780511770524.007},
  place     = {Cambridge}
}

@article{debruijn,
  title         = {{Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem}},
  author        = {de Bruijn, Nicolaas Govert},
  year          = {1972},
  journal       = {Indagationes Mathematicae (Proceedings)},
  publisher     = {Elsevier BV},
  volume        = {75},
  number        = {5},
  pages         = {381--392},
  doi           = {10.1016/1385-7258(72)90034-0},
  timestamp     = {2015.05.08},
  __markedentry = {[rae:6]},
  issn          = {1385-7258},
  owner         = {rae}
}

@article{dunfield:bidirectional-survey,
  title      = {{Bidirectional Typing}},
  author     = {Dunfield, Jana and Krishnaswami, Neel},
  year       = {2021},
  journal    = {ACM Comput. Surv.},
  publisher  = {Association for Computing Machinery},
  address    = {New York, NY, USA},
  volume     = {54},
  number     = {5},
  numpages   = {38},
  doi        = {10.1145/3450952},
  keywords   = {Type checking, type inference},
  issue_date = {June 2022},
  issn       = {0360-0300},
  articleno  = {98}
}

@inproceedings{gregoire:strong-reduction,
  title     = {{A Compiled Implementation of Strong Reduction}},
  author    = {Gr\'{e}goire, Benjamin and Leroy, Xavier},
  year      = {2002},
  booktitle = {Proceedings of the Seventh ACM SIGPLAN International Conference on Functional Programming},
  publisher = {Association for Computing Machinery},
  address   = {New York, NY, USA},
  location  = {Pittsburgh, PA, USA},
  series    = {ICFP '02},
  pages     = {235--246},
  numpages  = {12},
  doi       = {10.1145/581478.581501},
  keywords  = {beta-equivalence, calculus of constructions, virtual machine, abstract machine, Coq, strong reduction, normalization by evaluation},
  isbn      = {1581134878}
}

@inproceedings{icc-star,
  title     = {{The Implicit Calculus of Constructions as a Programming Language with Dependent Types}},
  author    = {Barras, Bruno and Bernardo, Bruno},
  year      = {2008},
  booktitle = {Foundations of Software Science and Computational Structures},
  editor    = {Amadio, Roberto},
  publisher = {Springer Berlin Heidelberg},
  address   = {Berlin, Heidelberg},
  pages     = {365--379},
  doi       = {10.1007/978-3-540-78499-9_26}
}

@inproceedings{idris2,
  title     = {{Idris 2: Quantitative Type Theory in Practice}},
  author    = {Edwin C. Brady},
  year      = {2021},
  booktitle = {35th European Conference on Object-Oriented Programming, {ECOOP} 2021, July 11-17, 2021, Aarhus, Denmark (Virtual Conference)},
  editor    = {Anders M{\o}ller and Manu Sridharan},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  series    = {LIPIcs},
  volume    = {194},
  pages     = {9:1--9:26},
  doi       = {10.4230/LIPIcs.ECOOP.2021.9},
  timestamp = {Sun, 25 Jul 2021 11:47:10 +0200},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  biburl    = {https://dblp.org/rec/conf/ecoop/Brady21.bib}
}

@misc{kovacs:tutorial,
  title        = {{Elaboration Zoo}},
  author       = {Andras Kovacs},
  howpublished = 2022,
  note         = {\url{https://github.com/AndrasKovacs/elaboration-zoo/}}
}

@article{loeh:tutorial,
  title   = {{A Tutorial Implementation of a Dependently Typed Lambda Calculus}},
  author  = {Löh, Andres and McBride, Conor and Swierstra, Wouter},
  year    = {2010},
  journal = {Fundam. Inform.},
  volume  = {102},
  pages   = {177--207},
  doi     = {10.3233/FI-2010-304},
  note    = {Available from \url{http://www.andres-loeh.de/LambdaPi/}}
}

@phdthesis{luo-ecc,
  title  = {{An Extended Calculus of Constructions}},
  author = {Luo, Zhaohui},
  year   = {1990},
  school = {University of Edinburgh},
  url    = {http://hdl.handle.net/1842/12487}
}

@unpublished{martin-lof71,
  title  = {{A Theory of Types}},
  author = {Per Martin-L\"of},
  year   = 1971,
  note   = {Preprint, Stockholm University},
  url    = {https://raw.githubusercontent.com/michaelt/martin-lof/master/pdfs/martin-loef1971%20-%20A%20Theory%20of%20Types.pdf}
}

@incollection{martin-lof73,
  title      = {{An intuitionistic theory of types: predicative part}},
  author     = {Martin-L{\"o}f, Per},
  year       = 1975,
  booktitle  = {Logic Colloquium '73, Proceedings of the Logic Colloquium},
  editor     = {H.E. Rose and J.C. Shepherdson},
  publisher  = {North-Holland},
  series     = {Studies in Logic and the Foundations of Mathematics},
  volume     = 80,
  pages      = {73--118},
  mrclass    = {02C15 (02D99)},
  mrnumber   = {0387009 (52 \#7856)},
  mrreviewer = {Horst Luckhardt},
  doi        = {10.1016/S0049-237X(08)71945-1}
}

@inproceedings{miquel,
  title     = {{The Implicit Calculus of Constructions Extending Pure Type Systems with an Intersection Type Binder and Subtyping}},
  author    = {Miquel, Alexandre},
  year      = {2001},
  booktitle = {Typed Lambda Calculi and Applications},
  editor    = {Abramsky, Samson},
  publisher = {Springer Berlin Heidelberg},
  address   = {Berlin, Heidelberg},
  pages     = {344--359},
  doi       = {10.1007/3-540-45413-6_27}
}

@inproceedings{mishra-linger:epts,
  title     = {{Erasure and Polymorphism in Pure Type Systems}},
  author    = {Mishra-Linger, Nathan and Sheard, Tim},
  year      = {2008},
  booktitle = {Proceedings of the Theory and Practice of Software, 11th International Conference on Foundations of Software Science and Computational Structures},
  publisher = {Springer-Verlag},
  address   = {Berlin, Heidelberg},
  location  = {Budapest, Hungary},
  series    = {FOSSACS'08/ETAPS'08},
  pages     = {350--364},
  numpages  = {15},
  doi       = {10.1007/978-3-540-78499-9_25}
}

@inproceedings{ott,
  title     = {{Ott: Effective Tool Support for the Working Semanticist}},
  author    = {Sewell, Peter and Nardelli, Francesco Zappa and Owens, Scott and Peskine, Gilles and Ridge, Thomas and Sarkar, Susmit and Strni\v{s}a, Rok},
  year      = {2007},
  booktitle = {Proceedings of the 12th ACM SIGPLAN International Conference on Functional Programming},
  publisher = {Association for Computing Machinery},
  address   = {New York, NY, USA},
  location  = {Freiburg, Germany},
  series    = {ICFP '07},
  pages     = {1--12},
  numpages  = {12},
  doi       = {10.1145/1291151.1291155},
  isbn      = {9781595938152}
}

@inproceedings{pfenning:2001,
  title     = {{Intensionality, Extensionality, and Proof Irrelevance in Modal Type Theory}},
  author    = {Pfenning, Frank},
  year      = {2001},
  booktitle = {Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science},
  publisher = {IEEE Computer Society},
  address   = {Washington, DC, USA},
  series    = {LICS '01},
  pages     = {221--230},
  url       = {https://www.cs.cmu.edu/~fp/papers/lics01.pdf},
  doi       = {10.1109/LICS.2001.932499}
}

@book{pfpl,
  title     = {{Practical Foundations for Programming Languages}},
  edition   = {2nd},
  author    = {Harper, Robert},
  year      = {2016},
  publisher = {Cambridge University Press},
  address   = {USA},
  isbn      = {1107150302}
}

@article{pierce:lti,
  title      = {{Local Type Inference}},
  author     = {Pierce, Benjamin C. and Turner, David N.},
  year       = {2000},
  journal    = {ACM Trans. Program. Lang. Syst.},
  publisher  = {ACM},
  address    = {New York, NY, USA},
  volume     = {22},
  number     = {1},
  pages      = {1--44},
  numpages   = {44},
  doi        = {10.1145/345099.345100},
  keywords   = {polymorphism, subtyping, type inference},
  issue_date = {Jan. 2000},
  issn       = {0164-0925},
  acmid      = {345100}
}

@article{practical-type-inference,
  title   = {{Practical type inference for arbitrary-rank types}},
  author  = {{Peyton Jones}, Simon and Dimitrios Vytiniotis and Stephanie Weirich and Mark Shields},
  year    = {2007},
  journal = {Journal of Functional Programming},
  volume  = {17},
  number  = {1},
  doi     = {10.1017/S0956796806006034}
}

@misc{rompf:tutorial,
  title  = {{Implementing Dependent Types}},
  author = {Tiark Rompf},
  year   = 2020,
  note   = {Available from {\url{https://tiarkrompf.github.io/notes/?/dependent-types/}}}
}

@inproceedings{steele:ppop17,
  title     = {{It's Time for a New Old Language}},
  author    = {Steele, Guy L.},
  year      = {2017},
  booktitle = {Proceedings of the 22nd ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming},
  publisher = {Association for Computing Machinery},
  address   = {New York, NY, USA},
  location  = {Austin, Texas, USA},
  series    = {PPoPP '17},
  pages     = {1},
  numpages  = {1},
  doi       = {10.1145/3018743.3018773},
  keywords  = {programming languages, specifications, compilers},
  isbn      = {9781450344937}
}

@book{tapl,
  title     = {{Types and Programming Languages}},
  edition   = {1st},
  author    = {Pierce, Benjamin C.},
  year      = {2002},
  publisher = {The MIT Press},
  isbn      = {0262162091}
}

@inproceedings{vytiniotis2006simple,
  title        = {{Simple unification-based type inference for GADTs}},
  author       = {Vytiniotis, Dimitrios and Weirich, Stephanie and Peyton Jones, Simon},
  year         = {2006},
  booktitle    = {International Conference on Functional Programming (ICFP'06)},
  url          = {https://www.microsoft.com/en-us/research/publication/simple-unification-based-type-inference-for-gadts/},
  note         = {2016 ACM SIGPLAN Most Influential ICFP Paper Award},
  doi          = {10.1145/1159803.1159811},
  organization = {ACM SIGPLAN}
}

@article{vytiniotis2011outsidein,
  title     = {{OutsideIn(X): Modular type inference with local assumptions}},
  edition   = {Journal of Functional Programming},
  author    = {Vytiniotis, Dimitrios and Peyton Jones, Simon and Schrijvers, Tom and Sulzmann, Martin},
  year      = {2011},
  journal   = {Journal of Functional Programming},
  publisher = {Cambridge University Press},
  volume    = {21},
  pages     = {333--412},
  doi       = {10.1017/S0956796811000098}
}

@article{weirich:systemd,
  title      = {{A Specification for Dependent Types in Haskell}},
  author     = {Weirich, Stephanie and Voizard, Antoine and de Amorim, Pedro Henrique Avezedo and Eisenberg, Richard A.},
  year       = {2017},
  journal    = {Proc. ACM Program. Lang.},
  publisher  = {ACM},
  address    = {New York, NY, USA},
  volume     = {1},
  number     = {ICFP},
  pages      = {31:1--31:29},
  numpages   = {29},
  doi        = {10.1145/3110275},
  keywords   = {Dependent Types, Haskell},
  issue_date = {September 2017},
  issn       = {2475-1421},
  articleno  = {31},
  acmid      = {3110275},
  plclub     = {yes}
}