finite-dtypes.bib

@Misc{whatwg,
  author =	 {{WHATWG}},
  title =	 {{HTML} Living Standard},
  howpublished = {\url{https://html.spec.whatwg.org/}},
}

@Misc{loc,
  author =	 {C. Gagliardi},
  title =	 {Count lines of code quickly},
  howpublished = {\url{https://github.com/cgag/loc}},
}

@Misc{webidl,
  author =	 {C. McCormack and B. Zbarsky and T. Langel and others},
  title =	 {Web {IDL}},
  howpublished = {\url{https://heycam.github.io/webidl/}},
}

@Misc{servo.org,
  author = 	 {The Servo Project Developers},
  title =	 {Servo, the Parallel Browser Engine Project},
  howpublished = {\url{https://servo.org/}},
}

@Misc{crates.io,
  author =	 {The Rust Community},
  title =	 {Rust Package Registry},
  howpublished = {\url{https://crates.io/}},
}

@Misc{racket-lang.org,
  author =	 {The Racket Community},
  title =	 {Racket: Solve Problems, Make Languages},
  howpublished = {\url{https://racket-lang.org/}},
}

@Misc{semver.org,
  author =	 {T. Preston-Werner},
  title =	 {Semantic Versioning 2.0.0},
  howpublished = {\url{http://semver.org/}},
}

@Misc{agda,
  author =	 {U. Norell and N. A. Danielsson and A. Abel and others},
  title =	 {Agda},
  howpublished = {\url{http://wiki.portal.chalmers.se/agda}},
}

@Book{coq,
  author = 	 {Yves Bertot and Pierre Cast\'eran},
  title = 	 {Interactive Theorem Proving and Program Development: Coq'Art: The Calculus of Inductive Constructions},
  publisher = 	 {Springer},
  year = 	 {2004},
}

@Book{idris,
  author =	 {E. Brady},
  title = 	 {Type-Driven Development with {Idris}},
  publisher = 	 {Manning},
  year = 	 {2017},
}

@Book{hott,
  author =    {The {Univalent Foundations Program}},
  title =     {Homotopy Type Theory: Univalent Foundations of Mathematics},
  publisher = {\url{https://homotopytypetheory.org/book}},
  address =   {Institute for Advanced Study},
  year =      2013}
  
@Misc{rust-book,
  author =	 {The Rust Project Developers},
  title =	 {The {Rust} Programming Language, 1st ed},
  howpublished = {\url{https://doc.rust-lang.org/book/first-edition/}},
  year =	 {2011},
}

@Misc{rfcs,
  author =	 {The Rust Community},
  title =	 {Rust {RFC}s},
  howpublished = {\url{http://rust-lang.github.io/rfcs/}},
}

@inproceedings{CHAGN07,
 author = {Condit, J. and Harren, M. and Anderson, Z. and Gay, D. and Necula, G. C.},
 title = {Dependent Types for Low-level Programming},
 booktitle = {Proc. Euro. Symp. Programming},
 year = {2007},
 pages = {520--535},
} 

@inproceedings{AM03,
 author = {T. Altenkirch and C. McBride},
 title = {Generic Programming Within Dependently Typed Programming},
 booktitle = {Proc. {IFIP TC2/WG2.1} Generic Programming},
 year = {2003},
 pages = {1--20},
} 

@InProceedings{Chl10,
  author = 	 {Adam Chlipala},
  title = 	 {Ur: Statically-Typed Metaprogramming with Type-Level Record Computation},
  booktitle =	 {Proc. {ACM} Programming Language Design and Implementation},
  year =	 {2010},
  pages =	 {122--133},
}

@inproceedings{McQ86,
 author = {MacQueen, D. B.},
 title = {Using Dependent Types to Express Modular Structure},
 booktitle = {Proc. ACM Sympo. Principles of Programming Languages},
 year = {1986},
 pages = {277--286},
} 

@inproceedings{HMM90,
 author = {Harper, R. and Mitchell, J. C. and Moggi, E.},
 title = {Higher-order Modules and the Phase Distinction},
 booktitle = {Proc. ACM Symp. Principles of Programming Languages},
 year = {1990},
 pages = {341--354},
} 

@article{Har93,
 author = {Harper, R. and Mitchell, J. C.},
 title = {On the Type Structure of {Standard ML}},
 journal = {ACM Trans. Program. Lang. Syst.},
 volume = {15},
 number = {2},
 year = {1993},
 pages = {211--252},
} 

@Misc{self,
  author =	 {A. S. A. Jeffrey},
  title =	 {Thoughts on Finite Dependent Types},
  howpublished = {\url{https://github.com/asajeffrey/finite-dtypes}},
}

@Article{AP16,
  author =       {A. Abel and B. Pientka},
  title =        {Well-founded recursion with copatterns and sized types},
  journal =      {J. Functional Programming},
  year =         {2016},
  volume =       {26},
}

@InProceedings{FGGvW18,
  author =       {D. Frumin and H. Geuvers and L. Gondelman and N. van der Weide},
  title =        {Finite Sets in Homotopy Type Theory},
  year =         {2018},
  note =         {Submitted for publication},
}