Procs and Locks: A Portable Multiprocessing Platform for Standard ML of New Jersey. - J. Gregory Morrisett; Andrew P. Tolmach (PPoPP, 1993)

Composing First-Class Transactions. - Nicholas Haines; Darrell Kindred; J. Gregory Morrisett; Scott Nettles; Jeannette M. Wing (ACM Trans. Program. Lang. Syst., 1994)

Abstract Models of Memory Management. - J. Gregory Morrisett; Matthias Felleisen; Robert Harper 001 (FPCA, 1995)

Compiling Polymorphism Using Intensional Type Analysis. - Robert Harper 001; J. Gregory Morrisett (POPL, 1995)

TIL: A Type-Directed Optimizing Compiler for ML. - David Tarditi; J. Gregory Morrisett; Perry Cheng; Christopher A. Stone; Robert Harper 001; Peter Lee 001 (PLDI, 1996)

TIL: a type-directed, optimizing compiler for ML (with retrospective) - David Tarditi; J. Gregory Morrisett; Perry Cheng; Christopher A. Stone; Robert Harper 001; Peter Lee 001 (Best of PLDI, 1996)

Typed Closure Conversion. - Yasuhiko Minamide; J. Gregory Morrisett; Robert Harper 001 (POPL, 1996)

Typed Closure Conversion for Recursively-Defined Functions. - J. Gregory Morrisett; Robert Harper 001 (HOOTS, 1997)

Promela++: A Language for Constructing Correct and Efficient Protocols. - Anindya Basu; J. Gregory Morrisett; Thorsten von Eicken (INFOCOM, 1998)

Comparing Mostly-Copying and Mark-Sweep Conservative Collection. - Frederick Smith; J. Gregory Morrisett (ISMM, 1998)

Type Structure for Low-Level Programming Languages. - Karl Crary; J. Gregory Morrisett (ICALP, 1999)

Principals in Programming Languages: A Syntactic Proof Technique. - Steve Zdancewic; Dan Grossman; J. Gregory Morrisett (ICFP, 1999)

Typed Memory Management in a Calculus of Capabilities. - Karl Crary; David Walker 001; J. Gregory Morrisett (POPL, 1999)

Type-Safe Linking and Modular Assembly Language. - Neal Glew; J. Gregory Morrisett (POPL, 1999)

From system F to typed assembly language. - J. Gregory Morrisett; David Walker 001; Karl Crary; Neal Glew (ACM Trans. Program. Lang. Syst., 1999)

Alias Types. - Frederick Smith; David Walker 001; J. Gregory Morrisett (ESOP, 2000)

Scalable Certification for Typed Assembly Language. - Dan Grossman; J. Gregory Morrisett (Types in Compilation, 2000)

Alias Types for Recursive Data Structures. - David Walker 001; J. Gregory Morrisett (Types in Compilation, 2000)

Attacking Malicious Code: A Report to the Infosec Research Council. - Gary McGraw; J. Gregory Morrisett (IEEE Softw., 2000)

Syntactic type abstraction. - Dan Grossman; J. Gregory Morrisett; Steve Zdancewic (ACM Trans. Program. Lang. Syst., 2000)

Typed memory management via static capabilities. - David Walker 001; Karl Crary; J. Gregory Morrisett (ACM Trans. Program. Lang. Syst., 2000)

A Language-Based Approach to Security. - Fred B. Schneider; J. Gregory Morrisett; Robert Harper 001 (Informatics, 2001)

Type Checking Systems Code. - J. Gregory Morrisett (ESOP, 2002)

Analysis issues for cyclone. - J. Gregory Morrisett (PASTE, 2002)

Region-Based Memory Management in Cyclone. - Dan Grossman; J. Gregory Morrisett; Trevor Jim; Michael W. Hicks; Yanling Wang; James Cheney (PLDI, 2002)

Cyclone: A Safe Dialect of C. - Trevor Jim; J. Gregory Morrisett; Dan Grossman; Michael W. Hicks; James Cheney; Yanling Wang (USENIX ATC, General Track, 2002)

Intensional polymorphism in type-erasure semantics. - Karl Crary; Stephanie Weirich; J. Gregory Morrisett (J. Funct. Program., 2002)

Achieving Type Safety for Low-Level Code. - J. Gregory Morrisett (ICLP, 2003)

Stack-based typed assembly language. - J. Gregory Morrisett; Karl Crary; Neal Glew; David Walker 001 (J. Funct. Program., 2003)

Compiling for template-based run-time code generation. - Frederick Smith; Dan Grossman; J. Gregory Morrisett; Luke Hornof; Trevor Jim (J. Funct. Program., 2003)

Experience with safe manual memory-management in cyclone. - Michael W. Hicks; J. Gregory Morrisett; Dan Grossman; Trevor Jim (ISMM, 2004)

Invited talk: what's the future for proof-carrying code? - J. Gregory Morrisett (PEPM, 2004)

Editorial. - Paul Hudak; Greg Morrisett (J. Funct. Program., 2004)

A step-indexed model of substructural state. - Amal J. Ahmed 001; Matthew Fluet; Greg Morrisett (ICFP, 2005)

"Language-Based Security". - Martín Abadi; Greg Morrisett; Andrei Sabelfeld (J. Funct. Program., 2005)

Linear Regions Are All You Need. - Matthew Fluet; Greg Morrisett; Amal J. Ahmed 001 (ESOP, 2006)

Polymorphism and separation in hoare type theory. - Aleksandar Nanevski; Greg Morrisett; Lars Birkedal (ICFP, 2006)

Certified In-lined Reference Monitoring on .NET. - Kevin W. Hamlen; Greg Morrisett; Fred B. Schneider (PLAS, 2006)

Evaluating SFI for a CISC Architecture. - Stephen McCamant; Greg Morrisett (USENIX Security Symposium, 2006)

Monadic regions. - Matthew Fluet; Greg Morrisett (J. Funct. Program., 2006)

Safe manual memory management in Cyclone. - Nikhil Swamy; Michael W. Hicks; Greg Morrisett; Dan Grossman; Trevor Jim (Sci. Comput. Program., 2006)

Computability classes for enforcement mechanisms. - Kevin W. Hamlen; J. Gregory Morrisett; Fred B. Schneider (ACM Trans. Program. Lang. Syst., 2006)

Abstract Predicates and Mutable ADTs in Hoare Type Theory. - Aleksandar Nanevski; Amal Ahmed 001; Greg Morrisett; Lars Birkedal (ESOP, 2007)

The regiment macroprogramming system. - Ryan Newton; Greg Morrisett; Matt Welsh (IPSN, 2007)

Ilea: inter-language analysis across java and c. - Gang Tan; Greg Morrisett (OOPSLA, 2007)

Sensor network programming with Flask. - Geoffrey Mainland; J. Gregory Morrisett; Matt Welsh; Ryan Newton (SenSys, 2007)

L3: A Linear Language with Locations. - Amal Ahmed 001; Matthew Fluet; Greg Morrisett (Fundam. Informaticae, 2007)

08061 Executive Summary – Types, Logics and Semantics for State. - Amal Ahmed 001; Nick Benton; Martin Hofmann 001; Greg Morrisett (Types, Logics and Semantics for State, 2008)

08061 Abstracts Collection – Types, Logics and Semantics for State. - Amal Ahmed 001; Nick Benton; Martin Hofmann 001; Greg Morrisett (Types, Logics and Semantics for State, 2008)

A Realizability Model for Impredicative Hoare Type Theory. - Rasmus Lerchedahl Petersen; Lars Birkedal; Aleksandar Nanevski; Greg Morrisett (ESOP, 2008)

Flask: staged functional programming for sensor networks. - Geoffrey Mainland; Greg Morrisett; Matt Welsh (ICFP, 2008)

Ynot: dependent types for imperative programs. - Aleksandar Nanevski; Greg Morrisett; Avraham Shinnar; Paul Govereau; Lars Birkedal (ICFP, 2008)

Design and evaluation of a compiler for embedded stream programs. - Ryan Newton; Lewis Girod; Michael B. Craig; Samuel Madden 001; J. Gregory Morrisett (LCTES, 2008)

Programming with Effects in Coq. - Greg Morrisett (MPC, 2008)

Hoare type theory, polymorphism and separation. - Aleksandar Nanevski; J. Gregory Morrisett; Lars Birkedal (J. Funct. Program., 2008)

Effective interactive proofs for higher-order imperative programs. - Adam Chlipala; J. Gregory Malecha; Greg Morrisett; Avraham Shinnar; Ryan Wisnesky (ICFP, 2009)

Towards type-theoretic semantics for transactional concurrency. - Aleksandar Nanevski; Paul Govereau; Greg Morrisett (TLDI, 2009)

Technical perspective - A compiler's story. - Greg Morrisett (Commun. ACM, 2009)

Robusta: taming the native beast of the JVM. - Joseph Siefers; Gang Tan; Greg Morrisett (CCS, 2010)

Nikola: embedding compiled GPU functions in Haskell. - Geoffrey Mainland; Greg Morrisett (Haskell, 2010)

Mechanized Verification with Sharing. - J. Gregory Malecha; Greg Morrisett (ICTAC, 2010)

Integrating Types and Specifications for Secure Software Development. - Greg Morrisett (MMM-ACNS, 2010)

Toward a verified relational database management system. - J. Gregory Malecha; Greg Morrisett; Avraham Shinnar; Ryan Wisnesky (POPL, 2010)

Combining control-flow integrity and static analysis for efficient and validated data sandboxing. - Bin Zeng 004; Gang Tan; Greg Morrisett (CCS, 2011)

Evaluating value-graph translation validation for LLVM. - Jean-Baptiste Tristan; Paul Govereau; Greg Morrisett (PLDI, 2011)

Preliminary design of the SAFE platform. - André DeHon; Ben Karel; Thomas F. Knight Jr.; Gregory Malecha; Benoît Montagu; Robin Morisset; Greg Morrisett; Benjamin C. Pierce; Randy Pollack; Sumit Ray; Olin Shivers; Jonathan M. Smith; et al. (PLOS@SOSP, 2011)

Trace-based verification of imperative programs with I/O. - Gregory Malecha; Greg Morrisett; Ryan Wisnesky (J. Symb. Comput., 2011)

Scalable Formal Machine Models. - Greg Morrisett (APLAS, 2012)

RockSalt: better, faster, stronger SFI for the x86. - Greg Morrisett; Gang Tan; Joseph Tassarotti; Jean-Baptiste Tristan; Edward Gan (PLDI, 2012)

Hardware Support for Safety Interlocks and Introspection. - Udit Dhawan; Albert Kwon; Edin Kadric; Catalin Hritcu; Benjamin C. Pierce; Jonathan M. Smith; André DeHon; Gregory Malecha; Greg Morrisett; Thomas F. Knight Jr.; Andrew Sutherland; Tom Hawkins; et al. (SASO Workshops, 2012)

Formalizing the SAFECode Type System. - Daniel Huang 001; Greg Morrisett (CPP, 2013)

Massively Parallel Model of Extended Memory Use in Evolutionary Game Dynamics. - Amanda Peters Randles; David G. Rand; Christopher Lee; Greg Morrisett; Jayanta Sircar; Martin A. Nowak; Hanspeter Pfister (IPDPS, 2013)

All Your IFCException Are Belong to Us. - Catalin Hritcu; Michael Greenberg 002; Ben Karel; Benjamin C. Pierce; Greg Morrisett (IEEE Symposium on Security and Privacy, 2013)

Bringing java's wild native world under control. - Mengtao Sun; Gang Tan; Joseph Siefers; Bin Zeng 004; Greg Morrisett (ACM Trans. Inf. Syst. Secur., 2013)

Type Classes for Lightweight Substructural Types. - Edward Gan; Jesse A. Tov; Greg Morrisett (LINEARITY, 2014)

A Mechanized Proof of Security for Searchable Symmetric Encryption. - Adam Petcher; Greg Morrisett (CSF, 2015)

The Foundational Cryptography Framework. - Adam Petcher; Greg Morrisett (POST, 2015)

An Application of Computable Distributions to the Semantics of Probabilistic Programming Languages. - Daniel Huang 001; Greg Morrisett (ESOP, 2016)

Challenges in compiling Coq. - Greg Morrisett (PPDP, 2016)

Compiling Markov chain Monte Carlo algorithms for probabilistic modeling. - Daniel Huang 001; Jean-Baptiste Tristan; Greg Morrisett (PLDI, 2017)

Revisiting Parametricity: Inductives and Uniformity of Propositions. - Abhishek Anand; Greg Morrisett (CoRR, 2017)

Safety and Security for Intelligent Infrastructure. - Kevin Fu; Ann W. Drobnis; Greg Morrisett; Elizabeth D. Mynatt; Shwetak N. Patel; Radha Poovendran; Benjamin G. Zorn (CoRR, 2017)

A National Research Agenda for Intelligent Infrastructure. - Elizabeth D. Mynatt; Jennifer Clark; Gregory D. Hager; Daniel P. Lopresti; Greg Morrisett; Klara Nahrstedt; George J. Pappas; Shwetak N. Patel; Jennifer Rexford; Helen V. Wright; Benjamin G. Zorn (CoRR, 2017)

An Application of Computable Distributions to the Semantics of Probabilistic Programs. - Daniel Huang 001; Greg Morrisett; Bas Spitters (CoRR, 2018)

Bidirectional Grammars for Machine-Code Decoding and Encoding. - Gang Tan; Greg Morrisett (J. Autom. Reason., 2018)

Evolving Academia/Industry Relations in Computing Research: Interim Report. - Greg Morrisett; Shwetak N. Patel; Jennifer Rexford; Benjamin G. Zorn (CoRR, 2019)

IPDL: A Probabilistic Dataflow Logic for Cryptography. - Xiong Fan; Joshua Gancher; Greg Morrisett; Elaine Shi; Kristina Sojakova (IACR Cryptol. ePrint Arch., 2019)

Application ofComputable Distributions to the Semantics of Probabilistic Programs. - Daniel Huang 001; Greg Morrisett; Bas Spitters (Foundations of Probabilistic Programming, 2020)

IPDL: A Simple Framework for Formally Verifying Distributed Cryptographic Protocols. - Greg Morrisett; Elaine Shi; Kristina Sojakova; Xiong Fan; Joshua Gancher (IACR Cryptol. ePrint Arch., 2021)

Leapfrog: certified equivalence for protocol parsers. - Ryan Doenges; Tobias Kappé; John Sarracino; Nate Foster; Greg Morrisett (PLDI, 2022)

Certified Parsing of Dependent Regular Grammars. - John Sarracino; Gang Tan; Greg Morrisett (SP (Workshops), 2022)

Interval Parsing Grammars for File Format Parsing. - Jialun Zhang; Greg Morrisett; Gang Tan (Proc. ACM Program. Lang., 2023)

A Core Calculus for Equational Proofs of Cryptographic Protocols. - Joshua Gancher; Kristina Sojakova; Xiong Fan; Elaine Shi; Greg Morrisett (Proc. ACM Program. Lang., 2023)