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
Publications

This is a bibliography of research papers and reports 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.

Several more specialized bibliographies are available:

  • on Typed Intermediate and Assembly Languages
  • on Proof-Carrying Code
  • on Logical Frameworks
  • on Staged Computation
  • on Language Design
  • on the FoxNet
  • on other topics
    • Currently these are all subsets of this bibliography.

    Last updated: Fri May 4 2001

    Shortcuts: A-B-C-D-E-F-G-H-I-J-K-L-M-N-O-P-Q-R-S-T-U-V-W-X-Y-Z

    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. Edoardo Biagioni. A structured TCP in Standard ML. In Proceedings of the ACM SIGCOMM Conference on Communications Architectures, Protocols and Applications, pages 36-45, London, England, 1994. Available electronically (Abstract, Postscript).

    3. Edoardo Biagioni, Ken Cline, Peter Lee, Chris Okasaki, and Chris Stone. Safe-for-space threads in Standard ML. In Olivier Danvy and Carolyn Talcott, editors, Proceedings of the ACM SIGPLAN Workshop on Continuations, Paris, France, January 1997. Available in special issue of Higher-Order and Symbolic Computation, 11(2):209-225, December 1998. Available electronically (Abstract, Postscript).

    4. Edoardo Biagioni, Robert Harper, and Peter Lee. A network protocol stack in Standard ML. Submitted for publication to Higher-Order and Symbolic Computation. Available electronically (Abstract, PDF).

    5. Edoardo Biagioni, Robert Harper, and Peter Lee. Standard ML signatures for a protocol stack. Technical Report CMU-CS-93-170, School of Computer Science, Carnegie Mellon University, October 1993. Available electronically (Abstract, Postscript).

    6. Edoardo Biagioni, Robert Harper, and Peter Lee. Implementing software architectures in Standard ML (position paper). In Informal Proceedings of the ICSE Workshop on Research Issues in the Intersection of Software Engineering and Programming Languages, Seattle, Washington, April 1995. Available electronically.

    7. Edoardo Biagioni, Robert Harper, Peter Lee, and Brian G. Milnes. Signatures for a network stack: A systems application of Standard ML. In Proceedings of the ACM Conference on LISP and Functional Programming, pages 55-64, Orlando, Florida, June 1994. ACM Press. Available electronically (Abstract, Postscript).

    8. Edoardo S. Biagioni. Program verification for optimized byte copy. Technical Report CMU-CS-94-172, School of Computer Science, Carnegie Mellon University, July 1994. Available electronically (Abstract, Postscript).

    9. Edoardo S. Biagioni. A structured TCP in Standard ML. Technical Report CMU-CS-94-171, School of Computer Science, Carnegie Mellon University, July 1994. Available electronically (Abstract, Postscript).

    10. Edoardo S. Biagioni. Sequence types for functional languages. Technical Report CMU-CS-95-180, School of Computer Science, Carnegie Mellon University, August 1995. Available electronically (Abstract, Postscript).

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

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

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

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

    15. Guy E. Blelloch and Perry Cheng. On bounding time and space for multiprocessor garbage collection. In Proceedings of the Conference on Programming Language Design and Implementation, pages 104-117, Atlanta, Georgia, May 1999. ACM Press. Available electronically (Abstract, Postscript, PDF).

    16. Gerth Stølting Brodal and Chris Okasaki. Optimal purely functional priority queues. Journal of Funtional Programming, 6(6):839-857, November 1996. Available electronically.

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

    18. Iliano Cervesato, Joshua S. Hodas, and Frank Pfenning. Efficient resource management for linear logic proof search. In R. Dyckhoff, H. Herre, and P. Schroeder-Heister, editors, Proceedings of the International Workshop on Extensions of Logic Programming, pages 67-81, Leipzig, Germany, March 1996. Springer-Verlag LNAI 1050. Available electronically.

    19. Iliano Cervesato, Joshua S. Hodas, and Frank Pfenning. Efficient resource management for linear logic proof search. Theoretical Computer Science, 232(1-2):133-163, February 2000. Available electronically.

    20. Iliano Cervesato and Frank Pfenning. Linear higher-order pre-unification. Submitted for publication to the Journal of Symbolic Computation.

    21. Iliano Cervesato and Frank Pfenning. A linear logical framework. Submitted for publication to Information and Computation. Available electronically.

    22. Iliano Cervesato and Frank Pfenning. Linear higher-order pre-unification. In D. Galmiche, editor, Informal Proceedings of the Workshop on Proof Search in Type-Theoretic Language, pages 41-50, New Brunswick, New Jersey, July 1996. Available electronically.

    23. Iliano Cervesato and Frank Pfenning. A linear logical framework. In E. Clarke, editor, Proceedings of the Symposium on Logic in Computer Science, pages 264-275, New Brunswick, New Jersey, July 1996. IEEE Computer Society Press. This work also appeared as Preprint 1834 of the Department of Mathematics of Technical University of Darmstadt, Germany. Available electronically (DVI, Postscript).

    24. Iliano Cervesato and Frank Pfenning. Linear higher-order pre-unification. Technical Report CMU-CS-97-160, School of Computer Science, Carnegie Mellon University, July 1997. Available electronically (Abstract, Postscript).

    25. Iliano Cervesato and Frank Pfenning. Linear higher-order pre-unification. In Glynn Winskel, editor, Proceedings of the Symposium on Logic in Computer Science, pages 422-433, Warsaw, Poland, June 1997. IEEE Computer Society Press. Available electronically (DVI, Postscript).

    26. Iliano Cervesato and Frank Pfenning. A linear spine calculus. Technical Report CMU-CS-97-125, School of Computer Science, Carnegie Mellon University, April 1997. Available electronically (Abstract, Postscript).

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

    28. Christopher Colby. Semantics-based Program Analysis via Symbolic Composition of Transfer Relations. PhD thesis, School of Computer Science, Carnegie Mellon University, August 1996. Available as Technical Report CMU-CS-96-162. Available electronically (Abstract, Postscript).

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

    30. Christopher Colby and Peter Lee. A modular implementation of partial evaluation. Technical Report CMU-CS-92-123, School of Computer Science, Carnegie Mellon University, March 1992. Available electronically (Abstract, Postscript).

    31. Christopher Colby and Peter Lee. Trace-based program analysis. Technical Report CMU-CS-95-179, School of Computer Science, Carnegie Mellon University, July 1995. Available electronically (Abstract, Postscript).

    32. Christopher Colby and Peter Lee. Trace-based program analysis. In Proceedings of the Symposium on Principles of Programming Languages, pages 195-207, St. Petersburg Beach, Florida, January 1996. ACM Press. Available electronically.

    33. Christopher Colby, Peter Lee, George C. Necula, Fred Blau, Mark Plesko, and Kenneth Cline. A certifying compiler for Java. In Proceedings of the Conference on Programming Language Design and Implementation, pages 95-107, Vancouver, Canada, June 2000. ACM Press. Available electronically.

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

    35. Eric Cooper, Robert Harper, and Peter Lee. The Fox project: Advanced development of systems software. Technical Report CMU-CS-91-178, School of Computer Science, Carnegie Mellon University, August 1991. Available electronically (Abstract, Postscript).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    51. Rowan Davies. A temporal logic approach to binding-time analysis. In E. Clarke, editor, Proceedings of the Symposium on Logic in Computer Science, pages 184-195, New Brunswick, New Jersey, July 1996. IEEE Computer Society Press. Available electronically.

    52. Rowan Davies and Frank Pfenning. A modal analysis of staged computation. To appear in the Journal of the ACM.

    53. Rowan Davies and Frank Pfenning. A modal analysis of staged computation. In Hanne Riis Nielson, editor, Informal Proceedings of the Workshop on Types for Program Analysis, Aarhus, Denmark, May 1995. Available electronically.

    54. Rowan Davies and Frank Pfenning. A modal analysis of staged computation. Technical Report CMU-CS-95-145, School of Computer Science, Carnegie Mellon University, May 1995. Available electronically.

    55. Rowan Davies and Frank Pfenning. A modal analysis of staged computation. In Guy Steele, Jr., editor, Proceedings of the Symposium on Principles of Programming Languages, pages 258-270, St. Petersburg Beach, Florida, January 1996. ACM Press. Available electronically.

    56. Rowan Davies and Frank Pfenning. A modal analysis of staged computation. Technical Report CMU-CS-99-153, School of Computer Science, Carnegie Mellon University, August 1999. Available electronically (Abstract, Postscript, PDF).

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

    58. Herb Derby. The performance of FoxNet 2.0. Technical Report CMU-CS-99-137, School of Computer Science, Carnegie Mellon University, June 1999. Available electronically (Abstract, Postscript).

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

    60. Amer Diwan, David Tarditi, and Eliot Moss. Memory subsystem performance of programs using copying garbage collection. Technical Report CMU-CS-93-210, School of Computer Science, Carnegie Mellon University, December 1993. Available electronically.

    61. Amer Diwan, David Tarditi, and Eliot Moss. Memory subsystem performance of programs with intensive heap allocation. Technical Report CMU-CS-93-227, School of Computer Science, Carnegie Mellon University, December 1993. Available electronically.

    62. Amer Diwan, David Tarditi, and Eliot Moss. Memory subsystem performance of programs using copying garbage collection. In Proceedings of the Symposium on Principles of Programming Languages, pages 1-14, Portland, Oregon, January 1994. ACM Press. Available electronically.

    63. Amer Diwan, David Tarditi, and Eliot Moss. Memory-system performance of programs with intensive heap allocation. ACM Transactions on Computer Systems, 13(3):244-273, August 1995. Available electronically.

    64. Scott Draves. Lightweight languages for interactive graphics. Technical Report CMU-CS-95-148, School of Computer Science, Carnegie Mellon University, May 1995. Thesis proposal. Available electronically (Abstract, HTML, Postscript).

    65. Scott Draves. Compiler generation for interactive graphics using intermediate code. In O. Danvy, R. Glück, and P. Thiemann, editors, Proceedings of the International Seminar on Partial Evaluation, Dagstuhl Castle, Germany, February 1996. Springer-Verlag LNCS 1110. Available electronically (Abstract, HTML, Postscript).

    66. Scott Draves. Automatic Program Specialization for Interactive Media. PhD thesis, School of Computer Science, Carnegie Mellon University, July 1997. Available as Technical Report CMU-CS-97-159. Available electronically (Abstract, Postscript, PDF).

    67. Scott Draves. Implementing bit-addressing with specialization. In Proceedings of the International Conference on Functional Programming, pages 239-250, Amsterdam, the Netherlands, June 1997. ACM Press. Available electronically (Abstract, HTML, Postscript).

    68. Scott Draves. Partial evaluation for media processing. ACM Computing Surveys, 30(3es), September 1998. Available electronically.

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

    70. Andrzej Filinski. Controlling Effects. PhD thesis, School of Computer Science, Carnegie Mellon University, May 1996. Available as Technical Report CMU-CS-96-119. Available electronically.

    71. John Greiner. Standard ML weak polymorphism can be sound. Technical Report CMU-CS-93-160R, School of Computer Science, Carnegie Mellon University, September 1993. Available electronically (Abstract, Postscript).

    72. John Greiner. Standard ML weak polymorphism can be sound. Technical Report CMU-CS-93-160, School of Computer Science, Carnegie Mellon University, May 1993. Available electronically.

    73. John Greiner. Semantics-based Parallel Cost Models and their Use in Provably Efficient Implementations. PhD thesis, School of Computer Science, Carnegie Mellon University, April 1997. Available as Technical Report CMU-CS-97-113. Available electronically.

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

    75. Nicholas Haines, Edoardo Biagioni, Robert Harper, and Brian G. Milnes. Note on conditional compilation in Standard ML. Technical Report CMU-CS-93-172, School of Computer Science, Carnegie Mellon University, June 1993. Available electronically (Abstract, Postscript).

    76. Joseph Y. Halpern, Robert Harper, Neil Immerman, Phokion G. Kolaitis, Moshe Y. Vardi, and Victor Vianu. On the unusual effectiveness of logic in computer science. Submitted for publication to the Bulletin of Symbolic Logic. Available electronically (Postscript, PDF).

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

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

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

    80. Robert Harper. Functional pearl: Proof-directed debugging. Journal of Functional Programming, 9(4):463-469, July 1999. Available electronically (Abstract, DVI, Postscript).

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

    82. Robert Harper, Furio Honsell, and Gordon Plotkin. A framework for defining logics. Journal of the ACM, 40(1):143-184, January 1993. Available electronically (Postscript, PDF).

    83. Robert Harper and Peter Lee. Advanced languages for systems software: The Fox project in 1994. Technical Report CMU-CS-94-104, School of Computer Science, Carnegie Mellon University, January 1994. Available electronically (Abstract, Postscript).

    84. Robert Harper, Peter Lee, and Frank Pfenning. The Fox project: Advanced language technology for extensible systems. Technical Report CMU-CS-98-107, School of Computer Science, Carnegie Mellon University, January 1998. Available electronically (Abstract, Postscript).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    100. Robert Harper and Frank Pfenning. A module system for a programming language based on the LF logical framework. Journal of Logic and Computation, 8(1):5-31, February 1998.

    101. Robert Harper and Frank Pfenning. On equivalence and canonical forms in the LF type theory (extended abstract). In Amy Felty, editor, Proceedings of the Workshop on Logical Frameworks and Meta-Languages, Paris, France, September 1999. Available electronically (Abstract, Postscript).

    102. Robert Harper and Frank Pfenning. On equivalence and canonical forms in the LF type theory. Technical Report CMU-CS-99-159, School of Computer Science, Carnegie Mellon University, September 1999. Available electronically (Abstract, Postscript, PDF).

    103. Robert Harper and Frank Pfenning. On equivalence and canonical forms in the LF type theory. Technical Report CMU-CS-00-148, School of Computer Science, Carnegie Mellon University, July 2000. Available electronically (Abstract, Postscript, PDF).

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

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

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

    107. Nevin Heintze. Practical aspects of set-based analysis. In Krzysztof R. Apt, editor, Proceedings of the Joint International Conference and Symposium on Logic Programming, pages 765-779, Washington, DC, November 1992. MIT Press. Available electronically.

    108. Nevin Heintze. Set Based Program Analysis. PhD thesis, School of Computer Science, Carnegie Mellon University, 1992. Available as Technical Report CMU-CS-92-201. Available electronically.

    109. Nevin Heintze. Set based analysis of arithmetic. Technical Report CMU-CS-93-221, School of Computer Science, Carnegie Mellon University, December 1993. Available electronically.

    110. Nevin Heintze. Set based analysis of ML programs (extended abstract). Technical Report CMU-CS-93-193, School of Computer Science, Carnegie Mellon University, July 1993. Available electronically.

    111. Nevin Heintze. Control-flow analysis and type systems. Technical Report CMU-CS-94-227, School of Computer Science, Carnegie Mellon University, December 1994. Available electronically.

    112. Nevin Heintze. Set-based analysis of ML programs (extended abstract). In Proceedings of the ACM Conference on LISP and Functional Programming, pages 306-317, Orlando, Florida, June 1994. ACM Press. Available electronically.

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

    114. Haim Kaplan, Chris Okasaki, and Robert E. Tarjan. Simple confluently persistent catenable lists (extended abstract). In Proceedings of the Scandinavian Workshop on Algorithm Theory, pages 119-130, Stockholm, Sweden, July 1998. Springer-Verlag LNCS 1432. Available electronically.

    115. Philip J. Koopman, Jr., Peter Lee, and Daniel P. Siewiorek. Cache behavior of combinator graph reduction. Transactions on Programming Languages and Systems, 14(2):265-297, April 1992. Available electronically.

    116. Peter Lee and Mark Leone. Optimizing ML with run-time code generation. In Proceedings of the Conference on Programming Language Design and Implementation, pages 137-148, Philadelphia, Pennsylvania, May 1996. ACM Press. Available electronically (Abstract, Postscript).

    117. Mark Leone and Peter Lee. Deferred compilation: The automation of run-time code generation. Technical Report CMU-CS-93-225, School of Computer Science, Carnegie Mellon University, December 1993. Available electronically (Abstract, HTML, Postscript).

    118. Mark Leone and Peter Lee. Lightweight run-time code generation. In Proceedings of the Workshop on Partial Evaluation and Semantics-Based Program Manipulation, pages 97-106, Orlando, Florida, June 1994. Proceedings published as University of Melbourne Department of Computer Science Technical Report 94/9. Available electronically (Abstract, Postscript).

    119. Mark Leone and Peter Lee. Optimizing ML with run-time code generation. Technical Report CMU-CS-95-205, School of Computer Science, Carnegie Mellon University, December 1995. Available electronically (Abstract, Postscript).

    120. Mark Leone and Peter Lee. A declarative approach to run-time code generation. In Informal Proceedings of the Workshop on Compiler Support for Systems Software, Tucson, Arizona, February 1996. Available electronically (Abstract, Postscript).

    121. Mark Leone and Peter Lee. Multi-stage specialization with relative binding times. Technical Report 497, Computer Science Department, Indiana University, November 1997. Available electronically (Abstract, Postscript).

    122. Mark Leone and Peter Lee. Dynamic specialization in the Fabius system. ACM Computing Surveys, 30(3es), September 1998. Available electronically.

    123. Mark Lillibridge. Exceptions are strictly more powerful than call/CC. Technical Report CMU-CS-95-178, School of Computer Science, Carnegie Mellon University, July 1995. Available electronically.

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

    125. Spiro Michaylov. Design and Implementation of Practical Constraint Logic Programming Systems. PhD thesis, School of Computer Science, Carnegie Mellon University, May 1992. Available as Technical Report CMU-CS-92-168.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    141. Greg Morrisett and Maurice Herlihy. Optimistic parallelization. Technical Report CMU-CS-93-171, School of Computer Science, Carnegie Mellon University, October 1993. Available electronically.

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

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

    144. J. Gregory Morrisett. Refining first-class stores. In Paul Hudak, editor, Proceedings of the ACM SIGPLAN Workshop on State in Programming Languages, pages 73-87, Copenhagen, Denmark, June 1993. Proceedings published as Yale Technical Report YALE/DCS/tr968. Available electronically (Abstract, Postscript).

    145. J. Gregory Morrisett and Andrew Tolmach. A portable multiprocessor interface for Standard ML of New Jersey. Technical Report CMU-CS-92-155, School of Computer Science, Carnegie Mellon University, June 1992. Available electronically (Abstract, Postscript).

    146. J. Gregory Morrisett and Andrew Tolmach. Procs and locks: A portable multiprocessing interface for Standard ML of New Jersey. In Proceedings of the Symposium on Principles and Practice of Parallel Programming, pages 198-207, San Diego, California, May 1993. ACM Press. Available electronically (Abstract, Postscript).

    147. George C. Necula. Proof-carrying code. In Neil D. Jones, editor, Proceedings of the Symposium on Principles of Programming Languages, pages 106-119, Paris, France, January 1997. ACM Press. Available electronically (Abstract, Postscript).

    148. George C. Necula. Compiling with Proofs. PhD thesis, Carnegie Mellon University, October 1998. Available as Technical Report CMU-CS-98-154. Available electronically (Abstract, Postscript, PDF).

    149. George C. Necula and Peter Lee. Proof-carrying code. Technical Report CMU-CS-96-165, School of Computer Science, Carnegie Mellon University, September 1996. Available electronically (Abstract, Postscript).

    150. George C. Necula and Peter Lee. Safe kernel extensions without run-time checking. In Proceedings of the Symposium on Operating System Design and Implementation, pages 229-243, Seattle, Washington, October 1996. Available electronically (Abstract, HTML, Postscript).

    151. George C. Necula and Peter Lee. Efficient representation and validation of logical proofs. Technical Report CMU-CS-97-172, School of Computer Science, Carnegie Mellon University, October 1997. Available electronically (Abstract, Postscript).

    152. George C. Necula and Peter Lee. The design and implementation of a certifying compiler. In Keith D. Cooper, editor, Proceedings of the Conference on Programming Language Design and Implementation, pages 333-344, Montreal, Canada, June 1998. ACM Press. Available electronically (Abstract, Postscript).

    153. George C. Necula and Peter Lee. Efficient representation and validation of logical proofs. In Vaughan Pratt, editor, Proceedings of the Symposium on Logic in Computer Science, pages 93-104, Indianapolis, Indiana, June 1998. IEEE Computer Society Press. Available electronically (Abstract, Postscript).

    154. George C. Necula and Peter Lee. Safe, untrusted agents using proof-carrying code. In Giovanni Vigna, editor, Mobile Agents and Security, pages 61-91. Springer-Verlag LNCS 1419, August 1998. Available electronically.

    155. George C. Necula and Peter Lee. Proof generation in the Touchstone theorem prover. In David McAllester, editor, Proceedings of the International Conference on Automated Deduction, pages 25-44, Pittsburgh, Pennsylvania, June 2000. Springer-Verlag LNAI 1831. Available electronically.

    156. Scott Nettles and James O'Toole. Real-time replication garbage collection. In Proceedings of the Conference on Programming Language Design and Implementation, pages 217-226, Albuquerque, New Mexico, June 1993. ACM Press. Available electronically.

    157. Scott Nettles, James O'Toole, and David Gifford. Concurrent garbage collection of persistent heaps. Technical Report CMU-CS-93-137, School of Computer Science, Carnegie Mellon University, April 1993. Available electronically.

    158. Scott Nettles, James O'Toole, David Pierce, and Nicholas Haines. Replication-based incremental copying collection. Technical Report CMU-CS-93-135, School of Computer Science, Carnegie Mellon University, April 1993. Available electronically.

    159. Scott M. Nettles, James W. O'Toole, David Pierce, and Nicholas Haines. Replication-based incremental copying collection. In J. Cohen and Y. Bekkers, editors, Proceedings of the International Workshop on Memory Management, pages 357-364, St. Malo, France, September 1992. Springer-Verlag LNCS 637.

    160. Chris Okasaki. Amortization, lazy evaluation, and persistence: Lists with catenation via lazy linking. In Proceedings of the Symposium on Foundations of Computer Science, pages 646-654, Milwaukee, Wisconsin, October 1995. IEEE. Available electronically (DVI, Postscript).

    161. Chris Okasaki. Purely functional random-access lists. In Proceedings of the International Conference on Functional Programming Languages and Computer Architecture, pages 86-95, La Jolla, California, June 1995. ACM Press. Available electronically (DVI, Postscript).

    162. Chris Okasaki. Simple and efficient purely functional queues and deques. Journal of Functional Programming, 5(4):583-592, October 1995. Available electronically (DVI, Postscript).

    163. Chris Okasaki. Functional data structures. In Proceedings of the International Summer School on Advanced Functional Programming Techniques, pages 131-158. Springer-Verlag LNCS 1129, August 1996. Available electronically (DVI, Postscript).

    164. Chris Okasaki. Purely Functional Data Structures. PhD thesis, School of Computer Science, Carnegie Mellon University, September 1996. Available as Technical Report CMU-CS-96-177. Available electronically.

    165. Chris Okasaki. The role of lazy evaluation in amortized data structures. In Proceedings of the International Conference on Functional Programming, pages 62-72, Philadelphia, Pennsylvania, May 1996. ACM Press. Available electronically (DVI, Postscript).

    166. Chris Okasaki. Catenable double-ended queues. In Proceedings of the International Conference on Functional Programming, pages 66-74, Amsterdam, the Netherlands, June 1997. ACM Press. Available electronically (DVI, Postscript).

    167. Chris Okasaki. Three algorithms on braun trees. Journal of Functional Programming, 7(6):661-666, November 1997. Available electronically (DVI, Postscript).

    168. Chris Okasaki. Even higher-order functions for parsing or why would anyone ever want to use a sixth-order function? Journal of Functional Programming, 8(2):195-199, March 1998. Available electronically (DVI, Postscript).

    169. Chris Okasaki, Peter Lee, and David Tarditi. Call-by-need and continuation-passing style. Lisp and Symbolic Computationj, 7(1):57-82, January 1994. Available electronically (Abstract, DVI, Postscript).

    170. James O'Toole, Scott Nettles, and David Gifford. Concurrent compacting garbage collection of a persistent heap. In Proceedings of the ACM Symposium on Operating Systems Principles, pages 161-174, Asheville, North Carolina, December 1993.

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

    172. Frank Pfenning. Logical frameworks. In press. Chapter 16 of Alan Robinson and Andrei Voronkov, editors, Handbook of Automated Reasoning, to be published by Elsevier Science and MIT Press.

    173. Frank Pfenning. The practice of logical frameworks. In Hélène Kirchner, editor, Proceedings of the Colloquium on Trees in Algebra and Programming, pages 119-134, Linköping, Sweden, April 1996. Springer-Verlag LNCS 1059. Invited talk. Available electronically (DVI, Postscript).

    174. Frank Pfenning. Computation and deduction. Early draft of book to be published by Cambridge University Press, April 1997. Available electronically.

    175. Frank Pfenning. Reasoning about deductions in linear logic. In Claude Kirchner and Hélène Kirchner, editors, Proceedings of the International Conference on Automated Deduction, pages 1-2, Lindau, Germany, July 1998. Springer-Verlag LNCS 1421. Abstract for invited talk. Available electronically.

    176. Frank Pfenning. Logical and meta-logical frameworks. In G. Nadathur, editor, Proceedings of the International Conference on Principles and Practice of Declarative Programming, page 206, Paris, France, September 1999. Springer-Verlag LNCS 1702. Abstract of invited talk. Available electronically.

    177. Frank Pfenning. On the logical foundations of staged computation. In Julia Lawall, editor, Proceedings of the Workshop on Partial Evaluation and Semantics-Based Program Manipulation, page 33, Boston, Massachusetts, January 2000. ACM Press. Abstract of invited talk. Available electronically.

    178. Frank Pfenning. Reasoning about staged computation. In W. Taha, editor, Proceedings of the International Workshop on Semantics, Applications, and Implementation of Program Generation, pages 5-6, Montreal, Canada, September 2000. Springer-Verlag LNCS 1924. Abstract of invited talk. Available electronically.

    179. Frank Pfenning. Structural cut elimination I. intuitionistic and classical logic. Information and Computation, 157(1/2):84-141, March 2000. Available electronically.

    180. Frank Pfenning and Rowan Davies. A judgmental reconstruction of modal logic. To appear in Mathematical Structures in Computer Science. Notes to an invited talk at the Workshop on Intuitionistic Modal Logics and Applications, Trento, Italy, July 1999. Available electronically.

    181. Frank Pfenning and Carsten Schürmann. Algorithms for equality and unification in the presence of notational definitions. In D. Galmiche, editor, Proceedings of the CADE Workshop on Proof Search in Type-Theoretic Languages. Electronic Notes in Theoretical Computer Science, July 1998.

    182. Frank Pfenning and Carsten Schürmann. Algorithms for equality and unification in the presence of notational definitions. In T. Altenkirch, W. Naraschewski, and B. Reus, editors, Proceedings of the Workshop on Types for Proofs and Programs, pages 179-193, Kloster Irsee, Germany, March 1998. Springer-Verlag LNCS 1657. Available electronically.

    183. Frank Pfenning and Carsten Schürmann. Twelf User's Guide, 1.2 edition, September 1998. Available as Technical Report CMU-CS-98-173. Available electronically (Abstract, HTML, Postscript, PDF).

    184. Frank Pfenning and Carsten Schürmann. System description: Twelf - A meta-logical framework for deductive systems. In H. Ganzinger, editor, Proceedings of the International Conference on Automated Deduction, pages 202-206, Trento, Italy, July 1999. Springer-Verlag LNAI 1632. Available electronically.

    185. Brigitte Pientka and Frank Pfenning. Termination and reduction checking in the logical framework. In Carsten Schürmann, editor, Proceedings of the CADE Workshop on Automation of Proofs by Mathematical Induction, Pittsburgh, Pennsylvania, June 2000. Available electronically.

    186. Mark Plesko and Frank Pfenning. A formalization of the proof-carrying code architecture in a linear logical framework. In A. Pnueli and P. Traverso, editors, Proceedings of the FLoC Workshop on Run-Time Result Verification, Trento, Italy, July 1999. Available electronically.

    187. Jeff Polakow and Frank Pfenning. Natural deduction for intuitionistic non-commutative linear logic. In J.-Y. Girard, editor, Proceedings of the International Conference on Typed Lambda Calculi and Applications, pages 295-309, L'Aquila, Italy, April 1999. Springer-Verlag LNCS 1581. Available electronically.

    188. Jeff Polakow and Frank Pfenning. Relating natural deduction and sequent calculus for intuitionistic non-commutative linear logic. In Andre Scedrov and Achim Jung, editors, Proceedings of the Conference on Mathematical Foundations of Programming Semantics, New Orleans, Louisiana, April 1999. Electronic Notes in Theoretical Computer Science, Volume 20. Available electronically.

    189. Jeff Polakow and Frank Pfenning. Properties of terms in continuation-passing style in an ordered logical framework. In Joëlle Despeyroux, editor, Proceedings of the Workshop on Logical Frameworks and Meta-languages, Santa Barbara, California, June 2000. Available electronically.

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

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

    192. Ekkehard Rohwedder and Frank Pfenning. Mode and termination checking for higher-order logic programs. In Hanne Riis Nielson, editor, Proceedings of the European Symposium on Programming, pages 296-310, Linköping, Sweden, April 1996. Springer-Verlag LNCS 1058. Available electronically.

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

    194. Carsten Schürmann. Automating the Meta Theory of Deductive Systems. PhD thesis, Department of Computer Science, Carnegie Mellon University, August 2000. Available as Technical Report CMU-CS-00-146. Available electronically (Abstract, Postscript, PDF).

    195. Carsten Schürmann. A meta logical framework based on realizability. In Joëlle Despeyroux, editor, Proceedings of the Workshop on Logical Frameworks and Meta-Languages, Santa Barbara, California, June 2000. Available electronically.

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

    197. Carsten Schürmann and Frank Pfenning. Automated theorem proving in a simple meta-logic for LF. In Claude Kirchner and Hélène Kirchner, editors, Proceedings of the International Conference on Automated Deduction, pages 286-300, Lindau, Germany, July 1998. Springer-Verlag LNCS 1421. Available electronically.

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

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

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

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

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

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

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

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

    206. David Tarditi and Amer Diwan. The full cost of a generational copying garbage collection implementation. In Eliot Moss, Paul Wilson, and Ben Zorn, editors, Informal Proceedings of the OOPSLA Workshop on Memory Management and Garbage Collection, Washington, USA, September 1993. Available electronically.

    207. David Tarditi and Amer Diwan. Measuring the cost of storage management. Technical Report CMU-CS-94-201, School of Computer Science, Carnegie Mellon University, May 1995. Available electronically (Abstract, Postscript).

    208. David Tarditi and Amer Diwan. Measuring the cost of storage management. Lisp and Symbolic Computation, 9(4):323-342, December 1996. Available electronically.

    209. David Tarditi, Peter Lee, and Anurag Acharya. No assembly required: Compiling ML to C. ACM Letters on Programming Languages and Systems, 1(2):161-177, June 1992. Available electronically (Abstract, Postscript).

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

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

    212. Roberto Virga. Higher-Order Rewriting with Dependent Types. PhD thesis, Department of Mathematical Sciences, Carnegie Mellon University, September 1999. Available as Technical Report CMU-CS-99-167. Available electronically (DVI, Postscript, PDF).

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

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

    215. Philip Wickline, Peter Lee, and Frank Pfenning. Run-time code generation and modal-ML. In Keith D. Cooper, editor, Proceedings of the Conference on Programming Language Design and Implementation, pages 224-235, Montreal, Canada, June 1998. ACM Press. Available electronically (Abstract, Postscript).

    216. Philip Wickline, Peter Lee, and Frank Pfenning. Run-time code generation in modal-ML. Technical Report CMU-CS-98-100, School of Computer Science, Carnegie Mellon University, January 1998. Available electronically (Abstract, Postscript).

    217. Philip Wickline, Peter Lee, Frank Pfenning, and Rowan Davies. Modal types as staging specifications for run-time code generation. ACM Computing Surveys, 30(3es), September 1998. Available electronically (Postscript, PDF).

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

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

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

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

    222. 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/