J. Gregory Morrisett

According to our database, J. Gregory Morrisett authored at least 92 papers between 1993 and 2023.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of four.

2023

A Core Calculus for Equational Proofs of Cryptographic Protocols.

Joshua Gancher, Kristina Sojakova, Xiong Fan, Elaine Shi, Greg Morrisett

Proc. ACM Program. Lang., January, 2023

Interval Parsing Grammars for File Format Parsing.

Jialun Zhang, Greg Morrisett, Gang Tan

Proc. ACM Program. Lang., 2023

2022

Certified Parsing of Dependent Regular Grammars.

John Sarracino, Gang Tan, Greg Morrisett

Proceedings of the 43rd IEEE Security and Privacy, 2022

Leapfrog: certified equivalence for protocol parsers.

Ryan Doenges, Tobias Kappé, John Sarracino, Nate Foster, Greg Morrisett

Proceedings of the PLDI '22: 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, San Diego, CA, USA, June 13, 2022

2021

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

2019

IPDL: A Probabilistic Dataflow Logic for Cryptography.

Xiong Fan, Joshua Gancher, Greg Morrisett, Elaine Shi, Kristina Sojakova

IACR Cryptol. ePrint Arch., 2019

Evolving Academia/Industry Relations in Computing Research: Interim Report.

Greg Morrisett, Shwetak N. Patel, Jennifer Rexford, Benjamin G. Zorn

CoRR, 2019

2018

Bidirectional Grammars for Machine-Code Decoding and Encoding.

Gang Tan, Greg Morrisett

J. Autom. Reason., 2018

An Application of Computable Distributions to the Semantics of Probabilistic Programs.

Daniel Huang, Greg Morrisett, Bas Spitters

CoRR, 2018

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

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

Revisiting Parametricity: Inductives and Uniformity of Propositions.

Abhishek Anand, Greg Morrisett

CoRR, 2017

Compiling Markov chain Monte Carlo algorithms for probabilistic modeling.

Daniel Huang, Jean-Baptiste Tristan, Greg Morrisett

Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2017

2016

Challenges in compiling Coq.

Greg Morrisett

Proceedings of the 18th International Symposium on Principles and Practice of Declarative Programming, 2016

An Application of Computable Distributions to the Semantics of Probabilistic Programming Languages.

Daniel Huang, Greg Morrisett

Proceedings of the Programming Languages and Systems, 2016

2015

The Foundational Cryptography Framework.

Adam Petcher, Greg Morrisett

Proceedings of the Principles of Security and Trust - 4th International Conference, 2015

A Mechanized Proof of Security for Searchable Symmetric Encryption.

Adam Petcher, Greg Morrisett

Proceedings of the IEEE 28th Computer Security Foundations Symposium, 2015

2014

Type Classes for Lightweight Substructural Types.

Edward Gan, Jesse A. Tov, Greg Morrisett

Proceedings of the Proceedings Third International Workshop on Linearity, 2014

2013

Bringing java's wild native world under control.

Mengtao Sun, Gang Tan, Joseph Siefers, Bin Zeng, Greg Morrisett

ACM Trans. Inf. Syst. Secur., 2013

All Your IFCException Are Belong to Us.

Catalin Hritcu, Michael Greenberg, Ben Karel, Benjamin C. Pierce, Greg Morrisett

Proceedings of the 2013 IEEE Symposium on Security and Privacy, 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

Proceedings of the 27th IEEE International Symposium on Parallel and Distributed Processing, 2013

Formalizing the SAFECode Type System.

Daniel Huang, Greg Morrisett

Proceedings of the Certified Programs and Proofs - Third International Conference, 2013

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, Amanda Zyxnfryx, David K. Wittenberg, Peter Trei, Sumit Ray, Greg Sullivan

Proceedings of the Sixth IEEE International Conference on Self-Adaptive and Self-Organizing Systems Workshops, 2012

RockSalt: better, faster, stronger SFI for the x86.

Greg Morrisett, Gang Tan, Joseph Tassarotti, Jean-Baptiste Tristan, Edward Gan

Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, 2012

Scalable Formal Machine Models.

Greg Morrisett

Proceedings of the Programming Languages and Systems - 10th Asian Symposium, 2012

2011

Trace-based verification of imperative programs with I/O.

Gregory Malecha, Greg Morrisett, Ryan Wisnesky

J. Symb. Comput., 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, Gregory Sullivan

Proceedings of the 6th Workshop on Programming Languages and Operating Systems, 2011

Evaluating value-graph translation validation for LLVM.

Jean-Baptiste Tristan, Paul Govereau, Greg Morrisett

Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, 2011

Combining control-flow integrity and static analysis for efficient and validated data sandboxing.

Bin Zeng, Gang Tan, Greg Morrisett

Proceedings of the 18th ACM Conference on Computer and Communications Security, 2011

2010

Toward a verified relational database management system.

J. Gregory Malecha, Greg Morrisett, Avraham Shinnar, Ryan Wisnesky

Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2010

Integrating Types and Specifications for Secure Software Development.

Greg Morrisett

Proceedings of the Computer Network Security, 2010

Mechanized Verification with Sharing.

J. Gregory Malecha, Greg Morrisett

Proceedings of the Theoretical Aspects of Computing, 2010

Nikola: embedding compiled GPU functions in Haskell.

Geoffrey Mainland, Greg Morrisett

Proceedings of the 3rd ACM SIGPLAN Symposium on Haskell, 2010

Robusta: taming the native beast of the JVM.

Joseph Siefers, Gang Tan, Greg Morrisett

Proceedings of the 17th ACM Conference on Computer and Communications Security, 2010

2009

Technical perspective - A compiler's story.

Greg Morrisett

Commun. ACM, 2009

Towards type-theoretic semantics for transactional concurrency.

Aleksandar Nanevski, Paul Govereau, Greg Morrisett

Proceedings of TLDI'09: 2009 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, 2009

Effective interactive proofs for higher-order imperative programs.

Adam Chlipala, J. Gregory Malecha, Greg Morrisett, Avraham Shinnar, Ryan Wisnesky

Proceedings of the Proceeding of the 14th ACM SIGPLAN international conference on Functional programming, 2009

2008

Hoare type theory, polymorphism and separation.

Aleksandar Nanevski, J. Gregory Morrisett, Lars Birkedal

J. Funct. Program., 2008

Programming with Effects in Coq.

Greg Morrisett

Proceedings of the Mathematics of Program Construction, 9th International Conference, 2008

Design and evaluation of a compiler for embedded stream programs.

Ryan Newton, Lewis Girod, Michael B. Craig, Samuel Madden, J. Gregory Morrisett

Proceedings of the 2008 ACM SIGPLAN/SIGBED Conference on Languages, 2008

Ynot: dependent types for imperative programs.

Aleksandar Nanevski, Greg Morrisett, Avraham Shinnar, Paul Govereau, Lars Birkedal

Proceedings of the Proceeding of the 13th ACM SIGPLAN international conference on Functional programming, 2008

Flask: staged functional programming for sensor networks.

Geoffrey Mainland, Greg Morrisett, Matt Welsh

Proceedings of the Proceeding of the 13th ACM SIGPLAN international conference on Functional programming, 2008

A Realizability Model for Impredicative Hoare Type Theory.

Rasmus Lerchedahl Petersen, Lars Birkedal, Aleksandar Nanevski, Greg Morrisett

Proceedings of the Programming Languages and Systems, 2008

08061 Abstracts Collection -- Types, Logics and Semantics for State.

Amal Ahmed, Nick Benton, Martin Hofmann, Greg Morrisett

Proceedings of the Types, Logics and Semantics for State, 03.02. - 08.02.2008, 2008

08061 Executive Summary -- Types, Logics and Semantics for State.

Amal Ahmed, Nick Benton, Martin Hofmann, Greg Morrisett

Proceedings of the Types, Logics and Semantics for State, 03.02. - 08.02.2008, 2008

2007

L³: A Linear Language with Locations.

Amal Ahmed, Matthew Fluet, Greg Morrisett

Fundam. Informaticae, 2007

Sensor network programming with Flask.

Geoffrey Mainland, J. Gregory Morrisett, Matt Welsh, Ryan Newton

Proceedings of the 5th International Conference on Embedded Networked Sensor Systems, 2007

Ilea: inter-language analysis across java and c.

Gang Tan, Greg Morrisett

Proceedings of the 22nd Annual ACM SIGPLAN Conference on Object-Oriented Programming, 2007

The regiment macroprogramming system.

Ryan Newton, Greg Morrisett, Matt Welsh

Proceedings of the 6th International Conference on Information Processing in Sensor Networks, 2007

Abstract Predicates and Mutable ADTs in Hoare Type Theory.

Aleksandar Nanevski, Amal Ahmed, Greg Morrisett, Lars Birkedal

Proceedings of the Programming Languages and Systems, 2007

2006

Computability classes for enforcement mechanisms.

Kevin W. Hamlen, J. Gregory Morrisett, Fred B. Schneider

ACM Trans. Program. Lang. Syst., 2006

Safe manual memory management in Cyclone.

Nikhil Swamy, Michael W. Hicks, Greg Morrisett, Dan Grossman, Trevor Jim

Sci. Comput. Program., 2006

Monadic regions.

Matthew Fluet, Greg Morrisett

J. Funct. Program., 2006

Evaluating SFI for a CISC Architecture.

Stephen McCamant, Greg Morrisett

Proceedings of the 15th USENIX Security Symposium, Vancouver, BC, Canada, July 31, 2006

Certified In-lined Reference Monitoring on .NET.

Kevin W. Hamlen, Greg Morrisett, Fred B. Schneider

Proceedings of the 2006 Workshop on Programming Languages and Analysis for Security, 2006

Polymorphism and separation in hoare type theory.

Aleksandar Nanevski, Greg Morrisett, Lars Birkedal

Proceedings of the 11th ACM SIGPLAN International Conference on Functional Programming, 2006

Linear Regions Are All You Need.

Matthew Fluet, Greg Morrisett, Amal J. Ahmed

Proceedings of the Programming Languages and Systems, 2006

2005

"Language-Based Security".

Martín Abadi, Greg Morrisett, Andrei Sabelfeld

J. Funct. Program., 2005

A step-indexed model of substructural state.

Amal J. Ahmed, Matthew Fluet, Greg Morrisett

Proceedings of the 10th ACM SIGPLAN International Conference on Functional Programming, 2005

2004

Editorial.

Paul Hudak, Greg Morrisett

J. Funct. Program., 2004

Invited talk: what's the future for proof-carrying code?

J. Gregory Morrisett

Proceedings of the 2004 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-based Program Manipulation, 2004

Experience with safe manual memory-management in cyclone.

Michael W. Hicks, J. Gregory Morrisett, Dan Grossman, Trevor Jim

Proceedings of the 4th International Symposium on Memory Management, 2004

2003

Compiling for template-based run-time code generation.

Frederick Smith, Dan Grossman, J. Gregory Morrisett, Luke Hornof, Trevor Jim

J. Funct. Program., 2003

Stack-based typed assembly language.

J. Gregory Morrisett, Karl Crary, Neal Glew, David Walker

J. Funct. Program., 2003

Achieving Type Safety for Low-Level Code.

J. Gregory Morrisett

Proceedings of the Logic Programming, 19th International Conference, 2003

2002

Intensional polymorphism in type-erasure semantics.

Karl Crary, Stephanie Weirich, J. Gregory Morrisett

J. Funct. Program., 2002

Cyclone: A Safe Dialect of C.

Trevor Jim, J. Gregory Morrisett, Dan Grossman, Michael W. Hicks, James Cheney, Yanling Wang

Proceedings of the General Track: 2002 USENIX Annual Technical Conference, 2002

Region-Based Memory Management in Cyclone.

Dan Grossman, J. Gregory Morrisett, Trevor Jim, Michael W. Hicks, Yanling Wang, James Cheney

Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), 2002

Analysis issues for cyclone.

J. Gregory Morrisett

Proceedings of the 2002 ACM SIGPLAN-SIGSOFT Workshop on Program Analysis For Software Tools and Engineering, 2002

Type Checking Systems Code.

J. Gregory Morrisett

Proceedings of the Programming Languages and Systems, 2002

2001

A Language-Based Approach to Security.

Fred B. Schneider, J. Gregory Morrisett, Robert Harper

Proceedings of the Informatics - 10 Years Back. 10 Years Ahead., 2001

2000

Typed memory management via static capabilities.

David Walker, Karl Crary, J. Gregory Morrisett

ACM Trans. Program. Lang. Syst., 2000

Syntactic type abstraction.

Dan Grossman, J. Gregory Morrisett, Steve Zdancewic

ACM Trans. Program. Lang. Syst., 2000

Attacking Malicious Code: A Report to the Infosec Research Council.

Gary McGraw, J. Gregory Morrisett

IEEE Softw., 2000

Alias Types for Recursive Data Structures.

David Walker, J. Gregory Morrisett

Proceedings of the Types in Compilation, Third International Workshop, 2000

Scalable Certification for Typed Assembly Language.

Dan Grossman, J. Gregory Morrisett

Proceedings of the Types in Compilation, Third International Workshop, 2000

Alias Types.

Frederick Smith, David Walker, J. Gregory Morrisett

Proceedings of the Programming Languages and Systems, 2000

1999

From system F to typed assembly language.

J. Gregory Morrisett, David Walker, Karl Crary, Neal Glew

ACM Trans. Program. Lang. Syst., 1999

Type-Safe Linking and Modular Assembly Language.

Neal Glew, J. Gregory Morrisett

Proceedings of the POPL '99, 1999

Typed Memory Management in a Calculus of Capabilities.

Karl Crary, David Walker, J. Gregory Morrisett

Proceedings of the POPL '99, 1999

Principals in Programming Languages: A Syntactic Proof Technique.

Steve Zdancewic, Dan Grossman, J. Gregory Morrisett

Proceedings of the fourth ACM SIGPLAN International Conference on Functional Programming (ICFP '99), 1999

Type Structure for Low-Level Programming Languages.

Karl Crary, J. Gregory Morrisett

Proceedings of the Automata, 1999

1998

Comparing Mostly-Copying and Mark-Sweep Conservative Collection.

Frederick Smith, J. Gregory Morrisett

Proceedings of the International Symposium on Memory Management, 1998

Promela++: A Language for Constructing Correct and Efficient Protocols.

Anindya Basu, J. Gregory Morrisett, Thorsten von Eicken

Proceedings of the Proceedings IEEE INFOCOM '98, The Conference on Computer Communications, Seventeenth Annual Joint Conference of the IEEE Computer and Communications Societies, Gateway to the 21st Century, San Francisco, CA, USA, March 29, 1998

1997

Typed Closure Conversion for Recursively-Defined Functions.

J. Gregory Morrisett, Robert Harper

Proceedings of the Second Workshop on Higher-Order Operational Techniques in Semantics, 1997

1996

Typed Closure Conversion.

Yasuhiko Minamide, J. Gregory Morrisett, Robert Harper

Proceedings of the Conference Record of POPL'96: The 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 1996

TIL: a type-directed, optimizing compiler for ML (with retrospective)

David Tarditi, J. Gregory Morrisett, Perry Cheng, Christopher A. Stone, Robert Harper, Peter Lee

Proceedings of the 20 Years of the ACM SIGPLAN Conference on Programming Language Design and Implementation 1979-1999, 1996

TIL: A Type-Directed Optimizing Compiler for ML.

David Tarditi, J. Gregory Morrisett, Perry Cheng, Christopher A. Stone, Robert Harper, Peter Lee

Proceedings of the ACM SIGPLAN'96 Conference on Programming Language Design and Implementation (PLDI), 1996

1995

Compiling Polymorphism Using Intensional Type Analysis.

Robert Harper, J. Gregory Morrisett

Proceedings of the Conference Record of POPL'95: 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 1995

Abstract Models of Memory Management.

J. Gregory Morrisett, Matthias Felleisen, Robert Harper

Proceedings of the seventh international conference on Functional programming languages and computer architecture, 1995

1994

Composing First-Class Transactions.

Nicholas Haines, Darrell Kindred, J. Gregory Morrisett, Scott Nettles, Jeannette M. Wing

ACM Trans. Program. Lang. Syst., 1994

1993

Procs and Locks: A Portable Multiprocessing Platform for Standard ML of New Jersey.

J. Gregory Morrisett, Andrew P. Tolmach

Proceedings of the Fourth ACM SIGPLAN Symposium on Principles & Practice of Parallel Programming (PPOPP), 1993