J. Gregory Morrisett

Orcid: 0000-0002-2619-5614

Affiliations:
  • Harvard University, Cambridge, USA


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

Collaborative distances:

Awards

ACM Fellow

ACM Fellow 2013, "For contributions to mathematically-based methods for ensuring the efficient implementation and verification of practical programming languages.".

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2023
A Core Calculus for Equational Proofs of Cryptographic Protocols.
Proc. ACM Program. Lang., January, 2023

Interval Parsing Grammars for File Format Parsing.
Proc. ACM Program. Lang., 2023

2022
Certified Parsing of Dependent Regular Grammars.
Proceedings of the 43rd IEEE Security and Privacy, 2022

Leapfrog: certified equivalence for protocol parsers.
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.
IACR Cryptol. ePrint Arch., 2021

2019
IPDL: A Probabilistic Dataflow Logic for Cryptography.
IACR Cryptol. ePrint Arch., 2019

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

2018
Bidirectional Grammars for Machine-Code Decoding and Encoding.
J. Autom. Reason., 2018

An Application of Computable Distributions to the Semantics of Probabilistic Programs.
CoRR, 2018

2017
A National Research Agenda for Intelligent Infrastructure.
CoRR, 2017

Safety and Security for Intelligent Infrastructure.
CoRR, 2017

Revisiting Parametricity: Inductives and Uniformity of Propositions.
CoRR, 2017

Compiling Markov chain Monte Carlo algorithms for probabilistic modeling.
Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2017

2016
Challenges in compiling Coq.
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.
Proceedings of the Programming Languages and Systems, 2016

2015
The Foundational Cryptography Framework.
Proceedings of the Principles of Security and Trust - 4th International Conference, 2015

A Mechanized Proof of Security for Searchable Symmetric Encryption.
Proceedings of the IEEE 28th Computer Security Foundations Symposium, 2015

2014
Type Classes for Lightweight Substructural Types.
Proceedings of the Proceedings Third International Workshop on Linearity, 2014

2013
Bringing java's wild native world under control.
ACM Trans. Inf. Syst. Secur., 2013

All Your IFCException Are Belong to Us.
Proceedings of the 2013 IEEE Symposium on Security and Privacy, 2013

Massively Parallel Model of Extended Memory Use in Evolutionary Game Dynamics.
Proceedings of the 27th IEEE International Symposium on Parallel and Distributed Processing, 2013

Formalizing the SAFECode Type System.
Proceedings of the Certified Programs and Proofs - Third International Conference, 2013

2012
Hardware Support for Safety Interlocks and Introspection.
Proceedings of the Sixth IEEE International Conference on Self-Adaptive and Self-Organizing Systems Workshops, 2012

RockSalt: better, faster, stronger SFI for the x86.
Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, 2012

Scalable Formal Machine Models.
Proceedings of the Programming Languages and Systems - 10th Asian Symposium, 2012

2011
Trace-based verification of imperative programs with I/O.
J. Symb. Comput., 2011

Preliminary design of the SAFE platform.
Proceedings of the 6th Workshop on Programming Languages and Operating Systems, 2011

Evaluating value-graph translation validation for LLVM.
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.
Proceedings of the 18th ACM Conference on Computer and Communications Security, 2011

2010
Toward a verified relational database management system.
Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2010

Integrating Types and Specifications for Secure Software Development.
Proceedings of the Computer Network Security, 2010

Mechanized Verification with Sharing.
Proceedings of the Theoretical Aspects of Computing, 2010

Nikola: embedding compiled GPU functions in Haskell.
Proceedings of the 3rd ACM SIGPLAN Symposium on Haskell, 2010

Robusta: taming the native beast of the JVM.
Proceedings of the 17th ACM Conference on Computer and Communications Security, 2010

2009
Technical perspective - A compiler's story.
Commun. ACM, 2009

Towards type-theoretic semantics for transactional concurrency.
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.
Proceedings of the Proceeding of the 14th ACM SIGPLAN international conference on Functional programming, 2009

2008
Hoare type theory, polymorphism and separation.
J. Funct. Program., 2008

Programming with Effects in Coq.
Proceedings of the Mathematics of Program Construction, 9th International Conference, 2008

Design and evaluation of a compiler for embedded stream programs.
Proceedings of the 2008 ACM SIGPLAN/SIGBED Conference on Languages, 2008

Ynot: dependent types for imperative programs.
Proceedings of the Proceeding of the 13th ACM SIGPLAN international conference on Functional programming, 2008

Flask: staged functional programming for sensor networks.
Proceedings of the Proceeding of the 13th ACM SIGPLAN international conference on Functional programming, 2008

A Realizability Model for Impredicative Hoare Type Theory.
Proceedings of the Programming Languages and Systems, 2008

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

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

2007
L<sup>3</sup>: A Linear Language with Locations.
Fundam. Informaticae, 2007

Sensor network programming with Flask.
Proceedings of the 5th International Conference on Embedded Networked Sensor Systems, 2007

Ilea: inter-language analysis across java and c.
Proceedings of the 22nd Annual ACM SIGPLAN Conference on Object-Oriented Programming, 2007

The regiment macroprogramming system.
Proceedings of the 6th International Conference on Information Processing in Sensor Networks, 2007

Abstract Predicates and Mutable ADTs in Hoare Type Theory.
Proceedings of the Programming Languages and Systems, 2007

2006
Computability classes for enforcement mechanisms.
ACM Trans. Program. Lang. Syst., 2006

Safe manual memory management in Cyclone.
Sci. Comput. Program., 2006

Monadic regions.
J. Funct. Program., 2006

Evaluating SFI for a CISC Architecture.
Proceedings of the 15th USENIX Security Symposium, Vancouver, BC, Canada, July 31, 2006

Certified In-lined Reference Monitoring on .NET.
Proceedings of the 2006 Workshop on Programming Languages and Analysis for Security, 2006

Polymorphism and separation in hoare type theory.
Proceedings of the 11th ACM SIGPLAN International Conference on Functional Programming, 2006

Linear Regions Are All You Need.
Proceedings of the Programming Languages and Systems, 2006

2005
"Language-Based Security".
J. Funct. Program., 2005

A step-indexed model of substructural state.
Proceedings of the 10th ACM SIGPLAN International Conference on Functional Programming, 2005

2004
Editorial.
J. Funct. Program., 2004

Invited talk: what's the future for proof-carrying code?
Proceedings of the 2004 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-based Program Manipulation, 2004

Experience with safe manual memory-management in cyclone.
Proceedings of the 4th International Symposium on Memory Management, 2004

2003
Compiling for template-based run-time code generation.
J. Funct. Program., 2003

Stack-based typed assembly language.
J. Funct. Program., 2003

Achieving Type Safety for Low-Level Code.
Proceedings of the Logic Programming, 19th International Conference, 2003

2002
Intensional polymorphism in type-erasure semantics.
J. Funct. Program., 2002

Cyclone: A Safe Dialect of C.
Proceedings of the General Track: 2002 USENIX Annual Technical Conference, 2002

Region-Based Memory Management in Cyclone.
Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), 2002

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

Type Checking Systems Code.
Proceedings of the Programming Languages and Systems, 2002

2001
A Language-Based Approach to Security.
Proceedings of the Informatics - 10 Years Back. 10 Years Ahead., 2001

2000
Typed memory management via static capabilities.
ACM Trans. Program. Lang. Syst., 2000

Syntactic type abstraction.
ACM Trans. Program. Lang. Syst., 2000

Attacking Malicious Code: A Report to the Infosec Research Council.
IEEE Softw., 2000

Alias Types for Recursive Data Structures.
Proceedings of the Types in Compilation, Third International Workshop, 2000

Scalable Certification for Typed Assembly Language.
Proceedings of the Types in Compilation, Third International Workshop, 2000

Alias Types.
Proceedings of the Programming Languages and Systems, 2000

1999
From system F to typed assembly language.
ACM Trans. Program. Lang. Syst., 1999

Type-Safe Linking and Modular Assembly Language.
Proceedings of the POPL '99, 1999

Typed Memory Management in a Calculus of Capabilities.
Proceedings of the POPL '99, 1999

Principals in Programming Languages: A Syntactic Proof Technique.
Proceedings of the fourth ACM SIGPLAN International Conference on Functional Programming (ICFP '99), 1999

Type Structure for Low-Level Programming Languages.
Proceedings of the Automata, 1999

1998
Comparing Mostly-Copying and Mark-Sweep Conservative Collection.
Proceedings of the International Symposium on Memory Management, 1998

Promela++: A Language for Constructing Correct and Efficient Protocols.
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.
Proceedings of the Second Workshop on Higher-Order Operational Techniques in Semantics, 1997

1996
Typed Closure Conversion.
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)
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.
Proceedings of the ACM SIGPLAN'96 Conference on Programming Language Design and Implementation (PLDI), 1996

1995
Compiling Polymorphism Using Intensional Type Analysis.
Proceedings of the Conference Record of POPL'95: 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 1995

Abstract Models of Memory Management.
Proceedings of the seventh international conference on Functional programming languages and computer architecture, 1995

1994
Composing First-Class Transactions.
ACM Trans. Program. Lang. Syst., 1994

1993
Procs and Locks: A Portable Multiprocessing Platform for Standard ML of New Jersey.
Proceedings of the Fourth ACM SIGPLAN Symposium on Principles & Practice of Parallel Programming (PPOPP), 1993


  Loading...