Steve Zdancewic

ORCID

Publication Activity (10 Years)

Years Active: 1999-2024
Publications (10 Years): 52

Top Venues

CoRR

Proc. ACM Program. Lang.

ITP

CPP

Publications

Stephen Mell, Steve Zdancewic, Osbert Bastani
Optimal Program Synthesis via Abstract Interpretation. Proc. ACM Program. Lang. 8 (POPL) (2024)
Calvin Beck, Irene Yoon, Hanxi Chen, Yannick Zakowski, Steve Zdancewic
A Two-Phase Infinite/Finite Low-Level Memory Model. CoRR (2024)
Stephen Mell, Steve Zdancewic, Osbert Bastani
An Opportunistically Parallel Lambda Calculus for Performant Composition of Large Language Models. CoRR (2024)
Nicolas Chappe, Paul He, Ludovic Henrio, Yannick Zakowski, Steve Zdancewic
Choice Trees: Representing Nondeterministic, Recursive, and Impure Programs in Coq. Proc. ACM Program. Lang. 7 (POPL) (2023)
Nick Rioux, Xuejing Huang, Bruno C. d. S. Oliveira, Steve Zdancewic
A Bowtie for a Beast: Overloading, Eta Expansion, and Extensible Data Types in F⋈. Proc. ACM Program. Lang. 7 (POPL) (2023)
Lawrence Dunn, Val Tannen, Steve Zdancewic
Tealeaves: Structured Monads for Generic First-Order Abstract Syntax Infrastructure. ITP (2023)
Lawrence Dunn, Val Tannen, Steve Zdancewic
Syntax Monads for the Working Formal Metatheorist. CoRR (2023)
Lucas Silver, Paul He, Ethan Cecchetti, Andrew K. Hirsch, Steve Zdancewic
Semantics for Noninterference with Interaction Trees. ECOOP (2023)
Lucas Silver, Paul He, Ethan Cecchetti, Andrew K. Hirsch, Steve Zdancewic
Semantics for Noninterference with Interaction Trees (Artifact). Dagstuhl Artifacts Ser. 9 (2) (2023)
Stephen Mell, Favyen Bastani, Steve Zdancewic, Osbert Bastani
Synthesizing Trajectory Queries from Examples. CAV (1) (2023)
Stephen Mell, Osbert Bastani, Steve Zdancewic
Ideograph: A Language for Expressing and Manipulating Structured Data. CoRR (2023)
George Tolkachev, Stephen Mell, Steve Zdancewic, Osbert Bastani
Counterfactual Explanations for Natural Language Interfaces. ACL (2) (2022)
Nicolas Chappe, Paul He, Ludovic Henrio, Yannick Zakowski, Steve Zdancewic
Choice Trees: Representing Nondeterministic, Recursive, and Impure Programs in Coq. CoRR (2022)
Mohsen Lesani, Li-yao Xia, Anders Kaseorg, Christian J. Bell, Adam Chlipala, Benjamin C. Pierce, Steve Zdancewic
C4: verified transactional objects. Proc. ACM Program. Lang. 6 (OOPSLA) (2022)
George Tolkachev, Stephen Mell, Steve Zdancewic, Osbert Bastani
Counterfactual Explanations for Natural Language Interfaces. CoRR (2022)
Irene Yoon, Yannick Zakowski, Steve Zdancewic
Formal reasoning about layered monadic interpreters. Proc. ACM Program. Lang. 6 (ICFP) (2022)
Hengchu Zhang, Wolf Honoré, Nicolas Koh, Yao Li, Yishuai Li, Li-yao Xia, Lennart Beringer, William Mansky, Benjamin C. Pierce, Steve Zdancewic
Verifying an HTTP Key-Value Server with Interaction Trees and VST. ITP (2021)
Yishuai Li, Benjamin C. Pierce, Steve Zdancewic
Model-based testing of networked applications. ISSTA (2021)
Paul He, Eddy Westbrook, Brent Carmer, Chris Phifer, Valentin Robert, Karl Smeltzer, Andrei Stefanescu, Aaron Tomb, Adam Wick, Matthew Yacavone, Steve Zdancewic
A type system for extracting functional specifications from memory-safe imperative programs. Proc. ACM Program. Lang. 5 (OOPSLA) (2021)
Yannick Zakowski, Calvin Beck, Irene Yoon, Ilia Zaichuk, Vadim Zaliva, Steve Zdancewic
Modular, compositional, and executable formal semantics for LLVM IR. Proc. ACM Program. Lang. 5 (ICFP) (2021)
Yishuai Li, Benjamin C. Pierce, Steve Zdancewic
Model-Based Testing of Networked Applications. CoRR (2021)
Lucas Silver, Steve Zdancewic
Dijkstra monads forever: termination-sensitive specifications for interaction trees. Proc. ACM Program. Lang. 5 (POPL) (2021)
Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce, Steve Zdancewic
Interaction trees: representing recursive and impure programs in Coq. Proc. ACM Program. Lang. 4 (POPL) (2020)
Nick Rioux, Steve Zdancewic
Computation focusing. Proc. ACM Program. Lang. 4 (ICFP) (2020)
Yannick Zakowski, Paul He, Chung-Kil Hur, Steve Zdancewic
An equational theory for weak bisimulation via generalized parameterized coinduction. CPP (2020)
Yannick Zakowski, Paul He, Chung-Kil Hur, Steve Zdancewic
An Equational Theory for Weak Bisimulation via Generalized Parameterized Coinduction. CoRR (2020)
Jennifer Paykin, Steve Zdancewic
A HoTT Quantum Equational Theory (Extended Version). CoRR (2019)
Marcella Hastings, Brett Hemenway, Daniel Noble, Steve Zdancewic
SoK: General Purpose Compilers for Secure Multi-Party Computation. IEEE Symposium on Security and Privacy (2019)
Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce, Steve Zdancewic
Interaction Trees: Representing Recursive and Impure Programs in Coq (Work In Progress). CoRR (2019)
Anders Miltner, Solomon Maina, Kathleen Fisher, Benjamin C. Pierce, David Walker, Steve Zdancewic
Synthesizing symmetric lenses. Proc. ACM Program. Lang. 3 (ICFP) (2019)
Nicolas Koh, Yao Li, Yishuai Li, Li-yao Xia, Lennart Beringer, Wolf Honoré, William Mansky, Benjamin C. Pierce, Steve Zdancewic
From C to interaction trees: specifying, verifying, and testing a networked server. CPP (2019)
Robert Rand, Jennifer Paykin, Dong-Ho Lee, Steve Zdancewic
ReQWIRE: Reasoning about Reversible Quantum Circuits. QPL (2018)
Nicolas Koh, Yao Li, Yishuai Li, Li-yao Xia, Lennart Beringer, Wolf Honoré, William Mansky, Benjamin C. Pierce, Steve Zdancewic
From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server. CoRR (2018)
Christine Rizkallah, Dmitri Garbuzov, Steve Zdancewic
A Formal Equational Theory for Call-By-Push-Value. ITP (2018)
Anders Miltner, Solomon Maina, Kathleen Fisher, Benjamin C. Pierce, David Walker, Steve Zdancewic
Synthesizing Symmetric Lenses. CoRR (2018)
Dmitri Garbuzov, William Mansky, Christine Rizkallah, Steve Zdancewic
Structural Operational Semantics for Control Flow Graph Machines. CoRR (2018)
Anders Miltner, Kathleen Fisher, Benjamin C. Pierce, David Walker, Steve Zdancewic
Synthesizing bijective lenses. Proc. ACM Program. Lang. 2 (POPL) (2018)
Jennifer Paykin, Steve Zdancewic
A linear/producer/consumer model of classical linear logic. Math. Struct. Comput. Sci. 28 (5) (2018)
Steve Zdancewic
Technical perspective: Building bug-free compilers. Commun. ACM 61 (2) (2018)
Solomon Maina, Anders Miltner, Kathleen Fisher, Benjamin C. Pierce, David Walker, Steve Zdancewic
Synthesizing quotient lenses. Proc. ACM Program. Lang. 2 (ICFP) (2018)
Jennifer Paykin, Robert Rand, Steve Zdancewic
QWIRE: a core language for quantum circuits. POPL (2017)
Robert Rand, Jennifer Paykin, Steve Zdancewic
QWIRE Practice: Formal Verification of Quantum Circuits in Coq. QPL (2017)
William Mansky, Yuanfeng Peng, Steve Zdancewic, Joseph Devietti
Verifying dynamic race detection. CPP (2017)
Jennifer Paykin, Steve Zdancewic
The linearity Monad. Haskell (2017)
Anders Miltner, Kathleen Fisher, Benjamin C. Pierce, David Walker, Steve Zdancewic
Synthesizing Bijective Lenses. CoRR (2017)
Jennifer Paykin, Steve Zdancewic
Linear λμ is CP (more or less). A List of Successes That Can Change the World (2016)
Jonathan Frankle, Peter-Michael Osera, David Walker, Steve Zdancewic
Example-directed synthesis: a type-theoretic interpretation. POPL (2016)
Robert Rand, Steve Zdancewic
VPHL: A Verified Partial-Correctness Logic for Probabilistic Programs. MFPS (2015)
Jeehoon Kang, Chung-Kil Hur, William Mansky, Dmitri Garbuzov, Steve Zdancewic, Viktor Vafeiadis
A formal C memory model supporting integer-pointer casts. PLDI (2015)
William Mansky, Dmitri Garbuzov, Steve Zdancewic
An Axiomatic Specification for Sequential Memory Models. CAV (2) (2015)
Santosh Nagarakatte, Milo M. K. Martin, Steve Zdancewic
Everything You Want to Know About Pointer-Based Checking. SNAPL (2015)
Peter-Michael Osera, Steve Zdancewic
Type-and-example-directed program synthesis. PLDI (2015)
Santosh Nagarakatte, Milo M. K. Martin, Steve Zdancewic
WatchdogLite: Hardware-Accelerated Compiler-Based Pointer Checking. CGO (2014)
Benoît Valiron, Steve Zdancewic
Finite Vector Spaces as Model of Simply-Typed Lambda-Calculi. ICTAC (2014)
Benoît Valiron, Steve Zdancewic
Modeling Simply-Typed Lambda Calculi in the Category of Finite Vector Spaces. Sci. Ann. Comput. Sci. 24 (2) (2014)
Aloïs Brunel, Marco Gaboardi, Damiano Mazza, Steve Zdancewic
A Core Quantitative Coeffect Calculus. ESOP (2014)
Benoît Valiron, Steve Zdancewic
Finite Vector Spaces as Model of Simply-Typed Lambda-Calculi. CoRR (2014)
Jennifer Paykin, Steve Zdancewic
A Linear/Producer/Consumer Model of Classical Linear Logic. LINEARITY (2014)
Jianzhou Zhao, Santosh Nagarakatte, Milo M. K. Martin, Steve Zdancewic
Formal verification of SSA-based optimizations for LLVM. PLDI (2013)
Christian DeLozier, Richard A. Eisenberg, Santosh Nagarakatte, Peter-Michael Osera, Milo M. K. Martin, Steve Zdancewic
Ironclad C++: a library-augmented type-safe subset of c++. OOPSLA (2013)
Santosh Nagarakatte, Milo M. K. Martin, Steve Zdancewic
Hardware-Enforced Comprehensive Memory Safety. IEEE Micro 33 (3) (2013)
Jianzhou Zhao, Santosh Nagarakatte, Milo M. K. Martin, Steve Zdancewic
Formalizing the LLVM intermediate representation for verified program transformations. POPL (2012)
Santosh Nagarakatte, Milo M. K. Martin, Steve Zdancewic
Watchdog: Hardware for safe and secure manual memory management and full memory safety. ISCA (2012)
Jianzhou Zhao, Steve Zdancewic
Mechanized Verification of Computing Dominators for Formalizing Compilers. CPP (2012)
Peter-Michael Osera, Vilhelm Sjöberg, Steve Zdancewic
Dependent interoperability. PLPV (2012)
Stephanie Weirich, Dimitrios Vytiniotis, Simon L. Peyton Jones, Steve Zdancewic
Generative type abstraction and type-level computation. POPL (2011)
Karl Mazurak, Steve Zdancewic
Lolliproc: to concurrency from classical linear logic via curry-howard and control. ICFP (2010)
Santosh Nagarakatte, Jianzhou Zhao, Milo M. K. Martin, Steve Zdancewic
CETS: compiler enforced temporal safety for C. ISMM (2010)
Karl Mazurak, Jianzhou Zhao, Steve Zdancewic
Lightweight linear types in system fdegree. TLDI (2010)
Peng Li, Steve Zdancewic
Arrows for secure information flow. Theor. Comput. Sci. 411 (19) (2010)
Jianzhou Zhao, Qi Zhang, Steve Zdancewic
Relational Parametricity for a Polymorphic Linear Lambda Calculus. APLAS (2010)
Michael J. May, Carl A. Gunter, Insup Lee, Steve Zdancewic
Strong and Weak Policy Relations. POLICY (2009)
Jim Allen, Zena M. Ariola, Pierre-Louis Curien, Matthew Fluet, Jeffrey S. Foster, Dan Grossman, Robert Harper, Hugo Herbelin, Yannis Smaragdakis, David Walker, Steve Zdancewic
An overview of the Oregon programming languages summer school. ACM SIGPLAN Notices 44 (11) (2009)
Limin Jia, Steve Zdancewic
Encoding information flow in Aura. PLAS (2009)
J. Nathan Foster, Benjamin C. Pierce, Steve Zdancewic
Updatable Security Views. CSF (2009)
Santosh Nagarakatte, Jianzhou Zhao, Milo M. K. Martin, Steve Zdancewic
SoftBound: highly compatible and complete spatial memory safety for c. PLDI (2009)
Aaron Bohannon, Benjamin C. Pierce, Vilhelm Sjöberg, Stephanie Weirich, Steve Zdancewic
Reactive noninterference. CCS (2009)
Joe Devietti, Colin Blundell, Milo M. K. Martin, Steve Zdancewic
Hardbound: architectural support for spatial safety of the C programming language. ASPLOS (2008)
Limin Jia, Jeffrey A. Vaughan, Karl Mazurak, Jianzhou Zhao, Luke Zarko, Joseph Schorr, Steve Zdancewic
AURA: a programming language for authorization and audit. ICFP (2008)
Jeffrey A. Vaughan, Limin Jia, Karl Mazurak, Steve Zdancewic
Evidence-Based Audit. CSF (2008)
Pierpaolo Degano, Ralf Küsters, Luca Viganò, Steve Zdancewic
Joint workshop on foundations of computer security and automated reasoning for security protocol analysis (FCS-ARSPA '06). Inf. Comput. 206 (2-4) (2008)
Jeffrey A. Vaughan, Steve Zdancewic
A Cryptographic Decentralized Label Model. IEEE Symposium on Security and Privacy (2007)
Steve Zdancewic
Application-level concurrency: combining events and treads: invited talk. DAMP (2007)
Peng Li, Steve Zdancewic
Combining events and threads for scalable network services implementation and evaluation of monadic, application-level concurrency primitives. PLDI (2007)
Stephen Tse, Steve Zdancewic
Run-time principals in information-flow type systems. ACM Trans. Program. Lang. Syst. 30 (1) (2007)
Jay Ligatti, David Walker, Steve Zdancewic
A type-theoretic interpretation of pointcuts and advice. Sci. Comput. Program. 63 (3) (2006)
Rajeev Alur, Pavol Cerný, Steve Zdancewic
Preserving Secrecy Under Refinement. ICALP (2) (2006)
Peng Li, Steve Zdancewic
Encoding Information Flow in Haskell. CSFW (2006)
Andrew C. Myers, Andrei Sabelfeld, Steve Zdancewic
Enforcing Robust Declassification and Qualified Robustness. J. Comput. Secur. 14 (2) (2006)
Nikhil Swamy, Michael Hicks, Stephen Tse, Steve Zdancewic
Managing Policy Updates in Security-Typed Languages. CSFW (2006)
Brian E. Aydemir, Aaron Bohannon, Matthew Fairbairn, J. Nathan Foster, Benjamin C. Pierce, Peter Sewell, Dimitrios Vytiniotis, Geoffrey Washburn, Stephanie Weirich, Steve Zdancewic
Mechanized Metatheory for the Masses: The PoplMark Challenge. TPHOLs (2005)
Benjamin C. Pierce, Peter Sewell, Stephanie Weirich, Steve Zdancewic
It Is Time to Mechanize Programming Language Metatheory. VSTTE (2005)
Peng Li, Steve Zdancewic
Practical Information-flow Control in Web-Based Information Systems. CSFW (2005)
Peng Li, Steve Zdancewic
Downgrading policies and relaxed noninterference. POPL (2005)
Stephen Tse, Steve Zdancewic
A Design for a Security-Typed Language with Certificate-Based Declassification. ESOP (2005)
Peng Li, Steve Zdancewic
Advanced control flow in Java card programming. LCTES (2004)
Stephen Tse, Steve Zdancewic
Run-time Principals in Information-flow Type Systems. IEEE Symposium on Security and Privacy (2004)
Stephen Tse, Steve Zdancewic
Translating dependency into parametricity. ICFP (2004)
Andrew C. Myers, Andrei Sabelfeld, Steve Zdancewic
Enforcing Robust Declassification. CSFW (2004)
David Walker, Steve Zdancewic, Jay Ligatti
A theory of aspects. ICFP (2003)

Steve Zdancewic.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Steve Zdancewic