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
  17 @article{Altenkirch2010,
  18 author = {Altenkirch, Thorsten and Danielsson, N and L\"{o}h, A and Oury, Nicolas},
  19 file = {:home/bitonic/docs/papers/PiSigma.pdf:pdf},
  20 journal = {Functional and Logic \ldots},
  21 number = {Sheard 2005},
  22 title = {{$\Pi$$\Sigma$: dependent types without the sugar}},
  23 url = {http://www.springerlink.com/index/91W712G2806R575H.pdf},
  24 year = {2010}
  25 }
  26 @article{Altenkirch2007,
  27 address = {New York, New York, USA},
  28 author = {Altenkirch, Thorsten and McBride, Conor and Swierstra, Wouter},
  29 doi = {10.1145/1292597.1292608},
  30 file = {:home/bitonic/docs/papers/OTT2.pdf:pdf},
  31 isbn = {9781595936776},
  32 journal = {Proceedings of the 2007 workshop on Programming languages meets program verification - PLPV '07},
  33 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},
  34 pages = {57},
  35 publisher = {ACM Press},
  36 title = {{Observational equality, now!}},
  37 url = {http://portal.acm.org/citation.cfm?doid=1292597.1292608},
  38 year = {2007}
  39 }
  40 @article{Barendregt1991,
  41 author = {Barendregt, Henk},
  42 file = {:home/bitonic/docs/papers/lambda-cube.pdf:pdf},
  43 journal = {Journal of functional programming},
  44 title = {{Introduction to generalized type systems}},
  45 url = {http://www.diku.dk/hjemmesider/ansatte/henglein/papers/barendregt1991.pdf},
  46 year = {1991}
  47 }
  48 @article{Brady2012,
  49 author = {Brady, Edwin},
  50 file = {:home/bitonic/docs/papers/idris-implementation.pdf:pdf},
  51 journal = {Unpublished draft},
  52 number = {November},
  53 title = {{Implementing General Purpose Dependently Typed Programming Languages}},
  54 url = {http://www.cs.st-andrews.ac.uk/~eb/drafts/impldtp.pdf},
  55 year = {2012}
  56 }
  57 @article{Chapman2010,
  58 address = {New York, New York, USA},
  59 author = {Chapman, James and Dagand, Pierre-\'{E}variste and McBride, Conor and Morris, Peter},
  60 doi = {10.1145/1863543.1863547},
  61 file = {:home/bitonic/docs/papers/conor-levitation.pdf:pdf},
  62 isbn = {9781605587943},
  63 journal = {Proceedings of the 15th ACM SIGPLAN international conference on Functional programming - ICFP '10},
  64 pages = {3},
  65 publisher = {ACM Press},
  66 title = {{The gentle art of levitation}},
  67 url = {http://portal.acm.org/citation.cfm?doid=1863543.1863547},
  68 year = {2010}
  69 }
  70 @article{Church1936,
  71 author = {Church, Alonzo},
  72 file = {:home/bitonic/docs/papers/church-lc.pdf:pdf},
  73 journal = {American journal of mathematics},
  74 number = {2},
  75 pages = {345--363},
  76 title = {{An unsolvable problem of elementary number theory}},
  77 url = {http://www.ams.org/leavingmsn?url=http://dx.doi.org/10.2307/2371045},
  78 volume = {58},
  79 year = {1936}
  80 }
  81 @article{Church1940,
  82 author = {Church, Alonzo},
  83 file = {:home/bitonic/docs/papers/church-stlc.pdf:pdf},
  84 journal = {J. Symb. Log.},
  85 number = {2},
  86 pages = {56--68},
  87 title = {{A formulation of the simple theory of types}},
  88 url = {http://www.ams.org/leavingmsn?url=http://dx.doi.org/10.2307/2266170},
  89 volume = {5},
  90 year = {1940}
  91 }
  92 @article{Coquand1986,
  93 author = {Coquand, Thierry and Huet, Gerard},
  94 file = {:home/bitonic/docs/papers/coc.pdf:pdf},
  95 title = {{The calculus of constructions}},
  96 url = {http://hal.inria.fr/docs/00/07/60/24/PDF/RR-0530.pdf},
  97 year = {1986}
  98 }
  99 @article{Curry1934,
 100 author = {Curry, Haskell B.},
 101 file = {:home/bitonic/docs/papers/curry-stlc.pdf:pdf},
 102 journal = {Proceedings of the National Academy of Sciences of \ldots},
 103 number = {1930},
 104 pages = {584--590},
 105 title = {{Functionality in combinatory logic}},
 106 url = {http://www.ncbi.nlm.nih.gov/pmc/articles/pmc1076489/},
 107 volume = {511},
 108 year = {1934}
 109 }
 110 @article{Hurkens1995,
 111 author = {Hurkens, Antonius J.C.},
 112 file = {:home/bitonic/docs/papers/hurkens-paradox.pdf:pdf},
 113 journal = {Typed Lambda Calculi and Applications},
 114 title = {{A simplification of Girard's paradox}},
 115 url = {http://www.springerlink.com/index/W718604JN467672H.pdf},
 116 year = {1995}
 117 }
 118 @book{Martin-Lof1984,
 119 author = {Martin-L\"{o}f, Per},
 120 file = {:home/bitonic/docs/papers/martin-lof-tt.pdf:pdf},
 121 isbn = {8870881059},
 122 publisher = {Bibliopolis},
 123 title = {{Intuitionistic type theory}},
 124 year = {1984}
 125 }
 126 @article{McBride2004,
 127 author = {McBride, Conor},
 128 doi = {10.1017/S0956796803004829},
 129 file = {:home/bitonic/docs/papers/view-from-the-left.ps.gz:gz},
 130 journal = {Journal of Functional Programming},
 131 month = jan,
 132 number = {1},
 133 pages = {69--111},
 134 title = {{The View from The Left}},
 135 url = {http://strictlypositive.org/view.ps.gz},
 136 volume = {14},
 137 year = {2004}
 138 }
 139 @phdthesis{Norell2007,
 140 author = {Norell, Ulf},
 141 file = {:home/bitonic/docs/papers/ulf-thesis.pdf:pdf},
 142 isbn = {9789172919969},
 143 school = {Chalmers University of Technology and G\"{o}teborg University},
 144 title = {{Towards a practical programming language based on dependent type theory}},
 145 url = {http://www.cse.chalmers.se/~ulfn/papers/thesis.pdf},
 146 year = {2007}
 147 }
 148 @article{Oury2008,
 149 address = {New York, New York, USA},
 150 author = {Oury, Nicolas and Swierstra, Wouter},
 151 doi = {10.1145/1411204.1411213},
 152 file = {:home/bitonic/docs/papers/powerofpi.pdf:pdf},
 153 isbn = {9781595939197},
 154 journal = {Proceeding of the 13th ACM SIGPLAN international conference on Functional programming - ICFP '08},
 155 pages = {39},
 156 publisher = {ACM Press},
 157 title = {{The power of Pi}},
 158 url = {http://portal.acm.org/citation.cfm?doid=1411204.1411213},
 159 year = {2008}
 160 }
 161 @article{Pierce2000,
 162 author = {Pierce, Benjamin C. and Turner, David N.},
 163 doi = {10.1145/345099.345100},
 164 file = {:home/bitonic/docs/papers/local-type-inference.pdf:pdf},
 165 issn = {01640925},
 166 journal = {ACM Transactions on Programming Languages and Systems},
 167 month = jan,
 168 number = {1},
 169 pages = {1--44},
 170 title = {{Local type inference}},
 171 url = {http://portal.acm.org/citation.cfm?doid=345099.345100},
 172 volume = {22},
 173 year = {2000}
 174 }
 175 @article{Pollack1990,
 176 author = {Pollack, Robert},
 177 file = {:home/bitonic/docs/papers/implicit-syntax.ps:ps},
 178 journal = {Informal Proceedings of First Workshop on Logical Frameworks},
 179 title = {{Implicit syntax}},
 180 url = {http://reference.kfupm.edu.sa/content/i/m/implicit\_syntax\_\_1183660.pdf},
 181 year = {1992}
 182 }
 183 @article{Reynolds1994,
 184 author = {Reynolds, John C.},
 185 file = {:home/bitonic/docs/papers/reynolds-polymorphic-lc.ps:ps},
 186 journal = {Logical Foundations of Functional Programming},
 187 title = {{An introduction to the polymorphic lambda calculus}},
 188 url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.7.9916\&rep=rep1\&type=pdf},
 189 year = {1994}
 190 }
 191 @article{Sulzmann2007,
 192 address = {New York, New York, USA},
 193 author = {Sulzmann, Martin and Chakravarty, Manuel M. T. and Jones, Simon Peyton and Donnelly, Kevin},
 194 doi = {10.1145/1190315.1190324},
 195 file = {:home/bitonic/docs/papers/systemf-coercions.pdf:pdf},
 196 isbn = {159593393X},
 197 journal = {Proceedings of the 2007 ACM SIGPLAN international workshop on Types in languages design and implementation - TLDI '07},
 198 pages = {53},
 199 publisher = {ACM Press},
 200 title = {{System F with type equality coercions}},
 201 url = {http://portal.acm.org/citation.cfm?doid=1190315.1190324},
 202 year = {2007}
 203 }
 204 @article{Vytiniotis2011,
 205 author = {Vytiniotis, Dimitrios and Jones, Simon Peyton and Schrijvers, Tom and Sulzmann, Martin},
 206 file = {:home/bitonic/docs/papers/outsidein.pdf:pdf},
 207 journal = {Journal of Functional Programming},
 208 number = {4-5},
 209 pages = {333--412},
 210 title = {{OutsideIn (X) Modular type inference with local assumptions}},
 211 url = {http://journals.cambridge.org/production/action/cjoGetFulltext?fulltextid=8274818},
 212 volume = {21},
 213 year = {2011}
 214 }
 215 @article{Yorgey2012,
 216 address = {New York, New York, USA},
 217 author = {Yorgey, Brent a. and Weirich, Stephanie and Cretin, Julien and {Peyton Jones}, Simon and Vytiniotis, Dimitrios and Magalh\~{a}es, Jos\'{e} Pedro},
 218 doi = {10.1145/2103786.2103795},
 219 file = {:home/bitonic/docs/papers/haskell-promotion.pdf:pdf},
 220 isbn = {9781450311205},
 221 journal = {Proceedings of the 8th ACM SIGPLAN workshop on Types in language design and implementation - TLDI '12},
 222 pages = {53},
 223 publisher = {ACM Press},
 224 title = {{Giving Haskell a promotion}},
 225 url = {http://dl.acm.org/citation.cfm?doid=2103786.2103795},
 226 year = {2012}
 227 }