| Detecting Locally Distributed Predicates | 1 | 0.35 | 2011 |
| A tale of two planners: modular robotic planning with LDP | 5 | 0.48 | 2009 |
| A Language for Large Ensembles of Independently Executing Nodes | 39 | 1.58 | 2009 |
| Beyond Audio and Video: Using Claytronics to Enable Pario | 5 | 0.65 | 2009 |
| THOR: A Tool for Reasoning about Shape and Arithmetic | 23 | 0.86 | 2008 |
| Distributed Watchpoints: Debugging Large Modular Robot Systems | 8 | 0.61 | 2007 |
| Enforcing resource bounds via static verification of dynamic checks | 27 | 1.56 | 2007 |
| Meld: A declarative approach to programming ensembles | 61 | 2.27 | 2007 |
| High-Confidence Medical Device Software and Systems | 46 | 26.05 | 2006 |
| Scalable Shape Sculpting via Hole Motion: Motion Planning in Lattice-constrained Modular Robots | 24 | 3.37 | 2006 |
| Claytronics: highly scalable communications, sensing, and actuation networks | 5 | 0.90 | 2005 |
| JVer: a java verifier | 5 | 0.51 | 2005 |
| What are we trying to prove? reflections on experiences with proof-carrying code | 0 | 0.34 | 2003 |
| A Network Protocol Stack in Standard ML | 9 | 0.69 | 2001 |
| A Proof-Carrying Code Architecture for Java | 9 | 0.89 | 2000 |
| A certifying compiler for Java | 93 | 6.77 | 2000 |
| Proof Generation in the Touchstone Theorem Prover | 17 | 1.59 | 2000 |
| How Generic is a Generic Black End? Using MLRISC as a Black End for the TIL Compiler | 0 | 0.34 | 1998 |
| Run-time code generation and modal-ML | 21 | 1.69 | 1998 |
| Safe, Untrusted Agents Using Proof-Carrying Code | 97 | 6.63 | 1998 |
| Modal types as staging specifications for run-time code generation | 17 | 1.93 | 1998 |
| Dynamic specialization in the Fabius system | 18 | 1.16 | 1998 |
| Safe-for-Space Threads in Standard ML | 10 | 0.71 | 1998 |
| The design and implementation of a certifying compiler (with retrospective) | 1 | 0.40 | 1998 |
| Research on Proof-Carrying Code for Untrusted-Code Security | 10 | 0.62 | 1997 |
| Safe kernel extensions without run-time checking | 230 | 51.43 | 1996 |
| Trace-based program analysis | 13 | 0.74 | 1996 |
| Optimizing ML with run-time code generation | 1 | 0.65 | 1996 |
| Research in programming languages for composability, safety, and performance | 0 | 0.34 | 1996 |
| TIL: a type-directed, optimizing compiler for ML (with retrospective) | 1 | 0.40 | 1996 |
| Optimizing ML with run-time code generation (with retrospective) | 0 | 0.34 | 1996 |
| Call-by-need and continuation-passing style | 16 | 1.21 | 1994 |
| Signatures for a network protocol stack: a systems application of Standard ML | 23 | 3.47 | 1994 |
| Lightweight Run-Time Code Generation | 29 | 7.53 | 1994 |
| Cache behavior of combinator graph reduction | 14 | 1.74 | 1992 |
| Visualizing evaluation in applicative languages | 10 | 1.02 | 1992 |
| No assembly required: compiling standard ML to C | 46 | 9.31 | 1992 |
| Metacircularity in the polymorphic &lgr;-calculus | 12 | 1.68 | 1991 |
| Cache Performance of Combinator Graph Reduction. | 6 | 1.38 | 1990 |
| Formal manipulation of modular software systems. | 1 | 0.40 | 1990 |
| Formal manipulation of modular software systems | 1 | 0.40 | 1990 |
| LEAP: A Language with Eval And Polymorphism | 19 | 2.33 | 1989 |
| An automatically generated, realistic compiler for imperative programming language | 2 | 0.42 | 1988 |
