Greg Morrisett

69 papers A* 10A 13B 4C 4Journal 22Unranked 13

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