Steve Zdancewic

131 papers A* 15A 14B 13C 3Journal 54Unranked 30

Year	Rank	Type	Title / Venue / Authors
2026	J	`jnl`	Compiling to Linear Neurons. Proc. ACM Program. Lang. Joey Velez-Ginorio, Nada Amin, Konrad P. Kording, Steve Zdancewic
2026	J	`jnl`	Optimal Program Synthesis via Abstract Interpretation. CoRR Stephen Mell, Steve Zdancewic, Osbert Bastani
2026	J	`jnl`	Synthesizing Trajectory Queries from Examples. CoRR Stephen Mell, Favyen Bastani, Steve Zdancewic, Osbert Bastani
2025	J	`jnl`	A Fast, Reliable, and Secure Programming Language for LLM Agents with Code Actions. CoRR Stephen Mell, Botong Zhang, David Mell, Shuo Li, Ramya Ramalingam, Nathan Yu, Steve Zdancewic, Osbert Bastani
2025	J	`jnl`	Choice trees: Representing and reasoning about nondeterministic, recursive, and impure programs in Rocq. J. Funct. Program. Nicolas Chappe, Paul He, Ludovic Henrio, Eleftherios Ioannidis, Yannick Zakowski, Steve Zdancewic
2025	J	`jnl`	Compiling to linear neurons. CoRR Joey Velez-Ginorio, Nada Amin, Konrad P. Kording, Steve Zdancewic
2025	J	`jnl`	Compiling to recurrent neurons. CoRR Joey Velez-Ginorio, Nada Amin, Konrad P. Kording, Steve Zdancewic
2025	J	`jnl`	Functional Meaning for Parallel Streaming. CoRR Nick Rioux, Steve Zdancewic
2025	J	`jnl`	Functional Meaning for Parallel Streaming. Proc. ACM Program. Lang. Nick Rioux, Steve Zdancewic
2025	J	`jnl`	Opportunistically Parallel Lambda Calculus. Proc. ACM Program. Lang. Stephen Mell, Konstantinos Kallas, Steve Zdancewic, Osbert Bastani
2025	J	`jnl`	Structural Temporal Logic for Mechanized Program Verification. Proc. ACM Program. Lang. Eleftherios Ioannidis, Yannick Zakowski, Steve Zdancewic, Sebastian Angel
2025	J	`jnl`	Structured Monads for Generic First-Order Syntax Metatheory. J. Autom. Reason. Lawrence Dunn, Val Tannen, Steve Zdancewic
2025	—	`conf`	Vellvm: Formalizing the Informal LLVM - (Experience Report). NFM Calvin Beck, Hanxi Chen, Steve Zdancewic
2025	—	`conf`	Verifying Fault-Tolerance of Quantum Error Correction Codes. CAV (4) Kean Chen, Yuhao Liu, Wang Fang, Jennifer Paykin, Xin-Chuan Wu, Albert T. Schmitz, Steve Zdancewic, Gushu Li
2024	J	`jnl`	A Two-Phase Infinite/Finite Low-Level Memory Model. CoRR Calvin Beck, Irene Yoon, Hanxi Chen, Yannick Zakowski, Steve Zdancewic
2024	J	`jnl`	A Two-Phase Infinite/Finite Low-Level Memory Model: Reconciling Integer-Pointer Casts, Finite Space, and undef at the LLVM IR Level of Abstraction. Proc. ACM Program. Lang. Calvin Beck, Irene Yoon, Hanxi Chen, Yannick Zakowski, Steve Zdancewic
2024	J	`jnl`	An Opportunistically Parallel Lambda Calculus for Performant Composition of Large Language Models. CoRR Stephen Mell, Steve Zdancewic, Osbert Bastani
2024	J	`jnl`	Optimal Program Synthesis via Abstract Interpretation. Proc. ACM Program. Lang. Stephen Mell, Steve Zdancewic, Osbert Bastani
2024	J	`jnl`	Structural temporal logic for mechanized program verification. CoRR Eleftherios Ioannidis, Yannick Zakowski, Steve Zdancewic, Sebastian Angel
2023	J	`jnl`	A Bowtie for a Beast: Overloading, Eta Expansion, and Extensible Data Types in F⋈. Proc. ACM Program. Lang. Nick Rioux, Xuejing Huang, Bruno C. d. S. Oliveira, Steve Zdancewic
2023	J	`jnl`	Choice Trees: Representing Nondeterministic, Recursive, and Impure Programs in Coq. Proc. ACM Program. Lang. Nicolas Chappe, Paul He, Ludovic Henrio, Yannick Zakowski, Steve Zdancewic
2023	B	`ed.`	Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2023, Boston, MA, USA, January 16-17, 2023 CPP Robbert Krebbers, Dmitriy Traytel, Brigitte Pientka, Steve Zdancewic
2023	J	`jnl`	Semantics for Noninterference with Interaction Trees (Artifact). Dagstuhl Artifacts Ser. Lucas Silver, Paul He, Ethan Cecchetti, Andrew K. Hirsch, Steve Zdancewic
2023	A	`conf`	Semantics for Noninterference with Interaction Trees. ECOOP Lucas Silver, Paul He, Ethan Cecchetti, Andrew K. Hirsch, Steve Zdancewic
2023	—	`conf`	Syntax Monads for the Working Formal Metatheorist. ACT Lawrence Dunn, Val Tannen, Steve Zdancewic
2023	—	`conf`	Synthesizing Trajectory Queries from Examples. CAV (1) Stephen Mell, Favyen Bastani, Steve Zdancewic, Osbert Bastani
2023	B	`conf`	Tealeaves: Structured Monads for Generic First-Order Abstract Syntax Infrastructure. ITP Lawrence Dunn, Val Tannen, Steve Zdancewic
2022	J	`jnl`	C4: verified transactional objects. Proc. ACM Program. Lang. Mohsen Lesani, Li-yao Xia, Anders Kaseorg, Christian J. Bell, Adam Chlipala, Benjamin C. Pierce, Steve Zdancewic
2022	B	`ed.`	CPP '22: 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, Philadelphia, PA, USA, January 17 - 18, 2022 CPP Andrei Popescu, Steve Zdancewic
2022	J	`jnl`	Choice Trees: Representing Nondeterministic, Recursive, and Impure Programs in Coq. CoRR Nicolas Chappe, Paul He, Ludovic Henrio, Yannick Zakowski, Steve Zdancewic
2022	—	`conf`	Counterfactual Explanations for Natural Language Interfaces. ACL (2) George Tolkachev, Stephen Mell, Steve Zdancewic, Osbert Bastani
2022	J	`jnl`	Counterfactual Explanations for Natural Language Interfaces. CoRR George Tolkachev, Stephen Mell, Steve Zdancewic, Osbert Bastani
2022	J	`jnl`	Formal reasoning about layered monadic interpreters. Proc. ACM Program. Lang. Irene Yoon, Yannick Zakowski, Steve Zdancewic
2022	—	`conf`	Ideograph: A Language for Expressing and Manipulating Structured Data. TERMGRAPH@FSCD Stephen Mell, Osbert Bastani, Steve Zdancewic
2021	J	`jnl`	A type system for extracting functional specifications from memory-safe imperative programs. Proc. ACM Program. Lang. Paul He, Eddy Westbrook, Brent Carmer, Chris Phifer, Valentin Robert, Karl Smeltzer, Andrei Stefanescu, Aaron Tomb, Adam Wick, Matthew Yacavone, Steve Zdancewic
2021	J	`jnl`	Dijkstra monads forever: termination-sensitive specifications for interaction trees. Proc. ACM Program. Lang. Lucas Silver, Steve Zdancewic
2021	J	`jnl`	Model-Based Testing of Networked Applications. CoRR Yishuai Li, Benjamin C. Pierce, Steve Zdancewic
2021	A	`conf`	Model-based testing of networked applications. ISSTA Yishuai Li, Benjamin C. Pierce, Steve Zdancewic
2021	J	`jnl`	Modular, compositional, and executable formal semantics for LLVM IR. Proc. ACM Program. Lang. Yannick Zakowski, Calvin Beck, Irene Yoon, Ilia Zaichuk, Vadim Zaliva, Steve Zdancewic
2021	B	`conf`	Verifying an HTTP Key-Value Server with Interaction Trees and VST. ITP Hengchu Zhang, Wolf Honoré, Nicolas Koh, Yao Li, Yishuai Li, Li-yao Xia, Lennart Beringer, William Mansky, Benjamin C. Pierce, Steve Zdancewic
2020	J	`jnl`	An Equational Theory for Weak Bisimulation via Generalized Parameterized Coinduction. CoRR Yannick Zakowski, Paul He, Chung-Kil Hur, Steve Zdancewic
2020	B	`conf`	An equational theory for weak bisimulation via generalized parameterized coinduction. CPP Yannick Zakowski, Paul He, Chung-Kil Hur, Steve Zdancewic
2020	J	`jnl`	Computation focusing. Proc. ACM Program. Lang. Nick Rioux, Steve Zdancewic
2020	J	`jnl`	Interaction trees: representing recursive and impure programs in Coq. Proc. ACM Program. Lang. Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce, Steve Zdancewic
2019	J	`jnl`	A HoTT Quantum Equational Theory (Extended Version). CoRR Jennifer Paykin, Steve Zdancewic
2019	B	`conf`	From C to interaction trees: specifying, verifying, and testing a networked server. CPP Nicolas Koh, Yao Li, Yishuai Li, Li-yao Xia, Lennart Beringer, Wolf Honoré, William Mansky, Benjamin C. Pierce, Steve Zdancewic
2019	J	`jnl`	Interaction Trees: Representing Recursive and Impure Programs in Coq (Work In Progress). CoRR Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce, Steve Zdancewic
2019	A*	`conf`	SoK: General Purpose Compilers for Secure Multi-Party Computation. IEEE Symposium on Security and Privacy Marcella Hastings, Brett Hemenway, Daniel Noble, Steve Zdancewic
2019	J	`jnl`	Synthesizing symmetric lenses. Proc. ACM Program. Lang. Anders Miltner, Solomon Maina, Kathleen Fisher, Benjamin C. Pierce, David Walker, Steve Zdancewic
2018	B	`conf`	A Formal Equational Theory for Call-By-Push-Value. ITP Christine Rizkallah, Dmitri Garbuzov, Steve Zdancewic
2018	J	`jnl`	A linear/producer/consumer model of classical linear logic. Math. Struct. Comput. Sci. Jennifer Paykin, Steve Zdancewic
2018	J	`jnl`	From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server. CoRR Nicolas Koh, Yao Li, Yishuai Li, Li-yao Xia, Lennart Beringer, Wolf Honoré, William Mansky, Benjamin C. Pierce, Steve Zdancewic
2018	—	`conf`	ReQWIRE: Reasoning about Reversible Quantum Circuits. QPL Robert Rand, Jennifer Paykin, Dong-Ho Lee, Steve Zdancewic
2018	J	`jnl`	Structural Operational Semantics for Control Flow Graph Machines. CoRR Dmitri Garbuzov, William Mansky, Christine Rizkallah, Steve Zdancewic
2018	J	`jnl`	Synthesizing Symmetric Lenses. CoRR Anders Miltner, Solomon Maina, Kathleen Fisher, Benjamin C. Pierce, David Walker, Steve Zdancewic
2018	J	`jnl`	Synthesizing bijective lenses. Proc. ACM Program. Lang. Anders Miltner, Kathleen Fisher, Benjamin C. Pierce, David Walker, Steve Zdancewic
2018	J	`jnl`	Synthesizing quotient lenses. Proc. ACM Program. Lang. Solomon Maina, Anders Miltner, Kathleen Fisher, Benjamin C. Pierce, David Walker, Steve Zdancewic
2018	J	`jnl`	Technical perspective: Building bug-free compilers. Commun. ACM Steve Zdancewic
2017	—	`conf`	QWIRE Practice: Formal Verification of Quantum Circuits in Coq. QPL Robert Rand, Jennifer Paykin, Steve Zdancewic
2017	A*	`conf`	QWIRE: a core language for quantum circuits. POPL Jennifer Paykin, Robert Rand, Steve Zdancewic
2017	J	`jnl`	Synthesizing Bijective Lenses. CoRR Anders Miltner, Kathleen Fisher, Benjamin C. Pierce, David Walker, Steve Zdancewic
2017	C	`conf`	The linearity Monad. Haskell Jennifer Paykin, Steve Zdancewic
2017	B	`conf`	Verifying dynamic race detection. CPP William Mansky, Yuanfeng Peng, Steve Zdancewic, Joseph Devietti
2016	A*	`conf`	Example-directed synthesis: a type-theoretic interpretation. POPL Jonathan Frankle, Peter-Michael Osera, David Walker, Steve Zdancewic
2016	—	`conf`	Linear λμ is CP (more or less). A List of Successes That Can Change the World Jennifer Paykin, Steve Zdancewic
2015	A*	`conf`	A formal C memory model supporting integer-pointer casts. PLDI Jeehoon Kang, Chung-Kil Hur, William Mansky, Dmitri Garbuzov, Steve Zdancewic, Viktor Vafeiadis
2015	—	`conf`	An Axiomatic Specification for Sequential Memory Models. CAV (2) William Mansky, Dmitri Garbuzov, Steve Zdancewic
2015	—	`conf`	Everything You Want to Know About Pointer-Based Checking. SNAPL Santosh Nagarakatte, Milo M. K. Martin, Steve Zdancewic
2015	A*	`conf`	Type-and-example-directed program synthesis. PLDI Peter-Michael Osera, Steve Zdancewic
2015	B	`conf`	VPHL: A Verified Partial-Correctness Logic for Probabilistic Programs. MFPS Robert Rand, Steve Zdancewic
2014	A	`conf`	A Core Quantitative Coeffect Calculus. ESOP Aloïs Brunel, Marco Gaboardi, Damiano Mazza, Steve Zdancewic
2014	—	`conf`	A Linear/Producer/Consumer Model of Classical Linear Logic. LINEARITY Jennifer Paykin, Steve Zdancewic
2014	C	`conf`	Finite Vector Spaces as Model of Simply-Typed Lambda-Calculi. ICTAC Benoît Valiron, Steve Zdancewic
2014	J	`jnl`	Finite Vector Spaces as Model of Simply-Typed Lambda-Calculi. CoRR Benoît Valiron, Steve Zdancewic
2014	J	`jnl`	Modeling Simply-Typed Lambda Calculi in the Category of Finite Vector Spaces. Sci. Ann. Comput. Sci. Benoît Valiron, Steve Zdancewic
2014	A	`conf`	WatchdogLite: Hardware-Accelerated Compiler-Based Pointer Checking. CGO Santosh Nagarakatte, Milo M. K. Martin, Steve Zdancewic
2013	A*	`conf`	Formal verification of SSA-based optimizations for LLVM. PLDI Jianzhou Zhao, Santosh Nagarakatte, Milo M. K. Martin, Steve Zdancewic
2013	J	`jnl`	Hardware-Enforced Comprehensive Memory Safety. IEEE Micro Santosh Nagarakatte, Milo M. K. Martin, Steve Zdancewic
2013	A	`conf`	Ironclad C++: a library-augmented type-safe subset of c++. OOPSLA Christian DeLozier, Richard A. Eisenberg, Santosh Nagarakatte, Peter-Michael Osera, Milo M. K. Martin, Steve Zdancewic
2012	—	`conf`	Dependent interoperability. PLPV Peter-Michael Osera, Vilhelm Sjöberg, Steve Zdancewic
2012	A*	`conf`	Formalizing the LLVM intermediate representation for verified program transformations. POPL Jianzhou Zhao, Santosh Nagarakatte, Milo M. K. Martin, Steve Zdancewic
2012	B	`conf`	Mechanized Verification of Computing Dominators for Formalizing Compilers. CPP Jianzhou Zhao, Steve Zdancewic
2012	A*	`conf`	Watchdog: Hardware for safe and secure manual memory management and full memory safety. ISCA Santosh Nagarakatte, Milo M. K. Martin, Steve Zdancewic
2011	A*	`conf`	Generative type abstraction and type-level computation. POPL Stephanie Weirich, Dimitrios Vytiniotis, Simon L. Peyton Jones, Steve Zdancewic
2010	J	`jnl`	Arrows for secure information flow. Theor. Comput. Sci. Peng Li, Steve Zdancewic
2010	C	`conf`	CETS: compiler enforced temporal safety for C. ISMM Santosh Nagarakatte, Jianzhou Zhao, Milo M. K. Martin, Steve Zdancewic
2010	—	`conf`	Lightweight linear types in system fdegree. TLDI Karl Mazurak, Jianzhou Zhao, Steve Zdancewic
2010	A	`conf`	Lolliproc: to concurrency from classical linear logic via curry-howard and control. ICFP Karl Mazurak, Steve Zdancewic
2010	B	`conf`	Relational Parametricity for a Polymorphic Linear Lambda Calculus. APLAS Jianzhou Zhao, Qi Zhang, Steve Zdancewic
2009	J	`jnl`	An overview of the Oregon programming languages summer school. ACM SIGPLAN Notices 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
2009	—	`conf`	Encoding information flow in Aura. PLAS Limin Jia, Steve Zdancewic
2009	A*	`conf`	Reactive noninterference. CCS Aaron Bohannon, Benjamin C. Pierce, Vilhelm Sjöberg, Stephanie Weirich, Steve Zdancewic
2009	A*	`conf`	SoftBound: highly compatible and complete spatial memory safety for c. PLDI Santosh Nagarakatte, Jianzhou Zhao, Milo M. K. Martin, Steve Zdancewic
2009	—	`conf`	Strong and Weak Policy Relations. POLICY Michael J. May, Carl A. Gunter, Insup Lee, Steve Zdancewic
2009	A	`conf`	Updatable Security Views. CSF J. Nathan Foster, Benjamin C. Pierce, Steve Zdancewic
2008	A	`conf`	AURA: a programming language for authorization and audit. ICFP Limin Jia, Jeffrey A. Vaughan, Karl Mazurak, Jianzhou Zhao, Luke Zarko, Joseph Schorr, Steve Zdancewic
2008	A	`conf`	Evidence-Based Audit. CSF Jeffrey A. Vaughan, Limin Jia, Karl Mazurak, Steve Zdancewic
2008	A*	`conf`	Hardbound: architectural support for spatial safety of the C programming language. ASPLOS Joe Devietti, Colin Blundell, Milo M. K. Martin, Steve Zdancewic
2008	J	`jnl`	Joint workshop on foundations of computer security and automated reasoning for security protocol analysis (FCS-ARSPA '06). Inf. Comput. Pierpaolo Degano, Ralf Küsters, Luca Viganò, Steve Zdancewic
2007	—	`conf`	A Cryptographic Decentralized Label Model. S&P Jeffrey A. Vaughan, Steve Zdancewic
2007	—	`conf`	Application-level concurrency: combining events and treads: invited talk. DAMP Steve Zdancewic
2007	A*	`conf`	Combining events and threads for scalable network services implementation and evaluation of monadic, application-level concurrency primitives. PLDI Peng Li, Steve Zdancewic
2007	J	`jnl`	Run-time principals in information-flow type systems. ACM Trans. Program. Lang. Syst. Stephen Tse, Steve Zdancewic
2006	J	`jnl`	A type-theoretic interpretation of pointcuts and advice. Sci. Comput. Program. Jay Ligatti, David Walker, Steve Zdancewic
2006	—	`conf`	Encoding Information Flow in Haskell. CSFW Peng Li, Steve Zdancewic
2006	J	`jnl`	Enforcing Robust Declassification and Qualified Robustness. J. Comput. Secur. Andrew C. Myers, Andrei Sabelfeld, Steve Zdancewic
2006	—	`conf`	Managing Policy Updates in Security-Typed Languages. CSFW Nikhil Swamy, Michael Hicks, Stephen Tse, Steve Zdancewic
2006	—	`conf`	Preserving Secrecy Under Refinement. ICALP (2) Rajeev Alur, Pavol Cerný, Steve Zdancewic
2006	—	`ed.`	Proceedings of the 2006 Workshop on Programming Languages and Analysis for Security, PLAS 2006, Ottawa, Ontario, Canada, June 10, 2006 PLAS Vugranam C. Sreedhar, Steve Zdancewic
2005	A	`conf`	A Design for a Security-Typed Language with Certificate-Based Declassification. ESOP Stephen Tse, Steve Zdancewic
2005	A*	`conf`	Downgrading policies and relaxed noninterference. POPL Peng Li, Steve Zdancewic
2005	—	`conf`	It Is Time to Mechanize Programming Language Metatheory. VSTTE Benjamin C. Pierce, Peter Sewell, Stephanie Weirich, Steve Zdancewic
2005	—	`conf`	Mechanized Metatheory for the Masses: The PoplMark Challenge. TPHOLs Brian E. Aydemir, Aaron Bohannon, Matthew Fairbairn, J. Nathan Foster, Benjamin C. Pierce, Peter Sewell, Dimitrios Vytiniotis, Geoffrey Washburn, Stephanie Weirich, Steve Zdancewic
2005	—	`conf`	Practical Information-flow Control in Web-Based Information Systems. CSFW Peng Li, Steve Zdancewic
2004	B	`conf`	Advanced control flow in Java card programming. LCTES Peng Li, Steve Zdancewic
2004	—	`conf`	Enforcing Robust Declassification. CSFW Andrew C. Myers, Andrei Sabelfeld, Steve Zdancewic
2004	—	`conf`	Run-time Principals in Information-flow Type Systems. S&P Stephen Tse, Steve Zdancewic
2004	A	`conf`	Translating dependency into parametricity. ICFP Stephen Tse, Steve Zdancewic
2003	B	`conf`	A Type System for Robust Declassification. MFPS Steve Zdancewic
2003	A	`conf`	A theory of aspects. ICFP David Walker, Steve Zdancewic, Jay Ligatti
2003	—	`conf`	Formalizing Java-MaC. RV@CAV Usa Sammapun, Raman Sharykin, Margaret DeLap, Myong Kim, Steve Zdancewic
2003	—	`conf`	Observational Determinism for Concurrent Program Security. CSFW Steve Zdancewic, Andrew C. Myers
2003	—	`conf`	Using Replication and Partitioning to Build Secure Distributed Systems. S&P Lantian Zheng, Stephen Chong, Andrew C. Myers, Steve Zdancewic
2002	—	`—`	Programming Languages for Information Security. Steve Zdancewic
2002	J	`jnl`	Secure Information Flow via Linear Continuations. High. Order Symb. Comput. Steve Zdancewic, Andrew C. Myers
2002	J	`jnl`	Secure program partitioning. ACM Trans. Comput. Syst. Steve Zdancewic, Lantian Zheng, Nathaniel Nystrom, Andrew C. Myers
2001	—	`conf`	Robust Declassification. CSFW Steve Zdancewic, Andrew C. Myers
2001	A	`conf`	Secure Information Flow and CPS. ESOP Steve Zdancewic, Andrew C. Myers
2001	A*	`conf`	Untrusted Hosts and Confidentiality: Secure Program Partitioning. SOSP Steve Zdancewic, Lantian Zheng, Nathaniel Nystrom, Andrew C. Myers
2000	J	`jnl`	Syntactic type abstraction. ACM Trans. Program. Lang. Syst. Dan Grossman, J. Gregory Morrisett, Steve Zdancewic
1999	A	`conf`	Principals in Programming Languages: A Syntactic Proof Technique. ICFP Steve Zdancewic, Dan Grossman, J. Gregory Morrisett