@misc{coq,
  title={{The {\sc Coq} proof assistant}},
  key={Coq},
  note={http://coq.inria.fr}
}

@conference{reynolds:defints1972,
  author    = {John C. Reynolds},
  title     = {Definitional interpreters for higher-order programming languages},
  booktitle = {{Proceedings of the ACM Annual Conference}},
  year      = {1972},
  month     = {august},
  pages     = {717--740},
  volume    = {2},
  publisher = {ACM, New York},
  note      = {Republié en tant que \cite[reynolds:defints].}
}

@article{reynolds:defints,
  title={{Definitional interpreters for higher-order programming languages}},
  author={Reynolds, J.C.},
  journal={Higher-order and symbolic computation},
  volume={11},
  number={4},
  pages={363--397},
  issn={1388-3690},
  year={1998},
  publisher={Springer}
}

@book{gordon:holbook,
  title={{Introduction to HOL: A theorem proving environment for higher order logic}},
  author={Gordon, M. and Melham, T.},
  year={1993},
  publisher={Cambridge University Press New York, NY, USA}
}

@unpublished{geuvers:gammainf,
  author = {Herman Geuvers and James McKinna and Freek Wiedijk},
  title = {{Pure Type Systems without Explicit Contexts}},
  month = {january},
  year = {2009},
  note = {Submitted}
}

@conference{maranget:cpm,
  title={{Compiling pattern matching to good decision trees}},
  author={Maranget, L.},
  booktitle={Proceedings of the 2008 ACM SIGPLAN workshop on ML},
  pages={35--46},
  year={2008},
  organization={ACM New York, NY, USA}
}