Now showing items 1-20 of 35

    • Abstract Models of Memory Management 

      Morrisett, John Gregory; Felleisen, Matthias; Harper, Robert (Association for Computing Machinery, 1995)
      Most specifications of garbage collectors concentrate on the low-level algorithmic details of how to find and preserve accessible objects. Often, they focus on bit-level manipulations such as "scanning stack frames," ...
    • Abstract Predicates and Mutable ADTs in Hoare Type Theory 

      Nanevski, Aleksandar; Ahmed, Amal; Morrisett, Greg Gregory; Birkedal, Lars (2006)
      Hoare Type Theory (HTT) combines a dependently typed, higher-order language with monadically-encapsulated, stateful computations. The type system incorporates pre- and post-conditions, in a fashion similar to Hoare and ...
    • Certified Web Services in Ynot 

      Wisnesky, Ryan; Malecha, Gregory Michael; Morrisett, John Gregory (2010-04-21)
      In this paper we demonstrate that it is possible to implement certi ed web systems in a way not much di erent from writing Standard ML or Haskell code, including use of imperative features like pointers, les, and socket ...
    • Combining Control-Flow Integrity and Static Analysis for Efficient and Validated Data Sandboxing 

      Zeng, Bin; Tan, Gang; Morrisett, John Gregory (Association for Computing Machinery, 2011)
      In many software attacks, inducing an illegal control-flow transfer in the target system is one common step. Control-Flow Integrity (CFI) protects a software system by enforcing a pre-determined control-flow graph. In ...
    • Comparing Mostly-copying and Mark-sweep Conservative Collection 

      Smith, Frederick; Morrisett, John Gregory (Association for Computing Machinery, 1998)
      Many high-level language compilers generate C code and then invoke a C compiler for code generation. To date, most, of these compilers link the resulting code against a conservative mark-sweep garbage collector in order ...
    • Compiling Polymorphism Using Intensional Type Analysis 

      Harper, Robert; Morrisett, John Gregory (Association for Computing Machinery, 1995)
      Traditional techniques for implementing polymorphism use a universal representation for objects of unknown type. Often, this forces a compiler to use universal representations even if the types of objects are known. We ...
    • Denotational Translation Validation 

      Govereau, Paul (2013-01-02)
      In this dissertation we present a simple and scalable system for validating the correctness of low-level program transformations. Proving that program transformations are correct is crucial to the development of security ...
    • Dependent type theory of stateful higher-order functions 

      Nanevski, Aleksandar; Morrisett, Greg Gregory (2005)
      In this paper we investigate a logic for reasoning about programs with higher-order functions and effectful features like non-termination and state with aliasing. We propose a dependent type theory HTT (short for Hoare ...
    • Design and Evaluation of a Compiler for Embedded Stream Programs 

      Newton, Ryan R.; Girod, Lewis D.; Craig, Michael B.; Madden, Samuel R.; Morrisett, John Gregory (Association for Computing Machinery, 2008)
      Applications that combine live data streams with embedded, parallel, and distributed processing are becoming more commonplace. WaveScript is a domain-specific language that brings high-level, type-safe, garbage-collected ...
    • Easy Freshness with Pequod Cache Joins 

      Kate, Bryan Nathan (2015-01-14)
      This thesis presents the design of Pequod, a distributed, application-level Web cache. Web developers store data in application-level caches to avoid expensive operations on persistent storage. While useful for reducing ...
    • Effective Interactive Proofs for Higher-Order Imperative Programs 

      Chlipala, Adam J.; Malecha, Gregory Michael; Morrisett, John Gregory; Shinnar, Avraham Ever; Wisnesky, Ryan (Association for Computing Machinery, 2009)
      We present a new approach for constructing and verifying higher-order, imperative programs using the Coq proof assistant. We build on the past work on the Ynot system, which is based on Hoare Type Theory. That original ...
    • Evaluating Value-Graph Translation Validation for LLVM 

      Tristan, Jean-Baptiste F.; Govereau, Paul; Morrisett, John Gregory (2011-03-22)
      Translation validators are static analyzers that attempt to verify that program transformations preserve semantics. Normalizing trans- lation validators do so by trying to match the value-graphs of an original function and ...
    • Evaluating Value-Graph Translation Validation for LLVM 

      Tristan, Jean-Baptiste F.; Govereau, Paul; Morrisett, Greg Gregory (2011)
      Translation validators are static analyzers that attempt to verify that program transformations preserve semantics. Normalizing trans- lation validators do so by trying to match the value-graphs of an original function and ...
    • Extensible Proof Engineering in Intensional Type Theory 

      Malecha, Gregory (2015-02-24)
      We increasingly rely on large, complex systems in our daily lives---from the computers that park our cars to the medical devices that regulate insulin levels to the servers that store our personal information in the cloud. ...
    • Flask: Staged Functional Programming for Sensor Networks 

      Mainland, Geoffrey; Morrisett, John Gregory; Welsh, Matt (Association for Computer Machinery, 2008)
      Severely resource-constrained devices present a confounding challenge to the functional programmer: we are used to having powerful abstraction facilities at our fingertips, but how can we make use of these tools on a device ...
    • A Foundational Proof Framework for Cryptography 

      Petcher, Adam (2015-05-18)
      I present a state-of-the-art mechanized framework for developing and checking proofs of security for cryptographic schemes in the computational model. This system, called the Foundational Cryptography Framework (FCF) is ...
    • From system F to Typed Assembly Language 

      Morrisett, John Gregory; Walker, David; Crary, Karl; Glew, Neal (Association for Computing Machinery, 1998)
      We motivate the design of a statically typed assembly language (TAL) and present a type-preserving translation from System F to TAL. The TAL we present is based on a conventional RISC assembly language, but its static type ...
    • Functional Query Languages with Categorical Types 

      Wisnesky, Ryan (2014-02-25)
      We study three category-theoretic types in the context of functional query languages (typed lambda-calculi extended with additional operations for bulk data processing). The types we study are:
    • Intensional Polymorphism in Type-erasure Semantics 

      Crary, Karl; Weirich, Stephanie; Morrisett, John Gregory (Association for Computing Machinery, 1998)
      Intensional polymorphism, the ability to dispatch to different routines based on types at run time, enables a variety of advanced implementation techniques for polymorphic languages, including tag-free garbage collection, ...
    • Mechanized Verification with Sharing 

      Malecha, Gregory Michael; Morrisett, John Gregory (Springer Verlag, 2010)
      We consider software verification of imperative programs by theorem proving in higher-order separation logic. Separation logic is quite effective for reasoning about tree-like data structures, but less so for data structures ...