Home
Contact Information
Publications
Researchers
Focus Areas
FoxNet
Typed Intermediate Languages
Proof-Carrying Code
Logical Frameworks
Staged Computation
Language Design
 
Fox_Project@cs.cmu.edu
http://www.cs.cmu.edu/~fox/
  

The Fox Project
Typed Intermediate Languages / Bibliography

This is a bibliography of research papers and reports related to Typed Intermediate Languages from the Fox project at Carnegie Mellon University. The BibTeX source is available. Papers with known URLs in the World-Wide Web have been annotated with their location and can be previewed or retrieved directly. Corrections, additions, and new URLs for papers and implementations are welcome.

Last updated: Fri May 4 2001

  1. Andrew Bernard, Robert Harper, and Peter Lee. How generic is a generic back end? Using MLRISC as a back end for the TIL compiler. In X. Leroy and A. Ohori, editors, Proceedings of the Workshop on Types in Compilation, pages 53-77, Kyoto, Japan, March 1998. Springer-Verlag LNCS 1473. Available electronically (Abstract, DVI, Postscript).

  2. Perry Cheng, Robert Harper, and Peter Lee. Generational stack collection and profile-drive pretenuring. In Proceedings of the Conference on Programming Language Design and Implementation, pages 162-173, Montreal, Canada, June 1998. ACM Press. Available electronically (Abstract, Postscript).

  3. Christopher Colby, Karl Crary, Robert Harper, Peter Lee, and Frank Pfenning. Automated techniques for provably safe mobile code. To appear in a special issue of Theoretical Computer Science on Dependable Computing. Available electronically (Abstract, Postscript, PDF).

  4. Karl Crary. A simple proof technique for certain parametricity results. In Proceedings of the International Conference on Functional Programming, pages 82-89, Paris, France, September 1999. Available electronically (Abstract, DVI, Postscript).

  5. Karl Crary. Sound and complete elimination of singleton kinds. In Proceedings of the Workshop on Types in Compilation, September 2000. Proceedings available as School of Computer Science, Carnegie Mellon University Technical Report CMU-CS-00-161. Available electronically (Postscript, PDF).

  6. Karl Crary. Sound and complete elimination of singleton kinds. Technical Report CMU-CS-00-104, School of Computer Science, Carnegie Mellon University, January 2000. Available electronically (Abstract, Postscript, PDF).

  7. Karl Crary. Typed compilation of inclusive subtyping. In Proceedings of the International Conference on Functional Programming, pages 68-81, Montreal, Canada, September 2000. ACM Press. Available electronically (Abstract, DVI, Postscript).

  8. Karl Crary, Robert Harper, Perry Cheng, Leaf Petersen, and Chris Stone. Transparent and opaque interpretations of datatypes. Technical Report CMU-CS-98-177, School of Computer Science, Carnegie Mellon University, November 1998. Available electronically (Abstract, DVI, Postscript, PDF).

  9. Karl Crary, Robert Harper, Peter Lee, and Frank Pfenning. Automated techniques for provably safe mobile code. In Proceedings of the DARPA Information Survivability Conference and Exposition, volume 1, pages 406-419, Hilton Head Island, South Carolina, January 2000. IEEE Computer Society Press. Available electronically (Abstract, PDF).

  10. Karl Crary and Greg Morrisett. Type structure for low-level programming langauges. In Proceedings of the International Colloquium on Automata, Languages, and Programming, pages 40-54, Prague, Czech Republic, July 1999. Springer-Verlag LNCS 1644. Available electronically (Abstract, DVI, Postscript).

  11. Karl Crary, David Walker, and Greg Morrisett. Typed memory management in a calculus of capabilities. In Proceedings of the Symposium on Principles of Programming Languages, pages 262-275, San Antonio, Texas, January 1999. Available electronically (Abstract, DVI, Postscript).

  12. Karl Crary and Stephanie Weirich. Flexible type analysis. In Proceedings of the International Conference on Functional Programming, pages 233-248, Paris, France, September 1999. Available electronically (Abstract, DVI, Postscript).

  13. Karl Crary and Stephanie Weirich. Resource bound certification. In Proceedings of the Symposium on Principles of Programming Languages, pages 184-198, Boston, Massachusetts, January 2000. Available electronically (Abstract, DVI, Postscript).

  14. Karl Crary, Stephanie Weirich, and Greg Morrisett. Intensional polymorphism in type-erasure semantics. In Proceedings of the International Conference on Functional Programming, pages 301-312, Baltimore, Maryland, September 1998. ACM Press. Extended version published as Cornell University Technical Report TR98-1721. Available electronically (Abstract, DVI, Postscript).

  15. Derek R. Dreyer, Robert Harper, and Karl Crary. Toward a practical type theory for recursive modules. Technical Report CMU-CS-01-112, School of Computer Science, Carnegie Mellon University, March 2001. Available electronically (Abstract, Postscript, PDF).

  16. Robert Harper and Mark Lillibridge. Explicit polymorphism and CPS conversion. Technical Report CMU-CS-92-210, School of Computer Science, Carnegie Mellon University, October 1992. Available electronically (Abstract, DVI, Postscript).

  17. Robert Harper and Mark Lillibridge. Polymorphic type assignment and CPS conversion. In Olivier Danvy and Carolyn Talcott, editors, Proceedings of the ACM SIGPLAN Workshop on Continuations, Stanford, California, June 1992. Department of Computer Science, Stanford University. Published as Technical Report STAN-CS-92-1426. Available electronically (Abstract, DVI, Postscript).

  18. Robert Harper and Mark Lillibridge. Polymorphic type assignment and CPS conversion. Technical Report CMU-CS-92-122, School of Computer Science, Carnegie Mellon University, April 1992. Available electronically.

  19. Robert Harper and Mark Lillibridge. Explicit polymorphism and CPS conversion. In Proceedings of the Symposium on Principles of Programming Languages, pages 206-219, Charleston, South Carolina, January 1993. ACM Press. Available electronically (Abstract, DVI, Postscript).

  20. Robert Harper and Mark Lillibridge. Polymorphic type assignment and CPS conversion. Lisp and Symbolic Computation, 6(3/4):361-380, November 1993. Available electronically (Abstract, DVI, Postscript).

  21. Robert Harper and Mark Lillibridge. A type-theoretic approach to higher-order modules with sharing. Technical Report CMU-CS-93-197, School of Computer Science, Carnegie Mellon University, October 1993. Available electronically (Abstract, DVI, Postscript).

  22. Robert Harper and Mark Lillibridge. A type-theoretic approach to higher-order modules with sharing. In Proceedings of the Symposium on Principles of Programming Languages, pages 123-137, Portland, Oregon, January 1994. ACM Press. Available electronically (Abstract, DVI, Postscript).

  23. Robert Harper and Mark Lillibridge. Operational interpretations of an extension of Fw with control operators. Journal of Functional Programming, 6(3):393-417, May 1996. Available electronically (DVI, Postscript).

  24. Robert Harper and Greg Morrisett. Compiling polymorphism using intensional type analysis. Technical Report CMU-CS-94-185, School of Computer Science, Carnegie Mellon University, September 1994. Available electronically (Abstract, DVI, Postscript).

  25. Robert Harper and Greg Morrisett. Compiling with non-parametric polymorphism (preliminary report). Technical Report CMU-CS-94-122, School of Computer Science, Carnegie Mellon University, February 1994. Available electronically.

  26. Robert Harper and Greg Morrisett. Compiling polymorphism using intensional type analysis. In Proceedings of the Symposium on Principles of Programming Languages, pages 130-141, San Francisco, California, January 1995. ACM Press. Available electronically (Abstract, DVI, Postscript).

  27. Robert Harper and Chris Stone. A type-theoretic account of Standard ML 1996 (version 2). Technical Report CMU-CS-96-136R, School of Computer Science, Carnegie Mellon University, September 1996. Available electronically.

  28. Robert Harper and Chris Stone. A type-theoretic interpretation of Standard ML. In Gordon Plotkin, Colin Stirling, and Mads Tofte, editors, Proof, Language, and Interaction: Essays in Honor of Robin Milner. MIT Press, 2000. Available electronically (DVI, Postscript).

  29. Robert Harper and Christopher Stone. An interpretation of Standard ML in type theory. Technical Report CMU-CS-97-147, School of Computer Science, Carnegie Mellon University, June 1997. Available electronically (Abstract, DVI, Postscript).

  30. Michael Hicks, Stephanie Weirich, and Karl Crary. Safe and flexible dynamic linking of native code. In Proceedings of the Workshop on Types in Compilation, September 2000. Proceedings available as School of Computer Science, Carnegie Mellon University Technical Report CMU-CS-00-161. Available electronically (Postscript, PDF).

  31. Mark Lillibridge. Translucent Sums: A Foundation for Higher-Order Module Systems. PhD thesis, School of Computer Science, Carnegie Mellon University, May 1997. Available as Technical Report CMU-CS-97-122. Available electronically (Abstract, DVI, Postscript, PDF).

  32. Yasuhiko Minamide, Greg Morrisett, and Robert Harper. Typed closure conversion. Technical Report CMU-CS-95-171, School of Computer Science, Carnegie Mellon University, July 1995. Available electronically (Abstract, DVI, Postscript).

  33. Yasuhiko Minamide, Greg Morrisett, and Robert Harper. Typed closure conversion. In Guy Steele, Jr., editor, Proceedings of the Symposium on Principles of Programming Languages, pages 271-283, St. Petersburg Beach, Florida, January 1996. ACM Press. Available electronically (Abstract, DVI, Postscript).

  34. Greg Morrisett. Thesis proposal: Data representations and polymorphic languages. Unpublished, December 1993. Available electronically (Abstract, Postscript).

  35. Greg Morrisett. Compiling with Types. PhD thesis, School of Computer Science, Carnegie Mellon University, December 1995. Available as Technical Report CMU-CS-95-226. Available electronically (Postscript, PDF).

  36. Greg Morrisett, Karl Crary, Neal Glew, Dan Grossman, Richard Samuels, Frederick Smith, David Walker, Stephanie Weirich, and Steve Zdancewic. TALx86: A realistic typed assembly language. In Informal Proceedings of the Workshop on Compiler Support for Systems Software, Atlanta, Georgia, May 1999. Available electronically (Abstract, DVI, Postscript).

  37. Greg Morrisett, Karl Crary, Neal Glew, and David Walker. Stack-based typed assembly language. To appear in the Journal of Functional Programming.

  38. Greg Morrisett, Karl Crary, Neal Glew, and David Walker. Stack-based typed assembly language. In X. Leroy and A. Ohori, editors, Proceedings of the Workshop on Types in Compilation, pages 28-52, Kyoto, Japan, March 1998. Springer-Verlag LNCS 1473. Available electronically (Abstract, DVI, Postscript, PDF).

  39. Greg Morrisett, Karl Crary, David Walker, and Neal Glew. Stack-based typed assembly language. Technical Report CMU-CS-98-178, School of Computer Science, Carnegie Mellon University, November 1998. Available electronically (Abstract, Postscript, PDF).

  40. Greg Morrisett, Matthias Felleisen, and Robert Harper. Abstract models of memory management. In Proceedings of the International Conference on Functional Programming Languages and Computer Architecture, pages 66-77, La Jolla, California, June 1995. ACM Press. Available electronically (Abstract, DVI, Postscript).

  41. Greg Morrisett, Matthias Felleisen, and Robert Harper. Abstract models of memory management. Technical Report CMU-CS-95-110, School of Computer Science, Carnegie Mellon University, January 1995. Available electronically (Abstract, DVI, Postscript).

  42. Greg Morrisett and Robert Harper. Semantics of memory management for polymorphic languages. Technical Report CMU-CS-96-176, School of Computer Science, Carnegie Mellon University, September 1996. Available electronically (Abstract, DVI, Postscript).

  43. Greg Morrisett and Robert Harper. Typed closure conversion for recursively-defined functions (extended abstract). In Andrew Gordon, Andrew Pitts, and Carolyn Talcott, editors, Proceedings of the Workshop on Higher-Order Operational Techniques in Semantics, volume 10 of Electronic Notes in Theoretical Computer Science, Stanford, California, December 1997. Elsevier Science Publishers. Available electronically (Abstract, DVI, Postscript).

  44. Greg Morrisett and Robert Harper. Semantics of memory management for polymorphic languages. In Andrew D. Gordon and Andrew M. Pitts, editors, Higher-Order Operational Techniques in Semantics, Publications of the Newton Institute, pages 175-226. Cambridge University Press, January 1998. Available electronically (DVI, Postscript).

  45. Greg Morrisett, David Tarditi, Perry Cheng, Chris Stone, Robert Harper, and Peter Lee. The TIL/ML compiler: Performance and safety through types. In Informal Proceedings of the Workshop on Compiler Support for Systems Software, Tucson, Arizona, February 1996. Available electronically (DVI, Postscript).

  46. Greg Morrisett, David Walker, Karl Crary, and Neal Glew. From System F to typed assembly language. ACM Transactions on Programming Languages and Systems, 21(3):527-568, May 1999. Extended version of paper presented at the Symposium on Principles of Programming Languages, San Diego, California, January 1998. Available electronically (Abstract, DVI, Postscript, PDF).

  47. Leaf Petersen, Perry Cheng, Robert Harper, and Chris Stone. Implementing the TILT internal language. Technical Report CMU-CS-00-180, School of Computer Science, Carnegie Mellon University, December 2000. Available electronically (Abstract, Postscript, PDF).

  48. Fred B. Schneider, Greg Morrisett, and Robert Harper. A language-based approach to security. In Reinhard Wilhelm, editor, Informatics - 10 Years Back, 10 Years Ahead. Proceedings of the Conference on the Occasion of Dagstuhl's 10th Anniversary, Saarbrücken, Germany, August 2000. Springer-Verlag LNCS 2000. Available electronically (Abstract, Postscript, PDF).

  49. Chris Stone. Elaboration and phase-splitting in the TIL/ML compiler. IC Research Symposium abstract, 1997. Available electronically.

  50. Chris Stone and Robert Harper. A type-theoretic account of Standard ML 1996 (version 1). Technical Report CMU-CS-96-136, School of Computer Science, Carnegie Mellon University, May 1996. Available electronically.

  51. Christopher A. Stone and Robert Harper. Deciding type equivalence for a language with singleton kinds. Technical Report CMU-CS-99-155, School of Computer Science, Carnegie Mellon University, September 1999. Available electronically (Abstract, Postscript, PDF).

  52. Christopher A. Stone and Robert Harper. Deciding type equivalence in a language with singleton kinds. In Proceedings of the Symposium on Principles of Programming Languages, pages 214-227, Boston, Massachusetts, January 2000. Available electronically.

  53. Christopher Allan Stone. Singleton Kinds and Singleton Types. PhD thesis, School of Computer Science, Carnegie Mellon University, August 2000. Available as Technical Report CMU-CS-00-153. Available electronically.

  54. David Tarditi. Using program structure to guide optimization in the presence of first-class functions. Thesis proposal (draft), November 1994. Available electronically (Abstract, Postscript).

  55. David Tarditi. Design and Implementation of Code Optimiziations for a Type-Directed Compiler for Standard ML. PhD thesis, School of Computer Science, Carnegie Mellon University, December 1996. Available as Technical Report CMU-CS-97-108. Available electronically (Abstract, Postscript).

  56. David Tarditi, Greg Morrisett, Perry Cheng, Chris Stone, Robert Harper, and Peter Lee. TIL: A type-directed optimizing compiler for ML. In Proceedings of the Conference on Programming Language Design and Implementation, pages 181-192, Philadelphia, Pennsylvania, May 1996. ACM Press. Available electronically (Abstract, DVI, Postscript).

  57. David Tarditi, Greg Morrisett, Perry Cheng, Chris Stone, Robert Harper, and Peter Lee. TIL: A type-directed optimizing compiler for ML. Technical Report CMU-CS-96-108, School of Computer Science, Carnegie Mellon University, February 1996. Available electronically (Abstract, DVI, Postscript).

  58. David Walker, Karl Crary, and Greg Morrisett. Typed memory management via static capabilities. Transactions on Programming Languages and Systems, 22(4):701-771, July 2000. Available electronically (Abstract, Postscript).

  59. Hongwei Xi and Robert Harper. A dependently typed assembly language. Technical Report OGI-CSE-99-008, Department of Computer Science and Engineering, Oregon Graduate Institute of Science and Technology, July 1999. Available electronically (Abstract, Postscript, PDF).

  60. Hongwei Xi and Robert Harper. A dependently typed assembly language. In Informal Proceedings of the Workshop on Dependent Types in Programming, Göteborg, March 1999.

[ Home | Contact Information | Publications | Researchers ]
[ FoxNet | Typed Intermediate Languages | Proof-Carrying Code ]
[ Logical Frameworks | Staged Computation | Language Design ]

Fox_Project@cs.cmu.edu
http://www.cs.cmu.edu/~fox/