-@article{Chapman2010,
-address = {New York, New York, USA},
-author = {Chapman, James and Dagand, Pierre-\'{E}variste and McBride, Conor and Morris, Peter},
-doi = {10.1145/1863543.1863547},
-file = {:home/bitonic/docs/papers/conor-levitation.pdf:pdf},
-isbn = {9781605587943},
-journal = {Proceedings of the 15th ACM SIGPLAN international conference on Functional programming - ICFP '10},
-pages = {3},
-publisher = {ACM Press},
-title = {{The gentle art of levitation}},
-url = {http://portal.acm.org/citation.cfm?doid=1863543.1863547},
-year = {2010}
-}
-@phdthesis{Norell2007,
-author = {Norell, Ulf},
-file = {:home/bitonic/docs/papers/ulf-thesis.pdf:pdf},
-isbn = {9789172919969},
-school = {Chalmers University of Technology and G\"{o}teborg University},
-title = {{Towards a practical programming language based on dependent type theory}},
-url = {http://www.cse.chalmers.se/~ulfn/papers/thesis.pdf},
-year = {2007}
-}
-@article{Coquand1986,
-author = {Coquand, Thierry and Huet, Gerard},
-file = {:home/bitonic/docs/papers/coc.pdf:pdf},
-title = {{The calculus of constructions}},
-url = {http://hal.inria.fr/docs/00/07/60/24/PDF/RR-0530.pdf},
-year = {1986}
-}
-@article{Reynolds1994,
-author = {Reynolds, John C.},
-file = {:home/bitonic/docs/papers/reynolds-polymorphic-lc.ps:ps},
-journal = {Logical Foundations of Functional Programming},
-title = {{An introduction to the polymorphic lambda calculus}},
-url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.7.9916\&rep=rep1\&type=pdf},
-year = {1994}
-}
-@article{Brady2012,
-author = {Brady, Edwin},
-file = {:home/bitonic/docs/papers/idris-implementation.pdf:pdf},
-journal = {Unpublished draft},
-number = {November},
-title = {{Implementing General Purpose Dependently Typed Programming Languages}},
-url = {http://www.cs.st-andrews.ac.uk/~eb/drafts/impldtp.pdf},
-year = {2012}
-}
-@article{Church1936,
-author = {Church, Alonzo},
-file = {:home/bitonic/docs/papers/church-lc.pdf:pdf},
-journal = {American journal of mathematics},
-number = {2},
-pages = {345--363},
-title = {{An unsolvable problem of elementary number theory}},
-url = {http://www.ams.org/leavingmsn?url=http://dx.doi.org/10.2307/2371045},
-volume = {58},
-year = {1936}
-}
-@article{Altenkirch2010,
-author = {Altenkirch, Thorsten and Danielsson, N and L\"{o}h, A and Oury, Nicolas},
-file = {:home/bitonic/docs/papers/PiSigma.pdf:pdf},
-journal = {Functional and Logic \ldots},
-number = {Sheard 2005},
-title = {{$\Pi$$\Sigma$: dependent types without the sugar}},
-url = {http://www.springerlink.com/index/91W712G2806R575H.pdf},
-year = {2010}