On the Use of LISP in Implementing Denotational Semantics. - Peter Lee 001; Uwe F. Pleban (LISP and Functional Programming, 1986)

High-Level Semantics: An Integrated Approach to Programming Language Semantics and the Specification of Implementations. - Uwe F. Pleban; Peter Lee 001 (MFPS, 1987)

A Realistic Compiler Generator Based on High-Level Semantics. - Peter Lee 001; Uwe F. Pleban (POPL, 1987)

An Automatically Generated, Realistic Compiler for an Imperative Programming Language. - Uwe F. Pleban; Peter Lee 001 (PLDI, 1988)

The Ergo Support System: An Integrated Set of Tools for Prototyping Integrated Environments. - Peter Lee 001; Frank Pfenning; Gene Rollins; William L. Scherlis (Software Development Environments (SDE), 1988)

Realistic compiler generation. - Peter Lee 001 (MIT Press, 1989)

A Fresh Look at Combinator Graph Reduction. - Philip J. Koopman Jr.; Peter Lee 001 (PLDI, 1989)

LEAP: A Language with Eval And Polymorphism. - Frank Pfenning; Peter Lee 001 (TAPSOFT, Vol.2, 1989)

Formal manipulation of modular software systems. - Robert L. Nord; Peter Lee 001; William L. Scherlis (Formal Methods in Software Development, 1990)

Cache Performance of Combinator Graph Reduction. - Philip J. Koopman Jr.; Peter Lee 001; Daniel P. Siewiorek (ICCL, 1990)

An Implementation of Parametrized Partial Evaluation. - Christopher Colby; Peter Lee 001 (JTASPEFT/WSA, 1991)

Metacircularity in the Polymorphic lambda-Calculus. - Frank Pfenning; Peter Lee 001 (Theor. Comput. Sci., 1991)

Visualizing Evaluation in Applicative Languages. - David S. Touretzky; Peter Lee 001 (Commun. ACM, 1992)

No Assembly Required: Compiling Standard ML to C. - David Tarditi; Peter Lee 001; Anurag Acharya 001 (LOPLAS, 1992)

Cache Behavior of Combinator Graph Reduction. - Philip J. Koopman Jr.; Peter Lee 001; Daniel P. Siewiorek (ACM Trans. Program. Lang. Syst., 1992)

Signatures for a Network Protocol Stack: A Systems Application of Standard ML. - Edoardo Biagioni; Robert Harper 001; Peter Lee 001; Brian Milnes (LISP and Functional Programming, 1994)

Lightweight Run-Time Code Generation. - Mark Leone; Peter Lee 001 (PEPM, 1994)

Call-by-Need and Continuation-Passing Style. - Chris Okasaki; Peter Lee 001; David Tarditi (LISP Symb. Comput., 1994)

An FPGA Prototype for a Multiplierless FIR Filter Built Using the Logarithmic Number System. - Peter Lee 001 (FPL, 1995)

Implementing Threads in Standard ML. - Peter Lee 001 (Advanced Functional Programming, 1996)

Safe Kernel Extensions Without Run-Time Checking. - George C. Necula; Peter Lee 001 (OSDI, 1996)

Optimizing ML with Run-Time Code Generation. - Peter Lee 001; Mark Leone (PLDI, 1996)

Optimizing ML with run-time code generation (with retrospective) - Peter Lee 001; Mark Leone (Best of PLDI, 1996)

TIL: A Type-Directed Optimizing Compiler for ML. - David Tarditi; J. Gregory Morrisett; Perry Cheng; Christopher A. Stone; Robert Harper 001; Peter Lee 001 (PLDI, 1996)

TIL: a type-directed, optimizing compiler for ML (with retrospective) - David Tarditi; J. Gregory Morrisett; Perry Cheng; Christopher A. Stone; Robert Harper 001; Peter Lee 001 (Best of PLDI, 1996)

Trace-Based Program Analysis. - Christopher Colby; Peter Lee 001 (POPL, 1996)

Research in Programming Languages for Composability, Safety, and Performance. - Robert Harper 001; Peter Lee 001 (ACM Comput. Surv., 1996)

Benchmarking Implementations of Functional Languages with 'Pseudoknot', a Float-Intensive Benchmark. - Pieter H. Hartel; Marc Feeley; Martin Helmut Alt; Lennart Augustsson; Peter Baumann; Marcel Beemster; Emmanuel Chailloux; Christine H. Flood; Wolfgang Grieskamp; John H. G. van Groningen; Kevin Hammond; Bogumil Hausman; et al. (J. Funct. Program., 1996)

Research on Proof-Carrying Code for Untrusted-Code Security. - George C. Necula; Peter Lee 001 (S&P, 1997)

Efficient Representation and Validation of Proofs. - George C. Necula; Peter Lee 001 (LICS, 1998)

Safe, Untrusted Agents Using Proof-Carrying Code. - George C. Necula; Peter Lee 001 (Mobile Agents and Security, 1998)

Generational Stack Collection and Profile-Driven Pretenuring. - Perry Cheng; Robert Harper 001; Peter Lee 001 (PLDI, 1998)

The Design and Implementation of a Certifying Compiler. - George C. Necula; Peter Lee 001 (PLDI, 1998)

The design and implementation of a certifying compiler (with retrospective) - George C. Necula; Peter Lee 001 (Best of PLDI, 1998)

Run-time Code Generation and Modal-ML. - Philip Wickline; Peter Lee 001; Frank Pfenning (PLDI, 1998)

Certifying, Optimizing Compilation (Abstract). - Peter Lee 001 (SAS, 1998)

How Generic is a Generic Black End? Using MLRISC as a Black End for the TIL Compiler. - Andrew Bernard; Robert Harper 001; Peter Lee 001 (Types in Compilation, 1998)

Dynamic Specialization in the Fabius System. - Mark Leone; Peter Lee 001 (ACM Comput. Surv., 1998)

Modal Types as Staging Specifications for Run-Time Code Generation. - Philip Wickline; Peter Lee 001; Frank Pfenning; Rowan Davies (ACM Comput. Surv., 1998)

Safe-for-Space Threads in Standard ML. - Edoardo Biagioni; Kenneth Cline; Peter Lee 001; Chris Okasaki; Christopher A. Stone (High. Order Symb. Comput., 1998)

SIGPLAN Supports Your Professional Activities. - Peter Lee 001 (ACM SIGPLAN Notices, 1998)

Proof Generation in the Touchstone Theorem Prover. - George C. Necula; Peter Lee 001 (CADE, 2000)

A Proof-Carrying Code Architecture for Java. - Christopher Colby; Peter Lee 001; George C. Necula (CAV, 2000)

Production-Quality Proof-Carrying Code. - Peter Lee 001 (PADL, 2000)

A certifying compiler for Java. - Christopher Colby; Peter Lee 001; George C. Necula; Fred Blau; Mark Plesko; Kenneth Cline (PLDI, 2000)

A Network Protocol Stack in Standard ML. - Edoardo Biagioni; Robert Harper 001; Peter Lee 001 (High. Order Symb. Comput., 2001)

Temporal Logic for Proof-Carrying Code. - Andrew Bernard; Peter Lee 001 (CADE, 2002)

What Are We Trying to Prove? Reflections on Experiences with Proof-Carrying Code. - Peter Lee 001 (TACAS, 2003)

Automated techniques for provably safe mobile code. - Christopher Colby; Karl Crary; Robert Harper 001; Peter Lee 001; Frank Pfenning (Theor. Comput. Sci., 2003)

JVer: A Java Verifier. - Ajay Chander; David Espinosa; Nayeem Islam; Peter Lee 001; George C. Necula (CAV, 2005)

An evaluation of a hybrid-logarithmic number system DCT/IDCT algorithm [image compression applications]. - Peter Lee 001 (ISCAS (5), 2005)

Claytronics: highly scalable communications, sensing, and actuation networks. - Burak Aksak; Preethi Srinivas Bhat; Jason Campbell; Michael DeRosa; Stanislav Funiak; Phillip B. Gibbons; Seth Copen Goldstein; Carlos Guestrin; Ashish Gupta 003; Casey Helfrich; James F. Hoburg; Brian T. Kirby; et al. (SenSys, 2005)

Scalable Shape Sculpting via Hole Motion: Motion Planning in Lattice-constrained Modular Robots. - Michael DeRosa; Seth Copen Goldstein; Peter Lee 001; Jason Campbell; Padmanabhan Pillai (ICRA, 2006)

High-Confidence Medical Device Software and Systems. - Insup Lee 001; George J. Pappas; Rance Cleaveland; John Hatcliff; Bruce H. Krogh; Peter Lee 001; Harvey Rubin; Lui Sha (Computer, 2006)

Distributed Watchpoints: Debugging Large Multi-Robot Systems. - Michael DeRosa; Jason Campbell; Padmanabhan Pillai; Seth Copen Goldstein; Peter Lee 001; Todd C. Mowry (ICRA, 2007)

Meld: A declarative approach to programming ensembles. - Michael P. Ashley-Rollman; Seth Copen Goldstein; Peter Lee 001; Todd C. Mowry; Padmanabhan Pillai (IROS, 2007)

Model-Driven Construction of Certified Binaries. - Sagar Chaki; James Ivers; Peter Lee 001; Kurt C. Wallnau; Noam Zeilberger (MoDELS, 2007)

Enforcing resource bounds via static verification of dynamic checks. - Ajay Chander; David Espinosa; Nayeem Islam; Peter Lee 001; George C. Necula (ACM Trans. Program. Lang. Syst., 2007)

THOR: A Tool for Reasoning about Shape and Arithmetic. - Stephen Magill; Ming-Hsien Tsai 001; Peter Lee 001; Yih-Kuen Tsay (CAV, 2008)

Programming modular robots with locally distributed predicates. - Michael DeRosa; Seth Copen Goldstein; Peter Lee 001; Padmanabhan Pillai; Jason Campbell (ICRA, 2008)

Distributed Watchpoints: Debugging Large Modular Robot Systems. - Michael DeRosa; Seth Copen Goldstein; Peter Lee 001; Jason Campbell; Padmanabhan Pillai (Int. J. Robotics Res., 2008)

A Language for Large Ensembles of Independently Executing Nodes. - Michael P. Ashley-Rollman; Peter Lee 001; Seth Copen Goldstein; Padmanabhan Pillai; Jason Campbell (ICLP, 2009)

A tale of two planners: Modular robotic planning with LDP. - Michael DeRosa; Seth Copen Goldstein; Peter Lee 001; Padmanabhan Pillai; Jason Campbell (IROS, 2009)

Beyond Audio and Video: Using Claytronics to Enable Pario. - Seth Copen Goldstein; Todd C. Mowry; Jason Campbell; Michael P. Ashley-Rollman; Michael DeRosa; Stanislav Funiak; James F. Hoburg; Mustafa Emre Karagozler; Brian T. Kirby; Peter Lee 001; Padmanabhan Pillai; James Robert Reid; et al. (AI Mag., 2009)

Automatic numeric abstractions for heap-manipulating programs. - Stephen Magill; Ming-Hsien Tsai 001; Peter Lee 001; Yih-Kuen Tsay (POPL, 2010)

Detecting Locally Distributed Predicates. - Michael DeRosa; Seth Copen Goldstein; Peter Lee 001; Jason Campbell; Padmanabhan Pillai (ACM Trans. Auton. Adapt. Syst., 2011)

The fox and the hedgehog: technical perspective. - Peter Lee 001 (Commun. ACM, 2012)

Coding by Everyone, Every Day. - Peter Lee 001 (POPL, 2015)