# programming languages stuff

@techreport{nanevski02b,
author="A. Nanevski",
title="Meta-programming with Names and Necessity",
number="CMU-CS-02-123R",
year=2002,
month=nov,
institution="Carnegie Mellon University"}

@inproceedings{nanevski02,
 author = {A. Nanevski},
 title = {Meta-Programming with Names and Necessity},
 booktitle = {Proceedings of the 7th ACM SIGPLAN International Conference on Functional Programming},
 year = {2002},
 pages = {206--217}
 }

@article{NP03,
author={A. Nanevski and F. Pfenning},
title={{Meta-Programming with Names and Necessity}},
journal={{Journal of Functional Programming}},
note="under review",
URL = {http://www.cs.cmu.edu/\homedir fp/papers/names03.ps}}

@article{MWCG99,
title = {{From System F to Typed Assembly Language}},
author = "G. Morrisett and D. Walker and K. Crary and N. Glew",
journal = {{ACM Transactions on Programming Languages and Systems}},
volume = 21,
number = 3,
pages = "527--568",
month = May,
year= 1999}

@article{schurmann04,
author={{C. Sch\"{u}rmann}},
title={{Programming with Higher-Order Abstract Syntax}},
note={{Draft paper available from Sch\"{u}rmann's web page}},
year=2004}

@inproceedings{lmc03,
author="S. Lerner and T. Millstein and C. Chambers",
editor="R. Gupta",
title={{Automatically Proving the Correctness of Compiler Optimizations}},
booktitle="In ACM SIGPLAN Conference on Programming Language Design and Implementation",
note="received best paper award",
year=2003}

@inproceedings{dreyer+03,
  author = 	 {D. Dreyer and K. Crary and R. Harper},
  title = 	 {{A Type Theory for Higher-Order Modules}},
  booktitle={ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
  editor= "G. Morrisett",
  year =	 2003
}

@inproceedings{XiSEFM03,
author = "H. Xi",
title = {{Facilitating Program Verification with Dependent Types}},
booktitle = "Proceedings of the International Conference on Software Engineering and Formal Methods",
year = 2003,
pages = "72--81",
}

@book{nps90,
title={{Programming in Martin-L\"{o}f's Type Theory}},
author={B. Nordstr\"{o}m and K. Petersson and J. Smith},
publisher="Oxford University Press",
year=1990}

@book{nnh99,
author="F. Nielson and H. Nielson and C. Hankin",
title={{Principles of Program Analysis}},
publisher="Springer",
year=1999}

@inproceedings{sheard04,
author="T. Sheard",
title="Languages of the Future",
booktitle="Proceedings of 19th ACM Conference on Object-Oriented Programming,
Systems, Languages, and Applications",
editor="D. Schmidt",
year=2004}

@inproceedings{crary03b,
author="K. Crary",
title={{Toward a Foundational Typed Assembly Language}},
booktitle="In Proceedings of the 30th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages",
editor="G. Morrisett",
year=2003}

@InProceedings{alti:wcgp02,
  author = 	 {Thorsten Altenkirch and Conor McBride},
  title = 	 {Generic Programming Within Dependently Typed Programming},
  booktitle = 	 {Generic Programming},
  year =	 {2003},
  note =	 {Proceedings of the IFIP TC2 Working Conference on Generic Programming, Schloss Dagstuhl, July 2002}
}

@inproceedings{brady+03,
  author    = {E. Brady and
               C. McBride and
               J. McKinna},
  title     = {{Inductive Families Need Not Store Their Indices}},
  booktitle = {TYPES},
  year      = {2003},
  pages     = {115-129}}


@phdthesis{ mcbride99,
    author = "C. McBride",
    title = {{Dependently Typed Functional Programs and Their Proofs}},
    year = "1999",
    institution="University of Edinburgh"}

@article{mcbride+04,
author="C. McBride and J. McKinna",
title={{The View from the Left}},
journal="Journal of Functional Programming",
year=2004,
volume=14,
number=1}

@unpublished{cheneyhinze04,
author="J. Cheney and R. Hinze",
title={{Phantom Types}},
note="in preparation; available from Hinze's web site",
year=2003}

@unpublished{voda03,
author="P. Voda",
title={{What Can We Gain by Integrating a Language Processor 
with a Theorem Prover}},
note="unpublished; available from the author's web site",
year=2003}

@article{hinze+04,
 author = {R. Hinze and J. Jeuring and A. L\"{o}h},
 title = {Type-indexed data types},
 journal = {Science of Computer Programming},
 volume = {51},
 number = {1-2},
 year = {2004},
 pages = {117--151},
 publisher = {Elsevier}
 }

@inproceedings{ pierce98local,
    author = "Benjamin C. Pierce and David N. Turner",
    title = "Local Type Inference",
    booktitle = "25TH {ACM} {SIGPLAN}-{SIGACT} Symposium on Principles of Programming Languages",
    pages = "252--265",
    year = "1998"}

@unpublished{ocaml04,
author="X. Leroy",
note={with D. Doligez, J. Garrigue, D. R\'{e}my and J. Vouillon},
title={{The Object Caml System: Release 3.08}},
year=2004}

@inproceedings{findler02,
author = "R. Findler and M. Felleisen",
booktitle="International Conference on Functional Programming",
title={{Contracts for Higher-Order Functions}},
year=2002}

@inproceedings{chenxi03,
author = "C. Chen and H. Xi",
title = {{Implementing Typeful Program Transformations}},
booktitle = "Proceedings of ACM SIGPLAN Workshop on Partial Evaluation and Semantics Based Program Manipulation",
year = "2003",
month = "June",
address = "San Diego, CA",
pages = "20--28"}

@inproceedings{chenxi05,
author = "C. Chen and H. Xi",
title = {{Combining Programming with Theorem Proving}},
booktitle = "Proceedings of the 10th International Conference on Functional Programming (ICFP05)",
year = "2005",
month = "September",
address = "Tallinn, Estonia"}

@inproceedings{zhuxi-padl05,
author = "D. Zhu and H. Xi",
title = {{Safe Programming with Pointers through Stateful Views}},
booktitle = "Proceedings of the 7th International Symposium on Practical Aspects of Declarative Languages",
publisher = "Springer-Verlag LNCS vol. 3350",
year = "2005",
month = "January",
pages = "83--97",
address = "Long Beach, CA"}

@inproceedings{sch-pos-sarnat-tlca05,
author = {C. Sch\"{u}rmann and A. Poswolsky and J. Sarnat},
title = {{The $\nabla$-Calculus. Functional Programming with Higher-Order Encodings}},
booktitle = "Proceedings of the 7th International Conference on Typed Lambda Calculi and Applications",
publisher = "Springer-Verlag",
year = "2005",
pages = "339--353"}

@article{betarte00,
title = {Type Checking Dependent (Record) Types and Subtyping},
author = "Gustavo Betarte",
journal = {{Journal of Functional Programming}},
volume = 10,
number = 2,
pages = "137--166",
month = "March",
year= 2000}

@inproceedings{f-p-refinement91,
author = {T. Freeman and F. Pfenning},
title = {Refinement types for {ML}},
booktitle = "ACM Conference on Programming Language Design and Implementation (PLDI)",
year = "1991",
pages = "268--277"}

@inproceedings{d-p-tridirectional04,
author="J. Dunfield and F. Pfenning",
title={Tridirectional Typechecking},
booktitle="Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages",
editor="N. D. Jones and X. Leroy",
year=2004,
month="January",
pages="281--292"}

@inproceedings{xi-chen-chen03,
author="H. Xi and C. Chen and G. Chen",
title={Guarded recursive datatype constructors},
booktitle="Proceedings of the 30th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages",
year=2003,
pages="224--235"}

@UNPUBLISHED{simonet-pottier-hmg-toplas,
  AUTHOR = {V. Simonet and F. Pottier},
  TITLE = {{Constraint-Based Type Inference for Guarded Algebraic
                 Data Types}},
  MONTH = MAR,
  YEAR = {2005},
  NOTE = {Submitted},
  URL =
{http://cristal.inria.fr/~fpottier/publis/simonet-pottier-hmg-toplas.ps.gz},
  PDF =
{http://cristal.inria.fr/~fpottier/publis/simonet-pottier-hmg-toplas.pdf}}

@inproceedings{dowek-tlca93,
author = {Gilles Dowek},
title = {The Undecidability of Typability in the {Lambda-Pi-Calculus}},
booktitle = "Proceedings of the International Conference on Typed Lambda Calculi and Applications (TLCA)",
series = "Lecture Notes in Computer Science",
publisher = "Springer-Verlag",
volume = "664",
year = "1993",
pages = "139--145"}

@inproceedings{TschantzE2005,
   author = {Matthew S. Tschantz and Michael D. Ernst},
   title = {Javari: Adding reference immutability to {Java}},
   booktitle = {Object-Oriented Programming Systems, Languages, and
	Applications (OOPSLA 2005)},
   address = {San Diego, CA, USA},
   month = {October~16--20,},
   year = {2005}
}

@inproceedings{BirkaE2004,
   author = {Adrian Birka and Michael D. Ernst},
   title = {A practical type system and language for reference immutability},
   booktitle = {Object-Oriented Programming Systems, Languages, and
	Applications (OOPSLA 2004)},
   pages = {35--49},
   address = {Vancouver, BC, Canada},
   month = {October~26--28,},
   year = {2004}
}

@misc{fahndrich03declaring,
  author = "M. Fahndrich and K. Leino",
  title = "Declaring and checking non-null types in an object-oriented language",
  text = "Manuel Fahndrich and K. Rustan M. Leino. Declaring and checking non-null
    types in an object-oriented language. In OOPSLA'03, 2003.",
  year = "2003",}
pages = "20--28"}

@inproceedings{boyapati+03,
title={{Ownership Types for Object Encapsulation}},
author="C. Boyapati and B. Liskov and L. Shrira",
booktitle="ACM Symposium on Principles of Programming Languages",
editor="G. Morrisett",
year=2003}

@inproceedings{ernst06,
 author = {E. Ernst and K. Ostermann and W. Cook},
 title = {{A Virtual Class Calculus}},
 booktitle = {The 33rd ACM Symposium on Principles of Programming Languages},
 year = {2006},
 pages = {270--282},
 location = {Charleston, South Carolina, USA},
 publisher = {ACM Press} }

@INPROCEEDINGS{poplmark,
  AUTHOR = {B. Aydemir and A. Bohannon and M. Fairbairn
                  and J. Foster and B. Pierce and P.
                  Sewell and D. Vytiniotis and G. Washburn and
                  S. Weirich and S. Zdancewic},
  TITLE = {{Mechanized metatheory for the masses: The POPLmark
                  Challenge}},
  booktitle = "Proceedings of the Eighteenth International Conference on Theorem Proving
    in Higher Order Logics (TPHOLs 2005)",
  YEAR = 2005
}

@manuscript{poplmark-stump05,
author={A. Stump},
title={{POPLmark 1a with Named Bound Variables}},
year=2005,
note="available from \url{http://cl.cse.wustl.edu/poplmark.html}"}

@inproceedings{bellantoni_cook92,
author={S. Bellantoni and S. Cook},
title={{A New Recursion-Theoretic Characterization of the Polytime Functions}},
booktitle={Computational Complexity 2},
year=1992,
pages="97-110",
note="available from \url{http://www.cs.toronto.edu/~sacook/}"}

@article{ mogensen92,
    author = "T. Mogensen",
    title = {{Efficient Self-Interpretations in lambda Calculus}},
    journal = "Journal of Functional Programming",
    volume = "2",
    number = "3",
    pages = "345-363",
    year = "1992"}

@techreport{shutt06,
author = "J. Shutt",
institution = {{Worcester Polytechnic Institute}},
title = {{Revised Report on the Kernel Programming Language}},
number = "WPI-CS-TR-05-07",
month = "August",
year = "2006"}

@article{ mccarthy60,
    author = "J. McCarthy",
    title = {{Recursive Functions of Symbolic Expressions and Their Computation by Machine, Part I}},
    journal = "Communications of the ACM",
    volume = "3",
    number = "4",
    pages = "184-195",
    year = "1960"}

@article{ wand98fexprs,
    author = "M. Wand",
    title = {{The Theory of Fexprs is Trivial}},
    journal = "Lisp and Symbolic Computation",
    volume = "10",
    number = "3",
    year = 1998,
    pages = "189-199"}

@inproceedings{KimYC06,
  author    = {I.-S. Kim and
               K. Yi and
               C. Calcagno},
  title     = {{A Polymorphic Modal Type System for Lisp-Like Multi-Staged
               Languages}},
  booktitle = {The 33rd ACM SIGPLAN-SIGACT Symposium on Principles
               of Programming Languages},
  year      = {2006},
  pages     = {257-268}
}

@phdthesis{ taha99multistage,
    author = "W. Taha",
    title = {{Multi-Stage Programming: Its Theory and Applications}},
    year = "1999",
    month = nov,
    school = {Oregon Graduate Institute}}

@techreport{licata+05,
title={{A Formulation of Dependent ML with Explicit Equality Proofs}},
author="D. Licata and R. Harper",
institution={{Carnegie Mellon University School of Computer Science}},
number="CMU-CS-05-178",
month=dec,
year=2005}

@inproceedings{sheard06,
author="T. Sheard",
title={{Type-Level Computation Using Narrowing in $\Omega$mega}},
booktitle="Programming Languages meets Program Verification",
year=2006,
editors="A. Stump and H. Xi"}

@Article{nanevski05names,
  author = 	 {A. Nanevski and F. Pfenning},
  title = 	 {Meta-Programming with Names and Necessity},
  journal = 	 {Journal of Functional Programming},
  year = 	 {2005},
  note = 	 {To appear},
  urlpdf =       {http://www.cs.cmu.edu/~fp/papers/jfp05.pdf},
  urlps =        {http://www.cs.cmu.edu/~fp/papers/jfp05.ps}
}

@unpublished{nanevski05contextual,
  author = 	 {A. Nanevski and F. Pfenning and B. Pientka},
  title = 	 {Contextual Modal Type Theory},
  year = 	 {2005},
  note = 	 {submitted},
  urlpdf =       {http://www.cs.cmu.edu/~fp/papers/cmtt05.pdf}
}

@unpublished{schurmann05temporal,
  author = {C. Sch\"{u}rmann and A. Poswolsky},
  title = {A Temporal-Logic Approach to Programming with Dependent Types and Higher-Order Encodings},
  note = {unpublished manuscript},
  year = {2005}
}

@book{girard-proofs-types,
title={{Proofs and Types}},
author={J.-Y. Girard and Y. Lafont and P. Taylor},
publisher="Cambridge University Press",
year=1989}


@inproceedings{pfenning88,
 author = {F. Pfenning},
 title = {Partial polymorphic type inference and higher-order unification},
 booktitle = {LFP '88: Proceedings of the 1988 ACM conference on LISP and functional programming},
 year = {1988},
 isbn = {0-89791-273-X},
 pages = {153--163},
 location = {Snowbird, Utah, United States},
 publisher = {ACM Press},
 address = {New York, NY, USA}
 }

@inproceedings{coquand92,
 author = {Thierry Coquand},
 title = {Pattern Matching with Dependent Types},
 booktitle = {Electronic Proceedings of the Third Annual BRA Workshop on Logical frameworks},
 editor = {Bengt Nordstr\"{o}m and Kent Petersson and Gordon Plotkin},
 year = {1992},
 location = {B\.{a}stad, Sweden}
 }

@inproceedings{pientka-plpv06,
 author = {Brigitte Pientka},
 title = {Functional programming with higher-order abstract syntax and explicit substitutions},
 booktitle = {PLPV '06: Proceedings of the First Workshop on Programming Languages meets Program Verification},
 year = {2006},
 location = {Seattle, WA},
}

@TechReport{licata-harper-techrep05,
  author = 	 {Daniel R. Licata and Robert Harper},
  title = 	 {A Formulation of Dependent ML with Explicit Equality Proofs},
  institution =  {Carnegie Mellon University Department of Computer Science},
  year = 	 {2005},
  number = 	 {CMU-CS-05-178},
}

@article{statman-tcs79,
author={R. Statman},
title={The Types $\lambda$-calculus is not Elementary Recursive},
journal={{Theoretical Computer Science}},
year=1979,
pages={73--81}
}

@article{schurmann-tcs01,
 author = {C. Schurmann and J. Despeyroux and F. Pfenning},
 title = {Primitive recursion for higher-order abstract syntax},
 journal = {Theoretical Computer Science},
 volume = {266},
 number = {1-2},
 year = {2001},
 pages = {1--57}
 }

@inproceedings{nogin-merlin05,
 author = {Aleksey Nogin and Alexei Kopylov and Xin Yu and Jason Hickey},
 title = {A computational approach to reflective meta-reasoning about languages with bindings},
 booktitle = {MERLIN '05: Proceedings of the 3rd ACM SIGPLAN workshop on Mechanized reasoning about languages with variable binding},
 year = {2005},
 pages = {2--12},
 location = {Tallinn, Estonia},
 publisher = {ACM Press}
 }

@article{coquand-scp96,
 author = {Thierry Coquand},
 title = {An algorithm for type-checking dependent types},
 journal = {Sci. Comput. Program.},
 volume = {26},
 number = {1-3},
 year = {1996},
 pages = {167--177}
 }

@article{betarte-jfp00,
 author = {Gustavo Betarte},
 title = {Type checking dependent (record) types and subtyping},
 journal = {J. Funct. Program.},
 volume = {10},
 number = {2},
 year = {2000},
 pages = {137--166}
 }

@article{spj-sigplan06,
 author = {Simon Peyton Jones and Dimitrios Vytiniotis and Stephanie Weirich and Geoffrey Washburn},
 title = {Simple unification-based type inference for GADTs},
 journal = {SIGPLAN Not.},
 volume = {41},
 number = {9},
 year = {2006},
 pages = {50--61}
 }

@inproceedings{pottier-popl06,
 author = {Fran\&\#231;ois Pottier and Yann R\&\#233;gis-Gianas},
 title = {Stratified type inference for generalized algebraic data types},
 booktitle = {POPL '06: Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages},
 year = {2006},
 pages = {232--244},
 location = {Charleston, South Carolina, USA},
 }

@inproceedings{GRDC03,
author = "H. Xi and C. Chen and G. Chen",
title = {{Guarded Recursive Datatype Constructors}},
booktitle = "Proceedings of the 30th ACM SIGPLAN Symposium on Principles of Programming Languages",
year = 2003,
month = "January",
pages = "224-235"}

@inproceedings{pasalic+07,
title={{Concoqtion: Indexed Types Now!}},
author="E Pasalic and J. Siek and W. Taha and S. Fogarty",
booktitle="ACM SIGPLAN 2007 Workshop on Partial Evaluation and Program Manipulation",
year="2007",
editor="G. Ramalingam and E. Visser"}


@inproceedings{jones06,
author="S. Peyton-Jones and D. Vytiniotis and S. Weirich and G. Washburn",
title={{Simple Unification-based Type Inference for GADTs}},
booktitle="ACM SIGPLAN International Conference on Functional Programming",
year=2006,
editor="J. Lawall"}

@article{xi06,
author="H. Xi",
title={{Dependent ML: an Approach to Practical Programming with Dependent Types}},
journal={Journal of Functional Programming},
year= 2006,
note="to appear"}

@inproceedings{tan+04,
title={{Construction of a Semantic Model for a Typed Assembly Language}},
author="G. Tan and A. Appel and K. Swadi and D. Wu",
booktitle="5th International Conference on Verification, Model Checking, and Abstract Interpretation",
year=2004}

@inproceedings{wadler89,
title={{Theorems for free!}},
author="P. Wadler",
booktitle={{4th International Conference on Functional Programming and Computer Architecture}},
year=1989}


@inproceedings{jefferson+92,
    author = "S. Jefferson and D. Friedman",
    title = "{A} {S}imple {R}eflective {I}nterpreter",
    booktitle = "{IMSA}'92 International Workshop on Reflection and Meta-level architecture",
    year = "1992"}

@inproceedings{smith84,
 author = {B. Smith},
 title = {{Reflection and Semantics in LISP}},
 booktitle = {{Proceedings of the 11th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages}},
 year = {1984},
 pages = {23--35}}}

@book{steele90,
 author = {G. Steele},
 title = {{Common LISP: the Language (2nd ed.)}},
 year = {1990},
 isbn = {1-55558-041-6},
 publisher = {Digital Press}
 }

@book{lewis+00,
title={{GNU Emacs Lisp Reference Manual}},
author="B. Lewis and D. LaLiberte and R. Stallman and the GNU Manual Group",
year=2000,
isbn={1-882114-73-6},
publisher="GNU Press"}

@article{kelsey1998rra,
  title={{Revised$^5$ Report on the Algorithmic Language Scheme}},
  author={Kelsey, R. and Clinger, W. and Rees, J. and others},
  journal={SIGPLAN Notices},
  volume={33},
  number={9},
  pages={26--76},
  year={1998}
}

@book{smalltalk,
title={{Smalltalk-80: The Language and Its Implementation}},
author={A. Goldberg and D. Robson},
year="1983",
publisher="Addison-Wesley",
isbn="0-201-11371-6"}

@book{java,
title={{The Java Programming Language}},
author="K. Arnold and J. Gosling and D. Holmes",
publisher="Prentice Hall",
year=2000,
isbn="978-0201704334"}

@article{milner78,
author="R Milner",
title={A theory of type polymorphism in programming},
journal="Journal of Computer and System Sciences",
volume=17,
pages="348-375",
month=aug,
year=1978}

@inproceedings{ferber89,
 author = {J. Ferber},
 title = {Computational reflection in class based object-oriented languages},
 booktitle = {{OOPSLA '89: Conference Proceedings on Object-Oriented Programming Systems, Languages and Applications}},
 year = {1989},
 pages = {317--326},
 publisher = {ACM Press},
 address = {New York, NY, USA}
 }

@inproceedings{ganz01macros,
    author = "S. Ganz and A. Sabry and W. Taha",
    title = {{Macros as Multi-Stage Computations: Type-Safe, Generative, Binding Macros in MacroML}},
    booktitle = "International Conference on Functional Programming",
    pages = "74-85",
    year = "2001"}



@article{CX-JFP05,
author = "C. Chen and H. Xi",
title = {{Meta-Programming through Typeful Code Representation}},
journal = "Journal of Functional Programming",
year = 2005,
volume = "15",
number = "6",
pages = "797-835"}


@inproceedings{luc97syntactic,
    author = "L. Moreau",
    title = "{A} {S}yntactic {T}heory of {D}ynamic {B}inding",
    booktitle = "International Joint Conference on Theory and Practice of Software Development ({TAPSOFT}/{FASE}'97)",
    volume = "1214",
    month = "apr",
    publisher = "Springer-Verlag",
    pages = "727--741",
    year = "1997"}

@inproceedings{kohlbecker+86,
 author = {E. Kohlbecker and D. Friedman and M. Felleisen and B. Duba},
 title = {Hygienic macro expansion},
 booktitle = {LFP '86: Proceedings of the 1986 ACM conference on LISP and functional programming},
 year = {1986},
 pages = {151--161},
 publisher = {ACM Press}
 }

@book{c++,
title={{The C++ Programming Language (3rd Edition)}},
author="B. Stroustrup",
publisher="Addison-Wesley",
isbn="0-201-88954-4",
year=1997}

@article{crary2002ipt,
  title={{Intensional polymorphism in type-erasure semantics}},
  author={Crary, K. and Weirich, S. and Morrisett, G.},
  journal={Journal of Functional Programming},
  volume={12},
  number={06},
  pages={567--600},
  year={2002},
  publisher={Cambridge Univ Press}
}

@book{pierce02,
 author="B. Pierce",
 title={{Types and Programming Languages}},
 year=2002,
 publisher="The MIT Press"}


@book{jones87,
author="S. Peyton Jones",
title={{The Implementation of Functional Programming Languages}},
publisher="Prentice Hall",
year="1987"}

@inproceedings{siskind+07,
author="J. Siskind and B. Pearlmutter",
title={{First-Class Nonstandard Interpretations by Opening Closures}},
booktitle={{Proceedings of the Symposium on Principles of Programming Languages (POPL)}},
year=2007}

@article{grundy2005rfl,
  title={{A reflective functional language for hardware design and theorem proving}},
  author={J. Grundy and T. Melham and J. O'Leary},
  journal={Journal of Functional Programming},
  volume={16},
  number={02},
  pages={157--196},
  year={2005},
  publisher={Cambridge Univ Press}
}

@techreport{nanevski+05,
title={{Dependent Type Theory of Stateful Higher-Order Functions}},
author="A. Nanevski and G. Morrisett",
number="TR-24-05",
year="2005",
institution="Harvard University"}

@article{plotkin75,
author="G. Plotkin",
title={{Call-by-name, Call-by-value, and the Lambda calculus}},
journal="Theoretical Computer Science",
volume=1,
pages="125--159",
publisher="North-Holland",
year=1975}

@incollection{martinlof72,
  author={Per Martin-L\"{o}f},
  title="An Intuitionistic Theory of Types",
  booktitle="Twenty-Five Years of Constructive Type Theory",
  editor="G Sambin and J Smith",
  publisher="Oxford University Press",
  year=1998
}

@book{peytonjones87,
  author="Simon Peyton Jones",
  title="The Implementation of Functional Programming Languages",
  publisher="Prentice Hall",
  year="1987"
}

@inbook{peytonjones01awkward,
  author="Simon Peyton Jones",
  title="Tackling the awkward squad: monadic input/output, concurrency, exceptions, and foreign-language calls in Haskell",
  booktitle="Engineering Theories of Software Construction",
  publisher="IOS Press",
  year="2001",
  pages="47--96"
}

@article{urban07,
title={{Nominal Techniques in Isabelle/HOL}},
author="C. Urban",
journal="Journal of Automatic Reasoning",
note="To appear",
year=2007}

@inproceedings{megacz07,
author="A. Megacz",
title={{A Coinductive Monad for Prop-Bounded Recursion}},
booktitle="Proceedings of Programming Languages meets Program Verification (PLPV)",
year=2007,
editor="A. Stump and H. Xi"}

@inproceedings{parigot92,
 author = {Michel Parigot},
 title = {{Lambda-Mu-Calculus: An Algorithmic Interpretation of Classical Natural Deduction}},
 booktitle = {LPAR '92: Proceedings of the International Conference on Logic Programming and Automated Reasoning},
 year = {1992},
 pages = {190--201},
 publisher = {Springer-Verlag}
 }

@inproceedings{vanwyk07fase,
 author = "J. Gao and M. Heimdahl and E. Van Wyk",
 title = {{Flexible and Extensible Notations for Modeling Languages}},
 booktitle = "Fundamental Approaches to Software Engineering, FASE 2007",
 series    = "Lecture Notes in Computer Science",
 publisher = "Springer Verlag",
 volume = 4422,
 pages = "102--116",
 month = "March",
 year = 2007
}


@article{wright97+,
 author = {A. Wright and R. Cartwright},
 title = {{A Practical Soft Type System for Scheme}},
 journal = {ACM Trans. Program. Lang. Syst.},
 volume = {19},
 number = {1},
 year = {1997},
 pages = {87--152},
 publisher = {ACM Press}
 }

@manual{drscheme,
author={{The PLT Group}},
title={{PLT DrScheme: Programming Environment Manual}},
year=2007,
note={\url{http://download.plt-scheme.org/doc/drscheme/}}}

@manual{haskell,
title={{The Glorious Glasgow Haskell Compilation System User's Guide, Version 6.6.1}},
author={{The GHC Team}},
year=2007,
note={\url{http://www.haskell.org/ghc/docs/latest/html/users_guide/}}}

@inproceedings{altenkirch+07,
 author = {T. Altenkirch and C. McBride and W. Swierstra},
 title = {{Observational Equality, Now!}},
 booktitle = {PLPV '07: Proceedings of the 2007 Workshop on Programming Languages meets Program Verification},
 year = {2007},
 pages = {57--68},
 editor = {A. Stump and H. Xi}
 }

@article{chirimar96reference,
    author = "J. Chirimar and C. Gunter and J. Riecke",
    title = {{Reference Counting as a Computational Interpretation of Linear Logic}},
    journal = "Journal of Functional Programming",
    volume = "6",
    number = "2",
    pages = "195-244",
    year = "1996"}


@inproceedings{walker01regions,
    author = "D. Walker and K. Watkins",
    title = {{On Regions and Linear Types}},
    booktitle = "International Conference on Functional Programming",
    pages = "181--192",
    year = "2001"}

@inproceedings{ridge07,
author="T. Ridge",
title="To arrive where we started: experience of mechanizing binding",
booktitle={Workshop on Mechanizing Metatheory},
year=2007,
note="1-page abstract available from author's homepage."}

@inproceedings{hertz+05,
 author = {M. Hertz and E. Berger},
 title = {{Quantifying the Performance of Garbage Collection vs. Explicit Memory Management}},
 booktitle = {Proc. 20th Annual ACM SIGPLAN Conference on Object Oriented Programming, Systems, Languages, and Applications},
 year = {2005},
 pages = {313--326},
 publisher = {ACM}}

@article{capretta05,
author="V. Capretta",
title={{General Recursion via Coinductive Types}},
journal={{Logical Methods in Computer Science}},
volume="1",
number="2",
year="2005",
pages="1--28"}

@InProceedings{swierstra+07,
  author =	 "W. Swierstra and T. Altenkirch",
  title =	 {{Beauty in the Beast}},
  year =	 {2007},
  booktitle =	 {Haskell Workshop}
}

@inproceedings{barendsen+93,
 author = "E. Barendsen and S. Smetsers",
 title = {{Conventional and Uniqueness Typing in Graph Rewrite Systems}},
 booktitle = {Proc. 13th Conference on Foundations of Software Technology and Theoretical Computer Science},
 year = {1993},
 pages = {41--51},
 publisher = {Springer-Verlag}
 }

@inproceedings{blanqui+08,
author="F. Blanqui and J.-P. Jouannaud and P.-Y. Strub",
title={{From Formal Proofs to Mathematical Proofs: a Safe, Incremental Way for Building in First-Order Decision Procedures}},
booktitle={{Proc. 5th IFIP Conference on Theoretical Computer Science}},
year="2008",
publisher="Springer-Verlag"}

@phdthesis{norell07,
author="U. Norell",
title={{Towards a Practical Programming Language Based on Dependent Type Theory}},
school={{Chalmers University of Technology}},
year=2007} 

@inproceedings{nanevski+08,
  author    = {A. Nanevski and
               G. Morrisett and
               A. Shinnar and
               P. Govereau and
               L. Birkedal},
  title     = {{Ynot: Dependent Types for Imperative Programs}},
  year      = {2008},
  pages     = {229-240},
  editor    = {James Hook and
               Peter Thiemann},
  booktitle     = {The 13th ACM SIGPLAN International Conference
               on Functional Programming (ICFP)},
}
                  
@article{Xian2008,
title = {{Garbage collection: Java application servers' Achilles heel}},
journal = "Science of Computer Programming",
volume = "70",
number = "2-3",
pages = "89 - 110",
year = "2008",
author = "F. Xian and W. Srisa-an and H. Jiang",
}

@inproceedings{oury+08,
	Author = {N. Oury and W. Swierstra},
	Booktitle = {Proceedings of the 2008 SIGPLAN International Conference on Functional Programming},
        editor="P. Thiemann",
	Title = {The {Power} of {Pi}},
	Year = {2008}}

@inproceedings{ynot09,
  author    = {A. Chlipala and
               G. Malecha and
               G. Morrisett and
               A. Shinnar and
               R. Wisnesky},
  title     = {{Effective interactive proofs for higher-order imperative
               programs}},
  editor    = {Graham Hutton and
               Andrew P. Tolmach},
  booktitle = {Proceeding of the 14th ACM SIGPLAN International Conference
               on Functional Programming (ICFP)},
  year      = {2009},
  pages     = {79-90},
}

@inproceedings{Bond+09,
  author    = {M. Bond and
               K. McKinley},
  title     = {{Leak Pruning}},
  booktitle = {Proceedings of the 14th International Conference on Architectural
               Support for Programming Languages and Operating Systems (ASPLOS)},
  year      = {2009},
  pages     = {277-288},
  editor    = {M. Soffa and
               M. Irwin}
}
                  
                  @techreport{swamy+09,
author="N. Swamy and J. Chen and R. Chugh",
title={{End-to-end Verification of Security Enforcement is Fine (Extended version)}},
number="MSR-TR-2009-98",
institution="Microsoft Research",
year="2009"}

 @inproceedings{vries08,
 author = {E. Vries and R. Plasmeijer and D. Abrahamson},
 title = {{Uniqueness Typing Simplified}},
 booktitle = {Implementation and Application of Functional Languages: 19th International Workshop, IFL 2007},
 year = {2008},
 pages = {201--218},
 publisher = {Springer-Verlag},
 }