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