docs/background.bib

   1
   2 @inbook{Thompson1991,
   3   author = {Thompson, Simon},
   4   title = {Type Theory and Functional Programming},
   5   publisher = {Addison-Wesley},
   6   year = {1991}
   7 }
   8
   9 @inbook{Pierce2002,
  10   author = {Pierce, Benjamin C.},
  11   title = {Types and Programming Languages},
  12   publisher = {The MIT Press},
  13   year = {2002}
  14 }
  15
  16 @online{Coq,
  17   author = {{The Coq Team}},
  18   title = {The Coq Proof Assistant},
  19   url = {\url{coq.inria.fr}},
  20   howpublished = {\url{http://coq.inria.fr}},
  21   year = 2013
  22 }
  23
  24 @online{GHC,
  25   author = {{The GHC Team}},
  26   title = {The Glorious Glasgow Haskell Compilation System User's Guide, Version 7.6.1},
  27   url = {http://www.haskell.org/ghc/docs/7.6.1/html/users_guide/},
  28   howpublished = {\url{http://www.haskell.org/ghc/docs/latest/html/users_guide/}},
  29   year = 2012
  30 }
  31
  32 @online{EpigramTut,
  33   author = {Conor McBride},
  34   title = {Epigram: Practical Programming with Dependent Types},
  35   url = {http://strictlypositive.org/epigram-notes.ps.gz},
  36   howpublished = {\url{http://strictlypositive.org/epigram-notes.ps.gz}},
  37   year = 2004
  38 }
  39
  40 @online{Haskell2010,
  41   author = {Simon Marlow},
  42   title = {Haskell 2010, Language Report},
  43   url = {http://www.haskell.org/onlinereport/haskell2010/},
  44   howpublished = {\url{http://www.haskell.org/onlinereport/haskell2010/}},
  45   year = 2010
  46 }
  47
  48 @online{LYAH,
  49   author = {Miran Lipova\v{c}a},
  50   title = {Learn You a Haskell for Great Good!},
  51   url = {http://learnyouahaskell.com/},
  52   howpublished = {\url{http://learnyouahaskell.com/}},
  53   year = 2009
  54 }
  55
  56 @inbook{ProgInHask,
  57   author = {Graham Hutton},
  58   title = {Programming in Haskell},
  59   year = 2007,
  60   publisher = {Cambridge University Press}
  61 }
  62
  63
  64 @inbook{Constable86,
  65 author = {Constable, Robert L. and Stuart F. Allen and H. M. Bromley and W. R. Cleaveland and J. F. Cremer and R. W. Harper and Douglas J. Howe and T. B. Knoblock and N. P. Mendler and P. Panangaden and James T. Sasaki and Scott F. Smith},
  66 title = {Implementing Mathematics with the NuPRL Proof Development System},
  67 year = {1986},
  68 publisher = {Prentice-Hall},
  69 address = {NJ}
  70 }
  71
  72
  73 @article{Altenkirch2010,
  74 author = {Altenkirch, Thorsten and Danielsson, N and L\"{o}h, A and Oury, Nicolas},
  75 file = {:home/bitonic/docs/papers/PiSigma.pdf:pdf},
  76 journal = {Functional and Logic \ldots},
  77 number = {Sheard 2005},
  78 title = {{$\Pi$$\Sigma$: dependent types without the sugar}},
  79 url = {http://www.springerlink.com/index/91W712G2806R575H.pdf},
  80 year = {2010}
  81 }
  82 @article{Altenkirch2007,
  83 address = {New York, New York, USA},
  84 author = {Altenkirch, Thorsten and McBride, Conor and Swierstra, Wouter},
  85 doi = {10.1145/1292597.1292608},
  86 file = {:home/bitonic/docs/papers/OTT2.pdf:pdf},
  87 isbn = {9781595936776},
  88 journal = {Proceedings of the 2007 workshop on Programming languages meets program verification - PLPV '07},
  89 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},
  90 pages = {57},
  91 publisher = {ACM Press},
  92 title = {{Observational equality, now!}},
  93 url = {http://portal.acm.org/citation.cfm?doid=1292597.1292608},
  94 year = {2007}
  95 }
  96 @article{Barendregt1991,
  97 author = {Barendregt, Henk},
  98 file = {:home/bitonic/docs/papers/lambda-cube.pdf:pdf},
  99 journal = {Journal of functional programming},
 100 title = {{Introduction to generalized type systems}},
 101 url = {http://www.diku.dk/hjemmesider/ansatte/henglein/papers/barendregt1991.pdf},
 102 year = {1991}
 103 }
 104 @article{Bove2009,
 105 author = {Bove, Ana and Dybjer, Peter and Norell, Ulf},
 106 file = {:home/bitonic/docs/papers/agda-overview.pdf:pdf},
 107 journal = {Theorem Proving in Higher Order Logics},
 108 title = {{A brief overview of Agda - a functional language with dependent types}},
 109 url = {http://www.springerlink.com/index/h12lq70470983732.pdf},
 110 year = {2009}
 111 }
 112 @article{Brady2012,
 113 author = {Brady, Edwin},
 114 file = {:home/bitonic/docs/papers/idris-implementation.pdf:pdf},
 115 journal = {Unpublished draft},
 116 number = {November},
 117 title = {{Implementing General Purpose Dependently Typed Programming Languages}},
 118 url = {http://www.cs.st-andrews.ac.uk/~eb/drafts/impldtp.pdf},
 119 year = {2012}
 120 }
 121 @article{Chapman2010,
 122 address = {New York, New York, USA},
 123 author = {Chapman, James and Dagand, Pierre-\'{E}variste and McBride, Conor and Morris, Peter},
 124 doi = {10.1145/1863543.1863547},
 125 file = {:home/bitonic/docs/papers/conor-levitation.pdf:pdf},
 126 isbn = {9781605587943},
 127 journal = {Proceedings of the 15th ACM SIGPLAN international conference on Functional programming - ICFP '10},
 128 pages = {3},
 129 publisher = {ACM Press},
 130 title = {{The gentle art of levitation}},
 131 url = {http://portal.acm.org/citation.cfm?doid=1863543.1863547},
 132 year = {2010}
 133 }
 134 @article{Church1936,
 135 author = {Church, Alonzo},
 136 file = {:home/bitonic/docs/papers/church-lc.pdf:pdf},
 137 journal = {American journal of mathematics},
 138 number = {2},
 139 pages = {345--363},
 140 title = {{An unsolvable problem of elementary number theory}},
 141 url = {http://www.ams.org/leavingmsn?url=http://dx.doi.org/10.2307/2371045},
 142 volume = {58},
 143 year = {1936}
 144 }
 145 @article{Church1940,
 146 author = {Church, Alonzo},
 147 file = {:home/bitonic/docs/papers/church-stlc.pdf:pdf},
 148 journal = {J. Symb. Log.},
 149 number = {2},
 150 pages = {56--68},
 151 title = {{A formulation of the simple theory of types}},
 152 url = {http://www.ams.org/leavingmsn?url=http://dx.doi.org/10.2307/2266170},
 153 volume = {5},
 154 year = {1940}
 155 }
 156 @article{Coquand1986,
 157 author = {Coquand, Thierry and Huet, Gerard},
 158 file = {:home/bitonic/docs/papers/coc.pdf:pdf},
 159 title = {{The calculus of constructions}},
 160 url = {http://hal.inria.fr/docs/00/07/60/24/PDF/RR-0530.pdf},
 161 year = {1986}
 162 }
 163 @article{Curry1934,
 164 author = {Curry, Haskell B.},
 165 file = {:home/bitonic/docs/papers/curry-stlc.pdf:pdf},
 166 journal = {Proceedings of the National Academy of Sciences of the United States of America},
 167 number = {1930},
 168 pages = {584--590},
 169 title = {{Functionality in combinatory logic}},
 170 url = {http://www.ncbi.nlm.nih.gov/pmc/articles/pmc1076489/},
 171 volume = {511},
 172 year = {1934}
 173 }
 174 @article{Dybjer1991,
 175 author = {Dybjer, Peter},
 176 file = {:home/bitonic/docs/papers/dybjer-inductive.ps:ps},
 177 journal = {Logical Frameworks},
 178 title = {{Inductive sets and families in Martin-L\"{o}f's type theory and their set-theoretic semantics}},
 179 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},
 180 year = {1991}
 181 }
 182 @article{Hurkens1995,
 183 author = {Hurkens, Antonius J.C.},
 184 file = {:home/bitonic/docs/papers/hurkens-paradox.pdf:pdf},
 185 journal = {Typed Lambda Calculi and Applications},
 186 title = {{A simplification of Girard's paradox}},
 187 url = {http://www.springerlink.com/index/W718604JN467672H.pdf},
 188 year = {1995}
 189 }
 190 @book{Martin-Lof1984,
 191 author = {Martin-L\"{o}f, Per},
 192 file = {:home/bitonic/docs/papers/martin-lof-tt.pdf:pdf},
 193 isbn = {8870881059},
 194 publisher = {Bibliopolis},
 195 title = {{Intuitionistic type theory}},
 196 year = {1984}
 197 }
 198 @article{McBride2004,
 199 author = {McBride, Conor},
 200 doi = {10.1017/S0956796803004829},
 201 file = {:home/bitonic/docs/papers/view-from-the-left.ps.gz:gz},
 202 journal = {Journal of Functional Programming},
 203 month = jan,
 204 number = {1},
 205 pages = {69--111},
 206 title = {{The View from The Left}},
 207 url = {http://strictlypositive.org/view.ps.gz},
 208 volume = {14},
 209 year = {2004}
 210 }
 211 @phdthesis{Norell2007,
 212 author = {Norell, Ulf},
 213 file = {:home/bitonic/docs/papers/ulf-thesis.pdf:pdf},
 214 isbn = {9789172919969},
 215 school = {Chalmers University of Technology and G\"{o}teborg University},
 216 title = {{Towards a practical programming language based on dependent type theory}},
 217 url = {http://www.cse.chalmers.se/~ulfn/papers/thesis.pdf},
 218 year = {2007}
 219 }
 220 @article{Oury2008,
 221 address = {New York, New York, USA},
 222 author = {Oury, Nicolas and Swierstra, Wouter},
 223 doi = {10.1145/1411204.1411213},
 224 file = {:home/bitonic/docs/papers/powerofpi.pdf:pdf},
 225 isbn = {9781595939197},
 226 journal = {Proceeding of the 13th ACM SIGPLAN international conference on Functional programming - ICFP '08},
 227 pages = {39},
 228 publisher = {ACM Press},
 229 title = {{The power of Pi}},
 230 url = {http://portal.acm.org/citation.cfm?doid=1411204.1411213},
 231 year = {2008}
 232 }
 233 @article{Pierce2000,
 234 author = {Pierce, Benjamin C. and Turner, David N.},
 235 doi = {10.1145/345099.345100},
 236 file = {:home/bitonic/docs/papers/local-type-inference.pdf:pdf},
 237 issn = {01640925},
 238 journal = {ACM Transactions on Programming Languages and Systems},
 239 month = jan,
 240 number = {1},
 241 pages = {1--44},
 242 title = {{Local type inference}},
 243 url = {http://portal.acm.org/citation.cfm?doid=345099.345100},
 244 volume = {22},
 245 year = {2000}
 246 }
 247 @article{Pollack1990,
 248 author = {Pollack, Robert},
 249 file = {:home/bitonic/docs/papers/implicit-syntax.ps:ps},
 250 journal = {Informal Proceedings of First Workshop on Logical Frameworks},
 251 title = {{Implicit syntax}},
 252 url = {http://reference.kfupm.edu.sa/content/i/m/implicit\_syntax\_\_1183660.pdf},
 253 year = {1992}
 254 }
 255 @article{Reynolds1994,
 256 author = {Reynolds, John C.},
 257 file = {:home/bitonic/docs/papers/reynolds-polymorphic-lc.ps:ps},
 258 journal = {Logical Foundations of Functional Programming},
 259 title = {{An introduction to the polymorphic lambda calculus}},
 260 url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.7.9916\&rep=rep1\&type=pdf},
 261 year = {1994}
 262 }
 263 @article{Sulzmann2007,
 264 address = {New York, New York, USA},
 265 author = {Sulzmann, Martin and Chakravarty, Manuel M. T. and Jones, Simon Peyton and Donnelly, Kevin},
 266 doi = {10.1145/1190315.1190324},
 267 file = {:home/bitonic/docs/papers/systemf-coercions.pdf:pdf},
 268 isbn = {159593393X},
 269 journal = {Proceedings of the 2007 ACM SIGPLAN international workshop on Types in languages design and implementation - TLDI '07},
 270 pages = {53},
 271 publisher = {ACM Press},
 272 title = {{System F with type equality coercions}},
 273 url = {http://portal.acm.org/citation.cfm?doid=1190315.1190324},
 274 year = {2007}
 275 }
 276 @article{Vytiniotis2011,
 277 author = {Vytiniotis, Dimitrios and Jones, Simon Peyton and Schrijvers, Tom and Sulzmann, Martin},
 278 file = {:home/bitonic/docs/papers/outsidein.pdf:pdf},
 279 journal = {Journal of Functional Programming},
 280 number = {4-5},
 281 pages = {333--412},
 282 title = {{OutsideIn (X) Modular type inference with local assumptions}},
 283 url = {http://journals.cambridge.org/production/action/cjoGetFulltext?fulltextid=8274818},
 284 volume = {21},
 285 year = {2011}
 286 }
 287 @article{Yorgey2012,
 288 address = {New York, New York, USA},
 289 author = {Yorgey, Brent a. and Weirich, Stephanie and Cretin, Julien and {Peyton Jones}, Simon and Vytiniotis, Dimitrios and Magalh\~{a}es, Jos\'{e} Pedro},
 290 doi = {10.1145/2103786.2103795},
 291 file = {:home/bitonic/docs/papers/haskell-promotion.pdf:pdf},
 292 isbn = {9781450311205},
 293 journal = {Proceedings of the 8th ACM SIGPLAN workshop on Types in language design and implementation - TLDI '12},
 294 pages = {53},
 295 publisher = {ACM Press},
 296 title = {{Giving Haskell a promotion}},
 297 url = {http://dl.acm.org/citation.cfm?doid=2103786.2103795},
 298 year = {2012}
 299 }