final.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.3},
  33   url = {http://www.haskell.org/ghc/docs/latest/html/users_guide/},
  34   howpublished = {\url{http://www.haskell.org/ghc/docs/7.6.3/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{Brady2013,
 108 author = {Brady, Edwin},
 109 file = {:home/bitonic/docs/papers/idris-implementation.pdf:pdf},
 110 journal = {Unpublished draft},
 111 number = {November},
 112 title = {{Implementing General Purpose Dependently Typed Programming Languages}},
 113 url = {http://www.cs.st-andrews.ac.uk/~eb/drafts/impldtp.pdf},
 114 year = {2013}
 115 }
 116 @article{Chapman2010,
 117 address = {New York, New York, USA},
 118 author = {Chapman, James and Dagand, Pierre-\'{E}variste and McBride, Conor and Morris, Peter},
 119 doi = {10.1145/1863543.1863547},
 120 file = {:home/bitonic/docs/papers/conor-levitation.pdf:pdf},
 121 isbn = {9781605587943},
 122 journal = {Proceedings of the 15th ACM SIGPLAN international conference on Functional programming - ICFP '10},
 123 pages = {3},
 124 publisher = {ACM Press},
 125 title = {{The gentle art of levitation}},
 126 url = {http://portal.acm.org/citation.cfm?doid=1863543.1863547},
 127 year = {2010}
 128 }
 129 @article{Church1936,
 130 author = {Church, Alonzo},
 131 file = {:home/bitonic/docs/papers/church-lc.pdf:pdf},
 132 journal = {American journal of mathematics},
 133 number = {2},
 134 pages = {345--363},
 135 title = {{An unsolvable problem of elementary number theory}},
 136 url = {http://www.ams.org/leavingmsn?url=http://dx.doi.org/10.2307/2371045},
 137 volume = {58},
 138 year = {1936}
 139 }
 140 @article{Church1940,
 141 author = {Church, Alonzo},
 142 file = {:home/bitonic/docs/papers/church-stlc.pdf:pdf},
 143 journal = {J. Symb. Log.},
 144 number = {2},
 145 pages = {56--68},
 146 title = {{A formulation of the simple theory of types}},
 147 url = {http://www.ams.org/leavingmsn?url=http://dx.doi.org/10.2307/2266170},
 148 volume = {5},
 149 year = {1940}
 150 }
 151 @article{Coquand1986,
 152 author = {Coquand, Thierry and Huet, Gerard},
 153 file = {:home/bitonic/docs/papers/coc.pdf:pdf},
 154 title = {{The calculus of constructions}},
 155 url = {http://hal.inria.fr/docs/00/07/60/24/PDF/RR-0530.pdf},
 156 year = {1986}
 157 }
 158 @article{Curry1934,
 159 author = {Curry, Haskell B.},
 160 file = {:home/bitonic/docs/papers/curry-stlc.pdf:pdf},
 161 journal = {Proceedings of the National Academy of Sciences of the United States of America},
 162 number = {1930},
 163 pages = {584--590},
 164 title = {{Functionality in combinatory logic}},
 165 url = {http://www.ncbi.nlm.nih.gov/pmc/articles/pmc1076489/},
 166 volume = {511},
 167 year = {1934}
 168 }
 169 @article{Dybjer1991,
 170 author = {Dybjer, Peter},
 171 file = {:home/bitonic/docs/papers/dybjer-inductive.ps:ps},
 172 journal = {Logical Frameworks},
 173 title = {{Inductive sets and families in Martin-L\"{o}f's type theory and their set-theoretic semantics}},
 174 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},
 175 year = {1991}
 176 }
 177 @article{Hurkens1995,
 178 author = {Hurkens, Antonius J.C.},
 179 file = {:home/bitonic/docs/papers/hurkens-paradox.pdf:pdf},
 180 journal = {Typed Lambda Calculi and Applications},
 181 title = {{A simplification of Girard's paradox}},
 182 url = {http://www.springerlink.com/index/W718604JN467672H.pdf},
 183 year = {1995}
 184 }
 185 @article{Jacobs1997,
 186 author = {Jacobs, Bart and Rutten, Jan},
 187 file = {:home/bitonic/docs/papers/coalgebra-coind.pdf:pdf},
 188 journal = {EATCS Bulletin},
 189 number = {1997},
 190 title = {{A tutorial on (co) algebras and (co) induction}},
 191 url = {http://synrc.com/publications/cat/Logic/CoinductionCoalgebrasTutorial.pdf},
 192 volume = {62},
 193 year = {1997}
 194 }
 195 @book{Martin-Lof1984,
 196 author = {Martin-L\"{o}f, Per},
 197 file = {:home/bitonic/docs/papers/martin-lof-tt.pdf:pdf},
 198 isbn = {8870881059},
 199 publisher = {Bibliopolis},
 200 title = {{Intuitionistic type theory}},
 201 year = {1984}
 202 }
 203
 204 @Article{McBride2004,
 205    journal = {{J}ournal of {F}unctional {P}rogramming},
 206    pages = {69--111},
 207    number = {1},
 208    volume = {14},
 209    title = {The view from the left},
 210    year = {2004},
 211    author = {C. McBride and J. McKinna}
 212 }
 213
 214 @phdthesis{Gimenez1996,
 215 author={Giménez, Eduardo},
 216 title={Un calcul de constructions infinies et son application {\`a} la v{\'e}rification de syst{\`e}mes communicants},
 217 school = {Ecole Normale Sup{\'e}rieure de Lyon},
 218 year = 1996
 219 }
 220
 221 @phdthesis{McBride1999,
 222 author = {McBride, Conor},
 223 file = {:home/bitonic/.local/share/data/Mendeley Ltd./Mendeley Desktop/Downloaded/McBride - 1999 - Dependently typed functional programs and their proofs.pdf:pdf},
 224 school = {University of Edinburgh},
 225 title = {{Dependently typed functional programs and their proofs}},
 226 url = {http://lac-repo-live7.is.ed.ac.uk/handle/1842/374},
 227 year = {1999}
 228 }
 229 @phdthesis{Norell2007,
 230 author = {Norell, Ulf},
 231 file = {:home/bitonic/docs/papers/ulf-thesis.pdf:pdf},
 232 isbn = {9789172919969},
 233 school = {Chalmers University of Technology and G\"{o}teborg University},
 234 title = {{Towards a practical programming language based on dependent type theory}},
 235 url = {http://www.cse.chalmers.se/~ulfn/papers/thesis.pdf},
 236 year = {2007}
 237 }
 238 @article{Oury2008,
 239 address = {New York, New York, USA},
 240 author = {Oury, Nicolas and Swierstra, Wouter},
 241 doi = {10.1145/1411204.1411213},
 242 file = {:home/bitonic/docs/papers/powerofpi.pdf:pdf},
 243 isbn = {9781595939197},
 244 journal = {Proceeding of the 13th ACM SIGPLAN international conference on Functional programming - ICFP '08},
 245 pages = {39},
 246 publisher = {ACM Press},
 247 title = {{The power of Pi}},
 248 url = {http://portal.acm.org/citation.cfm?doid=1411204.1411213},
 249 year = {2008}
 250 }
 251 @article{Pierce2000,
 252 author = {Pierce, Benjamin C. and Turner, David N.},
 253 doi = {10.1145/345099.345100},
 254 file = {:home/bitonic/docs/papers/local-type-inference.pdf:pdf},
 255 issn = {01640925},
 256 journal = {ACM Transactions on Programming Languages and Systems},
 257 month = jan,
 258 number = {1},
 259 pages = {1--44},
 260 title = {{Local type inference}},
 261 url = {http://portal.acm.org/citation.cfm?doid=345099.345100},
 262 volume = {22},
 263 year = {2000}
 264 }
 265 @article{Pollack1990,
 266 author = {Pollack, Robert},
 267 file = {:home/bitonic/docs/papers/implicit-syntax.ps:ps},
 268 journal = {Informal Proceedings of First Workshop on Logical Frameworks},
 269 title = {{Implicit syntax}},
 270 url = {http://reference.kfupm.edu.sa/content/i/m/implicit\_syntax\_\_1183660.pdf},
 271 year = {1992}
 272 }
 273 @article{Reynolds1994,
 274 author = {Reynolds, John C.},
 275 file = {:home/bitonic/docs/papers/reynolds-polymorphic-lc.ps:ps},
 276 journal = {Logical Foundations of Functional Programming},
 277 title = {{An introduction to the polymorphic lambda calculus}},
 278 url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.7.9916\&rep=rep1\&type=pdf},
 279 year = {1994}
 280 }
 281 @article{Sulzmann2007,
 282 address = {New York, New York, USA},
 283 author = {Sulzmann, Martin and Chakravarty, Manuel M. T. and Jones, Simon Peyton and Donnelly, Kevin},
 284 doi = {10.1145/1190315.1190324},
 285 file = {:home/bitonic/docs/papers/systemf-coercions.pdf:pdf},
 286 isbn = {159593393X},
 287 journal = {Proceedings of the 2007 ACM SIGPLAN international workshop on Types in languages design and implementation - TLDI '07},
 288 pages = {53},
 289 publisher = {ACM Press},
 290 title = {{System F with type equality coercions}},
 291 url = {http://portal.acm.org/citation.cfm?doid=1190315.1190324},
 292 year = {2007}
 293 }
 294 @article{Tait1967,
 295 author = {Tait, William W.},
 296 file = {:home/bitonic/docs/papers/tait-normalising.pdf:pdf},
 297 journal = {The Journal of Symbolic Logic},
 298 number = {2},
 299 pages = {198--212},
 300 title = {{Intensional Interpretations of Functionals of Finite Type}},
 301 volume = {32},
 302 year = {1967}
 303 }
 304 @article{Vytiniotis2011,
 305 author = {Vytiniotis, Dimitrios and Jones, Simon Peyton and Schrijvers, Tom and Sulzmann, Martin},
 306 file = {:home/bitonic/docs/papers/outsidein.pdf:pdf},
 307 journal = {Journal of Functional Programming},
 308 number = {4-5},
 309 pages = {333--412},
 310 title = {{OutsideIn (X) Modular type inference with local assumptions}},
 311 url = {http://journals.cambridge.org/production/action/cjoGetFulltext?fulltextid=8274818},
 312 volume = {21},
 313 year = {2011}
 314 }
 315 @article{Yorgey2012,
 316 address = {New York, New York, USA},
 317 author = {Yorgey, Brent a. and Weirich, Stephanie and Cretin, Julien and {Peyton Jones}, Simon and Vytiniotis, Dimitrios and Magalh\~{a}es, Jos\'{e} Pedro},
 318 doi = {10.1145/2103786.2103795},
 319 file = {:home/bitonic/docs/papers/haskell-promotion.pdf:pdf},
 320 isbn = {9781450311205},
 321 journal = {Proceedings of the 8th ACM SIGPLAN workshop on Types in language design and implementation - TLDI '12},
 322 pages = {53},
 323 publisher = {ACM Press},
 324 title = {{Giving Haskell a promotion}},
 325 url = {http://dl.acm.org/citation.cfm?doid=2103786.2103795},
 326 year = {2012}
 327 }
 328
 329 @ARTICLE{Loh2010,
 330   author = {Andres L{\"o}h and Conor McBride and Wouter Swierstra},
 331   title = {A Tutorial Implementation of a Dependently Typed Lambda Calculus},
 332   journal = {Fundam. Inform.},
 333   year = {2010},
 334   volume = {102},
 335   pages = {177-207},
 336   number = {2},
 337   bibsource = {DBLP, http://dblp.uni-trier.de},
 338   ee = {http://dx.doi.org/10.3233/FI-2010-304},
 339   file = {:home/bitonic/docs/papers/simply-easy.pdf:pdf},
 340   owner = {bitonic}
 341 }
 342
 343 @ARTICLE{Bruijn91,
 344   author = {de Bruijn, Nicolaas Govert},
 345   title = {Telescopic mappings in typed lambda calculus},
 346   journal = {Information and Computation},
 347   year = {1991},
 348   volume = {91},
 349   pages = {189--204},
 350   number = {2},
 351   file = {:/home/bitonic/docs/papers/telescopes.pdf:PDF},
 352   publisher = {Elsevier}
 353 }
 354
 355 @UNPUBLISHED{Huet1988,
 356   author = {Huet, Gerard P.},
 357   title = {Extending The Calculus of Constructions with Type:Type},
 358   note = {Unpublished draft},
 359   year = {1988},
 360   file = {:home/bitonic/docs/papers/huet-typtyp.pdf:pdf},
 361   owner = {bitonic},
 362   timestamp = {2013.06.10}
 363 }
 364
 365 @ARTICLE{Harper1991,
 366   author = {Harper, Robert and Pollack, Robert},
 367   title = {Type checking with universes},
 368   journal = {Theoretical computer science},
 369   year = {1991},
 370   volume = {89},
 371   pages = {107--136},
 372   number = {1},
 373   file = {:/home/bitonic/docs/papers/type-checking-universes.ps.gz:PostScript},
 374   publisher = {Elsevier}
 375 }
 376
 377 @ARTICLE{Jacobs1994,
 378     author = {Jacobs, Bart},
 379     title = {Quotients in Simple Type Theory},
 380     journal = {Manuscript, Math. Inst},
 381     year = {1994}
 382 }
 383
 384 @inproceedings{Hofmann1994,
 385   title={The groupoid model refutes uniqueness of identity proofs},
 386   author={Hofmann, Martin and Streicher, Thomas},
 387   booktitle={Logic in Computer Science, 1994. LICS'94. Proceedings., Symposium on},
 388   pages={208--212},
 389   year={1994},
 390   organization={IEEE}
 391 }
 392
 393 @INPROCEEDINGS{Coquand1992,
 394   author = {Coquand, Thierry},
 395   title = {Pattern matching with dependent types},
 396   booktitle = {Informal proceedings of Logical Frameworks},
 397   year = {1992},
 398   volume = {92},
 399   pages = {66--79},
 400   file = {:/home/bitonic/docs/papers/coquand-pattern.ps:PostScript}
 401 }
 402
 403 @INPROCEEDINGS{Abel2007,
 404   author = {Abel, Andreas and Coquand, Thierry and Dybjer, Peter},
 405   title = {Normalization by evaluation for Martin-Lof type theory with typed
 406         equality judgements},
 407   booktitle = {Logic in Computer Science, 2007. LICS 2007. 22nd Annual IEEE Symposium
 408         on},
 409   year = {2007},
 410   pages = {3--12},
 411   organization = {IEEE},
 412   file = {:/home/bitonic/docs/papers/nbe.pdf:PDF}
 413 }
 414
 415 @inproceedings{McBride2004b,
 416   title={I am not a number: I am a free variable},
 417   author={McBride, Conor and McKinna, James},
 418   booktitle={Proceedings of the ACM SIGPLAN Haskell Workshop},
 419   year={2004},
 420 }
 421
 422 @article{Bird1999,
 423   title={De Bruijn notation as a nested datatype},
 424   author={Richard S. Bird and Ross Paterson},
 425   journal={J. Functional Programming},
 426   volume={9},
 427   number={1},
 428   pages={77--91},
 429   year={1999},
 430   publisher={Cambridge Univ Press}
 431 }
 432
 433 @inproceedings{de1972lambda,
 434   title={Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem},
 435   author={de Bruijn, Nicolaas Govert},
 436   booktitle={Indagationes Mathematicae (Proceedings)},
 437   volume={75},
 438   number={5},
 439   pages={381--392},
 440   year={1972},
 441   organization={Elsevier}
 442 }
 443
 444 @article{henglein1993type,
 445   title={Type inference with polymorphic recursion},
 446   author={Henglein, Fritz},
 447   journal={ACM Transactions on Programming Languages and Systems (TOPLAS)},
 448   volume={15},
 449   number={2},
 450   pages={253--289},
 451   year={1993},
 452   publisher={ACM}
 453 }
 454
 455 @inproceedings{weirich2011binders,
 456   title={Binders unbound},
 457   author={Weirich, Stephanie and Yorgey, Brent A and Sheard, Tim},
 458   booktitle={ACM SIGPLAN Notices},
 459   volume={46},
 460   number={9},
 461   pages={333--345},
 462   year={2011},
 463   organization={ACM}
 464 }
 465
 466 @inproceedings{King1995,
 467   title={Structuring depth-first search algorithms in Haskell},
 468   author={King, David J and Launchbury, John},
 469   booktitle={Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages},
 470   pages={344--354},
 471   year={1995},
 472   organization={ACM}
 473 }
 474
 475 @article{milner1978theory,
 476   title={A theory of type polymorphism in programming},
 477   author={Milner, Robin},
 478   journal={Journal of computer and system sciences},
 479   volume={17},
 480   number={3},
 481   pages={348--375},
 482   year={1978},
 483   publisher={Elsevier}
 484 }
 485
 486 @article{dagand2012elaborating,
 487   title={Elaborating inductive definitions},
 488   author={Dagand, Pierre-Evariste and McBride, Conor},
 489   journal={arXiv preprint arXiv:1210.6390},
 490   year={2012}
 491 }
 492
 493 @inproceedings{chapman2010gentle,
 494   title={The gentle art of levitation},
 495   author={Chapman, James and Dagand, Pierre-{\'E}variste and McBride, Conor and Morris, Peter},
 496   booktitle={ACM Sigplan Notices},
 497   volume={45},
 498   number={9},
 499   pages={3--14},
 500   year={2010},
 501   organization={ACM}
 502 }
 503
 504 @article{dybjer2000general,
 505   title={A general formulation of simultaneous inductive-recursive definitions in type theory},
 506   author={Dybjer, Peter},
 507   journal={Journal of Symbolic Logic},
 508   pages={525--549},
 509   year={2000},
 510   publisher={JSTOR}
 511 }
 512
 513 @inproceedings{chakravarty2005associated,
 514   title={Associated types with class},
 515   author={Chakravarty, Manuel MT and Keller, Gabriele and Jones, Simon Peyton and Marlow, Simon},
 516   booktitle={ACM SIGPLAN Notices},
 517   volume={40},
 518   number={1},
 519   pages={1--13},
 520   year={2005},
 521   organization={ACM}
 522 }
 523
 524 @article{miller1992unification,
 525   title={Unification under a mixed prefix},
 526   author={Miller, Dale},
 527   journal={Journal of symbolic computation},
 528   volume={14},
 529   number={4},
 530   pages={321--358},
 531   year={1992},
 532   publisher={Elsevier}
 533 }
 534
 535 @UNPUBLISHED{gundrytutorial,
 536   title={A tutorial implementation of dynamic pattern unification},
 537   author={Gundry, Adam and McBride, Conor},
 538   note= {Unpublished draft},
 539   year={2013}
 540 }
 541
 542 @techreport{cockett1992charity,
 543   title={About charity},
 544   author={Cockett, Robin and Fukushima, Tom},
 545   year={1992},
 546   journal={Yellow Series Report}
 547 }
 548
 549 @incollection{mcbride2009let,
 550   title={Let’s see how things unfold: Reconciling the infinite with the intensional},
 551   author={McBride, Conor},
 552   booktitle={Algebra and Coalgebra in Computer Science},
 553   pages={113--126},
 554   year={2009},
 555   publisher={Springer}
 556 }
 557
 558 @article{huet1973undecidability,
 559   title={The undecidability of unification in third order logic},
 560   author={Huet, Gerard P.},
 561   journal={Information and Control},
 562   volume={22},
 563   number={3},
 564   pages={257--267},
 565   year={1973},
 566   publisher={Elsevier}
 567 }
 568
 569 @article{dybjer1997representing,
 570   title={Representing inductively defined sets by wellorderings in Martin-L{\"o}f's type theory},
 571   author={Dybjer, Peter},
 572   journal={Theoretical Computer Science},
 573   volume={176},
 574   number={1},
 575   pages={329--335},
 576   year={1997},
 577   publisher={Elsevier}
 578 }
 579
 580 @inbook{Nordstrom1990,
 581   author = {Nordstr{\"o}m, Bengt and Petersson, Kent and Smith, Jan M.},
 582   title = {Programming in Martin-L{\"o}f Type Theory: An Introduction},
 583   publisher = {Oxford University Press},
 584   year = {1990}
 585 }
 586
 587 @incollection{Gimenez1995,
 588 year={1995},
 589 isbn={978-3-540-60579-9},
 590 booktitle={Types for Proofs and Programs},
 591 volume={996},
 592 series={Lecture Notes in Computer Science},
 593 editor={Dybjer, Peter and Nordström, Bengt and Smith, Jan},
 594 doi={10.1007/3-540-60579-7_3},
 595 title={Codifying guarded definitions with recursive schemes},
 596 url={http://dx.doi.org/10.1007/3-540-60579-7_3},
 597 publisher={Springer Berlin Heidelberg},
 598 author={Giménez, Eduardo},
 599 pages={39-59}
 600 }
 601
 602 @article{Capretta2005,
 603   author    = {Venanzio Capretta},
 604   title     = {General recursion via coinductive types},
 605   journal   = {Logical Methods in Computer Science},
 606   volume    = {1},
 607   number    = {2},
 608   year      = {2005},
 609   ee        = {http://dx.doi.org/10.2168/LMCS-1(2:1)2005},
 610   bibsource = {DBLP, http://dblp.uni-trier.de}
 611 }
 612
 613 @article{Danielsson2012,
 614  author = {Danielsson, Nils Anders},
 615  title = {Operational semantics using the partiality monad},
 616  journal = {SIGPLAN Not.},
 617  issue_date = {September 2012},
 618  volume = {47},
 619  number = {9},
 620  month = sep,
 621  year = {2012},
 622  issn = {0362-1340},
 623  pages = {127--138},
 624  numpages = {12},
 625  url = {http://doi.acm.org/10.1145/2398856.2364546},
 626  doi = {10.1145/2398856.2364546},
 627  acmid = {2364546},
 628  publisher = {ACM},
 629  address = {New York, NY, USA},
 630  keywords = {dependent types, mixed induction and coinduction, partiality monad},
 631 }
 632
 633
 634 @incollection{Paulson1990,
 635         Author = {Paulson, Lawrence C.},
 636         Booktitle = {Logic and Computer Science},
 637         Date-Modified = {2005-04-20 12:07:55 +0100},
 638         Editor = {P. Odifreddi},
 639         Pages = {361-386},
 640         Publisher = {Academic Press},
 641         Title = {{Isabelle}: The Next 700 Theorem Provers},
 642         Year = {1990}}
 643
 644
 645 @book{Russell1927,
 646       author       = "Whitehead, Alfred North and Russell, Bertrand Arthur
 647                       William",
 648       title        = "Principia mathematica; 2nd ed.",
 649       publisher    = "Cambridge Univ. Press",
 650       address      = "Cambridge",
 651       year         = "1927",
 652 }