year = {2002}
}
+@inbook{Queinnec2003,
+ author = {Christian Queinnec},
+ title = {Lisp in Small Pieces},
+ publisher = {Cambridge University Press},
+ year = {2003},
+}
+
@online{Coq,
author = {{The Coq Team}},
title = {The Coq Proof Assistant},
publisher = Prentice-Hall
}
-
@article{Altenkirch2010,
-author = {Altenkirch, Thorsten and Danielsson, N and L\"{o}h, A and Oury, Nicolas},
+author = {Altenkirch, Thorsten and Danielsson, Nils Anders and L\"{o}h, Andres and Oury, Nicolas},
file = {:home/bitonic/docs/papers/PiSigma.pdf:pdf},
-journal = {Functional and Logic \ldots},
-number = {Sheard 2005},
+journal = {Functional and Logic Programming},
+pages = {40--55},
title = {{$\Pi$$\Sigma$: dependent types without the sugar}},
url = {http://www.springerlink.com/index/91W712G2806R575H.pdf},
year = {2010}
volume = {14},
year = {2004}
}
+@phdthesis{McBride1999,
+author = {McBride, Conor},
+file = {:home/bitonic/.local/share/data/Mendeley Ltd./Mendeley Desktop/Downloaded/McBride - 1999 - Dependently typed functional programs and their proofs.pdf:pdf},
+school = {University of Edinburgh},
+title = {{Dependently typed functional programs and their proofs}},
+url = {http://lac-repo-live7.is.ed.ac.uk/handle/1842/374},
+year = {1999}
+}
@phdthesis{Norell2007,
author = {Norell, Ulf},
file = {:home/bitonic/docs/papers/ulf-thesis.pdf:pdf},
url = {http://portal.acm.org/citation.cfm?doid=1190315.1190324},
year = {2007}
}
+@article{Tait1967,
+author = {Tait, William W.},
+file = {:home/bitonic/docs/papers/tait-normalising.pdf:pdf},
+journal = {The Journal of Symbolic Logic},
+number = {2},
+pages = {198--212},
+title = {{Intensional Interpretations of Functionals of Finite Type}},
+volume = {32},
+year = {1967}
+}
@article{Vytiniotis2011,
author = {Vytiniotis, Dimitrios and Jones, Simon Peyton and Schrijvers, Tom and Sulzmann, Martin},
file = {:home/bitonic/docs/papers/outsidein.pdf:pdf},
url = {http://dl.acm.org/citation.cfm?doid=2103786.2103795},
year = {2012}
}
-@phdthesis{McBride1999,
-author = {McBride, Conor},
-file = {:home/bitonic/docs/papers/conorthesis.pdf:pdf},
-school = {University of Edinburgh},
-title = {{Dependently typed functional programs and their proofs}},
-url = {http://lac-repo-live7.is.ed.ac.uk/handle/1842/374},
-year = {1999}
+
+@ARTICLE{Loh2010,
+ author = {Andres L{\"o}h and Conor McBride and Wouter Swierstra},
+ title = {A Tutorial Implementation of a Dependently Typed Lambda Calculus},
+ journal = {Fundam. Inform.},
+ year = {2010},
+ volume = {102},
+ pages = {177-207},
+ number = {2},
+ bibsource = {DBLP, http://dblp.uni-trier.de},
+ ee = {http://dx.doi.org/10.3233/FI-2010-304},
+ file = {:home/bitonic/docs/papers/simply-easy.pdf:pdf},
+ owner = {bitonic}
}