thesis.bib

   1 @inbook{Thompson1991,
   2   author = {Thompson, Simon},
   3   title = {Type Theory and Functional Programming},
   4   publisher = {Addison-Wesley},
   5   year = {1991}
   6 }
   7
   8 @inbook{Pierce2002,
   9   author = {Pierce, Benjamin C.},
  10   title = {Types and Programming Languages},
  11   publisher = {The MIT Press},
  12   year = {2002}
  13 }
  14
  15 @inbook{Queinnec2003,
  16   author    = {Christian Queinnec},
  17   title     = {Lisp in Small Pieces},
  18   publisher = {Cambridge University Press},
  19   year      = {2003},
  20 }
  21
  22 @online{Coq,
  23   author = {{The Coq Team}},
  24   title = {The Coq Proof Assistant},
  25   url = {\url{coq.inria.fr}},
  26   howpublished = {\url{http://coq.inria.fr}},
  27   year = 2013
  28 }
  29
  30 @online{GHC,
  31   author = {{The GHC Team}},
  32   title = {The Glorious Glasgow Haskell Compilation System User's Guide, Version 7.6.1},
  33   url = {http://www.haskell.org/ghc/docs/7.6.1/html/users_guide/},
  34   howpublished = {\url{http://www.haskell.org/ghc/docs/latest/html/users_guide/}},
  35   year = 2012
  36 }
  37
  38 @online{EpigramTut,
  39   author = {Conor McBride},
  40   title = {Epigram: Practical Programming with Dependent Types},
  41   url = {http://strictlypositive.org/epigram-notes.ps.gz},
  42   howpublished = {\url{http://strictlypositive.org/epigram-notes.ps.gz}},
  43   year = 2004
  44 }
  45
  46 @online{Haskell2010,
  47   author = {Simon Marlow},
  48   title = {Haskell 2010, Language Report},
  49   url = {http://www.haskell.org/onlinereport/haskell2010/},
  50   howpublished = {\url{http://www.haskell.org/onlinereport/haskell2010/}},
  51   year = 2010
  52 }
  53
  54 @online{LYAH,
  55   author = {Miran Lipova\v{c}a},
  56   title = {Learn You a Haskell for Great Good!},
  57   url = {http://learnyouahaskell.com/},
  58   howpublished = {\url{http://learnyouahaskell.com/}},
  59   year = 2009
  60 }
  61
  62 @inbook{ProgInHask,
  63   author = {Graham Hutton},
  64   title = {Programming in Haskell},
  65   year = 2007,
  66   publisher = {Cambridge University Press}
  67 }
  68
  69 @inbook{NuPRL,
  70   author = {Robert L. Constable and the PRL Group},
  71   title = {Implementing Mathematics with The NuPRL Proof Development System},
  72   year = 1986,
  73   publisher = Prentice-Hall
  74 }
  75
  76 @article{Altenkirch2010,
  77 author = {Altenkirch, Thorsten and Danielsson, Nils Anders and L\"{o}h, Andres and Oury, Nicolas},
  78 file = {:home/bitonic/docs/papers/PiSigma.pdf:pdf},
  79 journal = {Functional and Logic Programming},
  80 pages = {40--55},
  81 title = {{$\Pi$$\Sigma$: dependent types without the sugar}},
  82 url = {http://www.springerlink.com/index/91W712G2806R575H.pdf},
  83 year = {2010}
  84 }
  85 @article{Altenkirch2007,
  86 address = {New York, New York, USA},
  87 author = {Altenkirch, Thorsten and McBride, Conor and Swierstra, Wouter},
  88 doi = {10.1145/1292597.1292608},
  89 file = {:home/bitonic/docs/papers/OTT2.pdf:pdf},
  90 isbn = {9781595936776},
  91 journal = {Proceedings of the 2007 workshop on Programming languages meets program verification - PLPV '07},
  92 keywords = {case analysis relies on,datatypes are indexed in,equality,of any language where,ole in the programs,play a crucial internal,rˆ,solving,some way,type theory},
  93 pages = {57},
  94 publisher = {ACM Press},
  95 title = {{Observational equality, now!}},
  96 url = {http://portal.acm.org/citation.cfm?doid=1292597.1292608},
  97 year = {2007}
  98 }
  99 @article{Barendregt1991,
 100 author = {Barendregt, Henk},
 101 file = {:home/bitonic/docs/papers/lambda-cube.pdf:pdf},
 102 journal = {Journal of functional programming},
 103 title = {{Introduction to generalized type systems}},
 104 url = {http://www.diku.dk/hjemmesider/ansatte/henglein/papers/barendregt1991.pdf},
 105 year = {1991}
 106 }
 107 @article{Bove2009,
 108 author = {Bove, Ana and Dybjer, Peter and Norell, Ulf},
 109 file = {:home/bitonic/docs/papers/agda-overview.pdf:pdf},
 110 journal = {Theorem Proving in Higher Order Logics},
 111 title = {{A brief overview of Agda - a functional language with dependent types}},
 112 url = {http://www.springerlink.com/index/h12lq70470983732.pdf},
 113 year = {2009}
 114 }
 115 @article{Brady2012,
 116 author = {Brady, Edwin},
 117 file = {:home/bitonic/docs/papers/idris-implementation.pdf:pdf},
 118 journal = {Unpublished draft},
 119 number = {November},
 120 title = {{Implementing General Purpose Dependently Typed Programming Languages}},
 121 url = {http://www.cs.st-andrews.ac.uk/~eb/drafts/impldtp.pdf},
 122 year = {2012}
 123 }
 124 @article{Chapman2010,
 125 address = {New York, New York, USA},
 126 author = {Chapman, James and Dagand, Pierre-\'{E}variste and McBride, Conor and Morris, Peter},
 127 doi = {10.1145/1863543.1863547},
 128 file = {:home/bitonic/docs/papers/conor-levitation.pdf:pdf},
 129 isbn = {9781605587943},
 130 journal = {Proceedings of the 15th ACM SIGPLAN international conference on Functional programming - ICFP '10},
 131 pages = {3},
 132 publisher = {ACM Press},
 133 title = {{The gentle art of levitation}},
 134 url = {http://portal.acm.org/citation.cfm?doid=1863543.1863547},
 135 year = {2010}
 136 }
 137 @article{Church1936,
 138 author = {Church, Alonzo},
 139 file = {:home/bitonic/docs/papers/church-lc.pdf:pdf},
 140 journal = {American journal of mathematics},
 141 number = {2},
 142 pages = {345--363},
 143 title = {{An unsolvable problem of elementary number theory}},
 144 url = {http://www.ams.org/leavingmsn?url=http://dx.doi.org/10.2307/2371045},
 145 volume = {58},
 146 year = {1936}
 147 }
 148 @article{Church1940,
 149 author = {Church, Alonzo},
 150 file = {:home/bitonic/docs/papers/church-stlc.pdf:pdf},
 151 journal = {J. Symb. Log.},
 152 number = {2},
 153 pages = {56--68},
 154 title = {{A formulation of the simple theory of types}},
 155 url = {http://www.ams.org/leavingmsn?url=http://dx.doi.org/10.2307/2266170},
 156 volume = {5},
 157 year = {1940}
 158 }
 159 @article{Coquand1986,
 160 author = {Coquand, Thierry and Huet, Gerard},
 161 file = {:home/bitonic/docs/papers/coc.pdf:pdf},
 162 title = {{The calculus of constructions}},
 163 url = {http://hal.inria.fr/docs/00/07/60/24/PDF/RR-0530.pdf},
 164 year = {1986}
 165 }
 166 @article{Curry1934,
 167 author = {Curry, Haskell B.},
 168 file = {:home/bitonic/docs/papers/curry-stlc.pdf:pdf},
 169 journal = {Proceedings of the National Academy of Sciences of the United States of America},
 170 number = {1930},
 171 pages = {584--590},
 172 title = {{Functionality in combinatory logic}},
 173 url = {http://www.ncbi.nlm.nih.gov/pmc/articles/pmc1076489/},
 174 volume = {511},
 175 year = {1934}
 176 }
 177 @article{Dybjer1991,
 178 author = {Dybjer, Peter},
 179 file = {:home/bitonic/docs/papers/dybjer-inductive.ps:ps},
 180 journal = {Logical Frameworks},
 181 title = {{Inductive sets and families in Martin-L\"{o}f's type theory and their set-theoretic semantics}},
 182 url = {http://books.google.com/books?hl=en\&lr=\&id=X9wfWwslFQIC\&oi=fnd\&pg=PA280\&dq=Inductive+Sets+and+Families+in+Martin-L\%C3\%B6f\%27s+Type+Theory+and+Their+Set-Theoretic+Semantics\&ots=LewzM17GcW\&sig=vF4GgtlEBSf1uwRV1o\_unDtLats},
 183 year = {1991}
 184 }
 185 @article{Hurkens1995,
 186 author = {Hurkens, Antonius J.C.},
 187 file = {:home/bitonic/docs/papers/hurkens-paradox.pdf:pdf},
 188 journal = {Typed Lambda Calculi and Applications},
 189 title = {{A simplification of Girard's paradox}},
 190 url = {http://www.springerlink.com/index/W718604JN467672H.pdf},
 191 year = {1995}
 192 }
 193 @article{Jacobs1997,
 194 author = {Jacobs, Bart and Rutten, Jan},
 195 file = {:home/bitonic/docs/papers/coalgebra-coind.pdf:pdf},
 196 journal = {EATCS Bulletin},
 197 number = {1997},
 198 title = {{A tutorial on (co) algebras and (co) induction}},
 199 url = {http://synrc.com/publications/cat/Logic/CoinductionCoalgebrasTutorial.pdf},
 200 volume = {62},
 201 year = {1997}
 202 }
 203 @book{Martin-Lof1984,
 204 author = {Martin-L\"{o}f, Per},
 205 file = {:home/bitonic/docs/papers/martin-lof-tt.pdf:pdf},
 206 isbn = {8870881059},
 207 publisher = {Bibliopolis},
 208 title = {{Intuitionistic type theory}},
 209 year = {1984}
 210 }
 211 @article{McBride2004,
 212 author = {McBride, Conor},
 213 doi = {10.1017/S0956796803004829},
 214 file = {:home/bitonic/docs/papers/view-from-the-left.ps.gz:gz},
 215 journal = {Journal of Functional Programming},
 216 month = jan,
 217 number = {1},
 218 pages = {69--111},
 219 title = {{The View from The Left}},
 220 url = {http://strictlypositive.org/view.ps.gz},
 221 volume = {14},
 222 year = {2004}
 223 }
 224 @phdthesis{McBride1999,
 225 author = {McBride, Conor},
 226 file = {:home/bitonic/.local/share/data/Mendeley Ltd./Mendeley Desktop/Downloaded/McBride - 1999 - Dependently typed functional programs and their proofs.pdf:pdf},
 227 school = {University of Edinburgh},
 228 title = {{Dependently typed functional programs and their proofs}},
 229 url = {http://lac-repo-live7.is.ed.ac.uk/handle/1842/374},
 230 year = {1999}
 231 }
 232 @phdthesis{Norell2007,
 233 author = {Norell, Ulf},
 234 file = {:home/bitonic/docs/papers/ulf-thesis.pdf:pdf},
 235 isbn = {9789172919969},
 236 school = {Chalmers University of Technology and G\"{o}teborg University},
 237 title = {{Towards a practical programming language based on dependent type theory}},
 238 url = {http://www.cse.chalmers.se/~ulfn/papers/thesis.pdf},
 239 year = {2007}
 240 }
 241 @article{Oury2008,
 242 address = {New York, New York, USA},
 243 author = {Oury, Nicolas and Swierstra, Wouter},
 244 doi = {10.1145/1411204.1411213},
 245 file = {:home/bitonic/docs/papers/powerofpi.pdf:pdf},
 246 isbn = {9781595939197},
 247 journal = {Proceeding of the 13th ACM SIGPLAN international conference on Functional programming - ICFP '08},
 248 pages = {39},
 249 publisher = {ACM Press},
 250 title = {{The power of Pi}},
 251 url = {http://portal.acm.org/citation.cfm?doid=1411204.1411213},
 252 year = {2008}
 253 }
 254 @article{Pierce2000,
 255 author = {Pierce, Benjamin C. and Turner, David N.},
 256 doi = {10.1145/345099.345100},
 257 file = {:home/bitonic/docs/papers/local-type-inference.pdf:pdf},
 258 issn = {01640925},
 259 journal = {ACM Transactions on Programming Languages and Systems},
 260 month = jan,
 261 number = {1},
 262 pages = {1--44},
 263 title = {{Local type inference}},
 264 url = {http://portal.acm.org/citation.cfm?doid=345099.345100},
 265 volume = {22},
 266 year = {2000}
 267 }
 268 @article{Pollack1990,
 269 author = {Pollack, Robert},
 270 file = {:home/bitonic/docs/papers/implicit-syntax.ps:ps},
 271 journal = {Informal Proceedings of First Workshop on Logical Frameworks},
 272 title = {{Implicit syntax}},
 273 url = {http://reference.kfupm.edu.sa/content/i/m/implicit\_syntax\_\_1183660.pdf},
 274 year = {1992}
 275 }
 276 @article{Reynolds1994,
 277 author = {Reynolds, John C.},
 278 file = {:home/bitonic/docs/papers/reynolds-polymorphic-lc.ps:ps},
 279 journal = {Logical Foundations of Functional Programming},
 280 title = {{An introduction to the polymorphic lambda calculus}},
 281 url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.7.9916\&rep=rep1\&type=pdf},
 282 year = {1994}
 283 }
 284 @article{Sulzmann2007,
 285 address = {New York, New York, USA},
 286 author = {Sulzmann, Martin and Chakravarty, Manuel M. T. and Jones, Simon Peyton and Donnelly, Kevin},
 287 doi = {10.1145/1190315.1190324},
 288 file = {:home/bitonic/docs/papers/systemf-coercions.pdf:pdf},
 289 isbn = {159593393X},
 290 journal = {Proceedings of the 2007 ACM SIGPLAN international workshop on Types in languages design and implementation - TLDI '07},
 291 pages = {53},
 292 publisher = {ACM Press},
 293 title = {{System F with type equality coercions}},
 294 url = {http://portal.acm.org/citation.cfm?doid=1190315.1190324},
 295 year = {2007}
 296 }
 297 @article{Tait1967,
 298 author = {Tait, William W.},
 299 file = {:home/bitonic/docs/papers/tait-normalising.pdf:pdf},
 300 journal = {The Journal of Symbolic Logic},
 301 number = {2},
 302 pages = {198--212},
 303 title = {{Intensional Interpretations of Functionals of Finite Type}},
 304 volume = {32},
 305 year = {1967}
 306 }
 307 @article{Vytiniotis2011,
 308 author = {Vytiniotis, Dimitrios and Jones, Simon Peyton and Schrijvers, Tom and Sulzmann, Martin},
 309 file = {:home/bitonic/docs/papers/outsidein.pdf:pdf},
 310 journal = {Journal of Functional Programming},
 311 number = {4-5},
 312 pages = {333--412},
 313 title = {{OutsideIn (X) Modular type inference with local assumptions}},
 314 url = {http://journals.cambridge.org/production/action/cjoGetFulltext?fulltextid=8274818},
 315 volume = {21},
 316 year = {2011}
 317 }
 318 @article{Yorgey2012,
 319 address = {New York, New York, USA},
 320 author = {Yorgey, Brent a. and Weirich, Stephanie and Cretin, Julien and {Peyton Jones}, Simon and Vytiniotis, Dimitrios and Magalh\~{a}es, Jos\'{e} Pedro},
 321 doi = {10.1145/2103786.2103795},
 322 file = {:home/bitonic/docs/papers/haskell-promotion.pdf:pdf},
 323 isbn = {9781450311205},
 324 journal = {Proceedings of the 8th ACM SIGPLAN workshop on Types in language design and implementation - TLDI '12},
 325 pages = {53},
 326 publisher = {ACM Press},
 327 title = {{Giving Haskell a promotion}},
 328 url = {http://dl.acm.org/citation.cfm?doid=2103786.2103795},
 329 year = {2012}
 330 }
 331
 332 @ARTICLE{Loh2010,
 333   author = {Andres L{\"o}h and Conor McBride and Wouter Swierstra},
 334   title = {A Tutorial Implementation of a Dependently Typed Lambda Calculus},
 335   journal = {Fundam. Inform.},
 336   year = {2010},
 337   volume = {102},
 338   pages = {177-207},
 339   number = {2},
 340   bibsource = {DBLP, http://dblp.uni-trier.de},
 341   ee = {http://dx.doi.org/10.3233/FI-2010-304},
 342   file = {:home/bitonic/docs/papers/simply-easy.pdf:pdf},
 343   owner = {bitonic}
 344 }
 345
 346 @ARTICLE{Bruijn91,
 347   author = {de Bruijn, Nicolaas Govert},
 348   title = {Telescopic mappings in typed lambda calculus},
 349   journal = {Information and Computation},
 350   year = {1991},
 351   volume = {91},
 352   pages = {189--204},
 353   number = {2},
 354   file = {:/home/bitonic/docs/papers/telescopes.pdf:PDF},
 355   publisher = {Elsevier}
 356 }
 357
 358 @UNPUBLISHED{Huet1988,
 359   author = {Huet, Gerard},
 360   title = {Extending The Calculus of Constructions with Type:Type},
 361   note = {Unpublished draft},
 362   year = {1988},
 363   file = {:home/bitonic/docs/papers/huet-typtyp.pdf:pdf},
 364   owner = {bitonic},
 365   timestamp = {2013.06.10}
 366 }
 367
 368 @ARTICLE{Harper1991,
 369   author = {Harper, Robert and Pollack, Robert},
 370   title = {Type checking with universes},
 371   journal = {Theoretical computer science},
 372   year = {1991},
 373   volume = {89},
 374   pages = {107--136},
 375   number = {1},
 376   file = {:/home/bitonic/docs/papers/type-checking-universes.ps.gz:PostScript},
 377   publisher = {Elsevier}
 378 }
 379
 380 @ARTICLE{Jacobs1994,
 381   author = {Jacobs, Bart},
 382   title = {Quotients in simple type theory},
 383   journal = {available from the Hypatia Electronic Library: http://hypatia. dcs.
 384         qmw. ac. uk},
 385   year = {1994},
 386   file = {:/home/bitonic/docs/papers/jacobs-quotients.pdf:PDF},
 387   publisher = {Citeseer}
 388 }
 389
 390
 391 @inproceedings{Hofmann1994,
 392   title={The groupoid model refutes uniqueness of identity proofs},
 393   author={Hofmann, Martin and Streicher, Thomas},
 394   booktitle={Logic in Computer Science, 1994. LICS'94. Proceedings., Symposium on},
 395   pages={208--212},
 396   year={1994},
 397   organization={IEEE}
 398 }
 399
 400 @INPROCEEDINGS{Coquand1992,
 401   author = {Coquand, Thierry},
 402   title = {Pattern matching with dependent types},
 403   booktitle = {Informal proceedings of Logical Frameworks},
 404   year = {1992},
 405   volume = {92},
 406   pages = {66--79},
 407   organization = {Citeseer},
 408   file = {:/home/bitonic/docs/papers/coquand-pattern.ps:PostScript}
 409 }
 410
 411 @INPROCEEDINGS{Abel2007,
 412   author = {Abel, Andreas and Coquand, Thierry and Dybjer, Peter},
 413   title = {Normalization by evaluation for Martin-Lof type theory with typed
 414         equality judgements},
 415   booktitle = {Logic in Computer Science, 2007. LICS 2007. 22nd Annual IEEE Symposium
 416         on},
 417   year = {2007},
 418   pages = {3--12},
 419   organization = {IEEE},
 420   file = {:/home/bitonic/docs/papers/nbe.pdf:PDF}
 421 }
 422
 423 @inproceedings{McBride2004b,
 424   title={I am not a number: I am a free variable},
 425   author={McBride, Conor and McKinna, James},
 426   booktitle={Proceedings of the ACM SIGPLAN Haskell Workshop},
 427   year={2004},
 428   organization={Citeseer}
 429 }
 430
 431 @article{Bird1999,
 432   title={De Bruijn notation as a nested datatype},
 433   author={Richard S. Bird and Ross Paterson},
 434   journal={J. Functional Programming},
 435   volume={9},
 436   number={1},
 437   pages={77--91},
 438   year={1999},
 439   publisher={Cambridge Univ Press}
 440 }
 441
 442 @inproceedings{de1972lambda,
 443   title={Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem},
 444   author={de Bruijn, Nicolaas Govert},
 445   booktitle={Indagationes Mathematicae (Proceedings)},
 446   volume={75},
 447   number={5},
 448   pages={381--392},
 449   year={1972},
 450   organization={Elsevier}
 451 }
 452
 453 @article{henglein1993type,
 454   title={Type inference with polymorphic recursion},
 455   author={Henglein, Fritz},
 456   journal={ACM Transactions on Programming Languages and Systems (TOPLAS)},
 457   volume={15},
 458   number={2},
 459   pages={253--289},
 460   year={1993},
 461   publisher={ACM}
 462 }
 463
 464 @inproceedings{weirich2011binders,
 465   title={Binders unbound},
 466   author={Weirich, Stephanie and Yorgey, Brent A and Sheard, Tim},
 467   booktitle={ACM SIGPLAN Notices},
 468   volume={46},
 469   number={9},
 470   pages={333--345},
 471   year={2011},
 472   organization={ACM}
 473 }