Greg Morrisett: links to publications:

Some of this material is based upon work supported by the National Science Foundation under Grant No. 9875536. Any opinions, findings and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the National Science Foundation (NSF).


A Realizability Model for Impredicative Hoare Type Theory.  To appear in European Symposium on Programming (ESOP'08). (pdf).  With R.L.Petersen, L.Birkedal, and A.Nanevski.

Type-Theoretic Semantics for Transactional Concurrency.  (pdf).  Extended version available as technical report TR-09-07, Harvard University, July 2007.  With A.Nanevski, and P.Govereau.

ILEA:  Inter-Language Analysis across Java and C.  To appear in OOPSLA'07 (pdf), with G. Tan.

The Regiment Macroprogramming System.  In International Conference on Information Processing in Sensor Networks (IPSN'07), April 2007.  With R.Newton and M.Welsh. (pdf)

Abstract Predicates and Separation in Hoare Type Theory.  In 16th European Symposium on Programming, March 2007.  With A.Nanevski, A.Ahmed, and L.Birkedal. (pdf)

Polymorphism and Separation in Hoare Type Theory.  To appear in Journal of Functional Programming (pdf).  Longer version of the original conference paper in 2006 International Conference on Functional Programming, October 2006.  (pdf).  Extended version available as Harvard Technical Report TR-10-06, (pdf).  April 2006.  With A. Nanevski and L. Birkedal. 

Evaluating SFI for a CISC Architecture.  This won the "best paper" award in 2006 Usenix Security Symposium.  With S. McCamant. (pdf).

Certified In-lined Reference Monitoring on .NET.  To appear in ACM Workshop on Programming Languages and Analysis for Security(pdf).  An extended version appears as Cornell Computer Science Technical Report TR-2005-2003 (pdf), November 2005.  With K. Hamlen and F.B Schneider.

Dependent Type Theory of Stateful Higher-Order Functions.  Harvard Computer Science Technical Report TR-24-05, with A. Nanevski.   (pdf).

Linear Regions Are All You Need.  Accepted to 2006 European Symposium on Programming, With M. Fluet and A. Ahmed. (pdf).

A Step-Indexed Model of Substructural State.   In 2005 International Conference on Functional Programming, Tallinn, Estonia, pp. 78-91, September 2005.  With A. Ahmed and M. Fluet.  (pdf).

Efficient, Verifiable Sandboxing for a CISC Architecture.  MIT Laboratory for Computer Science Technical Report 988 (MIT-LCS-TR-988). Also MIT Computer Science and Artificial Intelligence Laboratory Technical Report 2005-030 (MIT-CSAIL-TR-2005-030). May 2nd, 2005. With S. McCamant.  [Postscript] [PDF]

L3:  A Linear Language with Locations.  In the Seventh International Conference on Typed Lambda Calculi and Applications, pages 293-307. Springer-Verlag, April 2005, with A. Ahmed and M. Fluet. (pdf).  An extended version appears as Harvard Computer Science Technical Report TR-24-04, July 2004 (pdf).

Cyclone:  A Type-Safe Dialect of CIn C/C++ User's Journal, 23(1), January 2005.  With D.Grossman, M.Hicks, and T.Jim.  (pdf).

Monadic Regions.  In 2004 International Conference on Functional Programming, Park City, Utah, September 2004. With M. Fluet.(pdf).   An extended version is about to appear in JFP. 

Experience with Safe Manual Memory-Management in Cyclone.  In 2004 International Symposium on Memory Management. With M.Hicks, D.Grossman, and T.Jim. (pdf).

Computability Classes for Enforcement Mechanisms.  Cornell Technical Report 2003-1908.  With K. Hamlen and F.B. Schneider. (pdf). A version of this paper is going to appear soon in TOPLAS.

A Linearly Typed Assembly Language.  Cornell Technical Report.  With James Cheney. (pdf).

Compiling for Template-Based Runtime Code Generation. Journal of Functional Programming, 13(3):677-708, May 2003. With F.Smith, D.Grossman, L.Hornoff, and T.Jim. (abstract, pdf, ps).

Retrospective on "TIL:  A Type-Directed, Optimizing Compiler for ML".  To appear in 20 Years of ACM/SIGPLAN Conference on Programming Language Design and Implementation (1979-1999), 2003.  With D. Tarditi, P. Cheng, C. Stone, R. Harper, and P. Lee.  (pdf).

Type-Checking Systems Code.  European Symposium on Programming (invited paper).  (pdf).

Cyclone:  A Safe Dialect of C.  Usenix Annual Technical Conference, Monterey, CA, June 2002.  With T.Jim, D.Grossman, M.Hicks, J.Cheney, and Y.Wang.  A preliminary version is here.

Region-Based Memory Management in Cyclone.  ACM Conference on Programming Language Design and Implementation, Berlin, Germany, June 2002.  With T.Jim, D.Grossman, M.Hicks, J.Cheney, and Y.Wang.   Extended version appears as Cornell University Technical Report TR2001-1856.  

Intensional Polymorphism in Type Erasure SemanticsJournal of Functional Programming, 2002.  With K.Crary and S.Weirich. To Appear.

Syntactic Type Abstraction. In ACM Transactions on Programming Languages and Systems (TOPLAS), 22(6), November 2000, pp. 1037-1080. With D.Grossman and S.Zdancewic.

A language-based approach to security. Informatics: 10 Years Back, 10 Years Ahead, Lecture Notes in Computer Science, Vol. 2000, Springer-Verlag, Heidelberg, 86-101.  With F.B.Schneider and R.Harper. (ps)

Attacking Malicious Code:  A Report to the Infosec Research Council.  In IEEE Software, Volume 17(5), September/October 200.  With G.McGraw.

Alias Types for Recursive Data Structures. In 2000 ACM SIGPLAN Workshop on Types in Compilation, Montreal, Canada, September 2000. With D. Walker.(abstract, pdf, ps.gz)

Scalable Certification for Typed Assembly Language. In 2000 ACM SIGPLAN Workshop on Types in Compilation, Montreal, Canada, September 2000. With D. Grossman. (abstract, pdf, ps)

Alias Types.   In the European Symposium on Programming, Berlin, Germany, March 2000. With F. Smith and D. Walker. (abstract, pdf, ps.gz)

From System F to Typed Assembly Language.  In ACM Transactions on Programming Languages and Systems, 21(3):528-569, May 1999. With D. Walker, K. Crary, and N. Glew.  (abstract, dvi, pdf, ps.gz).  This is the expanded version of a paper that appeared in Twenty-Fifth ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 85-97, San Diego, CA, USA, January 1998. (abstract, dvi, pdf, ps.gz

Principals in Programming Languages: A Syntactic Proof Technique. In the 1999 International Conference on Functional Programming, pages 197-207, Paris, France, September 1999.  With S. Zdancewic and D. Grossman (abstract, dvi, pdf, ps)

TALx86: A Realistic Typed Assembly Language.  In 1999 ACM SIGPLAN Workshop on Compiler Support for System Software, pages 25-35, Atlanta, GA, USA, May 1999. With K. Crary, N. Glew, D. Grossman, R. Samuels, F. Smith, D. Walker, S. Weirich, and S. Zdancewic.  (abstract, dvi, pdf, ps.gz)

Type Structure for Low-Level Programming Languages. 1999 International Colloquium on Automata, Languages, and Programming. With K. Crary. (abstract, postscript, dvi)

Type-Safe Linking and Modular Assembly Language.  In Twenty-Sixth ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 250-261, San Antonio, TX, USA, January 1999. With N. Glew.  (abstract, dvi, pdf, ps.gz)

Typed Memory Management in a Calculus of Capabilities.   In Twenty-Sixth Symposium on Principles of Programming Languages, pages 262-275, San Antonio, TX, USA, January 1999. With K. Crary and D. Walker.  (abstract, dvi, pdf, ps.gz)

Stack-Based Typed Assembly Language. In 1998 Workshop on Types in Compilation, Kyoto, Japan, March 1998. Published in Xavier Leroy and Atsushi Ohori, editors, Lecture Notes in Computer Science, volume 1473, pages 28-52. Springer-Verlag, 1998. With K. Crary, N. Glew, and D. Walker.  (abstract, dvi, pdf, ps.gz)

Comparing Mostly-Copying and Mark-Sweep Conversative Collection.  In  1998 Internataional Symposium on Memory Management, pages 68-78, Vancouver, Canada, October 1998.  With F. Smith. (abstract, pdf, ps.gz)

Intensional Polymorphism in Type-Erasure Semantics. 1998 International Conference on Functional Programming, pages 301-312, Baltimore, September 1998. With K. Crary and S. Weirich.  (abstract, dvi, pdf, ps.gz)

Typed Closure Conversion for Recursively-Defined Functions (Extended Abstract). Proceedings of of Higher-Order Operational Techniques in Semantics (HOOTS) II.  With R. Harper. (ps)

A Language-Based Approach to Protocol Construction, Proceedings of the ACM SIGPLAN Workshop on Domain Specific Languages (WDSL), Paris, France, January 1997.  With A. Basu, M. Hayden, and T. von Eiken. (pdf).  

Semantics of Memory Management for Polymorphic Languages, CMU Technical Report CMU-CS-96-176 [Also appears as CMU-CS-FOX-96-04], September, 1996   With R. Harper. (ps)

Compiling with Types, Ph.D. Thesis, Published as CMU Technical Report CMU-CS-95-226, December, 1995. (ps.zip)

TIL: A Type-Directed Optimizing Compiler for ML. 1996 SIGPLAN Conference on Programming Language Design and Implementation, pages 181-192, Philadelphia, May 1996. With D. Tarditi, P. Cheng, C. Stone, R. Harper, and P. Lee.   (ps)

The TIL/ML Compiler: Performance and Safety Through Types. Workshop on Compiler Support for Systems Software. Tucson, February 1996.   With D. Tarditi, P. Cheng, C. Stone, R. Harper, and P. Lee.  (ps)

Typed Closure Conversion. ACM Symposium on Principles of Programming Languages.  St. Petersburg, pages 271-283, January, 1996.  With Y. Minamide and R. Harper.  (ps).   Extended version published as CMU Technical Report CMU-CS-FOX-95-05 , July 1995

Abstract Models of Memory Management. Conference on Functional Programming Languages and Computer Architecture.  San Diego, pages 66-77, June 1995.  With M. Felleisen and R. Harper.  (ps, dvi).  Extended version published as CMU Technical Report CMU-CS-95-110, (dvi) also as CMU Fox Note CMU-CS-95-01.

Compiling Polymorphism Using Intensional Type Analysis, ACM Symposium on Principles of Programming Languages, San Francisco, pages 130-141, January 1995. With R. Harper.  (ps)

Optimistic Parallelization Greg Morrisett and Maurice Herlihy. CMU-CS-93-171, October 1993.  (ps)

Refining First-Class StoresProceedings of the ACM SIGPLAN Workshop on State in Programming Languages, Copenhagen, Denmark, June 1993. (ps)

Procs and Locks: A Portable Multiprocessing Platform for Standard ML of New Jersey, Proceedings of the Fourth ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, San Diego, May 1993. With A. Tolmach.  (ps)

A Portable Multiprocessing Interface for Standard ML of New Jersey, J. Gregory Morrisett and Andrew Tolmach, CMU-CS-92-155, June 1992. With A. Tolmach.  

Adding Threads to Standard ML, Eric Cooper and J. Gregory Morrisett, CMU-CS-90-186, December 1990. With E. Cooper.  (ps)