Greg Morrisett

C. Hritcu, M. Greenberg, B. Karle, B. C. Pierce, and G. Morrisett. All your IFCException are belong to us. In Proceedings of the 34th IEEE Symposium on Security and Privacy (Oakland), May 2013. To appear. [ bib | .pdf ]

A. P. Randles, D. Rand, C. Lee, G. Morrisett, J. Sircar, M. Nowak, and H. Pfister. Massively parallel model of extended memory use in evolutionary game dynamics. In 27th IEEE International Parallel and Distributed Processing Symposium, May 2013. To appear. [ bib ]

U. Dhawan, A. Kwon, E. Kadric, C. Hritcu, B. C. Pierce, J. M. Smith, G. Malecha, G. Morrisett, T. F. Knight, Jr., A. Sutherland, T. Hawkins, A. Zyxnfryx, D. Wittenberg, P. Trei, S. Ray, G. Sullivan, and A. DeHon. Hardware support for safety interlocks and introspection. In SASO Workshop on Adaptive Host and Network Security, Sept. 2012. [ bib | .pdf ]

G. Morrisett, G. Tan, J. Tassarotti, J.-B. Tristan, and E. Gan. Rocksalt: better, faster, stronger sfi for the x86. In Proceedings of the 33rd ACM SIGPLAN conference on Programming Language Design and Implementation, PLDI '12, pages 395-404, New York, NY, USA, 2012. ACM. [ bib | DOI | http | Abstract ]

A. Dehon, B. Karel, B. Montagu, B. Pierce, J. Smith, T. Knight, S. Ray, G. Sullivan, G. Malecha, G. Morrisett, R. Pollack, R. Morisset, and O. Shivers. Preliminary design of the SAFE platform. In Proceedings of the 6th Workshop on Programming Languages and Operating Systems (PLOS 2011). ACM, Oct. 2011. [ bib | Abstract ]

B. Zeng, G. Tan, and G. Morrisett. Combining control-flow integrity and static analysis for efficient and validated data sandboxing. In 18th ACM Conference on Computer and Communications Security. ACM, Oct. 2011. [ bib | Abstract ]

J.-B. Tristan, P. Govereau, and G. Morrisett. Evaluating value-graph translation validation for LLVM. In Proceedings of the ACM SIGPLAN Conference on Programming Design and Implementation (PLDI), New York, NY, USA, 2011. ACM. [ bib | .pdf | Abstract ]

J. Siefers, G. Tan, and G. Morrisett. Robusta: Taming the native beast of the JVM. In 17th ACM Conference on Computer and Communications Security (CCS), New York, NY, USA, Nov. 2010. ACM. [ bib | .pdf | Abstract ]

G. Malecha and G. Morrisett. Mechanized verification with sharing. In 7th International Colloquium on Theoretical Aspects of Computing, Sept. 2010. [ bib | .pdf | Abstract ]

G. Mainland and G. Morrisett. Nikola: Embedding compiled GPU functions in Haskell. In Proceedings of the 2010 ACM SIGPLAN Symposium on Haskell (Haskell'10), New York, NY, USA, Sept. 2010. ACM. [ bib | .pdf | Abstract ]

G. Malecha, G. Morrisett, A. Shinnar, and R. Wisnesky. Toward a verified relational database management system. In POPL '10: Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 237-248, New York, NY, USA, 2010. ACM. [ bib | DOI | .pdf | Abstract ]

A. Chlipala, G. Malecha, G. Morrisett, A. Shinnar, and R. Wisnesky. Effective interactive proofs for higher-order imperative programs. In ICFP '09: Proceedings of the 14th ACM SIGPLAN International Conference on Functional Programming, September 2009. [ bib | .pdf | Abstract ]

R. Wisnesky, G. Malecha, and G. Morrisett. Certified web services in Ynot. In 5th International Workshop on Automated Specification and Verification of Web Systems, July 2009. [ bib | .pdf | Abstract ]

G. Morrisett. Technical perspective a compiler's story. Commun. ACM, 52(7):106-106, 2009. [ bib | DOI ]

A. Nanevski, P. Govereau, and G. Morrisett. Towards type-theoretic semantics for transactional concurrency. In ACM SIGPLAN Workshop on Types in Language Design and Implementation, January 2009. [ bib | .pdf | Abstract ]

G. Mainland, G. Morrisett, and M. Welsh. Flask: Staged functional programming for sensor networks. In ICFP '08: Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming, September 2008. [ bib | .pdf | Abstract ]

A. Nanevski, G. Morrisett, A. Shinnar, P. Govereau, and L. Birkedal. Ynot: Dependent types for imperative programs. In ICFP '08: Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming, September 2008. [ bib | .pdf | Abstract ]

R. L. Petersen, L. Birkedal, A. Nanevski, and G. Morrisett. A realizability model for impredicative Hoare type theory. In 17th European Symposium on Programming, ESOP 2008, volume 4960 of Lecture Notes in Computer Science, pages 337-352. Springer, 2008. [ bib | .pdf | Abstract ]

R. R. Newton, L. D. Girod, M. B. Craig, S. R. Madden, and J. G. Morrisett. Design and evaluation of a compiler for embedded stream programs. In LCTES '08: Proceedings of the 2008 ACM SIGPLAN-SIGBED conference on Languages, compilers, and tools for embedded systems, pages 131-140, New York, NY, USA, 2008. ACM. [ bib | .pdf | Abstract ]

A. Nanevski, P. Govereau, and G. Morrisett. Type-theoretic semantics for transactional concurrency. Technical Report TR-09-07, Harvard University, Cambridge, MA, USA, July 2007. [ bib | .pdf | Abstract ]

A. Nanevski, A. Ahmed, G. Morrisett, and L. Birkedal. Abstract predicates and mutable ADTs in Hoare type theory. In 16th European Symposium on Programming, ESOP 2007, volume 4421 of Lecture Notes in Computer Science, pages 189-204. Springer, 2007. [ bib | .pdf | Abstract ]

G. Mainland, G. Morrisett, M. Welsh, and R. Newton. Sensor network programming with Flask. In SenSys '07: Proceedings of the 5th International Conference on Embedded networked sensor systems, pages 385-386, New York, NY, USA, 2007. ACM. [ bib | Abstract ]

R. Newton, G. Morrisett, and M. Welsh. The Regiment macroprogramming system. In IPSN '07: Proceedings of the 6th International Conference on Information processing in sensor networks, pages 489-498, New York, NY, USA, 2007. ACM. [ bib | .pdf | Abstract ]

G. Tan and G. Morrisett. Ilea: inter-language analysis across Java and C. In OOPSLA '07: Proceedings of the 22nd annual ACM SIGPLAN conference on Object oriented programming systems and applications, pages 39-56, New York, NY, USA, 2007. ACM. [ bib | .pdf | Abstract ]

A. Ahmed, M. Fluet, and G. Morrisett. L3: A linear language with locations. Fundam. Inf., 77(4):397-449, 2007. [ bib | .pdf | Abstract ]

G. Mainland, M. Welsh, and G. Morrisett. Flask: A language for data-driven sensor network programs. Technical Report TR-13-06, Harvard University, May 2006. [ bib | .pdf | Abstract ]

M. Fluet, G. Morrisett, and A. Ahmed. Linear regions are all you need. In ESOP'06: Proceedings of the Fifteenth European Symposium on Programming, pages 7-21. Springer-Verlag, March 2006. [ bib | .pdf | Abstract ]

K. W. Hamlen, G. Morrisett, and F. B. Schneider. Certified in-lined reference monitoring on .NET. In PLAS '06: Proceedings of the 2006 workshop on Programming languages and analysis for security, pages 7-16, New York, NY, USA, 2006. ACM. [ bib | .pdf | Abstract ]

N. Swamy, M. Hicks, G. Morrisett, D. Grossman, and T. Jim. Safe manual memory management in Cyclone. Sci. Comput. Program., 62(2):122-144, 2006. [ bib | Abstract ]

M. Fluet and G. Morrisett. Monadic regions. J. Funct. Program., 16(4-5):485-545, 2006. [ bib | .pdf | Abstract ]

A. Nanevski, G. Morrisett, and L. Birkedal. Polymorphism and separation in Hoare type theory. In ICFP '06: Proceedings of the eleventh ACM SIGPLAN International Conference on Functional programming, pages 62-73, New York, NY, USA, 2006. ACM. [ bib | .pdf | Abstract ]

S. McCamant and G. Morrisett. Evaluating sfi for a cisc architecture. In Proceedings of the 15th conference on USENIX Security Symposium - Volume 15, USENIX-SS'06, Berkeley, CA, USA, 2006. USENIX Association. [ bib | http | .pdf | Abstract ]

K. W. Hamlen, G. Morrisett, and F. B. Schneider. Computability classes for enforcement mechanisms. ACM Trans. Program. Lang. Syst., 28(1):175-205, 2006. [ bib | .pdf | Abstract ]

S. McCamant and G. Morrisett. Efficient, verifiable sandboxing for a CISC architecture. Technical Report MIT-LCS-TR-988, MIT Laboratory for Computer Science, Cambridge, MA, USA, May 2005. [ bib | .pdf | Abstract ]

A. Nanevski and G. Morrisett. Dependent type theory of stateful higher-order functions. Technical Report TR-24-05, Harvard University, Cambridge, MA, USA, January 2005. [ bib | .pdf | Abstract ]

D. Grossman, M. Hicks, T. Jim, and G. Morrisett. Cyclone: A type-safe dialect of C. C/C++ User's Journal, 23(1), January 2005. [ bib | .pdf ]

A. Ahmed, M. Fluet, and G. Morrisett. A step-indexed model of substructural state. In ICFP '05: Proceedings of the tenth ACM SIGPLAN International Conference on Functional programming, pages 78-91, New York, NY, USA, 2005. ACM. [ bib | .pdf | Abstract ]

M. Abadi, G. Morrisett, and A. Sabelfeld. “language-based security”. J. Funct. Program., 15(2):129-129, 2005. [ bib | Abstract ]

M. Hicks, G. Morrisett, D. Grossman, and T. Jim. Experience with safe manual memory-management in Cyclone. In ISMM '04: Proceedings of the 4th international symposium on Memory management, pages 73-84, New York, NY, USA, 2004. ACM. [ bib | .pdf | Abstract ]

M. Fluet and G. Morrisett. Monadic regions. In ICFP '04: Proceedings of the ninth ACM SIGPLAN International Conference on Functional programming, pages 103-114, New York, NY, USA, 2004. ACM. [ bib | .pdf | Abstract ]

G. Morrisett. Invited talk: what's the future for proof-carrying code? In PPDP '04: Proceedings of the 6th ACM SIGPLAN International Conference on Principles and practice of declarative programming, pages 5-5, New York, NY, USA, 2004. ACM. [ bib | Abstract ]

J. Cheney and G. Morrisett. A linearly typed assembly language. Technical report, Cornell University, Ithaca, NY, USA, February 2003. [ bib | .pdf | Abstract ]

F. Smith, D. Grossman, G. Morrisett, L. Hornof, and T. Jim. Compiling for template-based run-time code generation. J. Funct. Program., 13(3):677-708, 2003. [ bib | .pdf | Abstract ]

K. Crary, S. Weirich, and G. Morrisett. Intensional polymorphism in type-erasure semantics. J. Funct. Program., 12(6):567-600, 2002. [ bib | Abstract ]

G. Morrisett, K. Crary, N. Glew, and D. Walker. Stack-based typed assembly language. J. Funct. Program., 12(1):43-88, 2002. [ bib | Abstract ]

D. Grossman, G. Morrisett, T. Jim, M. Hicks, Y. Wang, and J. Cheney. Region-based memory management in Cyclone. In PLDI '02: Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, pages 282-293, New York, NY, USA, 2002. ACM. [ bib | .pdf | Abstract ]

G. Morrisett. Analysis issues for cyclone. In PASTE '02: Proceedings of the 2002 ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering, pages 26-26, New York, NY, USA, 2002. ACM. [ bib | Abstract ]

J. G. Morrisett. Type checking systems code. In ESOP '02: Proceedings of the 11th European Symposium on Programming Languages and Systems, pages 1-5, London, UK, 2002. Springer-Verlag. [ bib | .pdf | Abstract ]

T. Jim, J. G. Morrisett, D. Grossman, M. W. Hicks, J. Cheney, and Y. Wang. Cyclone: A safe dialect of C. In ATEC '02: Proceedings of the General Track of the annual conference on USENIX Annual Technical Conference, pages 275-288, Berkeley, CA, USA, 2002. USENIX Association. [ bib | .pdf | Abstract ]

D. Walker and J. G. Morrisett. Alias types for recursive data structures. In TIC '00: Selected papers from the Third International Workshop on Types in Compilation, pages 177-206, London, UK, 2001. Springer-Verlag. [ bib | .pdf | Abstract ]

F. B. Schneider, J. G. Morrisett, and R. Harper. A language-based approach to security. In Informatics - 10 Years Back. 10 Years Ahead., pages 86-101, London, UK, 2001. Springer-Verlag. [ bib | .ps | Abstract ]

D. Grossman and J. G. Morrisett. Scalable certification for typed assembly language. In TIC '00: Selected papers from the Third International Workshop on Types in Compilation, pages 117-146, London, UK, 2001. Springer-Verlag. [ bib | .pdf | Abstract ]

D. Grossman, G. Morrisett, T. Jim, M. Hicks, Y. Wang, and J. Cheney. Formal type soundness for Cyclone's region system. Technical report, Cornell University, Ithaca, NY, USA, 2001. [ bib | Abstract ]

D. Grossman, G. Morrisett, T. Jim, M. Hicks, Y. Wang, and J. Cheney. Cyclone user's manual, version 0.1.3. Technical report, Cornell University, Ithaca, NY, USA, 2001. [ bib ]

D. Walker, K. Crary, and G. Morrisett. Typed memory management via static capabilities. ACM Trans. Program. Lang. Syst., 22(4):701-771, 2000. [ bib | Abstract ]

F. Smith, D. Walker, and J. G. Morrisett. Alias types. In ESOP '00: Proceedings of the 9th European Symposium on Programming Languages and Systems, pages 366-381, London, UK, 2000. Springer-Verlag. [ bib | .pdf | Abstract ]

D. Grossman, G. Morrisett, and S. Zdancewic. Syntactic type abstraction. ACM Trans. Program. Lang. Syst., 22(6):1037-1080, 2000. [ bib | .pdf | Abstract ]

G. McGraw and G. Morrisett. Attacking malicious code: A report to the infosec research council. IEEE Softw., 17(5):33-41, 2000. [ bib | Abstract ]

D. Grossman and G. Morrisett. Scalable certification of native code: Experience from compiling to TALx86. Technical report, Cornell University, Ithaca, NY, USA, 2000. [ bib | Abstract ]

F. Smith, D. Grossman, G. Morrisett, L. Hornof, and T. Jim. Compiling for runtime code generation (extended version). Technical report, Cornell University, Ithaca, NY, USA, 2000. [ bib | Abstract ]

D. Walker and G. Morrisett. Alias types for recursive data structures (extended version). Technical report, Cornell University, Ithaca, NY, USA, 2000. [ bib | Abstract ]

D. Walker, K. Crary, and G. Morrisett. Typed memory management in a calculus of capabilities. Technical report, Cornell University, Ithaca, NY, USA, 2000. [ bib | Abstract ]

F. Schneider, G. Morrisett, and R. Harper. A language-based approach to security. Technical report, Cornell University, Ithaca, NY, USA, 2000. [ bib | Abstract ]

G. Morrisett, K. Crary, N. Glew, D. Grossman, R. Samuels, F. Smith, D. Walker, S. Weirich, and S. Zdancewic. Talx86: A realistic typed assembly language. In In Second Workshop on Compiler Support for System Software, pages 25-35, 1999. [ bib | .pdf | Abstract ]

G. Morrisett, D. Walker, K. Crary, and N. Glew. From System F to typed assembly language. ACM Trans. Program. Lang. Syst., 21(3):527-568, 1999. [ bib | .pdf | Abstract ]

K. Crary, D. Walker, and G. Morrisett. Typed memory management in a calculus of capabilities. In POPL '99: Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 262-275, New York, NY, USA, 1999. ACM. [ bib | .pdf | Abstract ]

K. Crary and J. G. Morrisett. Type structure for low-level programming languages. In ICAL '99: Proceedings of the 26th International Colloquium on Automata, Languages and Programming, pages 40-54, London, UK, 1999. Springer-Verlag. [ bib ]

N. Glew and G. Morrisett. Type-safe linking and modular assembly language. In POPL '99: Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 250-261, New York, NY, USA, 1999. ACM. [ bib | .pdf | Abstract ]

S. Zdancewic, D. Grossman, and G. Morrisett. Principals in programming languages: a syntactic proof technique. In ICFP '99: Proceedings of the fourth ACM SIGPLAN International Conference on Functional programming, pages 197-207, New York, NY, USA, 1999. ACM. [ bib | .pdf | Abstract ]

F. Smith, D. Walker, and G. Morrisett. Alias types. Technical report, Cornell University, Ithaca, NY, USA, 1999. [ bib ]

G. Morrisett and R. Harper. Typed closure conversion for recursively-defined functions (extended abstract). In C. Talcott, editor, Higher-Order Techniques in Operational Semantics, volume 10 of Electronic Notes in Theoretical Computer Science. Elsevier, 1998. [ bib | .ps ]

K. Crary, S. Weirich, and G. Morrisett. Intensional polymorphism in type-erasure semantics. In ICFP '98: Proceedings of the third ACM SIGPLAN International Conference on Functional programming, pages 301-312, New York, NY, USA, 1998. ACM. [ bib | .pdf | Abstract ]

G. Morrisett, D. Walker, K. Crary, and N. Glew. From System F to typed assembly language. In POPL '98: Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 85-97, New York, NY, USA, 1998. ACM. [ bib | .pdf | Abstract ]

F. Smith and G. Morrisett. Comparing mostly-copying and mark-sweep conservative collection. In ISMM '98: Proceedings of the 1st international symposium on Memory management, pages 68-78, New York, NY, USA, 1998. ACM. [ bib | .pdf | Abstract ]

J. G. Morrisett, K. Crary, N. Glew, and D. Walker. Stack-based typed assembly language. In TIC '98: Proceedings of the Second International Workshop on Types in Compilation, pages 28-52, London, UK, 1998. Springer-Verlag. [ bib | .pdf | Abstract ]

K. Crary, S. Weirich, and G. Morrisett. Intensional polymorphism in type-erasure semantics. Technical report, Cornell University, Ithaca, NY, USA, 1998. [ bib | Abstract ]

G. Morrisett and R. Harper. Semantics of memory management for polymorphic languages. In Higher-Order Operational Techniques in Semantics, Electronic Notes in Theoretical Computer Science, pages 175-226, New York, NY, USA, 1998. Cambridge University Press. [ bib | .ps | Abstract ]

A. Basu, M. Hayden, G. Morrisett, and T. Eicken. A language-based approach to protocol construction. In In Proc. of the ACM SIGPLAN Workshop on Domain Specific Languages (WDSL, pages 87-99, 1997. [ bib | .pdf | Abstract ]

F. Smith and G. Morrisett. Mostly-copying collection: A viable alternative to conservative mark-sweep. Technical report, Cornell University, Ithaca, NY, USA, 1997. [ bib | Abstract ]

G. Morrisett, D. Walker, K. Crary, and N. Glew. From System F to typed assembly language (extended version). Technical report, Cornell University, Ithaca, NY, USA, 1997. [ bib | Abstract ]

G. Morrisett, D. Tarditi, P. Cheng, C. Stone, R. Harper, and P. Lee. The til/ml compiler: Performance and safety through types. In In Workshop on Compiler Support for Systems Software, Tucscon, AZ, USA, 1996. [ bib | .ps | Abstract ]

Y. Minamide, G. Morrisett, and R. Harper. Typed closure conversion. In POPL '96: Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 271-283, New York, NY, USA, 1996. ACM. [ bib | .ps | Abstract ]

D. Tarditi, G. Morrisett, P. Cheng, C. Stone, R. Harper, and P. Lee. Til: a type-directed optimizing compiler for ml. In PLDI '96: Proceedings of the ACM SIGPLAN 1996 conference on Programming language design and implementation, pages 181-192, New York, NY, USA, 1996. ACM. [ bib | .ps ]

G. Morrisett. Compiling with Types. PhD thesis, Carnegie Mellon University, December 1995. [ bib | http | Abstract ]

G. Morrisett, M. Felleisen, and R. Harper. Abstract models of memory management. In FPCA '95: Proceedings of the seventh International Conference on Functional programming languages and computer architecture, pages 66-77, New York, NY, USA, 1995. ACM. [ bib | .ps ]

R. Harper and G. Morrisett. Compiling polymorphism using intensional type analysis. In POPL '95: Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 130-141, New York, NY, USA, 1995. ACM. [ bib | .ps | Abstract ]

N. Haines, D. Kindred, J. G. Morrisett, S. M. Nettles, and J. M. Wing. Composing first-class transactions. ACM Trans. Program. Lang. Syst., 16(6):1719-1736, 1994. [ bib ]

R. Harper and G. Morrisett. Compiling with non-parametric polymorphism (preliminary report). Technical report, Carnegie Mellon University, Pittsburgh, PA, USA, 1994. [ bib | Abstract ]

R. Harper and G. Morrisett. Compiling polymorphism using intensional type analysis. Technical report, Carnegie Mellon University, Pittsburgh, PA, USA, 1994. [ bib | Abstract ]

G. Morrisett and M. Herlihy. Optimistic parallelization. Technical report, Carnegie Mellon University, Pittsburgh, PA, USA, October 1993. [ bib | .ps ]

J. G. Morrisett. Refining first-class stores. In In Proceedings of the ACM SIGPLAN Workshop on State in Programming Languages, pages 73-87, 1993. [ bib | .ps ]

J. G. Morrisett and A. Tolmach. Procs and locks: a portable multiprocessing platform for standard ml of new jersey. In PPOPP '93: Proceedings of the fourth ACM SIGPLAN symposium on Principles and practice of parallel programming, pages 198-207, New York, NY, USA, 1993. ACM. [ bib | .ps | Abstract ]

J. M. Wing, M. Faehndrich, N. Haines, K. Kietzke, D. Kindred, J. G. Morrisett, and S. Nettles. Venari/ML interfaces and examples. Technical report, Carnegie Mellon University, Pittsburgh, PA, USA, 1993. [ bib ]

N. Haines, D. Kindred, J. G. Morrisett, S. M. Nettles, and J. M. Wing. Tinkertoy transactions. Technical report, Carnegie Mellon University, Pittsburgh, PA, USA, 1993. [ bib | Abstract ]

J. M. Wing, M. Faehndrich, J. G. Morrisett, and S. Nettles. Extensions to Standard ML to support transactions. Technical report, Carnegie Mellon University, Pittsburgh, PA, USA, 1992. [ bib ]

J. G. Morrisett and A. Tolmach. A portable multiprocessor interface for standard ml of new jersey. Technical report, Carnegie Mellon University, Pittsburgh, PA, USA, 1992. [ bib ]

E. Cooper and J. G. Morrisett. Adding threads to Standard ML. Technical Report CMU-CS-90-186, Carnegie Mellon University, Pittsburgh, PA, USA, December 1990. [ bib | .ps ]

---

This file was generated by bibtex2html 1.96.