| Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
| 1 | Gregory Malecha, Greg Morrisett, Ryan Wisnesky |
Trace-based verification of imperative programs with I/O.  |
J. Symb. Comput.  |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Jean-Baptiste Tristan, Paul Govereau, Greg Morrisett |
Evaluating value-graph translation validation for LLVM. |
PLDI |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Bin Zeng, Gang Tan, Greg Morrisett |
Combining control-flow integrity and static analysis for efficient and validated data sandboxing. |
ACM Conference on Computer and Communications Security |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Greg Morrisett |
Integrating Types and Specifications for Secure Software Development. |
MMM-ACNS |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | J. Gregory Malecha, Greg Morrisett |
Mechanized Verification with Sharing. |
ICTAC |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | J. Gregory Malecha, Greg Morrisett, Avraham Shinnar, Ryan Wisnesky |
Toward a verified relational database management system. |
POPL |
2010 |
DBLP DOI BibTeX RDF |
relational model, dependent types, separation logic, b+ tree |
| 1 | Geoffrey Mainland, Greg Morrisett |
Nikola: embedding compiled GPU functions in Haskell. |
Haskell |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Joseph Siefers, Gang Tan, Greg Morrisett |
Robusta: taming the native beast of the JVM. |
ACM Conference on Computer and Communications Security |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Greg Morrisett |
Technical perspective - A compiler's story. |
Commun. ACM |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Adam Chlipala, J. Gregory Malecha, Greg Morrisett, Avraham Shinnar, Ryan Wisnesky |
Effective interactive proofs for higher-order imperative programs. |
ICFP |
2009 |
DBLP DOI BibTeX RDF |
functional programming, dependent types, separation logic, interactive proof assistants |
| 1 | Aleksandar Nanevski, Paul Govereau, Greg Morrisett |
Towards type-theoretic semantics for transactional concurrency. |
TLDI |
2009 |
DBLP DOI BibTeX RDF |
type theory, monads, hoare logic, separation logic |
| 1 | Amal Ahmed, Nick Benton, Martin Hofmann, Greg Morrisett |
08061 Executive Summary -- Types, Logics and Semantics for State. |
Types, Logics and Semantics for State |
2008 |
DBLP BibTeX RDF |
|
| 1 | Amal Ahmed, Nick Benton, Martin Hofmann, Greg Morrisett (eds.) |
Types, Logics and Semantics for State, 03.02. - 08.02.2008 |
Types, Logics and Semantics for State |
2008 |
DBLP BibTeX RDF |
|
| 1 | Amal Ahmed, Nick Benton, Martin Hofmann, Greg Morrisett |
08061 Abstracts Collection -- Types, Logics and Semantics for State. |
Types, Logics and Semantics for State |
2008 |
DBLP BibTeX RDF |
|
| 1 | Aleksandar Nanevski, Greg Morrisett, Avraham Shinnar, Paul Govereau, Lars Birkedal |
Ynot: dependent types for imperative programs. |
ICFP |
2008 |
DBLP DOI BibTeX RDF |
type theory, monads, Hoare logic, separation logic |
| 1 | Geoffrey Mainland, Greg Morrisett, Matt Welsh |
Flask: staged functional programming for sensor networks. |
ICFP |
2008 |
DBLP DOI BibTeX RDF |
meta programming |
| 1 | Greg Morrisett |
Programming with Effects in Coq. |
MPC |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Rasmus Lerchedahl Petersen, Lars Birkedal, Aleksandar Nanevski, Greg Morrisett |
A Realizability Model for Impredicative Hoare Type Theory. |
ESOP |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Aleksandar Nanevski, J. Gregory Morrisett, Lars Birkedal |
Hoare type theory, polymorphism and separation. |
J. Funct. Program. |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Ryan Newton, Lewis Girod, Michael B. Craig, Samuel Madden, J. Gregory Morrisett |
Design and evaluation of a compiler for embedded stream programs. |
LCTES |
2008 |
DBLP DOI BibTeX RDF |
stream processing language, sensor networks |
| 1 | Amal Ahmed, Matthew Fluet, Greg Morrisett |
L3: A Linear Language with Locations. |
Fundam. Inform. |
2007 |
DBLP BibTeX RDF |
|
| 1 | Greg Morrisett, Mooly Sagiv (eds.) |
Proceedings of the 6th International Symposium on Memory Management, ISMM 2007, Montreal, Quebec, Canada, October 21-22, 2007 |
ISMM |
2007 |
DBLP BibTeX RDF |
|
| 1 | Ryan Newton, Greg Morrisett, Matt Welsh |
The regiment macroprogramming system. |
IPSN |
2007 |
DBLP DOI BibTeX RDF |
functional macroprogramming, sensor networks |
| 1 | Gang Tan, Greg Morrisett |
Ilea: inter-language analysis across java and c. |
OOPSLA |
2007 |
DBLP DOI BibTeX RDF |
JVML, inter-language analysis, specification extraction, JNI, java native interface |
| 1 | Aleksandar Nanevski, Amal Ahmed, Greg Morrisett, Lars Birkedal |
Abstract Predicates and Mutable ADTs in Hoare Type Theory. |
ESOP |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Geoffrey Mainland, J. Gregory Morrisett, Matt Welsh, Ryan Newton |
Sensor network programming with Flask. |
SenSys |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Nikhil Swamy, Michael W. Hicks, Greg Morrisett, Dan Grossman, Trevor Jim |
Safe manual memory management in Cyclone. |
Sci. Comput. Program. |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Matthew Fluet, Greg Morrisett |
Monadic regions. |
J. Funct. Program. |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Kevin W. Hamlen, Greg Morrisett, Fred B. Schneider |
Certified In-lined Reference Monitoring on .NET. |
PLAS |
2006 |
DBLP DOI BibTeX RDF |
in-lined reference monitoring, program rewriting, reference monitors, security automata, execution monitoring |
| 1 | Aleksandar Nanevski, Greg Morrisett, Lars Birkedal |
Polymorphism and separation in hoare type theory. |
ICFP |
2006 |
DBLP DOI BibTeX RDF |
type theory, hoare logic, separation logic |
| 1 | Matthew Fluet, Greg Morrisett, Amal J. Ahmed |
Linear Regions Are All You Need. |
ESOP |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Kevin W. Hamlen, J. Gregory Morrisett, Fred B. Schneider |
Computability classes for enforcement mechanisms. |
ACM Trans. Program. Lang. Syst. |
2006 |
DBLP DOI BibTeX RDF |
Program rewriting, reference monitors, security automata, execution monitoring, inlined reference monitoring, edit automata |
| 1 | J. Gregory Morrisett, Simon L. Peyton Jones (eds.) |
Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2006, Charleston, South Carolina, USA, January 11-13, 2006 |
POPL |
2006 |
DBLP BibTeX RDF |
|
| 1 | MartÃn Abadi, Greg Morrisett, Andrei Sabelfeld |
"Language-Based Security". |
J. Funct. Program. |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Greg Morrisett, Amal J. Ahmed, Matthew Fluet |
L3: A Linear Language with Locations. |
TLCA |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Amal J. Ahmed, Matthew Fluet, Greg Morrisett |
A step-indexed model of substructural state. |
ICFP |
2005 |
DBLP DOI BibTeX RDF |
mutable references, stepindexed model, substructural type system |
| 1 | J. Gregory Morrisett, Manuel Fähndrich (eds.) |
Proceedings of TLDI'05: 2005 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, Long Beach, CA, USA, January 10, 2005 |
TLDI |
2005 |
DBLP BibTeX RDF |
|
| 1 | Paul Hudak, Greg Morrisett |
Editorial. |
J. Funct. Program. |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | J. Gregory Morrisett |
Invited talk: what's the future for proof-carrying code? |
PEPM |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Michael W. Hicks, J. Gregory Morrisett, Dan Grossman, Trevor Jim |
Experience with safe manual memory-management in cyclone. |
ISMM |
2004 |
DBLP DOI BibTeX RDF |
unique pointers, memory management, regions, memory safety, cyclone |
| 1 | Matthew Fluet, J. Gregory Morrisett |
Monadic regions. |
ICFP |
2004 |
DBLP DOI BibTeX RDF |
type system, effect, monad, region, parametric polymorphism, region-based memory management |
| 1 | J. Gregory Morrisett |
Invited talk: what's the future for proof-carrying code? |
PPDP |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Alex Aiken, Greg Morrisett (eds.) |
Conference Record of POPL 2003: The 30th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, New Orleans, Louisisana, USA, January 15-17, 2003 |
POPL |
2003 |
DBLP BibTeX RDF |
|
| 1 | Frederick Smith, Dan Grossman, J. Gregory Morrisett, Luke Hornof, Trevor Jim |
Compiling for template-based run-time code generation. |
J. Funct. Program. |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | J. Gregory Morrisett, Karl Crary, Neal Glew, David Walker |
Stack-based typed assembly language. |
J. Funct. Program. |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | J. Gregory Morrisett |
Achieving Type Safety for Low-Level Code. |
ICLP |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | J. Gregory Morrisett |
Achieving Type Safety for Low-Level Code. |
ASIAN |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Karl Crary, Stephanie Weirich, J. Gregory Morrisett |
Intensional polymorphism in type-erasure semantics. |
J. Funct. Program. |
2002 |
DBLP DOI BibTeX RDF |
|
| 1 | J. Gregory Morrisett, Karl Crary, Neal Glew, David Walker |
Stack-based typed assembly language. |
J. Funct. Program. |
2002 |
DBLP DOI BibTeX RDF |
|
| 1 | Dan Grossman, J. Gregory Morrisett, Trevor Jim, Michael W. Hicks, Yanling Wang, James Cheney |
Region-Based Memory Management in Cyclone. |
PLDI |
2002 |
DBLP DOI BibTeX RDF |
|
| 1 | Trevor Jim, J. Gregory Morrisett, Dan Grossman, Michael W. Hicks, James Cheney, Yanling Wang |
Cyclone: A Safe Dialect of C. |
USENIX Annual Technical Conference, General Track |
2002 |
DBLP BibTeX RDF |
|
| 1 | J. Gregory Morrisett |
Analysis issues for cyclone. |
PASTE |
2002 |
DBLP DOI BibTeX RDF |
|
| 1 | J. Gregory Morrisett |
Type Checking Systems Code. |
ESOP |
2002 |
DBLP DOI BibTeX RDF |
|
| 1 | Fred B. Schneider, J. Gregory Morrisett, Robert Harper |
A Language-Based Approach to Security. |
Informatics |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | Gary McGraw, J. Gregory Morrisett |
Attacking Malicious Code: A Report to the Infosec Research Council. |
IEEE Software |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | David Walker, Karl Crary, J. Gregory Morrisett |
Typed memory management via static capabilities. |
ACM Trans. Program. Lang. Syst. |
2000 |
DBLP DOI BibTeX RDF |
type-directed compilation, typed intermediate languages, certified code, region-based memory management |
| 1 | Dan Grossman, J. Gregory Morrisett, Steve Zdancewic |
Syntactic type abstraction. |
ACM Trans. Program. Lang. Syst. |
2000 |
DBLP DOI BibTeX RDF |
proof techniques, syntactic proofs, type abstraction, operational semantics, parametricity |
| 1 | David Walker, J. Gregory Morrisett |
Alias Types for Recursive Data Structures. |
Types in Compilation |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | Dan Grossman, J. Gregory Morrisett |
Scalable Certification for Typed Assembly Language. |
Types in Compilation |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | Frederick Smith, David Walker, J. Gregory Morrisett |
Alias Types. |
ESOP |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | J. Gregory Morrisett, David Walker, Karl Crary, Neal Glew |
From system F to typed assembly language. |
ACM Trans. Program. Lang. Syst. |
1999 |
DBLP DOI BibTeX RDF |
secure extensible systems, type-directed compilation, typed assembly language, typed intermediate languages, certified code, closure conversion |
| 1 | Karl Crary, J. Gregory Morrisett |
Type Structure for Low-Level Programming Languages. |
ICALP |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Karl Crary, David Walker, J. Gregory Morrisett |
Typed Memory Management in a Calculus of Capabilities. |
POPL |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Neal Glew, J. Gregory Morrisett |
Type-Safe Linking and Modular Assembly Language. |
POPL |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Steve Zdancewic, Dan Grossman, J. Gregory Morrisett |
Principals in Programming Languages: A Syntactic Proof Technique. |
ICFP |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | J. Gregory Morrisett, David Walker, Karl Crary, Neal Glew |
From System F to Typed Assembly Language. |
POPL |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Frederick Smith, J. Gregory Morrisett |
Comparing Mostly-Copying and Mark-Sweep Conservative Collection. |
ISMM |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Karl Crary, Stephanie Weirich, J. Gregory Morrisett |
Intensional Polymorphism in Type-Erasure Semantics. |
ICFP |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Anindya Basu, J. Gregory Morrisett, Thorsten von Eicken |
Promela++: A Language for Constructing Correct and Efficient Protocols. |
INFOCOM |
1998 |
DBLP BibTeX RDF |
|
| 1 | J. Gregory Morrisett, Karl Crary, Neal Glew, David Walker |
Stack-Based Typed Assembly Language. |
Types in Compilation |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | J. Gregory Morrisett, Robert Harper |
Typed Closure Conversion for Recursively-Defined Functions. |
Electr. Notes Theor. Comput. Sci. |
1997 |
DBLP DOI BibTeX RDF |
|
| 1 | 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 |
DBLP DOI BibTeX RDF |
|
| 1 | David Tarditi, J. Gregory Morrisett, Perry Cheng, Christopher A. Stone, Robert Harper, Peter Lee |
TIL: A Type-Directed Optimizing Compiler for ML. |
PLDI |
1996 |
DBLP DOI BibTeX RDF |
|
| 1 | Yasuhiko Minamide, J. Gregory Morrisett, Robert Harper |
Typed Closure Conversion. |
POPL |
1996 |
DBLP DOI BibTeX RDF |
|
| 1 | Robert Harper, J. Gregory Morrisett |
Compiling Polymorphism Using Intensional Type Analysis. |
POPL |
1995 |
DBLP DOI BibTeX RDF |
ML |
| 1 | J. Gregory Morrisett, Matthias Felleisen, Robert Harper |
Abstract Models of Memory Management. |
FPCA |
1995 |
DBLP BibTeX RDF |
|
| 1 | Nicholas Haines, Darrell Kindred, J. Gregory Morrisett, Scott Nettles, Jeannette M. Wing |
Composing First-Class Transactions. |
ACM Trans. Program. Lang. Syst. |
1994 |
DBLP DOI BibTeX RDF |
skeins, undoability, transactions, recovery, threads, modules, persistence, serializability, Standard ML |
| 1 | J. Gregory Morrisett, Andrew P. Tolmach |
Procs and Locks: A Portable Multiprocessing Platform for Standard ML of New Jersey. |
PPOPP |
1993 |
DBLP DOI BibTeX RDF |
Standard ML |
![[Valid RSS]](Pics/valid-rss.png "Validate my RSS feed")