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