%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% SYSTEMS (MISCELLANEOUS)

@article{Knowlton:1965:buddy,
 author = {Knowlton, Kenneth C.},
 title = {A fast storage allocator},
 journal = {Commun. ACM},
 volume = 8,
 number = 10,
 year = 1965,
 issn = {0001-0782},
 pages = {623--624},
 doi = {http://doi.acm.org/10.1145/365628.365655},
 publisher = {ACM},
 address = {New York, NY, USA},
 }

@inproceedings{Wahbe:1993:SOSP,
 author = {Wahbe, Robert and Lucco, Steven and Anderson, Thomas E. and Graham, Susan L.},
 title = {Efficient software-based fault isolation},
 booktitle = {SOSP '93: Proceedings of the fourteenth ACM symposium on Operating systems principles},
 year = 1993,
 isbn = {0-89791-632-8},
 pages = {203--216},
 location = {Asheville, North Carolina, United States},
 doi = {http://doi.acm.org/10.1145/168619.168635},
 publisher = {ACM},
 address = {New York, NY, USA},
 }

@article{Birrell:1984:TOCS,
 author = {Birrell, Andrew D. and Nelson, Bruce Jay},
 title = {Implementing remote procedure calls},
 journal = {ACM Trans. Comput. Syst.},
 volume = 2,
 number = 1,
 year = 1984,
 issn = {0734-2071},
 pages = {39--59},
 doi = {http://doi.acm.org/10.1145/2080.357392},
 publisher = {ACM},
 address = {New York, NY, USA},
 }

@article{Lamport:1978:CACM,
 author = {Lamport, Leslie},
 title = {Time, clocks, and the ordering of events in a distributed system},
 journal = {Commun. ACM},
 volume = 21,
 number = 7,
 year = 1978,
 issn = {0001-0782},
 pages = {558--565},
 doi = {http://doi.acm.org/10.1145/359545.359563},
 publisher = {ACM},
 address = {New York, NY, USA},
 }

@article{Burrows:1990:TOCS,
 author = {Burrows, Michael and Abadi, Martin and Needham, Roger},
 title = {A logic of authentication},
 journal = {ACM Trans. Comput. Syst.},
 volume = 8,
 number = 1,
 year = 1990,
 issn = {0734-2071},
 pages = {18--36},
 doi = {http://doi.acm.org/10.1145/77648.77649},
 publisher = {ACM},
 address = {New York, NY, USA},
 }

@article{Saltzer:1984:TOCS,
 author = {Saltzer, J. H. and Reed, D. P. and Clark, D. D.},
 title = {End-to-end arguments in system design},
 journal = {ACM Trans. Comput. Syst.},
 volume = 2,
 number = 4,
 year = 1984,
 issn = {0734-2071},
 pages = {277--288},
 doi = {http://doi.acm.org/10.1145/357401.357402},
 publisher = {ACM},
 address = {New York, NY, USA},
 }

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% OPERATING SYSTEMS

@misc{Liedtke:1996:L4,
    author = {Jochen Liedtke},
    title = "{Toward Real Microkernels}",
    year = {1996},
    howpublished = {CACM, 39(9):70--77}
}

@inproceedings{Ford:1996:microkernels,
    author = {Bryan Ford and Bryan Ford and Mike Hibler and Mike Hibler and Jay Lepreau and Jay Lepreau and Patrick Tullmann and Patrick Tullmann and Godmar Back and Godmar Back and Stephen Clawson and Stephen Clawson},
    title = {Microkernels Meet Recursive Virtual Machines},
    booktitle = {Proceedings of the Second Symposium on Operating Systems Design and Implementation},
    year = 1996,
    pages = {137--151}
}

@inproceedings{Bershad:1995:SPIN,
    author = {Brian N. Bershad and Stefan Savage and Przemyslaw Pardyak and Emin Gün Sirer and Emin Gun Sirer and Marc Fiuczynski and David Becker and Susan Eggers and Craig Chambers},
    title = "{Extensibility, Safety and Performance in the SPIN Operating System}",
    booktitle = {Proceedings of the Fifteenth ACM Symposium on Operating Systems Principles},
    year = 1995,
    pages = {267--284}
}

@InProceedings{Hunt:2007:Singularity,
  author =       {Hunt, Galen C. and Larus, James R.},
  title =        "{Singularity: Rethinking the Software Stack}",
  booktitle = {ACM SIGOPS Operating System Review},
  pages =     {37--49},
  year =      2007,
  volume =    41,
  month =     {Apr},
  organization = {Association for Computing Machinery}
}

@inproceedings{Engler:1995:SOSP,
 author = {Engler, D. R. and Kaashoek, M. F. and O'Toole,Jr., J.},
 title = {Exokernel: an operating system architecture for application-level resource management},
 booktitle = {SOSP '95: Proceedings of the fifteenth ACM symposium on Operating systems principles},
 year = 1995,
 isbn = {0-89791-715-4},
 pages = {251--266},
 location = {Copper Mountain, Colorado, United States},
 doi = {http://doi.acm.org/10.1145/224056.224076},
 publisher = {ACM},
 address = {New York, NY, USA},
 }

@inproceedings{Liedtke:1995:SOSP,
 author = {Liedtke, J.},
 title = {On micro-kernel construction},
 booktitle = {SOSP '95: Proceedings of the fifteenth ACM symposium on Operating systems principles},
 year = 1995,
 isbn = {0-89791-715-4},
 pages = {237--250},
 location = {Copper Mountain, Colorado, United States},
 doi = {http://doi.acm.org/10.1145/224056.224075},
 publisher = {ACM},
 address = {New York, NY, USA},
 }

@InProceedings{Barham:2003:SOSP,
  author =       {P. Barham and B. Dragovic and K. Fraser and S. Hand and T. Harris and A. Ho and R. Neugebauer and I. Pratt and A. Warfield},
  title =        "{Xen and the Art of Virtualization}",
  booktitle = {Proceedings of the Nineteenth ACM Symposium on Operating Systems Principles},
  pages =     {164--177},
  year =      2003,
  month =     {Oct}
}

@INPROCEEDINGS{Liedtke:1993:SOSP,
    author = {Jochen Liedtke},
    title = "{Improving IPC by Kernel Design}",
    booktitle = {14th ACM Symposium on Operating System Principles (SOSP},
    year = 1993,
    pages = {175--188}
}

@inproceedings{Bugnion:1997:SOSP,
 author = {Bugnion, Edouard and Devine, Scott and Rosenblum, Mendel},
 title = {Disco: running commodity operating systems on scalable multiprocessors},
 booktitle = {SOSP '97: Proceedings of the sixteenth ACM symposium on Operating systems principles},
 year = 1997,
 isbn = {0-89791-916-5},
 pages = {143--156},
 location = {Saint Malo, France},
 doi = {http://doi.acm.org/10.1145/268998.266672},
 publisher = {ACM},
 address = {New York, NY, USA},
 }

@Misc{Intel:Manuals,
  author = {Intel Inc},
  title = "{Intel\texttrademark 64 and IA-32 Architectures Software Developer's Manuals}",
  howpublished = {\url{http://www.intel.com/products/processor/manuals/}}
}

@InProceedings{Faendrich:2006:EuroSys,
  author    = {F\"andrich, Manuel and Aiken, Mark and Hawblitzel, Chris and Hodson, Orion and Hunt, Galen and Larus, James R. and Levi, Steven},
  title     = "{Language Support for Fast and Reliable Message-based Communication in Singularity OS}",
  booktitle = {Proceedings of EuroSys '06},
  year      = 2006,
  month     = {Apr},
  publisher = {ACM}
}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% OPERATING SYSTEM VERIFICATION


@misc{Tullmann:1997:formalmethods,
    author = {Patrick Tullmann and Jeff Turner and John Mccorquodale and Jay Lepreau and Ajay Chitturi and Godmar Back},
    title = "{Formal Methods: A Practical Tool for OS Implementors}",
    year = 1997
}

@inproceedings{Gerwin:2005:osverification,
    author = {Harvey Tuch Gerwin and Harvey Tuch and Gerwin Klein and Gernot Heiser},
    title = "{OS Verification --- Now!}",
    booktitle = {Proceedings of the 10th Workshop on Hot Topics in Operating Systems},
    year = 2005,
    pages = {7--12}
}

@InProceedings{Hohmuth:2005:VFiasco,
  author =       {Hohmuth, M. and Tews, H.},
  title =        "{The VFiasco approach for a verified operating system}",
  booktitle = {Proceedings of the 2nd ECOOP Workshop on Programming Languages and Operating Systems},
  year =      2005,
  note =      {\url{http://www.cs.ru.nl/H.Tews/Plos-2005/ecoop-plos-05-letter.pdf}}
}

@inproceedings{Alkassar:2008:VSTTE,
 author = {Alkassar, Eyad and Hillebrand, Mark A. and Leinenbach, Dirk and Schirmer, Norbert W. and Starostin, Artem},
 title = "{The Verisoft Approach to Systems Verification}",
 booktitle = {VSTTE '08: Proceedings of the 2nd international conference on Verified Software: Theories, Tools, Experiments},
 year = 2008,
 isbn = {978-3-540-87872-8},
 pages = {209--224},
 location = {Toronto, Canada},
 doi = {http://dx.doi.org/10.1007/978-3-540-87873-5_18},
 publisher = {Springer-Verlag},
 address = {Berlin, Heidelberg},
 }

@InProceedings{Klein:2009:SOSP,
  author =       {Klein, Gerwin and Elphinstone, Kevin and Heiser, Gernot and others},
  title =        "{seL4: Formal verification of an OS kernel}",
  booktitle = {Proceedings of the 22nd ACM Symposium on Operating Systems Principles},
  year =      2009,
  address =   {Big Sky, MT, USA},
  month =     {Oct}
}

@article{Hallgren:2005:ICFP,
 author = {Hallgren, Thomas and Jones, Mark P. and Leslie, Rebekah and Tolmach, Andrew},
 title = "{A principled approach to operating system construction in Haskell}",
 journal = {SIGPLAN Not.},
 volume = 40,
 number = 9,
 year = 2005,
 issn = {0362-1340},
 pages = {116--128},
 doi = {http://doi.acm.org/10.1145/1090189.1086380},
 publisher = {ACM},
 address = {New York, NY, USA},
 }

@MastersThesis{Fu:1999:Hello,
  author =       {Fu, Guangrui},
  title =        "{Design and Implementation of an Operating System in Standard ML}",
  school =       {University of Hawaii},
  year =         1999,
  month =     {Aug},
  note =      {\url{http://www2.hawaii.edu/~esb/prof/proj/hello/}}
}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% TYPE THEORY

@Article{Reynolds:1983:IP,
  author =       {Reynolds, J. C.},
  title =        {Types, abstraction, and parametric polymorphism},
  journal =      {Information Processing},
  year =         1983,
  volume =    83,
  pages =     {513--523}
}

@InProceedings{Damas:1982:POPL,
  author =       {Damas, L. and Milner, R.},
  title =        {Principal type schemes for functional programs},
  booktitle = {Proceedings of 9th Annual Symposium on Principles of Programming Languages},
  year =      1982,
  address =   {Albuquerque, NM},
  month =     {Jan},
  publisher = {ACM}
}

L. Damas and R. Milner, Principal type schemes for functional programs, , Albuquerque,
N.M., ACM, January 1982.

@Article{Milner:1978:JCSS,
  author =       {Milner, Robin},
  title =        {A theory of type polymorphism in programming},
  journal =      {Journal of Computers and Systems Science},
  year =         1978,
  volume =    17,
  pages =     {348--375}}

@InBook{Reynolds:1974:LNCS,
  author =    {Reynolds, J. C.},
  title =        {Towards a theory of type structure},
  chapter =      {Formal Semantics},
  publisher =    {Springer-Verlag},
  year =         1974,
  isbn = {978-3-540-06859-4},
  volume =    19,
  series =    {LNCS},
  pages =     {408--425}
}

@inproceedings{Wadler:1989:POPL,
 author = {Wadler, P. and Blott, S.},
 title = {How to make ad-hoc polymorphism less ad hoc},
 booktitle = {POPL '89: Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages},
 year = 1989,
 isbn = {0-89791-294-2},
 pages = {60--76},
 location = {Austin, Texas, United States},
 doi = {http://doi.acm.org/10.1145/75277.75283},
 publisher = {ACM},
 address = {New York, NY, USA},
 }

@inproceedings{Wadler:1989:FPCA,
 author = {Wadler, Philip},
 title = {Theorems for free!},
 booktitle = {FPCA '89: Proceedings of the fourth international conference on Functional programming languages and computer architecture},
 year = 1989,
 isbn = {0-89791-328-0},
 pages = {347--359},
 location = {Imperial College, London, United Kingdom},
 doi = {http://doi.acm.org/10.1145/99370.99404},
 publisher = {ACM},
 address = {New York, NY, USA},
 }

@article{Harper:1993:LF,
    author = {Robert Harper and Furio Honsell and Gordon Plotkin},
    title = {A Framework for Defining Logics},
    journal = {Journal of the Association for Computing Machinery},
    year = {1993},
    pages = {194--204}
}

@misc{Xi:2004:ATSLF,
    author = {Hongwei Xi},
    title = "{ATS/LF: a type system for constructing proofs as total functional programs}",
    year = {2004},
    howpublished = {\url{http://www.ats-lang.org/PAPER/ATSLF-PAfestschrift.pdf}}
}

@Misc{ATSLFex,
  author =    {Xi, Hongwei},
  title =     {Examples encoding deduction systems},
  howpublished = {\url{http://www.ats-lang.org/EXAMPLE/LF/LF.html}},
  year = 2009
}

@INPROCEEDINGS{Cervesato:1996:LICS,
    author = {Iliano Cervesato and Frank Pfenning},
    title = {A Linear Logical Framework},
    booktitle = {Proceedings of the Eleventh Annual Symposium on Logic in Computer Science},
    year = {1996},
    pages = {264--275},
    publisher = {IEEE Computer Society Press}
}

@InProceedings{Wadler:1991:PEPM,
  author =       {Wadler, Philip},
  title =        {Is there a use for linear logic?},
  booktitle = {Proceedings of Partial Evaluation and Semantics-Based Program Manipulation},
  year =      1991,
  address =   {New Haven, CT},
  month =     {Jun},
  publisher = {ACM Press}
}

@InCollection{Harper:2005:ATTAPL,
  author =	"Robert Harper and Benjamin C. Pierce",
  title =	"{Design Issues in Advanced Module Systems}",
  booktitle =	"Advanced Topics in Types and Programming Languages",
  publisher =	"MIT Press",
  year = 	"2005",
  editor =	"Benjamin C. Pierce",
  chapter =     8,
}

@InCollection{Walker:2005:ATTAPL,
  author =	"David Walker",
  title =	"{Substructural Type Systems}",
  booktitle =	"Advanced Topics in Types and Programming Languages",
  publisher =	"MIT Press",
  year = 	"2005",
  editor =	"Benjamin C. Pierce",
  chapter =     1,
}

@InCollection{Aspinall:2005:ATTAPL,
  author =	"David Aspinall and Martin Hofmann",
  title =	"{Dependent Types}",
  booktitle =	"Advanced Topics in Types and Programming Languages",
  publisher =	"MIT Press",
  year = 	"2005",
  editor =	"Benjamin C. Pierce",
  chapter =     2,
}

@InCollection{Henglein:2005:ATTAPL,
  author =	"Fritz Henglein and Henning Makholm and Henning Niss",
  title =	"{Effect Types and Region-Based Memory Management}",
  booktitle =	"Advanced Topics in Types and Programming Languages",
  publisher =	"MIT Press",
  year = 	"2005",
  editor =	"Benjamin C. Pierce",
  chapter =     3,
}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% PROGRAMMING LANGUAGES

@INPROCEEDINGS{Reynolds:2002:LICS,
    author = {John Reynolds},
    title = {Separation Logic: A Logic for Shared Mutable Data Structures},
    booktitle = {Proceedings of the Seventeenth Annual IEEE Symposium on Logic in Computer Science},
    year = 2002,
    pages = {55--74},
    publisher = {IEEE Computer Society}
}

@inproceedings{Augustsson:1998:ICFP,
 author = {Augustsson, Lennart},
 title = {Cayenne---a language with dependent types},
 booktitle = {ICFP '98: Proceedings of the third ACM SIGPLAN international conference on Functional programming},
 year = 1998,
 isbn = {1-58113-024-4},
 pages = {239--250},
 location = {Baltimore, Maryland, United States},
 doi = {http://doi.acm.org/10.1145/289423.289451},
 publisher = {ACM},
 address = {New York, NY, USA},
 }

@Article{Strachey:2000:HOSC,
  author =       {Strachey, C.},
  title =        {Fundamental concepts in programming languages},
  journal =      {Higher-Order and Symbolic Computation},
  year =         2000,
  volume =    13,
  number =    1,
  pages =     {11--49}
}

@article{Xi:2007:JFP,
 author = {Xi, Hongwei},
 title = "{Dependent ML: An approach to practical programming with dependent types}",
 journal = {J. Funct. Program.},
 volume = 17,
 number = 2,
 year = 2007,
 issn = {0956-7968},
 pages = {215--286},
 doi = {http://dx.doi.org/10.1017/S0956796806006216},
 publisher = {Cambridge University Press},
 address = {New York, NY, USA},
 }

@inproceedings{Xi:2004:TYPES,
    author = {Hongwei Xi},
    title = "{Applied Type System (extended abstract)}",
    booktitle = {Post-workshop Proceedings of TYPES 2003},
    year = 2004,
    pages = {394--408}
}

@TechReport{MODULA3,
  author =       {Cardelli, Luca and others},
  title =        {Modula-3 Report (revised)},
  institution =  {Digital Equipment Corp. (now HP Inc.)},
  year =         1989,
  month =     {Nov},
  note =      {\url{http://www.hpl.hp.com/techreports/Compaq-DEC/SRC-RR-52.html}}
}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% FUNCTIONAL PROGRAMMING

@inproceedings{Jones:1993:POPL,
 author = {Peyton Jones, Simon L. and Wadler, Philip},
 title = {Imperative functional programming},
 booktitle = {POPL '93: Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages},
 year = {1993},
 isbn = {0-89791-560-7},
 pages = {71--84},
 location = {Charleston, South Carolina, United States},
 doi = {http://doi.acm.org/10.1145/158511.158524},
 publisher = {ACM},
 address = {New York, NY, USA},
 }

@article{Hughes:1989:CJ,
	AUTHOR = {J. Hughes},
	TITLE = "{Why Functional Programming Matters}",
	JOURNAL = {Computer Journal},
	VOLUME = 32,
	NUMBER = 2,
        PAGES = {98--107},
	YEAR = 1989
}

@InBook{Barendregt:1984:ChurchRosser,
  author    = {Barendregt, H. P.},
  title     = "{The Lambda Calculus: Its Syntax and Semantics}",
  chapter   = 11,
  publisher = {Elsevier},
  year      = 1984,
  pages     = {277--282}
}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% TYPES AND SYSTEMS

@inproceedings{Zhou:2006:OSDI,
 author = {Zhou, Feng and Condit, Jeremy and Anderson, Zachary and Bagrak, Ilya and Ennals, Rob and Harren, Matthew and Necula, George and Brewer, Eric},
 title = "{SafeDrive: safe and recoverable extensions using language-based techniques}",
 booktitle = {OSDI '06: Proceedings of the 7th symposium on Operating systems design and implementation},
 year = {2006},
 isbn = {1-931971-47-1},
 pages = {45--60},
 location = {Seattle, Washington},
 publisher = {USENIX Association},
 address = {Berkeley, CA, USA},
 }

@inproceedings{Klein:2007:POPL,
 author = {Tuch, Harvey and Klein, Gerwin and Norrish, Michael},
 title = {Types, bytes, and separation logic},
 booktitle = {POPL '07: Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages},
 year = {2007},
 isbn = {1-59593-575-4},
 pages = {97--108},
 location = {Nice, France},
 doi = {http://doi.acm.org/10.1145/1190216.1190234},
 publisher = {ACM},
 address = {New York, NY, USA},
 }

@article{Necula:2005:CCured,
 author = {Necula, George C. and Condit, Jeremy and Harren, Matthew and McPeak, Scott and Weimer, Westley},
 title = "{CCured: type-safe retrofitting of legacy software}",
 journal = {ACM Trans. Program. Lang. Syst.},
 volume = {27},
 number = {3},
 year = {2005},
 issn = {0164-0925},
 pages = {477--526},
 doi = {http://doi.acm.org/10.1145/1065887.1065892},
 publisher = {ACM},
 address = {New York, NY, USA},
 }

@inproceedings{Shi:2007:PLPV,
 author = {Shi, Rui},
 title = "{Implementing reliable Linux device drivers in ATS}",
 booktitle = {PLPV '07: Proceedings of the 2007 workshop on Programming languages meets program verification},
 year = 2007,
 isbn = {978-1-59593-677-6},
 pages = {41--46},
 location = {Freiburg, Germany},
 doi = {http://doi.acm.org/10.1145/1292597.1292605},
 publisher = {ACM},
 address = {New York, NY, USA},
 }

@inproceedings{Xi:2005:pointers,
    author = {Zhu, Dengping and Xi, Hongwei},
    title = {Safe Programming with Pointers through Stateful Views},
    booktitle = {Proceedings of the 7th International Symposium on Practical Aspects of Declarative Languages},
    year = 2005,
    pages = {83--97},
    publisher = {Springer}
}

@inproceedings{Xi:2005:PADL,
    author = {Zhu, Dengping and Xi, Hongwei},
    title = {Safe Programming with Pointers through Stateful Views},
    booktitle = {Proceedings of the 7th International Symposium on Practical Aspects of Declarative Languages},
    year = 2005,
    pages = {83--97},
    publisher = {Springer}
}

@inproceedings{Chen:2005:proving,
    author = {Chiyan Chen and Hongwei Xi},
    title = {Combining programming with theorem proving},
    booktitle = {ICFP ’05: Proceedings of the tenth ACM SIGPLAN International Conference on Functional programming},
    year = 2005,
    pages = {66--77},
    publisher = {ACM Press}
}

@inproceedings{Shapiro:2008:APLAS,
 author = {Sridhar, Swaroop and Shapiro, Jonathan S. and Smith, Scott F.},
 title = {Sound and Complete Type Inference for a Systems Programming Language},
 booktitle = {APLAS '08: Proceedings of the 6th Asian Symposium on Programming Languages and Systems},
 year = 2008,
 isbn = {978-3-540-89329-5},
 pages = {290--306},
 location = {Bangalore, India},
 doi = {http://dx.doi.org/10.1007/978-3-540-89330-1_21},
 publisher = {Springer-Verlag},
 address = {Berlin, Heidelberg},
 }

@article{Diatchki:2005:ICFP,
 author = {Diatchki, Iavor S. and Jones, Mark P. and Leslie, Rebekah},
 title = {High-level views on low-level representations},
 journal = {SIGPLAN Not.},
 volume = 40,
 number = 9,
 year = 2005,
 issn = {0362-1340},
 pages = {168--179},
 doi = {http://doi.acm.org/10.1145/1090189.1086387},
 publisher = {ACM},
 address = {New York, NY, USA},
 }

@inproceedings{Stump:2009:PLPV,
 author = {Stump, Aaron and Deters, Morgan and Petcher, Adam and Schiller, Todd and Simpson, Timothy},
 title = "{Verified programming in Guru}",
 booktitle = {PLPV '09: Proceedings of the 3rd workshop on Programming languages meets program verification},
 year = {2008},
 isbn = {978-1-60558-330-3},
 pages = {49--58},
 location = {Savannah, GA, USA},
 doi = {http://doi.acm.org/10.1145/1481848.1481856},
 publisher = {ACM},
 address = {New York, NY, USA},
 }

@inproceedings{Morrisett:2002:ATEC,
 author = {Jim, Trevor and Morrisett, J. Greg and Grossman, Dan and Hicks, Michael W. and Cheney, James and Wang, Yanling},
 title = "{Cyclone: A Safe Dialect of C}",
 booktitle = {ATEC '02: Proceedings of the General Track of the annual conference on USENIX Annual Technical Conference},
 year = 2002,
 isbn = {1-880446-00-6},
 pages = {275--288},
 publisher = {USENIX Association},
 address = {Berkeley, CA, USA},
 }

@inproceedings{Morrisett:2008:ICFP,
 author = {Nanevski, Aleksandar and Morrisett, Greg and Shinnar, Avraham and Govereau, Paul and Birkedal, Lars},
 title = {Ynot: dependent types for imperative programs},
 booktitle = {ICFP '08: Proceeding of the 13th ACM SIGPLAN international conference on Functional programming},
 year = 2008,
 isbn = {978-1-59593-919-7},
 pages = {229--240},
 location = {Victoria, BC, Canada},
 doi = {http://doi.acm.org/10.1145/1411204.1411237},
 publisher = {ACM},
 address = {New York, NY, USA},
 }

@INPROCEEDINGS{Necula:1996:OSDI,
    author = {George C. Necula and Peter Lee},
    title = {Safe Kernel Extensions Without Run-Time Checking},
    booktitle = {Proceedings of OSDI'96},
    year = 1996,
    pages = {28--31}
}

@INPROCEEDINGS{Tarditi:1995:PLDI,
    author = {David Tarditi and Greg Morrisett and Perry Cheng and Chris Stone and Robert Harper and Peter Lee},
    title = "{TIL: A Type-Directed Optimizing Compiler for ML}",
    booktitle = {ACM SIGPLAN conference on Programming Language Design and Implementation},
    year = 1995,
    pages = {181--192},
    publisher = {ACM Press}
}

@InBook{Necula:2007:Deputy,
  author =    {Condit, Jeremy and Harren, Matthew and Anderson, Zachary and Gay, David and Necula, George C.},
  title =        "{Programming Languages and Systems}",
  chapter =      "{Dependent Types for Low-level Programming}",
  publisher =    {Springer Berlin / Heidelberg},
  year =         2007,
  series =    {Lecture Notes in Computer Science},
  pages =     {520--535}
}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% SOFTWARE

@Misc{GHC,
  author =    {Peyton-Jones, Simon and Marlow, Simon and others},
  title =     "{The Glasgow Haskell Compiler}",
  howpublished = {\url{http://www.haskell.org/ghc/}},
  year = 2009
}

@Misc{QEMU,
  author =    {Bellard, Fabrice and others},
  title =     "{QEMU: machine emulator}",
  howpublished = {\url{http://www.qemu.org/}},
  year =      2009
}

@Misc{BOCHS,
  author =    {Denny, Bryce and Bothamy, Christophe and Becker, Donald and others},
  title =     "{BOCHS: x86 PC emulator}",
  howpublished = {\url{http://bochs.sourceforge.net/}},
  year =      2009
}

@Misc{VMWARE,
  author =    {VMWare Inc.},
  title =     "{VMWare: Virtual Machine software}",
  howpublished = {\url{http://www.vmware.com/}},
  year =      2009
}

@Misc{SMLNJ,
  author =    {Blume, Matthias and others},
  title =     "{Standard ML of New Jersey}",
  howpublished = {\url{http://www.smlnj.org/}},
  year =      2009
}

@Misc{ATS,
  author =    {Xi, Hongwei and others},
  title =     "{The ATS language}",
  howpublished = {\url{http://www.ats-lang.org/}},
  year =      2009
}

@Misc{QUEST,
  author =    {West, Richard},
  title =     "{The Quest operating system}",
  howpublished = {\url{http://www.cs.bu.edu/fac/richwest/quest}},
  year =      2009
}

@Misc{ISABELLE,
  author =    {Paulson, Larry and Nipkow, Tobias},
  title =     {Isabelle Proof Assistant},
  howpublished = {\url{http://www.cl.cam.ac.uk/research/hvg/Isabelle/}},
  year =      2009
}

@Misc{COQ,
  author =    {Herbelin, Hugo},
  title =     {Coq proof assistant},
  howpublished = {\url{http://coq.inria.fr/}},
  year = 2009
}