Principals in Programming Languages: A Syntactic Proof Technique. - Steve Zdancewic; Dan Grossman; J. Gregory Morrisett (ICFP, 1999)

Syntactic type abstraction. - Dan Grossman; J. Gregory Morrisett; Steve Zdancewic (ACM Trans. Program. Lang. Syst., 2000)

Robust Declassification. - Steve Zdancewic; Andrew C. Myers (CSFW, 2001)

Secure Information Flow and CPS. - Steve Zdancewic; Andrew C. Myers (ESOP, 2001)

Untrusted Hosts and Confidentiality: Secure Program Partitioning. - Steve Zdancewic; Lantian Zheng; Nathaniel Nystrom; Andrew C. Myers (SOSP, 2001)

Secure Information Flow via Linear Continuations. - Steve Zdancewic; Andrew C. Myers (High. Order Symb. Comput., 2002)

Secure program partitioning. - Steve Zdancewic; Lantian Zheng; Nathaniel Nystrom; Andrew C. Myers (ACM Trans. Comput. Syst., 2002)

Programming Languages for Information Security. - Steve Zdancewic (2002)

Observational Determinism for Concurrent Program Security. - Steve Zdancewic; Andrew C. Myers (CSFW, 2003)

A theory of aspects. - David Walker 001; Steve Zdancewic; Jay Ligatti (ICFP, 2003)

A Type System for Robust Declassification. - Steve Zdancewic (MFPS, 2003)

Using Replication and Partitioning to Build Secure Distributed Systems. - Lantian Zheng; Stephen Chong; Andrew C. Myers; Steve Zdancewic (S&P, 2003)

Formalizing Java-MaC. - Usa Sammapun; Raman Sharykin; Margaret DeLap; Myong Kim; Steve Zdancewic (RV@CAV, 2003)

Enforcing Robust Declassification. - Andrew C. Myers; Andrei Sabelfeld; Steve Zdancewic (CSFW, 2004)

Translating dependency into parametricity. - Stephen Tse; Steve Zdancewic (ICFP, 2004)

Advanced control flow in Java card programming. - Peng Li; Steve Zdancewic (LCTES, 2004)

Practical Information-flow Control in Web-Based Information Systems. - Peng Li; Steve Zdancewic (CSFW, 2005)

A Design for a Security-Typed Language with Certificate-Based Declassification. - Stephen Tse; Steve Zdancewic (ESOP, 2005)

Downgrading policies and relaxed noninterference. - Peng Li; Steve Zdancewic (POPL, 2005)

Mechanized Metatheory for the Masses: The PoplMark Challenge. - Brian E. Aydemir; Aaron Bohannon; Matthew Fairbairn; J. Nathan Foster; Benjamin C. Pierce; Peter Sewell; Dimitrios Vytiniotis; Geoffrey Washburn; Stephanie Weirich; Steve Zdancewic (TPHOLs, 2005)

It Is Time to Mechanize Programming Language Metatheory. - Benjamin C. Pierce; Peter Sewell; Stephanie Weirich; Steve Zdancewic (VSTTE, 2005)

Encoding Information Flow in Haskell. - Peng Li; Steve Zdancewic (CSFW, 2006)

Managing Policy Updates in Security-Typed Languages. - Nikhil Swamy; Michael Hicks 001; Stephen Tse; Steve Zdancewic (CSFW, 2006)

Preserving Secrecy Under Refinement. - Rajeev Alur; Pavol Cerný; Steve Zdancewic (ICALP (2), 2006)

Enforcing Robust Declassification and Qualified Robustness. - Andrew C. Myers; Andrei Sabelfeld; Steve Zdancewic (J. Comput. Secur., 2006)

A type-theoretic interpretation of pointcuts and advice. - Jay Ligatti; David Walker 001; Steve Zdancewic (Sci. Comput. Program., 2006)

Combining events and threads for scalable network services implementation and evaluation of monadic, application-level concurrency primitives. - Peng Li; Steve Zdancewic (PLDI, 2007)

Application-level concurrency: combining events and treads: invited talk. - Steve Zdancewic (DAMP, 2007)

A Cryptographic Decentralized Label Model. - Jeffrey A. Vaughan; Steve Zdancewic (S&P, 2007)

Run-time principals in information-flow type systems. - Stephen Tse; Steve Zdancewic (ACM Trans. Program. Lang. Syst., 2007)

Hardbound: architectural support for spatial safety of the C programming language. - Joe Devietti; Colin Blundell; Milo M. K. Martin; Steve Zdancewic (ASPLOS, 2008)

Evidence-Based Audit. - Jeffrey A. Vaughan; Limin Jia 001; Karl Mazurak; Steve Zdancewic (CSF, 2008)

AURA: a programming language for authorization and audit. - Limin Jia 001; Jeffrey A. Vaughan; Karl Mazurak; Jianzhou Zhao; Luke Zarko; Joseph Schorr; Steve Zdancewic (ICFP, 2008)

Joint workshop on foundations of computer security and automated reasoning for security protocol analysis (FCS-ARSPA '06). - Pierpaolo Degano; Ralf Küsters; Luca Viganò 001; Steve Zdancewic (Inf. Comput., 2008)

Reactive noninterference. - Aaron Bohannon; Benjamin C. Pierce; Vilhelm Sjöberg; Stephanie Weirich; Steve Zdancewic (CCS, 2009)

Updatable Security Views. - J. Nathan Foster; Benjamin C. Pierce; Steve Zdancewic (CSF, 2009)

Encoding information flow in Aura. - Limin Jia 001; Steve Zdancewic (PLAS, 2009)

SoftBound: highly compatible and complete spatial memory safety for c. - Santosh Nagarakatte; Jianzhou Zhao; Milo M. K. Martin; Steve Zdancewic (PLDI, 2009)

Strong and Weak Policy Relations. - Michael J. May; Carl A. Gunter; Insup Lee 001; Steve Zdancewic (POLICY, 2009)

An overview of the Oregon programming languages summer school. - Jim Allen; Zena M. Ariola; Pierre-Louis Curien; Matthew Fluet; Jeffrey S. Foster; Dan Grossman; Robert Harper 001; Hugo Herbelin; Yannis Smaragdakis; David Walker 001; Steve Zdancewic (ACM SIGPLAN Notices, 2009)

Relational Parametricity for a Polymorphic Linear Lambda Calculus. - Jianzhou Zhao; Qi Zhang; Steve Zdancewic (APLAS, 2010)

Lolliproc: to concurrency from classical linear logic via curry-howard and control. - Karl Mazurak; Steve Zdancewic (ICFP, 2010)

CETS: compiler enforced temporal safety for C. - Santosh Nagarakatte; Jianzhou Zhao; Milo M. K. Martin; Steve Zdancewic (ISMM, 2010)

Lightweight linear types in system fdegree. - Karl Mazurak; Jianzhou Zhao; Steve Zdancewic (TLDI, 2010)

Arrows for secure information flow. - Peng Li; Steve Zdancewic (Theor. Comput. Sci., 2010)

Generative type abstraction and type-level computation. - Stephanie Weirich; Dimitrios Vytiniotis; Simon L. Peyton Jones; Steve Zdancewic (POPL, 2011)

Mechanized Verification of Computing Dominators for Formalizing Compilers. - Jianzhou Zhao; Steve Zdancewic (CPP, 2012)

Watchdog: Hardware for safe and secure manual memory management and full memory safety. - Santosh Nagarakatte; Milo M. K. Martin; Steve Zdancewic (ISCA, 2012)

Dependent interoperability. - Peter-Michael Osera; Vilhelm Sjöberg; Steve Zdancewic (PLPV, 2012)

Formalizing the LLVM intermediate representation for verified program transformations. - Jianzhou Zhao; Santosh Nagarakatte; Milo M. K. Martin; Steve Zdancewic (POPL, 2012)

Ironclad C++: a library-augmented type-safe subset of c++. - Christian DeLozier; Richard A. Eisenberg; Santosh Nagarakatte; Peter-Michael Osera; Milo M. K. Martin; Steve Zdancewic (OOPSLA, 2013)

Formal verification of SSA-based optimizations for LLVM. - Jianzhou Zhao; Santosh Nagarakatte; Milo M. K. Martin; Steve Zdancewic (PLDI, 2013)

Hardware-Enforced Comprehensive Memory Safety. - Santosh Nagarakatte; Milo M. K. Martin; Steve Zdancewic (IEEE Micro, 2013)

WatchdogLite: Hardware-Accelerated Compiler-Based Pointer Checking. - Santosh Nagarakatte; Milo M. K. Martin; Steve Zdancewic (CGO, 2014)

A Core Quantitative Coeffect Calculus. - Aloïs Brunel; Marco Gaboardi; Damiano Mazza; Steve Zdancewic (ESOP, 2014)

Finite Vector Spaces as Model of Simply-Typed Lambda-Calculi. - Benoît Valiron; Steve Zdancewic (ICTAC, 2014)

A Linear/Producer/Consumer Model of Classical Linear Logic. - Jennifer Paykin; Steve Zdancewic (LINEARITY, 2014)

Modeling Simply-Typed Lambda Calculi in the Category of Finite Vector Spaces. - Benoît Valiron; Steve Zdancewic (Sci. Ann. Comput. Sci., 2014)

An Axiomatic Specification for Sequential Memory Models. - William Mansky; Dmitri Garbuzov; Steve Zdancewic (CAV (2), 2015)

A formal C memory model supporting integer-pointer casts. - Jeehoon Kang; Chung-Kil Hur; William Mansky; Dmitri Garbuzov; Steve Zdancewic; Viktor Vafeiadis (PLDI, 2015)

Type-and-example-directed program synthesis. - Peter-Michael Osera; Steve Zdancewic (PLDI, 2015)

Everything You Want to Know About Pointer-Based Checking. - Santosh Nagarakatte; Milo M. K. Martin; Steve Zdancewic (SNAPL, 2015)

VPHL: A Verified Partial-Correctness Logic for Probabilistic Programs. - Robert Rand 001; Steve Zdancewic (MFPS, 2015)

Linear λμ is CP (more or less). - Jennifer Paykin; Steve Zdancewic (A List of Successes That Can Change the World, 2016)

Example-directed synthesis: a type-theoretic interpretation. - Jonathan Frankle; Peter-Michael Osera; David Walker 001; Steve Zdancewic (POPL, 2016)

Verifying dynamic race detection. - William Mansky; Yuanfeng Peng; Steve Zdancewic; Joseph Devietti (CPP, 2017)

The linearity Monad. - Jennifer Paykin; Steve Zdancewic (Haskell, 2017)

QWIRE: a core language for quantum circuits. - Jennifer Paykin; Robert Rand 001; Steve Zdancewic (POPL, 2017)

QWIRE Practice: Formal Verification of Quantum Circuits in Coq. - Robert Rand 001; Jennifer Paykin; Steve Zdancewic (QPL, 2017)

A Formal Equational Theory for Call-By-Push-Value. - Christine Rizkallah; Dmitri Garbuzov; Steve Zdancewic (ITP, 2018)

Technical perspective: Building bug-free compilers. - Steve Zdancewic (Commun. ACM, 2018)

Structural Operational Semantics for Control Flow Graph Machines. - Dmitri Garbuzov; William Mansky; Christine Rizkallah; Steve Zdancewic (CoRR, 2018)

ReQWIRE: Reasoning about Reversible Quantum Circuits. - Robert Rand 001; Jennifer Paykin; Dong-Ho Lee; Steve Zdancewic (QPL, 2018)

Synthesizing quotient lenses. - Solomon Maina; Anders Miltner; Kathleen Fisher; Benjamin C. Pierce; David Walker 001; Steve Zdancewic (Proc. ACM Program. Lang., 2018)

Synthesizing bijective lenses. - Anders Miltner; Kathleen Fisher; Benjamin C. Pierce; David Walker 001; Steve Zdancewic (Proc. ACM Program. Lang., 2018)

From C to interaction trees: specifying, verifying, and testing a networked server. - Nicolas Koh; Yao Li 004; Yishuai Li; Li-yao Xia; Lennart Beringer; Wolf Honoré; William Mansky; Benjamin C. Pierce; Steve Zdancewic (CPP, 2019)

SoK: General Purpose Compilers for Secure Multi-Party Computation. - Marcella Hastings; Brett Hemenway; Daniel Noble; Steve Zdancewic (IEEE Symposium on Security and Privacy, 2019)

A HoTT Quantum Equational Theory (Extended Version). - Jennifer Paykin; Steve Zdancewic (CoRR, 2019)

Interaction Trees: Representing Recursive and Impure Programs in Coq (Work In Progress). - Li-yao Xia; Yannick Zakowski; Paul He; Chung-Kil Hur; Gregory Malecha; Benjamin C. Pierce; Steve Zdancewic (CoRR, 2019)

Synthesizing symmetric lenses. - Anders Miltner; Solomon Maina; Kathleen Fisher; Benjamin C. Pierce; David Walker 001; Steve Zdancewic (Proc. ACM Program. Lang., 2019)

An equational theory for weak bisimulation via generalized parameterized coinduction. - Yannick Zakowski; Paul He; Chung-Kil Hur; Steve Zdancewic (CPP, 2020)

Computation focusing. - Nick Rioux; Steve Zdancewic (Proc. ACM Program. Lang., 2020)

Interaction trees: representing recursive and impure programs in Coq. - Li-yao Xia; Yannick Zakowski; Paul He; Chung-Kil Hur; Gregory Malecha; Benjamin C. Pierce; Steve Zdancewic (Proc. ACM Program. Lang., 2020)

Model-based testing of networked applications. - Yishuai Li; Benjamin C. Pierce; Steve Zdancewic (ISSTA, 2021)

Verifying an HTTP Key-Value Server with Interaction Trees and VST. - Hengchu Zhang; Wolf Honoré; Nicolas Koh; Yao Li 004; Yishuai Li; Li-yao Xia; Lennart Beringer; William Mansky; Benjamin C. Pierce; Steve Zdancewic (ITP, 2021)

A type system for extracting functional specifications from memory-safe imperative programs. - Paul He; Eddy Westbrook; Brent Carmer; Chris Phifer; Valentin Robert; Karl Smeltzer; Andrei Stefanescu; Aaron Tomb; Adam Wick; Matthew Yacavone; Steve Zdancewic (Proc. ACM Program. Lang., 2021)

Dijkstra monads forever: termination-sensitive specifications for interaction trees. - Lucas Silver; Steve Zdancewic (Proc. ACM Program. Lang., 2021)

Modular, compositional, and executable formal semantics for LLVM IR. - Yannick Zakowski; Calvin Beck; Irene Yoon 001; Ilia Zaichuk; Vadim Zaliva; Steve Zdancewic (Proc. ACM Program. Lang., 2021)

Replication Package for Article: Model-Based Testing of Networked Applications. - Yishuai Li; Benjamin C. Pierce; Steve Zdancewic (Zenodo, 2021)

Counterfactual Explanations for Natural Language Interfaces. - George Tolkachev; Stephen Mell; Steve Zdancewic; Osbert Bastani (ACL (2), 2022)

Ideograph: A Language for Expressing and Manipulating Structured Data. - Stephen Mell; Osbert Bastani; Steve Zdancewic (TERMGRAPH@FSCD, 2022)

C4: verified transactional objects. - Mohsen Lesani; Li-yao Xia; Anders Kaseorg; Christian J. Bell; Adam Chlipala; Benjamin C. Pierce; Steve Zdancewic (Proc. ACM Program. Lang., 2022)

Formal reasoning about layered monadic interpreters. - Irene Yoon 001; Yannick Zakowski; Steve Zdancewic (Proc. ACM Program. Lang., 2022)

Synthesizing Trajectory Queries from Examples. - Stephen Mell; Favyen Bastani; Steve Zdancewic; Osbert Bastani (CAV (1), 2023)

Semantics for Noninterference with Interaction Trees. - Lucas Silver; Paul He; Ethan Cecchetti; Andrew K. Hirsch; Steve Zdancewic (ECOOP, 2023)

Tealeaves: Structured Monads for Generic First-Order Abstract Syntax Infrastructure. - Lawrence Dunn; Val Tannen; Steve Zdancewic (ITP, 2023)

Syntax Monads for the Working Formal Metatheorist. - Lawrence Dunn; Val Tannen; Steve Zdancewic (ACT, 2023)

Semantics for Noninterference with Interaction Trees (Artifact). - Lucas Silver; Paul He; Ethan Cecchetti; Andrew K. Hirsch; Steve Zdancewic (Dagstuhl Artifacts Ser., 2023)

Choice Trees: Representing Nondeterministic, Recursive, and Impure Programs in Coq. - Nicolas Chappe; Paul He; Ludovic Henrio; Yannick Zakowski; Steve Zdancewic (Proc. ACM Program. Lang., 2023)

A Bowtie for a Beast: Overloading, Eta Expansion, and Extensible Data Types in F⋈. - Nick Rioux; Xuejing Huang; Bruno C. d. S. Oliveira; Steve Zdancewic (Proc. ACM Program. Lang., 2023)

A Two-Phase Infinite/Finite Low-Level Memory Model. - Calvin Beck; Irene Yoon 001; Hanxi Chen; Yannick Zakowski; Steve Zdancewic (CoRR, 2024)

An Opportunistically Parallel Lambda Calculus for Performant Composition of Large Language Models. - Stephen Mell; Steve Zdancewic; Osbert Bastani (CoRR, 2024)

Structural temporal logic for mechanized program verification. - Eleftherios Ioannidis; Yannick Zakowski; Steve Zdancewic; Sebastian Angel (CoRR, 2024)

A Two-Phase Infinite/Finite Low-Level Memory Model: Reconciling Integer-Pointer Casts, Finite Space, and undef at the LLVM IR Level of Abstraction. - Calvin Beck; Irene Yoon 001; Hanxi Chen; Yannick Zakowski; Steve Zdancewic (Proc. ACM Program. Lang., 2024)

Optimal Program Synthesis via Abstract Interpretation. - Stephen Mell; Steve Zdancewic; Osbert Bastani (Proc. ACM Program. Lang., 2024)

Verifying Fault-Tolerance of Quantum Error Correction Codes. - Kean Chen; Yuhao Liu; Wang Fang 001; Jennifer Paykin; Xin-Chuan Wu; Albert T. Schmitz; Steve Zdancewic; Gushu Li (CAV (4), 2025)

Vellvm: Formalizing the Informal LLVM - (Experience Report). - Calvin Beck; Hanxi Chen; Steve Zdancewic (NFM, 2025)

Functional Meaning for Parallel Streaming. - Nick Rioux; Steve Zdancewic (Proc. ACM Program. Lang., 2025)

A Fast, Reliable, and Secure Programming Language for LLM Agents with Code Actions. - Stephen Mell; Botong Zhang; David Mell; Shuo Li; Ramya Ramalingam; Nathan Yu; Steve Zdancewic; Osbert Bastani (CoRR, 2025)

Structured Monads for Generic First-Order Syntax Metatheory. - Lawrence Dunn; Val Tannen; Steve Zdancewic (J. Autom. Reason., 2025)