@misc(BlanquiCoLoR,
 author       = {Fr\IeC{\'e}d\IeC{\'e}ric Blanqui},
 title        = {CoLoR, a Coq Library on Rewriting and Termination},
 url          = {http://color.inria.fr},
)
@misc(coquand92baastad,
 author       = {Thierry Coquand},
 year         = {1992},
 title        = {Pattern Matching with Dependent Types},
 url          = {http://www.cs.chalmers.se/~coquand/pattern.ps},
 note         = {Proceedings of the Workshop on Logical Frameworks},
)
@phdthesis(eades2014semantic,
 author       = {Eades III, Harley D},
 year         = {2014},
 title        = {The semantic analysis of advanced programming languages},
 school       = {The University of Iowa},
 url          = {http://metatheorem.org/wp-content/papers/thesis.pdf},
)
@misc(goguen2006,
 author       = {Healfdene Goguen, Conor McBride and James McKinna},
 year         = {2006},
 title        = {Eliminating Dependent Pattern Matching},
 url          = {http://cs.ru.nl/~james/RESEARCH/goguen2006.pdf},
)
@conference(eadespstt10,
 author       = {Harley D. Eades III and Aaron Stump},
 year         = {2010},
 title        = {{Hereditary Substitution for Stratified System F}},
 booktitle    = {International Workshop on Proof-Search in Type Theories},
 organization = {A FLoC workshop},
 address      = {Edinburgh, Scotland},
 url          = {http://homepage.divms.uiowa.edu/~astump/papers/pstt-2010.pdf},
)
@techreport(leivant90,
 author       = {Daniel Leivant},
 year         = {1990},
 title        = {Finitely stratified polymorphism},
 type         = {Technical Report},
 institution  = {Carnegie Mellon University},
 url          = {http://repository.cmu.edu/cgi/viewcontent.cgi?article=2961\&context=compsci},
)
@conference(DBLP:conf/itp/MalechaCB14,
 author       = {Gregory Malecha and Adam Chlipala and Thomas Braibant},
 year         = {2014},
 title        = {Compositional Computational Reflection},
 editor       = {Gerwin Klein and Ruben Gamboa},
 booktitle    = {ITP'14},
 series       = {Lecture Notes in Computer Science},
 volume       = {8558},
 publisher    = {Springer},
 pages        = {374--389},
 doi          = {10.1007/978-3-319-08970-6\_24},
)
@article(epigram:pratprog,
 author       = {Conor McBride},
 year         = {2005},
 title        = {Epigram: {P}ractical {P}rogramming with {D}ependent {T}ypes},
 journal      = {Advanced Functional Programming},
 pages        = {130--170},
 doi          = {10.1007/11546382\_3},
)
@phdthesis(norell:thesis,
 author       = {Ulf Norell},
 year         = {2007},
 title        = {Towards a practical programming language based on dependent type theory},
 school       = {Department of Computer Science and Engineering, Chalmers University of Technology},
 address      = {SE-412 96 G\"{o}teborg, Sweden},
 url          = {http://www.cs.chalmers.se/~ulfn/papers/thesis.html},
)
@conference(sozeau10,
 author       = {Matthieu Sozeau},
 year         = {2010},
 title        = {Equations: A Dependent Pattern-Matching Compiler},
 booktitle    = {First International Conference on Interactive Theorem Proving},
 publisher    = {Springer},
 doi          = {10.1007/978-3-642-14052-5\_29},
)
@misc(vouillonpoplmark,
 author       = {J\IeC{\'e}r\IeC{\^o}me Vouillon},
 title        = {POPLmark challenge solution},
 url          = {http://www.seas.upenn.edu/~plclub/poplmark/vouillon.html},
)