@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
}
url = {http://www.diku.dk/hjemmesider/ansatte/henglein/papers/barendregt1991.pdf},
year = {1991}
}
-@article{Bove2009,
-author = {Bove, Ana and Dybjer, Peter and Norell, Ulf},
-file = {:home/bitonic/docs/papers/agda-overview.pdf:pdf},
-journal = {Theorem Proving in Higher Order Logics},
-title = {{A brief overview of Agda - a functional language with dependent types}},
-url = {http://www.springerlink.com/index/h12lq70470983732.pdf},
-year = {2009}
-}
-@article{Brady2012,
+@article{Brady2013,
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}
+year = {2013}
}
@article{Chapman2010,
address = {New York, New York, USA},
title = {{Intuitionistic type theory}},
year = {1984}
}
-@article{McBride2004,
-author = {McBride, Conor},
-doi = {10.1017/S0956796803004829},
-file = {:home/bitonic/docs/papers/view-from-the-left.ps.gz:gz},
-journal = {Journal of Functional Programming},
-month = jan,
-number = {1},
-pages = {69--111},
-title = {{The View from The Left}},
-url = {http://strictlypositive.org/view.ps.gz},
-volume = {14},
-year = {2004}
+
+@Article{McBride2004,
+ journal = {{J}ournal of {F}unctional {P}rogramming},
+ pages = {69--111},
+ number = {1},
+ volume = {14},
+ title = {The view from the left},
+ year = {2004},
+ author = {C. McBride and J. McKinna}
+}
+
+@phdthesis{Gimenez1996,
+author={Giménez, Eduardo},
+title={Un calcul de constructions infinies et son application {\`a} la v{\'e}rification de syst{\`e}mes communicants},
+school = {Ecole Normale Sup{\'e}rieure de Lyon},
+year = 1996
}
+
@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},
url = {http://dl.acm.org/citation.cfm?doid=2103786.2103795},
year = {2012}
}
+
+@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}
+}
+
+@ARTICLE{Bruijn91,
+ author = {de Bruijn, Nicolaas Govert},
+ title = {Telescopic mappings in typed lambda calculus},
+ journal = {Information and Computation},
+ year = {1991},
+ volume = {91},
+ pages = {189--204},
+ number = {2},
+ file = {:/home/bitonic/docs/papers/telescopes.pdf:PDF},
+ publisher = {Elsevier}
+}
+
+@UNPUBLISHED{Huet1988,
+ author = {Huet, Gerard P.},
+ title = {Extending The Calculus of Constructions with Type:Type},
+ note = {Unpublished draft},
+ year = {1988},
+ file = {:home/bitonic/docs/papers/huet-typtyp.pdf:pdf},
+ owner = {bitonic},
+ timestamp = {2013.06.10}
+}
+
+@ARTICLE{Harper1991,
+ author = {Harper, Robert and Pollack, Robert},
+ title = {Type checking with universes},
+ journal = {Theoretical computer science},
+ year = {1991},
+ volume = {89},
+ pages = {107--136},
+ number = {1},
+ file = {:/home/bitonic/docs/papers/type-checking-universes.ps.gz:PostScript},
+ publisher = {Elsevier}
+}
+
+@ARTICLE{Jacobs1994,
+ 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},
+ booktitle={Logic in Computer Science, 1994. LICS'94. Proceedings., Symposium on},
+ pages={208--212},
+ year={1994},
+ organization={IEEE}
+}
+
+@INPROCEEDINGS{Coquand1992,
+ author = {Coquand, Thierry},
+ title = {Pattern matching with dependent types},
+ booktitle = {Informal proceedings of Logical Frameworks},
+ year = {1992},
+ volume = {92},
+ pages = {66--79},
+ file = {:/home/bitonic/docs/papers/coquand-pattern.ps:PostScript}
+}
+
+@INPROCEEDINGS{Abel2007,
+ author = {Abel, Andreas and Coquand, Thierry and Dybjer, Peter},
+ title = {Normalization by evaluation for Martin-Lof type theory with typed
+ equality judgements},
+ booktitle = {Logic in Computer Science, 2007. LICS 2007. 22nd Annual IEEE Symposium
+ on},
+ year = {2007},
+ pages = {3--12},
+ 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},
+}
+
+@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}
+}
+
+@incollection{Gimenez1995,
+year={1995},
+isbn={978-3-540-60579-9},
+booktitle={Types for Proofs and Programs},
+volume={996},
+series={Lecture Notes in Computer Science},
+editor={Dybjer, Peter and Nordström, Bengt and Smith, Jan},
+doi={10.1007/3-540-60579-7_3},
+title={Codifying guarded definitions with recursive schemes},
+url={http://dx.doi.org/10.1007/3-540-60579-7_3},
+publisher={Springer Berlin Heidelberg},
+author={Giménez, Eduardo},
+pages={39-59}
+}
+
+@article{Capretta2005,
+ author = {Venanzio Capretta},
+ title = {General recursion via coinductive types},
+ journal = {Logical Methods in Computer Science},
+ volume = {1},
+ number = {2},
+ year = {2005},
+ ee = {http://dx.doi.org/10.2168/LMCS-1(2:1)2005},
+ bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+
+@article{Danielsson2012,
+ author = {Danielsson, Nils Anders},
+ title = {Operational semantics using the partiality monad},
+ journal = {SIGPLAN Not.},
+ issue_date = {September 2012},
+ volume = {47},
+ number = {9},
+ month = sep,
+ year = {2012},
+ issn = {0362-1340},
+ pages = {127--138},
+ numpages = {12},
+ url = {http://doi.acm.org/10.1145/2398856.2364546},
+ doi = {10.1145/2398856.2364546},
+ acmid = {2364546},
+ publisher = {ACM},
+ address = {New York, NY, USA},
+ keywords = {dependent types, mixed induction and coinduction, partiality monad},
+}
+
+
+@incollection{Paulson1990,
+ Author = {Paulson, Lawrence C.},
+ Booktitle = {Logic and Computer Science},
+ Date-Modified = {2005-04-20 12:07:55 +0100},
+ Editor = {P. Odifreddi},
+ Pages = {361-386},
+ Publisher = {Academic Press},
+ Title = {{Isabelle}: The Next 700 Theorem Provers},
+ Year = {1990}}
+
+
+@book{Russell1927,
+ author = "Whitehead, Alfred North and Russell, Bertrand Arthur
+ William",
+ title = "Principia mathematica; 2nd ed.",
+ publisher = "Cambridge Univ. Press",
+ address = "Cambridge",
+ year = "1927",
+}
\ No newline at end of file
projects / bitonic-mengthesis.git / blobdiff