thesis.bib

@article{hughes86,
 author = {Hughes, R J M},
 title = {A novel representation of lists and its application to the function "reverse"},
 journal = {Information Processing Letters},
 volume = {22},
 number = {3},
 year = {1986},
 pages = {141--144},
 publisher = {Elsevier North-Holland, Inc.},
 address = {Amsterdam},
 }
@INPROCEEDINGS{meyer85,
  author = {Albert R. Meyer and Mitchell Wand},
  title = {Continuation Semantics in Typed Lambda-Calculi},
  booktitle = {Logics of Programs},
  year = {1985},
  pages = {219--224},
  publisher = {Springer-Verlag}
}
@inproceedings{meijer95,
 author = {Meijer, Erik and Hutton, Graham},
 title = {Bananas in space: extending fold and unfold to exponential types},
 booktitle = {Proceedings of the seventh international conference on Functional programming languages and computer architecture},
 series = {FPCA '95},
 year = {1995},
 isbn = {0-89791-719-7},
 location = {La Jolla, California, United States},
 pages = {324--333},
 numpages = {10},
 url = {http://doi.acm.org/10.1145/224164.224225},
 doi = {http://doi.acm.org/10.1145/224164.224225},
 acmid = {224225},
 publisher = {ACM},
 address = {New York, NY, USA},
}
@article{erwig07,
  author    = {Martin Erwig and
               Deling Ren},
  title     = {An update calculus for expressing type-safe program updates},
  journal   = {Sci. Comput. Program.},
  volume    = {67},
  number    = {2-3},
  year      = {2007},
  pages     = {199-222},
  ee        = {http://dx.doi.org/10.1016/j.scico.2007.01.003},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@techreport{heeren02,
    address = {University Utrecht, Netherlands},
    author = {Heeren, Bastiaan and Hage, Jurriaan and Swierstra, Doaitse},
    citeulike-article-id = {271085},
    citeulike-linkout-0 = {http://archive.cs.uu.nl/pub/RUU/CS/techreps/CS-2002/2002-031.pdf},
    institution = {Institute of Information and Computing Science},
    keywords = {gradu, type-errors, type-inference},
    month = jul,
    posted-at = {2005-08-01 21:45:40},
    priority = {2},
    title = {{Generalizing Hindley-Milner Type Inference Algorithms}},
    url = {http://archive.cs.uu.nl/pub/RUU/CS/techreps/CS-2002/2002-031.pdf},
    year = {2002}
}
@inproceedings{keller10,
  author = {Keller, Chantal and Altenkirch, Thorsten},
  title = {Hereditary substitutions for simple types, formalized},
  booktitle = {Proceedings of the third ACM SIGPLAN workshop on Mathematically structured functional programming},
  series = {MSFP '10},
  year = {2010},
  isbn = {978-1-4503-0255-5},
  location = {Baltimore, Maryland, USA},
  pages = {3--10},
  numpages = {8},
  url = {http://doi.acm.org/10.1145/1863597.1863601},
  doi = {10.1145/1863597.1863601},
  acmid = {1863601},
  publisher = {ACM},
  address = {New York, NY, USA},
  keywords = {decidability of {\$\beta\$}\&\#951;-equality, hereditary substitutions, normalizer, type theory},
} 
@inproceedings{keuchel11,
 author = {Keuchel, Steven and Jeuring, Johan T.},
 title = {Generic conversions of abstract syntax representations},
 booktitle = {Proceedings of the 8th ACM SIGPLAN workshop on Generic programming},
 series = {WGP '12},
 year = {2012},
 isbn = {978-1-4503-1576-0},
 location = {Copenhagen, Denmark},
 pages = {57--68},
 numpages = {12},
 url = {http://doi.acm.org/10.1145/2364394.2364403},
 doi = {10.1145/2364394.2364403},
 acmid = {2364403},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {abstract syntax, datatype-generic programming, fixed points},
} 

@INPROCEEDINGS{coutts07,
    author = {Duncan Coutts and Roman Leshchinskiy and Don Stewart},
    title = {Stream Fusion. From Lists to Streams to Nothing at All},
    booktitle = {ICFP},
    year = {2007},
    publisher = {}
}
@INPROCEEDINGS{coutts07b,
    author = {Duncan Coutts and Don Stewart and Roman Leshchinskiy},
    title = {Rewriting Haskell Strings},
    booktitle = {In Practical Aspects of Declarative Languages 8th International Symposium, PADL 2007},
    year = {2007},
    pages = {50--64},
    publisher = {Springer-Verlag}
}
@book{mitchell96,
  author    = {John C. Mitchell},
  title     = {Foundations for programming languages},
  publisher = {MIT Press},
  series    = {Foundation of computing series},
  year      = {1996},
  isbn      = {978-0-262-13321-0},
  pages     = {I-XIX, 1-846}
}
@inproceedings{ahmed11,
  author    = {Amal Ahmed and
               Matthias Blume},
  title     = {An equivalence-preserving CPS translation via multi-language
               semantics},
  booktitle = {ICFP},
  year      = {2011},
  pages     = {431-444}
}
@inproceedings{schurmann08,
  author    = {Carsten Sch{\"u}rmann and
               Jeffrey Sarnat},
  title     = {Structural Logical Relations},
  booktitle = {LICS},
  year      = {2008},
  pages     = {69-80},
  ee        = {http://doi.ieeecomputersociety.org/10.1109/LICS.2008.44},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@phdthesis{hinze00,
  title = "Generic Programs and Proofs",
  author = "Hinze, Ralf",
  year = "2000",
  school = "Bonn University",
}
@inproceedings{reynolds83,
    author = {Reynolds, John C.},
    booktitle = {IFIP Congress},
    keywords = {classic-papers-fall09, rg-2005, rg-2009},
    pages = {513--523},
    posted-at = {2009-08-18 07:12:47},
    priority = {2},
    title = {Types, Abstraction and Parametric Polymorphism},
    url = {ftp://ftp.cs.cmu.edu/user/jcr/typesabpara.pdf},
    year = {1983}
}
@inproceedings{cunha06,
 author = {Cunha, Alcino and Oliveira, Jos{\'e} Nuno and Visser, Joost},
 title = {Type-safe two-level data transformation},
 booktitle = {Proceedings of the 14th international conference on Formal Methods},
 series = {FM'06},
 year = {2006},
 isbn = {3-540-37215-6, 978-3-540-37215-8},
 location = {Hamilton, Canada},
 pages = {284--299},
 numpages = {16},
 url = {http://dx.doi.org/10.1007/11813040_20},
 doi = {10.1007/11813040_20},
 acmid = {2164849},
 publisher = {Springer-Verlag},
 address = {Berlin, Heidelberg},
 keywords = {coupled transformation, data mappings, format evolution, generalized abstract datatypes, generic programming, program calculation, refinement calculus, strategic term rewriting, two-level transformation},
}
@article{cunha07,
 author = {Cunha, Alcino and Visser, Joost},
 title = {Strongly Typed Rewriting For Coupled Software Transformation},
 journal = {Electron. Notes Theor. Comput. Sci.},
 issue_date = {April, 2007},
 volume = {174},
 number = {1},
 month = apr,
 year = {2007},
 issn = {1571-0661},
 pages = {17--34},
 numpages = {18},
 url = {http://dx.doi.org/10.1016/j.entcs.2006.10.019},
 doi = {10.1016/j.entcs.2006.10.019},
 acmid = {1241123},
 publisher = {Elsevier Science Publishers B. V.},
 address = {Amsterdam, The Netherlands, The Netherlands},
 keywords = {Program transformation, data refinement, generalized abstract datatypes, strategic programming, term rewriting},
} 
@article{johann09,
  author    = {Patricia Johann and
               Janis Voigtl{\"a}nder},
  title     = {A family of syntactic logical relations for the semantics
               of Haskell-like languages},
  journal   = {Inf. Comput.},
  volume    = {207},
  number    = {2},
  year      = {2009},
  pages     = {341-368},
  ee        = {http://dx.doi.org/10.1016/j.ic.2007.11.009},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{johann04,
 author = {Johann, Patricia and Voigtl\"{a}nder, Janis},
 title = {Free theorems in the presence of seq},
 journal = {SIGPLAN Not.},
 issue_date = {January 2004},
 volume = {39},
 number = {1},
 month = jan,
 year = {2004},
 issn = {0362-1340},
 pages = {99--110},
 numpages = {12},
 url = {http://doi.acm.org/10.1145/982962.964010},
 doi = {10.1145/982962.964010},
 acmid = {964010},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {Haskell, controlling strict evaluation, correctness proofs, denotational semantics, logical relations, parametricity, program transformations, short cut fusion, theorems for free},
} 

@inproceedings{wadler89,
 author = {Wadler, Philip},
 title = {Theorems for free!},
 booktitle = {Proceedings of the fourth international conference on Functional programming languages and computer architecture},
 series = {FPCA '89},
 year = {1989},
 isbn = {0-89791-328-0},
 location = {Imperial College, London, United Kingdom},
 pages = {347--359},
 numpages = {13},
 url = {http://doi.acm.org/10.1145/99370.99404},
 doi = {10.1145/99370.99404},
 acmid = {99404},
 publisher = {ACM},
 address = {New York, NY, USA},
}
@TECHREPORT{kucan97,
    author = {Jakov Kucan},
    title = {Metatheorems about Convertibility in Typed Lambda Calculi: Applications to CPS transform and "Free Theorems"},
    institution = {},
    year = {1997}
}
@article{crary07,
 author = {Crary, Karl and Harper, Robert},
 title = {Syntactic Logical Relations for Polymorphic and Recursive Types},
 journal = {Electron. Notes Theor. Comput. Sci.},
 issue_date = {April, 2007},
 volume = {172},
 month = apr,
 year = {2007},
 issn = {1571-0661},
 pages = {259--299},
 numpages = {41},
 url = {http://dx.doi.org/10.1016/j.entcs.2007.02.010},
 doi = {10.1016/j.entcs.2007.02.010},
 acmid = {1230585},
 publisher = {Elsevier Science Publishers B. V.},
 address = {Amsterdam, The Netherlands, The Netherlands},
 keywords = {Operational semantics, data abstraction, lambda calculus and related systems, logics of programs, polymorphism, type structure},
}
@inproceedings{honsell99,
 author = {Honsell, Furio and Sannella, Donald},
 title = {Pre-logical Relations},
 booktitle = {Proceedings of the 13th International Workshop and 8th Annual Conference of the EACSL on Computer Science Logic},
 series = {CSL '99},
 year = {1999},
 isbn = {3-540-66536-6},
 pages = {546--561},
 numpages = {16},
 url = {http://dl.acm.org/citation.cfm?id=647849.737068},
 acmid = {737068},
 publisher = {Springer-Verlag},
 address = {London, UK, UK},
} 
@article{gill09,
	author = "Andy Gill and Graham Hutton",
  title  = "{The Worker/Wrapper Transformation}",
  journal = "Journal of Functional Programming",
  publisher = "Cambridge University Press",
  volume = 19,
  number = 2,
  pages = "227--251",
  month = mar,
  year = 2009
}
@phdthesis{norell07,
  author  = {Ulf Norell},
  title	  = {Towards a practical programming language based on dependent type
	     theory},
  school  = {Department of Computer Science and Engineering, Chalmers University of Technology},
  year	  = 2007,
  month	  = {September},
  address = {SE-412 96 G\"{o}teborg, Sweden}
}

@misc{program-transformation,
title = {Program-Transformation.Org},
howpublished = {\url{http://http://www.program-transformation.org/}}
}
@misc{poplmark,
title = {The POPLMark Challenge},
howpublished = {\url{http://www.seas.upenn.edu/~plclub/poplmark/}}
}
@misc{source,
title = {Source Code},
howpublished = {\url{https://github.com/craffit/thesis}}
}

@INPROCEEDINGS{visser98,
    author = {Eelco Visser and Zine-el-abidine Benaissa},
    title = {A Core Language for Rewriting},
    booktitle = {Electronic Notes in Theoretical Computer Science},
    year = {1998},
    pages = {1--4},
    publisher = {Elsevier}
}
@misc{stratego,
title = {Stratego/XT},
howpublished = {\url{http://strategoxt.org/}}
}
@inproceedings{backhouse02,
 author = {Backhouse, Kevin and Backhouse, Roland},
 title = {Logical Relations and Galois Connections},
 booktitle = {Proceedings of the 6th International Conference on Mathematics of Program Construction},
 series = {MPC '02},
 year = {2002},
 isbn = {3-540-43857-2},
 pages = {23--39},
 numpages = {17},
 url = {http://dl.acm.org/citation.cfm?id=648086.747310},
 acmid = {747310},
 publisher = {Springer-Verlag},
 address = {London, UK, UK},
} 
@inproceedings{swierstra12,
  author    = {Wouter Swierstra},
  title     = {From Mathematics to Abstract Machine: A formal derivation
               of an executable Krivine machine},
  booktitle = {MSFP},
  year      = {2012},
  pages     = {163-177},
  ee        = {http://dx.doi.org/10.4204/EPTCS.76.10},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}