Travelled to:1 × Denmark
1 × Germany
1 × India
14 × USA
2 × Canada
2 × Spain
2 × United Kingdom
Collaborated with:G.C.Necula C.Colby M.Leone U.F.Pleban ∅ R.Harper F.Pfenning P.Cheng S.Magill M.Tsai Y.Tsay A.Bernard S.Paschalakis P.J.K.Jr. A.Chander D.Espinosa N.Islam P.Wickline D.Tarditi J.G.Morrisett C.A.Stone E.Biagioni B.Milnes M.P.Ashley-Rollman S.C.Goldstein P.Pillai J.Campbell S.Chaki J.Ivers K.C.Wallnau N.Zeilberger F.Blau M.Plesko K.Cline
Talks about:generat (8) compil (7) code (7) ml (7) implement (5) certifi (4) proof (4) optim (4) time (4) run (4)
Person: Peter Lee
DBLP: Lee_0001:Peter
Facilitated 3 volumes:
Ed
EdEdContributed to:
20152010
2009
2008
20072005
2005
200220002000
2000
20001998
19981998
1996199619961996
1994
1994
19911989198819871986
1989Wrote 31 papers:
- POPL-2015-Lee
- Coding by Everyone, Every Day (PL), p. 485.
- POPL-2010-MagillTLT #abstraction #automation #source code
- Automatic numeric abstractions for heap-manipulating programs (SM, MHT, PL, YKT), pp. 211–222.
- ICLP-2009-Ashley-RollmanLGPC #independence #scalability
- A Language for Large Ensembles of Independently Executing Nodes (MPAR, PL, SCG, PP, JC), pp. 265–280.
- CAV-2008-MagillTLT #named #reasoning
- THOR: A Tool for Reasoning about Shape and Arithmetic (SM, MHT, PL, YKT), pp. 428–432.
- MoDELS-2007-ChakiILWZ #modelling
- Model-Driven Construction of Certified Binaries (SC, JI, PL, KCW, NZ), pp. 666–681.
- CAV-2005-ChanderEILN #java #named #verification
- JVer: A Java Verifier (AC, DE, NI, PL, GCN), pp. 144–147.
- ESOP-2005-ChanderEILN #bound #dynamic analysis #verification
- Enforcing Resource Bounds via Static Verification of Dynamic Checks (AC, DE, NI, PL, GCN), pp. 311–325.
- CADE-2002-BernardL #logic
- Temporal Logic for Proof-Carrying Code (AB, PL), pp. 31–46.
- CADE-2000-NeculaL #generative #proving #theorem proving
- Proof Generation in the Touchstone Theorem Prover (GCN, PL), pp. 25–44.
- CAV-2000-ColbyLN #architecture #java
- A Proof-Carrying Code Architecture for Java (CC, PL, GCN), pp. 557–560.
- ICPR-v3-2000-PaschalakisL #geometry #image #invariant #recognition
- Combined Geometric Transformation and Illumination Invariant Object Recognition in RGB Color Images (SP, PL), pp. 3588–3591.
- PLDI-2000-ColbyLNBPC #compilation #java
- A certifying compiler for Java (CC, PL, GCN, FB, MP, KC), pp. 95–107.
- Best-of-PLDI-1998-NeculaL98a #compilation #design #implementation
- The design and implementation of a certifying compiler (with retrospective) (GCN, PL), pp. 612–625.
- LICS-1998-NeculaL #performance #proving #representation #validation
- Efficient Representation and Validation of Proofs (GCN, PL), pp. 93–104.
- PLDI-1998-ChengHL #stack
- Generational Stack Collection and Profile-Driven Pretenuring (PC, RH, PL), pp. 162–173.
- PLDI-1998-NeculaL #compilation #design #implementation
- The Design and Implementation of a Certifying Compiler (GCN, PL), pp. 333–344.
- PLDI-1998-WicklineLP #code generation #runtime
- Run-time Code Generation and Modal-ML (PW, PL, FP), pp. 224–235.
- AFP-1996-Lee96 #implementation #ml #standard #thread
- Implementing Threads in Standard ML (PL), pp. 115–130.
- Best-of-PLDI-1996-LeeL96a #code generation #ml #optimisation #runtime
- Optimizing ML with run-time code generation (with retrospective) (PL, ML), pp. 540–553.
- Best-of-PLDI-1996-TarditiMCSHL96a #compilation #ml #named #optimisation
- TIL: a type-directed, optimizing compiler for ML (with retrospective) (DT, JGM, PC, CAS, RH, PL), pp. 554–567.
- PLDI-1996-LeeL #code generation #ml #optimisation #runtime
- Optimizing ML with Run-Time Code Generation (PL, ML), pp. 137–148.
- PLDI-1996-TarditiMCSHL #compilation #ml #named #optimisation
- TIL: A Type-Directed Optimizing Compiler for ML (DT, JGM, PC, CAS, RH, PL), pp. 181–192.
- POPL-1996-ColbyL #program analysis
- Trace-Based Program Analysis (CC, PL), pp. 195–207.
- LFP-1994-BiagioniHLM #ml #network #protocol #stack #standard
- Signatures for a Network Protocol Stack: A Systems Application of Standard ML (EB, RH, PL, BM), pp. 55–64.
- PEPM-1994-LeoneL #code generation #lightweight #runtime
- Lightweight Run-Time Code Generation (ML, PL), pp. 97–106.
- WSA-1991-ColbyL #implementation #partial evaluation
- An Implementation of Parametrized Partial Evaluation (CC, PL), pp. 82–89.
- PLDI-1989-KoopmanL #combinator #fresh look #graph #reduction
- A Fresh Look at Combinator Graph Reduction (PJKJ, PL), pp. 110–119.
- PLDI-1988-PlebanL #automation #compilation #imperative #programming language
- An Automatically Generated, Realistic Compiler for an Imperative Programming Language (UFP, PL), pp. 222–232.
- POPL-1987-LeeP #compilation #generative #semantics
- A Realistic Compiler Generator Based on High-Level Semantics (PL, UFP), pp. 284–295.
- LFP-1986-LeeP #implementation #lisp #on the #semantics #using
- On the Use of LISP in Implementing Denotational Semantics (PL, UFP), pp. 233–248.
- CCIPL-1989-PfenningL #morphism #named #polymorphism
- LEAP: A Language with Eval And Polymorphism (FP, PL), pp. 345–359.