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
Programming Language Design / Bibliography

This is a bibliography of research papers and reports related to Programming Language Design 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: Thu Mar 22 2001

  1. Lars Birkedal and Robert Harper. Relational interpretations of recursive types in an operational setting. To appear in Theoretical Computer Science. Available electronically (DVI, Postscript).

  2. Lars Birkedal and Robert Harper. Relational interpretations of recursive types in an operational setting (summary). In M. Abadi and T. Ito, editors, Proceedings of the International Symposium on Theoretical Aspects of Computer Software, pages 458-490, Sendai, Japan, September 1997. Springer-Verlag LNCS 1281. Available electronically.

  3. Lars Birkedal and Robert Harper. Relational interpretations of recursive types in an operational setting. Technical Report CMU-CS-98-125, School of Computer Science, Carnegie Mellon University, April 1998. Available electronically (Abstract, Postscript).

  4. Lars Birkedal and Robert Harper. Relational interpretations of recursive types in an operational setting. Information and Computation, 155(1/2):3-63, November 1999. Available electronically.

  5. Kim B. Bruce, Leaf Petersen, and Adrian Fiech. Subtyping is not a good ``match'' for object-oriented languages. In M. Aksit and S. Matsuoka, editors, Proceedings of the European Conference for Object-Oriented Programming, pages 104-127, Jyväskylä, Finnland, June 1997. Springer-Verlag LNCS 1241. Available electronically (Abstract, DVI, Postscript).

  6. Robert L. Constable and Karl Crary. Computational complexity and induction for partial computable functions in type theory. To appear in Feferman Festschrift. Available electronically (Abstract, DVI, Postscript).

  7. Karl Crary. Admissibility of fixpoint induction over partial types. Technical Report CMU-CS-98-164, School of Computer Science, Carnegie Mellon University, October 1998. A shorter version of this paper was presented at the International Conference on Automated Deduction, Lindau, Germany, July 1998. Available electronically (Abstract, DVI, Postscript, PDF).

  8. Karl Crary. Simple, efficient object encoding using intersection types. Technical Report CMU-CS-99-100, School of Computer Science, Carnegie Mellon University, January 1999. Available electronically (Abstract, Postscript, PDF).

  9. 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).

  10. Karl Crary, Robert Harper, and Sidd Puri. What is a recursive module? In Proceedings of the Conference on Programming Language Design and Implementation, pages 50-63, Atlanta, Georgia, May 1999. ACM Press. Available electronically (Abstract, DVI, Postscript).

  11. Karl Crary and Joseph C. Vanderwaart. An expressive, scalable type theory for certified code. Technical Report CMU-CS-01-113, School of Computer Science, Carnegie Mellon University, May 2001. Available electronically (Abstract, Postscript, PDF).

  12. Rowan Davies and Frank Pfenning. Intersection types and computational effects. In P. Wadler, editor, Proceedings of the International Conference on Functional Programming, pages 198-208, Montreal, Canada, September 2000. ACM Press. Available electronically.

  13. Joëlle Despeyroux, Frank Pfenning, and Carsten Schürmann. Primitive recursion for higher-order abstract syntax. Technical Report CMU-CS-96-172, School of Computer Science, Carnegie Mellon University, August 1996. Available electronically.

  14. 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).

  15. The ML2000 Working Group. Principles and a preliminary design for ML2000. Unpublished, March 1999. Available electronically (Abstract, Postscript).

  16. Rober Harper. A simplified account of polymorphic references. Information Processing Letters, 51(4):201-206, August 1994. Available electronically (Abstract, DVI, Postscript).

  17. Robert Harper. A simplified account of polymorphic references. Technical Report CMU-CS-93-169, School of Computer Science, Carnegie Mellon University, June 1993. Available electronically (Abstract, DVI, Postscript).

  18. Robert Harper. A note on ``A simplified account of polymorphic references''. Information Processing Letters, 57(1):15-16, January 1996. Available electronically (DVI, Postscript).

  19. Robert Harper, Bruce F. Duba, and David MacQueen. Typing first-class continuations in ML. Journal of Functional Programming, 3(4):465-484, October 1993. Available electronically (DVI, Postscript).

  20. Robert Harper, Peter Lee, Frank Pfenning, and Eugene Rollins. Incremental recompilation for Standard ML of New Jersey. In Proceedings of the ACM SIGPLAN Workshop on ML and its Applications, pages 136-147, Orlando, Florida, June 1994. Proceedings available as INRIA Research Report 2265. Available electronically.

  21. Robert Harper, Peter Lee, Frank Pfenning, and Eugene Rollins. Incremental recompilation for Standard ML of New Jersey. Technical Report CMU-CS-94-116, School of Computer Science, Carnegie Mellon University, February 1994. Available electronically (Abstract, Postscript).

  22. 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).

  23. 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).

  24. 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).

  25. Robert Harper and John C. Mitchell. On the type structure of Standard ML. Transactions on Programming Languages and Systems, 15(2):211-252, April 1993. Earlier version titled ``The Essense of ML'' presented at the Symposium on Principles of Programming Languages, San Diego, California, January, 1988. Available electronically (Abstract, DVI, Postscript).

  26. Robert Harper and John C. Mitchell. Parametricity and variants of girard's J operator. Information Processing Letters, 70(1):1-5, April 1999. 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 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).

  29. 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).

  30. Robin Milner, Mads Tofte, Robert Harper, and David MacQueen. The Definition of Standard ML (Revised). MIT Press, 1997.

  31. Alberto Momigliano and Frank Pfenning. The relative complement problem for higher-order patterns. In D. De Schreye, editor, Proceedings of the International Conference on Logic Programming, pages 380-394, Las Cruces, New Mexico, November 1999. MIT Press. Available electronically.

  32. 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).

  33. Jon G. Riecke and Christopher A. Stone. Privacy via subsumption. Submitted for publication to Information and Computation. Available electronically.

  34. Jon G. Riecke and Christopher A. Stone. Privacy via subsumption. In Informal Proceedings of the Workshop on Foundations of Object-Oriented Languages, San Diego, California, January 1998. Available electronically.

  35. Carsten Schürmann, Jöelle Despeyroux, and Frank Pfenning. Primitive recursion for higher-order abstract syntax. To appear in Theoretical Computer Science.

  36. Frederick Smith, David Walker, and Greg Morrisett. Alias types. In Proceedings of the European Symposium on Programming, pages 366-381, Berlin, Germany, March 2000. Springer-Verlag LNCS 1782. Available electronically (Abstract, Postscript, PDF).

  37. 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.

  38. David Walker and Greg Morrisett. Alias types for recursive data structures. 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).

  39. Hongwei Xi. Dependent Types in Practical Programming. PhD thesis, School of Computer Science, Carnegie Mellon University, December 1998. Available electronically.

  40. 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).

  41. 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.

  42. Hongwei Xi and Frank Pfenning. Eliminating array bound checking through dependent types. In Proceedings of the Conference on Programming Language Design and Implementation, pages 249-257, Montreal, Canada, June 1998. ACM Press. Available electronically (Postscript, PDF).

  43. Hongwei Xi and Frank Pfenning. Dependent types in practical programming (extended abstract). In A. Aiken, editor, Proceedings of the Symposium on Principles of Programming Languages, pages 214-227, San Antonio, Texas, January 1999. Available electronically (Postscript, PDF).

[ 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/