Fox Project Publications

General overviews

• The Fox Project: Advanced Language Technology for Extensible Systems, Robert Harper, Peter Lee, and Frank Pfenning.
  Abstract CMU-CS-98-107 BibTeX

• Advanced Languages for Systems Software: The Fox Project in 1994, Robert Harper and Peter Lee.
  Abstract CMU-CS-94-104 BibTeX

• The Fox Project: Advanced Development of Systems Software, Eric Cooper, Robert Harper, and Peter Lee.
  Abstract CMU-CS-91-187 BibTeX

Recent Papers

• Efficient Representation and Validation of Proofs, George C. Necula and Peter Lee.
  Abstract LICS '98 CMU-CS-97-172

• Run-time Code Generation and Modal-ML, Philip Wickline, Peter Lee, and Frank Pfenning.
  Abstract PLDI '98 CMU-CS-98-100

• The Design and Implementation of a Certifying Compiler, George C. Necula and Peter Lee.
  Abstract PLDI '98

• Generational Stack Collection and Profile-Driven Pretenuring, Perry Cheng, Robert Harper, and Peter Lee.
  Abstract PLDI '98

• Relational Interpretations of Recursive Types in an Operational Setting, Lars Birkedal and Robert Harper.
  CMU-CS-98-125

Systems

• Implementing Bit-addressing with Specialization, Scott Draves.
  Abstract ICFP '97 Hypertext

• Safe-for-Space Threads in Standard ML, Edoardo Biagioni, Ken Cline, Peter Lee, Chris Okasaki, and Chris Stone.
  Abstract CW '97

• Proof-Carrying Code, George C. Necula.
  Abstract POPL '97

• Proof-Carrying Code, George C. Necula and Peter Lee.
  Abstract CMU-CS-96-165

• Safe Kernel Extensions Without Run-Time Checking, George C. Necula and Peter Lee.
  Abstract OSDI '96 HTML Version

• Memory-System Performance of Programs with Intensive Heap Allocation, Amer Diwan, David Tarditi, and Eliot Moss.
  TOCS (Aug. 1995)

• Abstract Models of Memory Management, Greg Morrisett, Matthias Felleisen, and Robert Harper.
  Abstract CMU-CS-95-110 FPCA '95

• Implementing Software Architectures in Standard ML (Position Paper), E. Biagioni, R. Harper, and P. Lee.
  ICSE-17

• Signatures for a Network Protocol Stack: A Systems Application of Standard ML, Edoardo Biagioni, Rober Harper, Peter Lee, and Brian G. Milnes.
  Abstract LFP '94

• Measuring the Cost of Storage Management, David Tarditi and Amer Diwan.
  Abstract CMU-CS-94-201

• Program Verification for Optimized Byte Copy, Edoardo Biagioni.
  Abstract CMU-CS-94-172

• A Structured TCP in Standard ML, Edoardo Biagioni.
  Abstract CMU-CS-94-171 SIGCOMM '94

• Memory Subsystem Performance of Programs with Intensive Heap Allocation, David Tarditi, Amer Diwan, and Eliot Moss.
  CMU-CS-93-227

• Memory Subsystem Performance of Programs Using Copying Garbage Collection, David Tarditi, Amer Diwan, and Eliot Moss.
  CMU-CS-93-210 POPL '93 BibTeX

• Standard ML Signatures for a Protocol Stack, Edoardo Biagioni, Robert Harper, and Peter Lee.
  CMU-CS-93-170

Compilation

• How Generic is a Generic Back End? Using MLRISC as a Back End for the TILT Compiler, Andrew Bernard, Robert Harper, and Peter Lee.
  Second Types in Compilation Workshop, Kyoto, Japan, March, 1998. (To appear.)

• Design and Implementation of Code Optimizations for a Type-Directed Compiler for Standard ML (Ph.D. Dissertation), David Tarditi.
  Abstract CMU-CS-97-108

• TIL: A Type-Directed Optimizing Compiler for ML, D. Tarditi, G. Morrisett, P. Cheng, C. Stone, R. Harper, and P. Lee.
  Abstract CMU-CS-96-108 PLDI '96

• Compiler Generation for Interactive Graphics using Intermediate Code, Scott Draves.
  Abstract LNCS-1110 HTML Version

• The TIL/ML Compiler: Performance and Safety Through Types (Position Paper), G. Morrisett, D. Tarditi, P. Cheng, C. Stone, R. Harper, and P. Lee.
  WCSSS '96

• Optimizing ML with Run-Time Code Generation, Mark Leone and Peter Lee.
  Abstract CMU-CS-95-205 PLDI '96

• Trace-based Program Analysis, Christopher Colby and Peter Lee.
  Abstract CMU-CS-95-179 Slides

• Typed Closure Conversion, Yasuhiko Minamide, Greg Morrisett, and Robert Harper.
  Abstract CMU-CS-95-171 POPL '96

• Lightweight Languages for Interactive Graphics, Scott Draves.
  CMU-CS-95-148 CMU-CS-95-148A

• Lightweight Run-Time Code Generation, Mark Leone and Peter Lee.
  Abstract PEPM '94

• Control-Flow Analysis and Type Systems, Nevin Heintze.
  CMU-CS-94-227

• Compiling Polymorphism Using Intensional Type Analysis, Robert Harper and Greg Morrisett.
  Abstract CMU-CS-94-185 POPL '95

• Compiling with Non-Parametric Polymorphism (Preliminary Report) , Robert Harper and Greg Morrisett.
  CMU-CS-94-122

• Incremental Recompilation for Standard ML of New Jersey, Robert Harper, Peter Lee, Frank Pfenning, and Eugene Rollins.
  Abstract CMU-CS-94-116

• Data Representations and Polymorphic Languages, Greg Morrisett.
  Abstract Thesis Proposal

• Deferred Compilation: The Automation of Run-Time Code Generation, Mark Leone and Peter Lee.
  Abstract CMU-CS-93-225 Hypertext

• Set Based Analysis of Arithmetic Nevin Heintze.
  CMU-CS-93-221

• Set Based Analysis of ML Programs, Nevin Heintze.
  CMU-CS-93-193

• Note on Conditional Compilation in Standard ML, Nicholas Haines, Edoardo Biagioni, Robert Harper, and Brian G. Milnes.
  CMU-CS-93-172

• No Assembly Required: Compiling Standard ML to C, David Tarditi, Peter Lee, and Anurag Acharya.
  Abstract LOPLAS (June 92)

• Procs and Locks: A Portable Multiprocessing Platform for Standard ML of New Jersey, J. Gregory Morrisett and Andrew Tolmach.
  Abstract CMU-CS-92-155 PPOPP '93

• A Modular Implementation of Partial Evaluation, Christopher Colby and Peter Lee.
  Abstract CMU-CS-92-123

• Adding Threads to Standard ML, Eric Cooper and J. Gregory Morrisett.
  Abstract CMU-CS-90-186

Language Design

• An Interpretation of Standard ML in Type Theory, Robert Harper and Chris Stone.
  Supersedes A Type-Theoretic Account of Standard ML 1996 (Version 2)
  CMU-CS-97-147

• A Type-Theroretic Interpretation of Standard ML, Robert Harper and Chris Stone.
  Submitted for publication

• Translucent Sums: A Foundation for Higher-Order Module Systems (Ph.D. Dissertation), Mark Lillibridge.
  Abstract CMU-CS-97-122

• Semantics of Memory Management for Polymorphic Languages, Greg Morrisett and Robert Harper.
  Abstract CMU-CS-96-176

• Sequence Types for Functional Languages, Edoardo Biagioni.
  Abstract, CMU-CS-95-180,

• Exceptions Are Strictly More Powerful Than Call/CC, Mark Lillibridge.
  CMU-CS-95-178

• Call-by-need and Continuation-passing Style, Chris Okasaki, Peter Lee, and David Tarditi.
  Abstract LASC '93

• Refining First-Class Stores, J. Gregory Morrisett.
  Abstract WSPL '93

• A Type-Theoretic Approach to Higher-Order Modules with Sharing, Robert Harper and Mark Lillibridge.
  Abstract CMU-CS-93-197 POPL '94

• A Simplified Account of Polymorphic References, Robert Harper.
  Abstract CMU-CS-93-169 IPL (Aug. 94) IPL (Jan. 96)

• Standard ML Weak Polymorphism Can Be Sound, John Greiner.
  Abstract CMU-CS-93-160R

• Cache Behavior of Combinator Graph Reduction, Philip J. Koopman, Jr., Peter Lee, and Daniel P. Siewiorek.
  TOPLAS (Apr. 92)

• Explicit Polymorphism and CPS Conversion, Robert Harper and Mark Lillibridge.
  Abstract CMU-CS-92-210 POPL '93 JFP

• Polymorphic Type Assignment and CPS Conversion, Robert Harper and Mark Lillibridge.
  Abstract CW '92 LASC (Nov. 93)

• Typing First-Class Continuations in ML, Robert Harper, Bruce F. Duba, and David MacQueen.
  Abstract POPL '91 JFP (Oct. 93)

• Higher Order Modules and the Phase Distinction, Robert Harper, John C. Mitchell, and Eugenio Moggi.
  Abstract CMU-CS-89-197 POPL '90

Dissertations

• Compiling with Proofs, George C. Necula.
  CMU-CS-98-154

• Automatic Program Specialization for Interactive Media, Scott Draves.
  Abstract CMU-CS-97-159 Hypertext BibTeX

• Translucent Sums: A Foundation for Higher-Order Module Systems, Mark Lillibridge.
  Abstract CMU-CS-97-122

• Design and Implementation of Code Optimizations for a Type-Directed Compiler for Standard ML, David Tarditi.
  Abstract CMU-CS-97-108

• Semantics-based Parallel Cost Models and their Use in Provably Efficient Implementations, John Greiner.
  CMU-CS-97-113

• Purely Functional Data Structures, Chris Okasaki.
  CMU-CS-96-177

• Semantics-based Program Analysis via Symbolic Composition of Transfer Relations, Christopher Colby.
  Abstract CMU-CS-96-162

• Compiling with Types, Greg Morrisett.
  CMU-CS-95-226

• Controlling Effects, Andrzej Filinski.
  CMU-CS-96-119

• Set Based Program Analysis, Nevin Heintze.
  CMU-CS-92-201

• Design and Implementation of Practical Constraint Logic Programming Systems, Spiro Michaylov.
  CMU-CS-92-168

Maintained by