Travelled to:
1 × Austria
1 × China
1 × Estonia
1 × Hungary
1 × Japan
1 × Portugal
1 × Spain
1 × United Kingdom
2 × Canada
2 × USA
Collaborated with:
L.Birkedal A.Nanevski M.Fluet A.J.Ahmed J.Tristan G.Mainland D.H.0001 G.Tan A.Shinnar P.Govereau ∅ J.G.Malecha R.Wisnesky M.Welsh R.L.Petersen A.Ahmed J.Tassarotti E.Gan A.Chlipala
Talks about:
program (4) type (4) languag (3) theori (3) compil (3) model (3) hoar (3) probabilist (2) function (2) linear (2)
Person: Greg Morrisett
DBLP: Morrisett:Greg
Facilitated 3 volumes:
Contributed to:
Wrote 17 papers:
- PLDI-2012-MorrisettTTTG #named #performance
- RockSalt: better, faster, stronger SFI for the x86 (GM, GT, JT, JBT, EG), pp. 395–404.
- PLDI-2011-TristanGM #validation
- Evaluating value-graph translation validation for LLVM (JBT, PG, GM), pp. 295–305.
- POPL-2010-MalechaMSW #database #relational #towards
- Toward a verified relational database management system (JGM, GM, AS, RW), pp. 237–248.
- ICFP-2009-ChlipalaMMSW #effectiveness #higher-order #imperative #interactive #proving #source code
- Effective interactive proofs for higher-order imperative programs (AC, JGM, GM, AS, RW), pp. 79–90.
- ESOP-2008-PetersenBNM #hoare #type system
- A Realizability Model for Impredicative Hoare Type Theory (RLP, LB, AN, GM), pp. 337–352.
- ICFP-2008-MainlandMW #functional #named #network #programming #staged
- Flask: staged functional programming for sensor networks (GM, GM, MW), pp. 335–346.
- ICFP-2008-NanevskiMSGB #dependent type #imperative #named #source code
- Ynot: dependent types for imperative programs (AN, GM, AS, PG, LB), pp. 229–240.
- ESOP-2007-NanevskiAMB #data type #hoare #type system
- Abstract Predicates and Mutable ADTs in Hoare Type Theory (AN, AA, GM, LB), pp. 189–204.
- OOPSLA-2007-TanM #analysis #c #java #named
- Ilea: inter-language analysis across java and c (GT, GM), pp. 39–56.
- ESOP-2006-FluetMA #linear
- Linear Regions Are All You Need (MF, GM, AJA), pp. 7–21.
- ICFP-2006-NanevskiMB #hoare #morphism #polymorphism #type system
- Polymorphism and separation in hoare type theory (AN, GM, LB), pp. 62–73.
- ICFP-2005-AhmedFM
- A step-indexed model of substructural state (AJA, MF, GM), pp. 78–91.
- TLCA-2005-MorrisettAF #linear #named
- L3: A Linear Language with Locations (GM, AJA, MF), pp. 293–307.
- ESOP-2016-HuangM #probability #programming language #semantics
- An Application of Computable Distributions to the Semantics of Probabilistic Programming Languages (DH0, GM), pp. 337–363.
- Haskell-2010-MainlandM #gpu #haskell #named
- Nikola: embedding compiled GPU functions in Haskell (GM, GM), pp. 67–78.
- PPDP-2016-Morrisett #challenge #compilation #coq
- Challenges in compiling Coq (GM), p. 9.
- PLDI-2017-HuangTM #algorithm #compilation #markov #modelling #monte carlo #probability
- Compiling Markov chain Monte Carlo algorithms for probabilistic modeling (DH0, JBT, GM), pp. 111–125.