paper.bib

@ARTICLE{schneider00enforceable,
  AUTHOR = {Fred B. Schneider},
  TITLE = {Enforceable Security Policies},
  JOURNAL = {{ACM} Transactions on Information and System Security},
  VOLUME = 3,
  NUMBER = 1,
  MONTH = FEB,
  YEAR = 2000
}

@INPROCEEDINGS{schneider01lbs,
  AUTHOR = {Fred B. Schneider and
               Gregory Morrisett and
               Robert Harper},
  TITLE = {A Language-Based Approach to Security.},
  BOOKTITLE = {Informatics},
  YEAR = {2001},
  PAGES = {86-101}
}

@TECHREPORT{hamlen03computability,
  AUTHOR = {Kevin W. Hamlen and Greg Morrisett and Fred B. Schneider},
  TITLE = {Computability Classes for Enforcement Mechanisms},
  NUMBER = {TR 2003-1908},
  YEAR = {2003},
  MONTH = {August},
  INSTITUTION = {Cornell Computer Science Department}
}

@INCOLLECTION{cardelli97type,
  AUTHOR = {Luca Cardelli},
  TITLE = {Type Systems.},
  BOOKTITLE = {The Computer Science and Engineering Handbook},
  YEAR = {1997},
  PAGES = {2208-2236},
  PUBLISHER = {{CRC} press}
}

@ARTICLE{Harper89framework,
  AUTHOR = {Robert Harper and Furio Honsell and Gordon Plotkin},
  TITLE = {A Framework for Defining Logics},
  JOURNAL = {Journal of the {ACM}},
  VOLUME = 40,
  NUMBER = 1,
  PAGES = {143-184},
  MONTH = JAN,
  YEAR = 1993
}

@INCOLLECTION{Pfenning02mdorf,
  AUTHOR = {Frank Pfenning},
  TITLE = {Logical Frameworks---A Brief Introduction},
  BOOKTITLE = {Proof and System-Reliability},
  PAGES = {137--166},
  PUBLISHER = {Kluwer Academic Publishers},
  YEAR = 2002,
  EDITOR = {H. Schwichtenberg and R. Steinbr{\"u}ggen},
  VOLUMN = 62,
  SERIES = {NATO Science Series {II}},
  NOTE = {Lecture notes from the Marktoberdorf Summer School, July 2001},
  URLPDF = {http://www.cs.cmu.edu/~fp/papers/mdorf01.pdf},
  URLPS = {http://www.cs.cmu.edu/~fp/papers/mdorf01.ps}
}

@INPROCEEDINGS{Pfenning88pldi,
  AUTHOR = {Frank Pfenning and Conal Elliott},
  TITLE = {Higher-Order Abstract Syntax},
  BOOKTITLE = {Proceedings of the {ACM SIGPLAN '88} Symposium on Language
  Design and Implementation},
  ADDRESS = {Atlanta, Georgia},
  MONTH = JUN,
  YEAR = {1988},
  PAGES = {199--208},
  URLPDF = {http://www.cs.cmu.edu/~fp/papers/pldi88.pdf},
  URLPS = {http://www.cs.cmu.edu/~fp/papers/pldi88.ps}
}

@INPROCEEDINGS{schurmann01induction,
  AUTHOR = {Carsten Sch{\"u}rmann},
  TITLE = {A Type-Theoretic Approach to Induction with Higher-Order
               Encodings.},
  BOOKTITLE = {LPAR},
  YEAR = {2001},
  PAGES = {266-281}
}

@INPROCEEDINGS{schurmann01recursion,
  AUTHOR = {Carsten Sch{\"u}rmann},
  TITLE = {Recursion for Higher-Order Encodings.},
  BOOKTITLE = {CSL},
  YEAR = {2001},
  PAGES = {585-599}
}

@INPROCEEDINGS{wadler93taste,
  AUTHOR = {P. L. Wadler},
  TITLE = {A Taste of Linear Logic},
  BOOKTITLE = {Proceedings of the 18th International Symposium on Mathematical Foundations of Computer Science, Gd{\'a}nsk},
  PUBLISHER = {Springer-Verlag},
  ADDRESS = {New York, NY},
  YEAR = {1993}
}

@ARTICLE{Chirimar93reference,
  AUTHOR = {Jawahar L. Chirimar and  Carl A. Gunter and  Jon G. Riecke},
  TITLE = {Reference Counting as a Computational Interpretation of
  Linear Logic},
  JOURNAL = {Journal of Functional Programming},
  YEAR = 1996,
  VOLUME = 6,
  NUMBER = 2,
  PAGES = {195-244},
  URLPDF = {http://www-faculty.cs.uiuc.edu/~cgunter/publications/documents/ChirimarGR96.pdf}
}


This file has been generated by bibtex2html 1.77