default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDJ. Gregory Morrisett
Greg Morrisett
Person information
- affiliation: Harvard University, Cambridge, USA
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
showing all ?? records
2020 – today
- 2023
[j22]Jialun Zhang
, Greg Morrisett, Gang Tan:
Interval Parsing Grammars for File Format Parsing. Proc. ACM Program. Lang. 7(PLDI): 1073-1095 (2023)- [j21]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): 866-892 (2023) - [i12]Jialun Zhang, Greg Morrisett, Gang Tan:
Interval Parsing Grammars for File Format Parsing. CoRR abs/2304.04859 (2023) - 2022
- [c71]Ryan Doenges, Tobias Kappé, John Sarracino, Nate Foster, Greg Morrisett:
Leapfrog: certified equivalence for protocol parsers. PLDI 2022: 950-965 - [c70]John Sarracino, Gang Tan, Greg Morrisett:
Certified Parsing of Dependent Regular Grammars. SP (Workshops) 2022: 113-123 - [i11]Ryan Doenges, Tobias Kappé, John Sarracino, Nate Foster, Greg Morrisett:
Leapfrog: Certified Equivalence for Protocol Parsers. CoRR abs/2205.08762 (2022) - 2021
- [i10]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: 147 (2021)
2010 – 2019
- 2019
- [i9]Greg Morrisett, Shwetak N. Patel, Jennifer Rexford, Benjamin G. Zorn:
Evolving Academia/Industry Relations in Computing Research: Interim Report. CoRR abs/1903.10375 (2019) - [i8]Xiong Fan, Joshua Gancher, Greg Morrisett, Elaine Shi, Kristina Sojakova:
IPDL: A Probabilistic Dataflow Logic for Cryptography. IACR Cryptol. ePrint Arch. 2019: 1422 (2019) - 2018
- [j20]Gang Tan, Greg Morrisett:
Bidirectional Grammars for Machine-Code Decoding and Encoding. J. Autom. Reason. 60(3): 257-277 (2018) - [i7]Daniel Huang, Greg Morrisett, Bas Spitters:
An Application of Computable Distributions to the Semantics of Probabilistic Programs. CoRR abs/1806.07966 (2018) - 2017
- [c69]Daniel Huang, Jean-Baptiste Tristan, Greg Morrisett:
Compiling Markov chain Monte Carlo algorithms for probabilistic modeling. PLDI 2017: 111-125 - [i6]Abhishek Anand, Greg Morrisett:
Revisiting Parametricity: Inductives and Uniformity of Propositions. CoRR abs/1705.01163 (2017) - [i5]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 abs/1705.01920 (2017) - [i4]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 abs/1705.02002 (2017) - 2016
- [c68]Daniel Huang, Greg Morrisett:
An Application of Computable Distributions to the Semantics of Probabilistic Programming Languages. ESOP 2016: 337-363 - [c67]Greg Morrisett:
Challenges in compiling Coq. PPDP 2016: 9 - [c66]Gang Tan, Greg Morrisett:
Bidirectional Grammars for Machine-Code Decoding and Encoding. VSTTE 2016: 73-89 - 2015
- [c65]Adam Petcher, Greg Morrisett:
A Mechanized Proof of Security for Searchable Symmetric Encryption. CSF 2015: 481-494 - [c64]Adam Petcher, Greg Morrisett:
The Foundational Cryptography Framework. POST 2015: 53-72 - [e7]Thomas Ball, Rastislav Bodík, Shriram Krishnamurthi, Benjamin S. Lerner, Greg Morrisett:
1st Summit on Advances in Programming Languages, SNAPL 2015, May 3-6, 2015, Asilomar, California, USA. LIPIcs 32, Schloss Dagstuhl - Leibniz-Zentrum für Informatik 2015, ISBN 978-3-939897-80-4 [contents] - 2014
- [c63]Edward Gan, Jesse A. Tov, Greg Morrisett:
Type Classes for Lightweight Substructural Types. LINEARITY 2014: 34-48 - [i3]Adam Petcher, Greg Morrisett:
The Foundational Cryptography Framework. CoRR abs/1410.3735 (2014) - 2013
- [j19]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): 9 (2013) - [c62]Daniel Huang, Greg Morrisett:
Formalizing the SAFECode Type System. CPP 2013: 211-226 - [c61]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: 1217-1228 - [c60]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: 3-17 - [e6]Greg Morrisett, Tarmo Uustalu:
ACM SIGPLAN International Conference on Functional Programming, ICFP'13, Boston, MA, USA - September 25 - 27, 2013. ACM 2013, ISBN 978-1-4503-2326-0 [contents] - 2012
- [c59]Greg Morrisett:
Scalable Formal Machine Models. APLAS 2012: 312-314 - [c58]Greg Morrisett:
Scalable Formal Machine Models. CPP 2012: 1-3 - [c57]Greg Morrisett, Gang Tan, Joseph Tassarotti, Jean-Baptiste Tristan, Edward Gan:
RockSalt: better, faster, stronger SFI for the x86. PLDI 2012: 395-404 - [c56]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: 1-8 - 2011
- [j18]Gregory Malecha, Greg Morrisett, Ryan Wisnesky:
Trace-based verification of imperative programs with I/O. J. Symb. Comput. 46(2): 95-118 (2011) - [c55]Bin Zeng, Gang Tan, Greg Morrisett:
Combining control-flow integrity and static analysis for efficient and validated data sandboxing. CCS 2011: 29-40 - [c54]Jean-Baptiste Tristan, Paul Govereau, Greg Morrisett:
Evaluating value-graph translation validation for LLVM. PLDI 2011: 295-305 - [c53]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: 4:1-4:5 - 2010
- [c52]Joseph Siefers, Gang Tan, Greg Morrisett:
Robusta: taming the native beast of the JVM. CCS 2010: 201-211 - [c51]Geoffrey Mainland, Greg Morrisett:
Nikola: embedding compiled GPU functions in Haskell. Haskell 2010: 67-78 - [c50]J. Gregory Malecha, Greg Morrisett:
Mechanized Verification with Sharing. ICTAC 2010: 245-259 - [c49]Greg Morrisett:
Integrating Types and Specifications for Secure Software Development. MMM-ACNS 2010: 32-35 - [c48]J. Gregory Malecha, Greg Morrisett, Avraham Shinnar, Ryan Wisnesky:
Toward a verified relational database management system. POPL 2010: 237-248
2000 – 2009
- 2009
- [j17]Greg Morrisett:
Technical perspective - A compiler's story. Commun. ACM 52(7): 106 (2009) - [c47]Adam Chlipala, J. Gregory Malecha, Greg Morrisett, Avraham Shinnar, Ryan Wisnesky:
Effective interactive proofs for higher-order imperative programs. ICFP 2009: 79-90 - [c46]Aleksandar Nanevski, Paul Govereau, Greg Morrisett:
Towards type-theoretic semantics for transactional concurrency. TLDI 2009: 79-90 - 2008
- [j16]Aleksandar Nanevski, J. Gregory Morrisett, Lars Birkedal:
Hoare type theory, polymorphism and separation. J. Funct. Program. 18(5-6): 865-911 (2008) - [c45]Rasmus Lerchedahl Petersen, Lars Birkedal, Aleksandar Nanevski, Greg Morrisett:
A Realizability Model for Impredicative Hoare Type Theory. ESOP 2008: 337-352 - [c44]Aleksandar Nanevski, Greg Morrisett, Avraham Shinnar, Paul Govereau, Lars Birkedal:
Ynot: dependent types for imperative programs. ICFP 2008: 229-240 - [c43]Geoffrey Mainland, Greg Morrisett, Matt Welsh:
Flask: staged functional programming for sensor networks. ICFP 2008: 335-346 - [c42]Ryan Newton, Lewis Girod, Michael B. Craig, Samuel Madden, J. Gregory Morrisett:
Design and evaluation of a compiler for embedded stream programs. LCTES 2008: 131-140 - [c41]Greg Morrisett:
Programming with Effects in Coq. MPC 2008: 28 - [e5]Amal Ahmed, Nick Benton, Martin Hofmann, Greg Morrisett:
Types, Logics and Semantics for State, 03.02. - 08.02.2008. Dagstuhl Seminar Proceedings 08061, Internationales Begegnungs- und Forschungszentrum fuer Informatik (IBFI), Schloss Dagstuhl, Germany 2008 [contents] - [i2]Amal Ahmed, Nick Benton, Martin Hofmann, Greg Morrisett:
08061 Executive Summary -- Types, Logics and Semantics for State. Types, Logics and Semantics for State 2008 - [i1]Amal Ahmed, Nick Benton, Martin Hofmann, Greg Morrisett:
08061 Abstracts Collection -- Types, Logics and Semantics for State. Types, Logics and Semantics for State 2008 - 2007
- [j15]Amal Ahmed, Matthew Fluet, Greg Morrisett:
L3: A Linear Language with Locations. Fundam. Informaticae 77(4): 397-449 (2007) - [c40]Aleksandar Nanevski, Amal Ahmed, Greg Morrisett, Lars Birkedal:
Abstract Predicates and Mutable ADTs in Hoare Type Theory. ESOP 2007: 189-204 - [c39]Ryan Newton, Greg Morrisett, Matt Welsh:
The regiment macroprogramming system. IPSN 2007: 489-498 - [c38]Gang Tan, Greg Morrisett:
Ilea: inter-language analysis across java and c. OOPSLA 2007: 39-56 - [c37]Geoffrey Mainland, J. Gregory Morrisett, Matt Welsh, Ryan Newton:
Sensor network programming with Flask. SenSys 2007: 385-386 - [e4]Greg Morrisett, Mooly Sagiv:
Proceedings of the 6th International Symposium on Memory Management, ISMM 2007, Montreal, Quebec, Canada, October 21-22, 2007. ACM 2007, ISBN 978-1-59593-893-0 [contents] - 2006
- [j14]Matthew Fluet, Greg Morrisett:
Monadic regions. J. Funct. Program. 16(4-5): 485-545 (2006) - [j13]Nikhil Swamy, Michael W. Hicks, Greg Morrisett, Dan Grossman, Trevor Jim:
Safe manual memory management in Cyclone. Sci. Comput. Program. 62(2): 122-144 (2006) - [j12]Kevin W. Hamlen, J. Gregory Morrisett, Fred B. Schneider:
Computability classes for enforcement mechanisms. ACM Trans. Program. Lang. Syst. 28(1): 175-205 (2006) - [c36]Matthew Fluet, Greg Morrisett, Amal J. Ahmed:
Linear Regions Are All You Need. ESOP 2006: 7-21 - [c35]Aleksandar Nanevski, Greg Morrisett, Lars Birkedal:
Polymorphism and separation in hoare type theory. ICFP 2006: 62-73 - [c34]Kevin W. Hamlen, Greg Morrisett, Fred B. Schneider:
Certified In-lined Reference Monitoring on .NET. PLAS 2006: 7-16 - [c33]Stephen McCamant, Greg Morrisett:
Evaluating SFI for a CISC Architecture. USENIX Security Symposium 2006 - [e3]J. Gregory Morrisett, Simon L. Peyton Jones:
Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2006, Charleston, South Carolina, USA, January 11-13, 2006. ACM 2006, ISBN 1-59593-027-2 [contents] - 2005
- [j11]Martín Abadi, Greg Morrisett, Andrei Sabelfeld:
"Language-Based Security". J. Funct. Program. 15(2): 129 (2005) - [c32]Amal J. Ahmed, Matthew Fluet, Greg Morrisett:
A step-indexed model of substructural state. ICFP 2005: 78-91 - [c31]Greg Morrisett, Amal J. Ahmed, Matthew Fluet:
L3: A Linear Language with Locations. TLCA 2005: 293-307 - [e2]J. Gregory Morrisett, Manuel Fähndrich:
Proceedings of TLDI'05: 2005 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, Long Beach, CA, USA, January 10, 2005. ACM 2005, ISBN 1-58113-999-3 [contents] - 2004
- [j10]Paul Hudak, Greg Morrisett:
Editorial. J. Funct. Program. 14(4) (2004) - [c30]Matthew Fluet, J. Gregory Morrisett:
Monadic regions. ICFP 2004: 103-114 - [c29]Michael W. Hicks, J. Gregory Morrisett, Dan Grossman, Trevor Jim:
Experience with safe manual memory-management in cyclone. ISMM 2004: 73-84 - [c28]J. Gregory Morrisett:
Invited talk: what's the future for proof-carrying code? PEPM 2004: 203 - [c27]J. Gregory Morrisett:
Invited talk: what's the future for proof-carrying code? PPDP 2004: 5 - 2003
- [j9]Frederick Smith, Dan Grossman, J. Gregory Morrisett, Luke Hornof, Trevor Jim:
Compiling for template-based run-time code generation. J. Funct. Program. 13(3): 677-708 (2003) - [j8]J. Gregory Morrisett, Karl Crary, Neal Glew, David Walker:
Stack-based typed assembly language. J. Funct. Program. 13(5): 957-959 (2003) - [c26]J. Gregory Morrisett:
Achieving Type Safety for Low-Level Code. ASIAN 2003: 1-2 - [c25]J. Gregory Morrisett:
Achieving Type Safety for Low-Level Code. ICLP 2003: 1-2 - [e1]Alex Aiken, Greg Morrisett:
Conference Record of POPL 2003: The 30th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, New Orleans, Louisisana, USA, January 15-17, 2003. ACM 2003, ISBN 1-58113-628-5 [contents] - 2002
- [j7]J. Gregory Morrisett, Karl Crary, Neal Glew, David Walker:
Stack-based typed assembly language. J. Funct. Program. 12(1): 3-88 (2002) - [j6]Karl Crary, Stephanie Weirich, J. Gregory Morrisett:
Intensional polymorphism in type-erasure semantics. J. Funct. Program. 12(6): 567-600 (2002) - [c24]J. Gregory Morrisett:
Type Checking Systems Code. ESOP 2002: 1-5 - [c23]J. Gregory Morrisett:
Analysis issues for cyclone. PASTE 2002: 26 - [c22]Dan Grossman, J. Gregory Morrisett, Trevor Jim, Michael W. Hicks, Yanling Wang, James Cheney:
Region-Based Memory Management in Cyclone. PLDI 2002: 282-293 - [c21]Trevor Jim, J. Gregory Morrisett, Dan Grossman, Michael W. Hicks, James Cheney, Yanling Wang:
Cyclone: A Safe Dialect of C. USENIX ATC, General Track 2002: 275-288 - 2001
- [c20]Fred B. Schneider, J. Gregory Morrisett, Robert Harper:
A Language-Based Approach to Security. Informatics 2001: 86-101 - 2000
- [j5]Gary McGraw, J. Gregory Morrisett:
Attacking Malicious Code: A Report to the Infosec Research Council. IEEE Softw. 17(5): 33-41 (2000) - [j4]David Walker, Karl Crary, J. Gregory Morrisett:
Typed memory management via static capabilities. ACM Trans. Program. Lang. Syst. 22(4): 701-771 (2000) - [j3]Dan Grossman, J. Gregory Morrisett, Steve Zdancewic:
Syntactic type abstraction. ACM Trans. Program. Lang. Syst. 22(6): 1037-1080 (2000) - [c19]Frederick Smith, David Walker, J. Gregory Morrisett:
Alias Types. ESOP 2000: 366-381 - [c18]Dan Grossman, J. Gregory Morrisett:
Scalable Certification for Typed Assembly Language. Types in Compilation 2000: 117-146 - [c17]David Walker, J. Gregory Morrisett:
Alias Types for Recursive Data Structures. Types in Compilation 2000: 177-206
1990 – 1999
- 1999
- [j2]J. Gregory Morrisett, David Walker, Karl Crary, Neal Glew:
From system F to typed assembly language. ACM Trans. Program. Lang. Syst. 21(3): 527-568 (1999) - [c16]Karl Crary, J. Gregory Morrisett:
Type Structure for Low-Level Programming Languages. ICALP 1999: 40-54 - [c15]Steve Zdancewic, Dan Grossman, J. Gregory Morrisett:
Principals in Programming Languages: A Syntactic Proof Technique. ICFP 1999: 197-207 - [c14]Neal Glew, J. Gregory Morrisett:
Type-Safe Linking and Modular Assembly Language. POPL 1999: 250-261 - [c13]Karl Crary, David Walker, J. Gregory Morrisett:
Typed Memory Management in a Calculus of Capabilities. POPL 1999: 262-275 - 1998
- [c12]Karl Crary, Stephanie Weirich, J. Gregory Morrisett:
Intensional Polymorphism in Type-Erasure Semantics. ICFP 1998: 301-312 - [c11]Anindya Basu, J. Gregory Morrisett, Thorsten von Eicken:
Promela++: A Language for Constructing Correct and Efficient Protocols. INFOCOM 1998: 455-462 - [c10]Frederick Smith, J. Gregory Morrisett:
Comparing Mostly-Copying and Mark-Sweep Conservative Collection. ISMM 1998: 68-78 - [c9]J. Gregory Morrisett, David Walker, Karl Crary, Neal Glew:
From System F to Typed Assembly Language. POPL 1998: 85-97 - [c8]J. Gregory Morrisett, Karl Crary, Neal Glew, David Walker:
Stack-Based Typed Assembly Language. Types in Compilation 1998: 28-52 - 1997
- [c7]J. Gregory Morrisett, Robert Harper:
Typed Closure Conversion for Recursively-Defined Functions. HOOTS 1997: 230-241 - 1996
- [c6]David Tarditi, J. Gregory Morrisett, Perry Cheng, Christopher A. Stone, Robert Harper, Peter Lee:
TIL: A Type-Directed Optimizing Compiler for ML. PLDI 1996: 181-192 - [c5]David Tarditi, J. Gregory Morrisett, Perry Cheng, Christopher A. Stone, Robert Harper, Peter Lee:
TIL: a type-directed, optimizing compiler for ML (with retrospective). Best of PLDI 1996: 554-567 - [c4]Yasuhiko Minamide, J. Gregory Morrisett, Robert Harper:
Typed Closure Conversion. POPL 1996: 271-283 - 1995
- [c3]J. Gregory Morrisett, Matthias Felleisen, Robert Harper:
Abstract Models of Memory Management. FPCA 1995: 66-77 - [c2]Robert Harper, J. Gregory Morrisett:
Compiling Polymorphism Using Intensional Type Analysis. POPL 1995: 130-141 - 1994
- [j1]Nicholas Haines, Darrell Kindred, J. Gregory Morrisett, Scott Nettles, Jeannette M. Wing:
Composing First-Class Transactions. ACM Trans. Program. Lang. Syst. 16(6): 1719-1736 (1994) - 1993
- [c1]J. Gregory Morrisett, Andrew P. Tolmach:
Procs and Locks: A Portable Multiprocessing Platform for Standard ML of New Jersey. PPoPP 1993: 198-207
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from 
to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the 
of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from 
, 
, and 
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from 
.
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-10-07 22:23 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
