gdp.bib

@article{Breitner:2014:SZC:2692915.2628141,
 author = {Breitner, Joachim and Eisenberg, Richard A. and Peyton Jones, Simon and Weirich, Stephanie},
 title = {Safe Zero-cost Coercions for Haskell},
 journal = {SIGPLAN Not.},
 issue_date = {September 2014},
 volume = {49},
 number = {9},
 month = aug,
 year = {2014},
 issn = {0362-1340},
 pages = {189--202},
 numpages = {14},
 url = {http://doi.acm.org/10.1145/2692915.2628141},
 doi = {10.1145/2692915.2628141},
 acmid = {2628141},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {coercion, haskell, newtype deriving, type class},
}

@article{timany2017logical,
  title={A logical relation for monadic encapsulation of state: Proving contextual equivalences in the presence of {runST}},
  author={Timany, Amin and Stefanesco, L{\'e}o and Krogh-Jespersen, Morten and Birkedal, Lars},
  journal={Proceedings of the ACM on Programming Languages},
  volume={2},
  number={POPL},
  pages={64},
  year={2017},
  publisher={ACM}
}

@inproceedings{launchbury1994lazy,
  title={Lazy functional state threads},
  author={Launchbury, John and Peyton Jones, Simon L},
  booktitle={ACM SIGPLAN Notices},
  volume={29},
  number={6},
  pages={24--35},
  year={1994},
  organization={ACM}
}

@misc{refined,
  title = {Announcing the refinement types library},
  author={Volkov, Nikita},
  year={2016},
  howpublished = {\url{http://nikita-volkov.github.io/refined/}},
  note = {Accessed: 2018-05-30}
}

@misc{this,
  title = {Ghosts of Departed Proofs},
  author={Noonan, Matt},
  year={2018},
  howpublished = {\url{http://www.github.com/matt-noonan/gdp-paper/}},
  note = {Accessed: 2018-06-03}
}

@misc{this-hackage,
  title = {The {gdp} library},
  author={Noonan, Matt},
  year={2018},
  howpublished = {\url{http://hackage.haskell.org/package/gdp}},
  note = {Accessed: 2018-06-03}
}

@book{smullyan1995first,
  title={First-order logic},
  author={Smullyan, Raymond M},
  year={1995},
  publisher={Courier Corporation}
}

@inproceedings{augustsson1998cayenne,
  title={Cayenne—a language with dependent types},
  author={Augustsson, Lennart},
  booktitle={International School on Advanced Functional Programming},
  pages={240--267},
  year={1998},
  organization={Springer}
}

@incollection{bove2009dependent,
  title={Dependent types at work},
  author={Bove, Ana and Dybjer, Peter},
  booktitle={Language engineering and rigorous software development},
  pages={57--99},
  year={2009},
  publisher={Springer}
}

@inproceedings{freeman1991refinement,
 author = {Freeman, Tim and Pfenning, Frank},
 title = {Refinement Types for {ML}},
 booktitle = {Proceedings of the ACM SIGPLAN 1991 Conference on Programming Language Design and Implementation},
 series = {PLDI '91},
 year = {1991},
 isbn = {0-89791-428-7},
 location = {Toronto, Ontario, Canada},
 pages = {268--277},
 numpages = {10},
 url = {http://doi.acm.org/10.1145/113445.113468},
 doi = {10.1145/113445.113468},
 acmid = {113468},
 publisher = {ACM},
 address = {New York, NY, USA},
}

@inproceedings{wadler1990linear,
  title={Linear types can change the world!},
  author={Wadler, Philip},
    booktitle = {Programming Concepts and Methods},
    year = {1990},
    publisher = {North}
}

@misc{pitofsuccess,
  title = {The Pit of Success},
  author={Abrams, Brad},
  year={2003},
  howpublished = {\url{https://blogs.msdn.microsoft.com/brada/2003/10/02/the-pit-of-success/}},
  note = {Accessed: 2018-06-04}
}

@incollection{leavens1999jml,
  title={{JML}: A notation for detailed design},
  author={Leavens, Gary T and Baker, Albert L and Ruby, Clyde},
  booktitle={Behavioral Specifications of Businesses and Systems},
  pages={175--188},
  year={1999},
  publisher={Springer}
}

@book{vazou2016liquid,
  title={Liquid Haskell: Haskell as a theorem prover},
  author={Vazou, Niki},
  year={2016},
  publisher={University of California, San Diego}
}

@inproceedings{spector2018total,
  title={Total {Haskell} is reasonable {Coq}},
  author={Spector-Zabusky, Antal and Breitner, Joachim and Rizkallah, Christine and Weirich, Stephanie},
  booktitle={Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs},
  pages={14--27},
  year={2018},
  organization={ACM}
}

@article{vytiniotis2011outsidein,
  title={{OutsideIn}(X): Modular type inference with local assumptions},
  author={Vytiniotis, Dimitrios and Jones, Simon Peyton and Schrijvers, Tom and Sulzmann, Martin},
  journal={Journal of functional programming},
  volume={21},
  number={4-5},
  pages={333--412},
  year={2011},
  publisher={Cambridge University Press}
}

@inproceedings{stolarek2015injective,
  title={Injective type families for {Haskell}},
  author={Stolarek, Jan and Peyton Jones, Simon and Eisenberg, Richard A.},
 booktitle = {Proceedings of the 2015 ACM SIGPLAN Symposium on Haskell},
 series = {Haskell '15},
 year = {2015},
 isbn = {978-1-4503-3808-0},
 location = {Vancouver, BC, Canada},
 pages = {118--128},
 numpages = {11},
 url = {http://doi.acm.org/10.1145/2804302.2804314},
 doi = {10.1145/2804302.2804314},
 acmid = {2804314},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {Haskell, functional dependencies, injectivity, type families, type-level programming},
}

@article{kiselyov2006lightweight,
 author = {Kiselyov, Oleg and Shan, Chung-chieh},
 title = {Lightweight Static Capabilities},
 journal = {Electron. Notes Theor. Comput. Sci.},
 issue_date = {June, 2007},
 volume = {174},
 number = {7},
 month = jun,
 year = {2007},
 issn = {1571-0661},
 pages = {79--104},
 numpages = {26},
 url = {http://dx.doi.org/10.1016/j.entcs.2006.10.039},
 doi = {10.1016/j.entcs.2006.10.039},
 acmid = {1265736},
 publisher = {Elsevier Science Publishers B. V.},
 address = {Amsterdam, The Netherlands, The Netherlands},
 keywords = {Modular programming, safety property, static types, verification},
}

@inproceedings{kiselyov2004functional,
  title={Functional pearl: {I}mplicit configurations--or, type classes reflect the values of types},
  author={Kiselyov, Oleg and Shan, Chung-chieh},
  booktitle={Proceedings of the 2004 ACM SIGPLAN workshop on Haskell},
  pages={33--44},
  year={2004},
  organization={ACM}
}

@inproceedings{Leijen:1999:DSE:1267936.1267945,
 author = {Leijen, Daan and Meijer, Erik},
 title = {Domain Specific Embedded Compilers},
 booktitle = {Proceedings of the 2Nd Conference on Conference on Domain-Specific Languages - Volume 2},
 series = {DSL'99},
 year = {1999},
 location = {Austin, Texas},
 pages = {9--9},
 numpages = {1},
 url = {http://dl.acm.org/citation.cfm?id=1267936.1267945},
 acmid = {1267945},
 publisher = {USENIX Association},
 address = {Berkeley, CA, USA},
}

@article{Fluet:2006:PTS:1180085.1180088,
 author = {Fluet, Matthew and Pucella, Riccardo},
 title = {Phantom Types and Subtyping},
 journal = {J. Funct. Program.},
 issue_date = {November 2006},
 volume = {16},
 number = {6},
 month = nov,
 year = {2006},
 issn = {0956-7968},
 pages = {751--791},
 numpages = {41},
 url = {http://dx.doi.org/10.1017/S0956796806006046},
 doi = {10.1017/S0956796806006046},
 acmid = {1180088},
 publisher = {Cambridge University Press},
 address = {New York, NY, USA},
}

@inproceedings{Leijen:2004:WPC:1017472.1017483,
 author = {Leijen, Daan},
 title = {{wxHaskell}: A Portable and Concise {GUI} Library for {Haskell}},
 booktitle = {Proceedings of the 2004 ACM SIGPLAN Workshop on Haskell},
 series = {Haskell '04},
 year = {2004},
 isbn = {1-58113-850-4},
 location = {Snowbird, Utah, USA},
 pages = {57--68},
 numpages = {12},
 url = {http://doi.acm.org/10.1145/1017472.1017483},
 doi = {10.1145/1017472.1017483},
 acmid = {1017483},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {C++, Haskell, combinator library, graphical user interface, layout, wxWidgets},
}