@online{GHC,
author = {{The GHC Team}},
- title = {The Glorious Glasgow Haskell Compilation System User's Guide, Version 7.6.1},
- url = {http://www.haskell.org/ghc/docs/7.6.1/html/users_guide/},
- howpublished = {\url{http://www.haskell.org/ghc/docs/latest/html/users_guide/}},
+ title = {The Glorious Glasgow Haskell Compilation System User's Guide, Version 7.6.3},
+ url = {http://www.haskell.org/ghc/docs/latest/html/users_guide/},
+ howpublished = {\url{http://www.haskell.org/ghc/docs/7.6.3/html/users_guide/}},
year = 2012
}
}
@UNPUBLISHED{Huet1988,
- author = {Huet, Gerard},
+ author = {Huet, Gerard P.},
title = {Extending The Calculus of Constructions with Type:Type},
note = {Unpublished draft},
year = {1988},
}
@ARTICLE{Jacobs1994,
- author = {Jacobs, Bart},
- title = {Quotients in simple type theory},
- journal = {available from the Hypatia Electronic Library: http://hypatia. dcs.
- qmw. ac. uk},
- year = {1994},
- file = {:/home/bitonic/docs/papers/jacobs-quotients.pdf:PDF},
- publisher = {Citeseer}
+ author = {Jacobs, Bart},
+ title = {Quotients in Simple Type Theory},
+ journal = {Manuscript, Math. Inst},
+ year = {1994}
}
-
@inproceedings{Hofmann1994,
title={The groupoid model refutes uniqueness of identity proofs},
author={Hofmann, Martin and Streicher, Thomas},
organization = {IEEE},
file = {:/home/bitonic/docs/papers/nbe.pdf:PDF}
}
+
+@inproceedings{McBride2004b,
+ title={I am not a number: I am a free variable},
+ author={McBride, Conor and McKinna, James},
+ booktitle={Proceedings of the ACM SIGPLAN Haskell Workshop},
+ year={2004},
+ organization={Citeseer}
+}
+
+@article{Bird1999,
+ title={De Bruijn notation as a nested datatype},
+ author={Richard S. Bird and Ross Paterson},
+ journal={J. Functional Programming},
+ volume={9},
+ number={1},
+ pages={77--91},
+ year={1999},
+ publisher={Cambridge Univ Press}
+}
+
+@inproceedings{de1972lambda,
+ title={Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem},
+ author={de Bruijn, Nicolaas Govert},
+ booktitle={Indagationes Mathematicae (Proceedings)},
+ volume={75},
+ number={5},
+ pages={381--392},
+ year={1972},
+ organization={Elsevier}
+}
+
+@article{henglein1993type,
+ title={Type inference with polymorphic recursion},
+ author={Henglein, Fritz},
+ journal={ACM Transactions on Programming Languages and Systems (TOPLAS)},
+ volume={15},
+ number={2},
+ pages={253--289},
+ year={1993},
+ publisher={ACM}
+}
+
+@inproceedings{weirich2011binders,
+ title={Binders unbound},
+ author={Weirich, Stephanie and Yorgey, Brent A and Sheard, Tim},
+ booktitle={ACM SIGPLAN Notices},
+ volume={46},
+ number={9},
+ pages={333--345},
+ year={2011},
+ organization={ACM}
+}
+
+@inproceedings{King1995,
+ title={Structuring depth-first search algorithms in Haskell},
+ author={King, David J and Launchbury, John},
+ booktitle={Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages},
+ pages={344--354},
+ year={1995},
+ organization={ACM}
+}
+
+@article{milner1978theory,
+ title={A theory of type polymorphism in programming},
+ author={Milner, Robin},
+ journal={Journal of computer and system sciences},
+ volume={17},
+ number={3},
+ pages={348--375},
+ year={1978},
+ publisher={Elsevier}
+}
+
+@article{dagand2012elaborating,
+ title={Elaborating inductive definitions},
+ author={Dagand, Pierre-Evariste and McBride, Conor},
+ journal={arXiv preprint arXiv:1210.6390},
+ year={2012}
+}
+
+@inproceedings{chapman2010gentle,
+ title={The gentle art of levitation},
+ author={Chapman, James and Dagand, Pierre-{\'E}variste and McBride, Conor and Morris, Peter},
+ booktitle={ACM Sigplan Notices},
+ volume={45},
+ number={9},
+ pages={3--14},
+ year={2010},
+ organization={ACM}
+}
+
+@article{dybjer2000general,
+ title={A general formulation of simultaneous inductive-recursive definitions in type theory},
+ author={Dybjer, Peter},
+ journal={Journal of Symbolic Logic},
+ pages={525--549},
+ year={2000},
+ publisher={JSTOR}
+}
+
+@inproceedings{chakravarty2005associated,
+ title={Associated types with class},
+ author={Chakravarty, Manuel MT and Keller, Gabriele and Jones, Simon Peyton and Marlow, Simon},
+ booktitle={ACM SIGPLAN Notices},
+ volume={40},
+ number={1},
+ pages={1--13},
+ year={2005},
+ organization={ACM}
+}
+
+@article{miller1992unification,
+ title={Unification under a mixed prefix},
+ author={Miller, Dale},
+ journal={Journal of symbolic computation},
+ volume={14},
+ number={4},
+ pages={321--358},
+ year={1992},
+ publisher={Elsevier}
+}
+
+@UNPUBLISHED{gundrytutorial,
+ title={A tutorial implementation of dynamic pattern unification},
+ author={Gundry, Adam and McBride, Conor},
+ note= {Unpublished draft},
+ year={2013}
+}
+
+@techreport{cockett1992charity,
+ title={About charity},
+ author={Cockett, Robin and Fukushima, Tom},
+ year={1992},
+ journal={Yellow Series Report}
+}
+
+@incollection{mcbride2009let,
+ title={Let’s see how things unfold: Reconciling the infinite with the intensional},
+ author={McBride, Conor},
+ booktitle={Algebra and Coalgebra in Computer Science},
+ pages={113--126},
+ year={2009},
+ publisher={Springer}
+}
+
+@article{huet1973undecidability,
+ title={The undecidability of unification in third order logic},
+ author={Huet, Gerard P.},
+ journal={Information and Control},
+ volume={22},
+ number={3},
+ pages={257--267},
+ year={1973},
+ publisher={Elsevier}
+}
+
+@article{dybjer1997representing,
+ title={Representing inductively defined sets by wellorderings in Martin-L{\"o}f's type theory},
+ author={Dybjer, Peter},
+ journal={Theoretical Computer Science},
+ volume={176},
+ number={1},
+ pages={329--335},
+ year={1997},
+ publisher={Elsevier}
+}
+
+@inbook{Nordstrom1990,
+ author = {Nordstr{\"o}m, Bengt and Petersson, Kent and Smith, Jan M.},
+ title = {Programming in Martin-L{\"o}f Type Theory: An Introduction},
+ publisher = {Oxford University Press},
+ year = {1990}
+}
projects / bitonic-mengthesis.git / blobdiff