Greg Morrisett

Publication Activity (10 Years)

Years Active: 2004-2023
Publications (10 Years): 20

Top Topics

Context Free Grammars

Probabilistic Model

Top Venues

Proc. ACM Program. Lang.

IACR Cryptol. ePrint Arch.

Publications

Joshua Gancher, Kristina Sojakova, Xiong Fan, Elaine Shi, Greg Morrisett
A Core Calculus for Equational Proofs of Cryptographic Protocols. Proc. ACM Program. Lang. 7 (POPL) (2023)
Jialun Zhang, Greg Morrisett, Gang Tan
Interval Parsing Grammars for File Format Parsing. CoRR (2023)
Jialun Zhang, Greg Morrisett, Gang Tan
Interval Parsing Grammars for File Format Parsing. Proc. ACM Program. Lang. 7 (PLDI) (2023)
Ryan Doenges, Tobias Kappé, John Sarracino, Nate Foster, Greg Morrisett
Leapfrog: Certified Equivalence for Protocol Parsers. CoRR (2022)
John Sarracino, Gang Tan, Greg Morrisett
Certified Parsing of Dependent Regular Grammars. SP Workshops (2022)
Ryan Doenges, Tobias Kappé, John Sarracino, Nate Foster, Greg Morrisett
Leapfrog: certified equivalence for protocol parsers. PLDI (2022)
Greg Morrisett, Elaine Shi, Kristina Sojakova, Xiong Fan, Joshua Gancher
IPDL: A Simple Framework for Formally Verifying Distributed Cryptographic Protocols. IACR Cryptol. ePrint Arch. 2021 (2021)
Xiong Fan, Joshua Gancher, Greg Morrisett, Elaine Shi, Kristina Sojakova
IPDL: A Probabilistic Dataflow Logic for Cryptography. IACR Cryptol. ePrint Arch. 2019 (2019)
Greg Morrisett, Shwetak N. Patel, Jennifer Rexford, Benjamin G. Zorn
Evolving Academia/Industry Relations in Computing Research: Interim Report. CoRR (2019)
Gang Tan, Greg Morrisett
Bidirectional Grammars for Machine-Code Decoding and Encoding. J. Autom. Reason. 60 (3) (2018)
Daniel Huang, Greg Morrisett, Bas Spitters
An Application of Computable Distributions to the Semantics of Probabilistic Programs. CoRR (2018)
Daniel Huang, Jean-Baptiste Tristan, Greg Morrisett
Compiling Markov chain Monte Carlo algorithms for probabilistic modeling. PLDI (2017)
Kevin Fu, Ann W. Drobnis, Greg Morrisett, Elizabeth D. Mynatt, Shwetak N. Patel, Radha Poovendran, Benjamin G. Zorn
Safety and Security for Intelligent Infrastructure. CoRR (2017)
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
A National Research Agenda for Intelligent Infrastructure. CoRR (2017)
Abhishek Anand, Greg Morrisett
Revisiting Parametricity: Inductives and Uniformity of Propositions. CoRR (2017)
Greg Morrisett
Challenges in compiling Coq. PPDP (2016)
Daniel Huang, Greg Morrisett
An Application of Computable Distributions to the Semantics of Probabilistic Programming Languages. ESOP (2016)
Gang Tan, Greg Morrisett
Bidirectional Grammars for Machine-Code Decoding and Encoding. VSTTE (2016)
Adam Petcher, Greg Morrisett
The Foundational Cryptography Framework. POST (2015)
Adam Petcher, Greg Morrisett
A Mechanized Proof of Security for Searchable Symmetric Encryption. CSF (2015)
Edward Gan, Jesse A. Tov, Greg Morrisett
Type Classes for Lightweight Substructural Types. LINEARITY (2014)
Adam Petcher, Greg Morrisett
The Foundational Cryptography Framework. CoRR (2014)
Amanda Peters Randles, David G. Rand, Christopher Lee, Greg Morrisett, Jayanta Sircar, Martin A. Nowak, Hanspeter Pfister
Massively Parallel Model of Extended Memory Use in Evolutionary Game Dynamics. IPDPS (2013)
Daniel Huang, Greg Morrisett
Formalizing the SAFECode Type System. CPP (2013)
Mengtao Sun, Gang Tan, Joseph Siefers, Bin Zeng, Greg Morrisett
Bringing java's wild native world under control. ACM Trans. Inf. Syst. Secur. 16 (3) (2013)
Catalin Hritcu, Michael Greenberg, Ben Karel, Benjamin C. Pierce, Greg Morrisett
All Your IFCException Are Belong to Us. IEEE Symposium on Security and Privacy (2013)
Greg Morrisett
Scalable Formal Machine Models. APLAS (2012)
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
Hardware Support for Safety Interlocks and Introspection. SASO Workshops (2012)
Greg Morrisett, Gang Tan, Joseph Tassarotti, Jean-Baptiste Tristan, Edward Gan
RockSalt: better, faster, stronger SFI for the x86. PLDI (2012)
Greg Morrisett
Scalable Formal Machine Models. CPP (2012)
Gregory Malecha, Greg Morrisett, Ryan Wisnesky
Trace-based verification of imperative programs with I/O. J. Symb. Comput. 46 (2) (2011)
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
Preliminary design of the SAFE platform. PLOS@SOSP (2011)
Bin Zeng, Gang Tan, Greg Morrisett
Combining control-flow integrity and static analysis for efficient and validated data sandboxing. CCS (2011)
Jean-Baptiste Tristan, Paul Govereau, Greg Morrisett
Evaluating value-graph translation validation for LLVM. PLDI (2011)
J. Gregory Malecha, Greg Morrisett, Avraham Shinnar, Ryan Wisnesky
Toward a verified relational database management system. POPL (2010)
Joseph Siefers, Gang Tan, Greg Morrisett
Robusta: taming the native beast of the JVM. CCS (2010)
Geoffrey Mainland, Greg Morrisett
Nikola: embedding compiled GPU functions in Haskell. Haskell (2010)
Greg Morrisett
Integrating Types and Specifications for Secure Software Development. MMM-ACNS (2010)
J. Gregory Malecha, Greg Morrisett
Mechanized Verification with Sharing. ICTAC (2010)
Adam Chlipala, J. Gregory Malecha, Greg Morrisett, Avraham Shinnar, Ryan Wisnesky
Effective interactive proofs for higher-order imperative programs. ICFP (2009)
Greg Morrisett
Technical perspective - A compiler's story. Commun. ACM 52 (7) (2009)
Aleksandar Nanevski, Paul Govereau, Greg Morrisett
Towards type-theoretic semantics for transactional concurrency. TLDI (2009)
Aleksandar Nanevski, Greg Morrisett, Avraham Shinnar, Paul Govereau, Lars Birkedal
Ynot: dependent types for imperative programs. ICFP (2008)
Amal Ahmed, Nick Benton, Martin Hofmann, Greg Morrisett
08061 Abstracts Collection -- Types, Logics and Semantics for State. Types, Logics and Semantics for State (2008)
Geoffrey Mainland, Greg Morrisett, Matt Welsh
Flask: staged functional programming for sensor networks. ICFP (2008)
Amal Ahmed, Nick Benton, Martin Hofmann, Greg Morrisett
08061 Executive Summary -- Types, Logics and Semantics for State. Types, Logics and Semantics for State (2008)
Greg Morrisett
Programming with Effects in Coq. MPC (2008)
Rasmus Lerchedahl Petersen, Lars Birkedal, Aleksandar Nanevski, Greg Morrisett
A Realizability Model for Impredicative Hoare Type Theory. ESOP (2008)
Ryan Newton, Greg Morrisett, Matt Welsh
The regiment macroprogramming system. IPSN (2007)
Gang Tan, Greg Morrisett
Ilea: inter-language analysis across java and c. OOPSLA (2007)
Amal Ahmed, Matthew Fluet, Greg Morrisett
: A Linear Language with Locations. Fundam. Informaticae 77 (4) (2007)
Aleksandar Nanevski, Amal Ahmed, Greg Morrisett, Lars Birkedal
Abstract Predicates and Mutable ADTs in Hoare Type Theory. ESOP (2007)
Kevin W. Hamlen, Greg Morrisett, Fred B. Schneider
Certified In-lined Reference Monitoring on .NET. PLAS (2006)
Aleksandar Nanevski, Greg Morrisett, Lars Birkedal
Polymorphism and separation in hoare type theory. ICFP (2006)
Stephen McCamant, Greg Morrisett
Evaluating SFI for a CISC Architecture. USENIX Security Symposium (2006)
Nikhil Swamy, Michael W. Hicks, Greg Morrisett, Dan Grossman, Trevor Jim
Safe manual memory management in Cyclone. Sci. Comput. Program. 62 (2) (2006)
Matthew Fluet, Greg Morrisett
Monadic regions. J. Funct. Program. 16 (4-5) (2006)
Matthew Fluet, Greg Morrisett, Amal J. Ahmed
Linear Regions Are All You Need. ESOP (2006)
Greg Morrisett, Amal J. Ahmed, Matthew Fluet
: A Linear Language with Locations. TLCA (2005)
Amal J. Ahmed, Matthew Fluet, Greg Morrisett
A step-indexed model of substructural state. ICFP (2005)
Martín Abadi, Greg Morrisett, Andrei Sabelfeld
"Language-Based Security". J. Funct. Program. 15 (2) (2005)
Paul Hudak, Greg Morrisett
Editorial. J. Funct. Program. 14 (4) (2004)