Greg Morrisett
Publication record assembled from the DBLP archive of ranked conferences.
Papers indexed
28
Venues
14
Active years
2005–2022
Best venue rank
A*
Where they publish
Papers
28 indexed papers, newest first.
| Year | Venue | Title | Authors |
|---|---|---|---|
| 2022 | PLDI | Leapfrog: certified equivalence for protocol parsers. | Ryan Doenges, Tobias Kapp, John Sarracino, Nate Foster, Greg Morrisett |
| 2022 | SP | Certified Parsing of Dependent Regular Grammars. | John Sarracino, Gang Tan, Greg Morrisett |
| 2017 | PLDI | Compiling Markov chain Monte Carlo algorithms for probabilistic modeling. | Daniel Huang, Jean-Baptiste Tristan, Greg Morrisett |
| 2016 | ESOP | An Application of Computable Distributions to the Semantics of Probabilistic Programming Languages. | Daniel Huang, Greg Morrisett |
| 2016 | PPDP | Challenges in compiling Coq. | Greg Morrisett |
| 2013 | CPP | Formalizing the SAFECode Type System. | Daniel Huang, Greg Morrisett |
| 2013 | SP | All Your IFCException Are Belong to Us. | Catalin Hritcu, Michael Greenberg, Ben Karel, Benjamin C. Pierce, Greg Morrisett |
| 2012 | APLAS | Scalable Formal Machine Models. | Greg Morrisett |
| 2012 | CPP | Scalable Formal Machine Models. | Greg Morrisett |
| 2012 | PLDI | RockSalt: better, faster, stronger SFI for the x86. | Greg Morrisett, Gang Tan, Joseph Tassarotti, Jean-Baptiste Tristan, Edward Gan |
| 2011 | CCS | Combining control-flow integrity and static analysis for efficient and validated data sandboxing. | Bin Zeng, Gang Tan, Greg Morrisett |
| 2011 | PLDI | Evaluating value-graph translation validation for LLVM. | Jean-Baptiste Tristan, Paul Govereau, Greg Morrisett |
| 2011 | SOSP | Preliminary design of the SAFE platform. | Andr DeHon, Ben Karel, Thomas F. Knight Jr., Gregory Malecha, Benot Montagu, Robin Morisset, Greg Morrisett, Benjamin C. Pierce, Randy Pollack, Sumit Ray, Olin Shivers, Jonathan M. Smith, Gregory Sullivan |
| 2010 | CCS | Robusta: taming the native beast of the JVM. | Joseph Siefers, Gang Tan, Greg Morrisett |
| 2010 | HASKELL | Nikola: embedding compiled GPU functions in Haskell. | Geoffrey Mainland, Greg Morrisett |
| 2010 | ICTAC | Mechanized Verification with Sharing. | J. Gregory Malecha, Greg Morrisett |
| 2010 | POPL | Toward a verified relational database management system. | J. Gregory Malecha, Greg Morrisett, Avraham Shinnar, Ryan Wisnesky |
| 2009 | ICFP | Effective interactive proofs for higher-order imperative programs. | Adam Chlipala, J. Gregory Malecha, Greg Morrisett, Avraham Shinnar, Ryan Wisnesky |
| 2008 | ESOP | A Realizability Model for Impredicative Hoare Type Theory. | Rasmus Lerchedahl Petersen, Lars Birkedal, Aleksandar Nanevski, Greg Morrisett |
| 2008 | ICFP | Flask: staged functional programming for sensor networks. | Geoffrey Mainland, Greg Morrisett, Matt Welsh |
| 2008 | ICFP | Ynot: dependent types for imperative programs. | Aleksandar Nanevski, Greg Morrisett, Avraham Shinnar, Paul Govereau, Lars Birkedal |
| 2008 | MPC | Programming with Effects in Coq. | Greg Morrisett |
| 2007 | ESOP | Abstract Predicates and Mutable ADTs in Hoare Type Theory. | Aleksandar Nanevski, Amal Ahmed, Greg Morrisett, Lars Birkedal |
| 2007 | OOPSLA | Ilea: inter-language analysis across java and c. | Gang Tan, Greg Morrisett |
| 2006 | ESOP | Linear Regions Are All You Need. | Matthew Fluet, Greg Morrisett, Amal J. Ahmed |
| 2006 | ICFP | Polymorphism and separation in hoare type theory. | Aleksandar Nanevski, Greg Morrisett, Lars Birkedal |
| 2006 | PLDI | Certified In-lined Reference Monitoring on .NET. | Kevin W. Hamlen, Greg Morrisett, Fred B. Schneider |
| 2005 | ICFP | A step-indexed model of substructural state. | Amal J. Ahmed, Matthew Fluet, Greg Morrisett |