Steve Zdancewic’s Publications

Journal Articles

[1] Joey Velev-Ginorio, Nada Amin, Konrad Kording, and Steve Zdancewic. Compiling to Linear Neurons. Proceedings of the ACM on Programming Languages, 10(POPL), 2026. [ DOI | http | Abstract ]
[2] Eleftherios Ioannidis, Yannick Zakowski, Steve Zdancewic, and Sebastian Angel. Structural Temporal Logic for Mechanized Program Verification. Proceedings of the ACM on Programming Languages, 9(OOPSLA2), October 2025. [ DOI | http | Abstract ]
[3] Stephen Mell, Konstantinos Kallas, Steve Zdancewic, and Osbert Bastani. Opportunistically Parallel Lambda Calculus. Proceedings of the ACM on Programming Languages, 9(OOPSLA2), October 2025. [ DOI | http | Abstract ]
[4] Nick Rioux and Steve Zdancewic. Functional Meaning for Parallel Streaming. Proceedings of the ACM on Programming Languages (PACMPL), 9(PLDI), 2025. [ PDF | Abstract ]
[5] Lawrence Dunn, Val Tannen, and Steve Zdancewic. Structured Monads for Generic First-Order Syntax Metatheory. Journal of Automated Reasoning (JAR), 69(22), 2025. [ DOI | PDF | Abstract ]
[6] Nicolas Chappe, Paul He, Ludovic Henrio, Eleftherios Ioannidis, Yannick Zakowski, and Steve Zdancewic. Choice trees: Representing and reasoning about nondeterministic, recursive, and impure programs in Rocq. Journal of Functional Programming, 35, 2025. [ DOI ]
[7] Stephen Mell, Steve Zdancewic, and Osbert Bastani. Optimal Program Synthesis via Abstract Interpretation. 8(POPL), 2024. [ PDF | Abstract ]
[8] Calvin Beck, Irene Yoon, Hanxi Chen, Yannick Zakowski, and Steve Zdancewic. A Two-Phase Infinite/Finite Low-Level Memory Model: Reconciling Integer-Pointer Casts, Finite Space, and undef at the LLVM IR Level of Abstraction. Proceedings of the ACM on Programming Languages, 8(ICFP), 2024. [ DOI | PDF | Abstract ]
[9] Nicolas Chappe, Paul He, Ludovic Henrio, Yannick Zakowski, and Steve Zdancewic. Choice Trees: Representing Nondeterministic, Recursive, and Impure Programs in Coq. Proceedings of the ACM on Programming Languages, 7(POPL), 2023. [ PDF | Abstract ]
[10] Nick Rioux, Xuejing Huang, Bruno C. d. S. Oliviera, and Steve Zdancewic. A Bowtie for a Beast: Overloading, Eta Expansion, and Extensible Data Types in F. Proceedings of the ACM on Programming Languages, 7(POPL), 2023. [ PDF | Abstract ]
[11] Mohsen Lesani, Li-Yao Xia, Anders Kaseorg, Christian J. Bell, Adam Chlipala, Benjamin C. Pierce, and Steve Zdancewic. C4: Verified Transactional Objects. Proceedings of the ACM on Programming Languages, OOPSLA, 2022. [ PDF | Abstract ]
[12] Irene Yoon, Yannick Zakowski, and Steve Zdancewic. Formal Reasoning About Layered Monadic Interpreters. Proceedings of the ACM on Programming Languages, 6(ICFP), 2022. [ PDF | Abstract ]
[13] Lucas Silver and Steve Zdancewic. Dijkstra Monads Forever: Termination-Sensitive Specifications for Interaction Trees. Proceedings of the ACM on Programming Languages, 5(POPL), January 2021. [ PDF | Abstract ]
[14] Yannick Zakowski, Calvin Beck, Irene Yoon, Ilya Zaichuk, Vadim Zaliva, and Steve Zdancewic. Modular, Compositional, and Executable Formal Semantics for LLVM IR. Proceedings of the ACM on Programming Languages, 5(ICFP), 2021. [ PDF | Abstract ]
[15] Paul He, Eddy Westbrook, Brent Carmer, Chris Phifer, Valentin Robert, Karl Smeltzer, Andrei Andrei Ştefănescu, Aaron Tomb, Adam Wick, Matthew Yacavone, and Steve Zdancewic. A Type System for Extracting Functional Specifications from Memory-Safe Imperative Programs. Proceedings of the ACM on Programming Languages, OOPSLA, 2021. [ PDF | Abstract ]
[16] Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce, and Steve Zdancewic. Interaction Trees. Proceedings of the ACM on Programming Languages, 4(POPL), January 2020. [ PDF | Abstract ]
[17] Nick Rioux and Steve Zdancewic. Computation Focusing. Proceedings of the ACM on Programming Languages, 5(ICFP), 2020. [ PDF | Abstract ]
[18] Anders Miltner, Solomon Maina, Kathleen Fisher, Benjamin C. Pierce, David Walker, and Steve Zdancewic. Synthesizing Symmetric Lenses. Proceedings of the ACM on Programming Languages, 3(ICFP), 2019. [ PDF | Abstract ]
[19] Anders Miltner, Kathleen Fisher, Benjamin C. Pierce, David Walker, and Steve Zdancewic. Synthesizing Bijective Lenses. Proceedings of the ACM on Programming Languages, 2(POPL), January 2018. [ PDF | Abstract ]
[20] Solomon Maina, Anders Miltner, Kathleen Fisher, Benjamin C. Pierce, David Walker, and Steve Zdancewic. Synthesizing Quotient Lenses. Proceedings of the ACM on Programming Languages, 2(ICFP), 2018. [ PDF | Abstract ]
[21] Andrew W. Appel, Lennart Beringer, Adam Chlipala, Benjamin C. Pierce, Zhong Shao, Stephanie Weirich, and Steve Zdancewic. Position paper: The Science of Deep Specification. Philosophical Transactions of the Royal Society of London A: Mathematical, Physical and Engineering Sciences, 375(2104), 2017. [ DOI | http | Abstract ]
[22] B. Valiron and S. Zdancewic. Modeling Simply-Typed Lambda Calculi in the Category of Finite Vector Spaces. Scientific Annals of Computer Science, 24(2):325--368, 2014. [ DOI | PDF | Abstract ]
[23] Peng Li and Steve Zdancewic. Arrows for Secure Information Flow. Theoretical Computer Science, 411(19):1974--1994, 2010. [ PDF | Abstract ]
[24] Stephen Tse and Steve Zdancewic. Run-time principals in information-flow type systems. Transactions on Programming Languages and Systems, 30(1):6, 2008. [ PDF | Abstract ]
[25] Andrew C. Myers, Andrei Sabelfeld, and Steve Zdancewic. Enforcing Robust Declassification and Qualified Robustness. Journal of Computer Security, 14(2):157--196, 2006. [ PDF | Abstract ]
[26] Jay Ligatti, David Walker, and Steve Zdancewic. A Type-theoretic Interpretation of Pointcuts and Advice. Science of Computer Programming: Special Issue on Foundations of Aspect-Oriented Programming, pages 240--266, 2006. [ PDF | Abstract ]
[27] Steve Zdancewic, Lantian Zheng, Nathaniel Nystrom, and Andrew C. Myers. Secure Program Partitioning. Transactions on Computer Systems, 20(3):283--328, 2002. [ PDF | PS | Abstract ]
[28] Steve Zdancewic and Andrew C. Myers. Secure Information Flow via Linear Continuations. Higher Order and Symbolic Computation, 15(2/3):209--234, 2002. [ PDF | PS | Abstract ]
[29] Dan Grossman, Greg Morrisett, and Steve Zdancewic. Syntactic Type Abstraction. Transactions on Programming Languages and Systems, 22(6):1037--1080, November 2000. [ PDF | PS | Abstract ]

Invited Papers

[1] Steve Zdancewic. Challenges for Information-flow Security. In Proceedings of the 1st International Workshop on the Programming Language Interference and Dependence (PLID'04), 2004. (5 pages). [ PDF ]
[2] Steve Zdancewic. A Type System for Robust Declassification. In Proceedings of the Nineteenth Conference on the Mathematical Foundations of Programming Semantics (MFPS). Electronic Notes in Theoretical Computer Science, March 2003. (16 pages). [ PDF | PS | Abstract ]

Conference and Selective Workshop Papers

[1] Calvin Beck, Hanxi Chen, and Steve Zdancewic. Vellvm: Formalizing the informal LLVM (Experience Report). In Proceedings of the 17th NASA Formal Methods Symposium, 2025. [ PDF | Abstract ]
[2] Kean Chen, Yuhao Liu, Wang Fang, Jennifer Paykin, Xin-Chuan Wu, Albert Schmitz, Steve Zdancewic, and Gushu Li. Verifying Fault-Tolerance of Quantum Error Correction Codes. In Ruzica Piskac and Zvonimir Rakamarić, editors, Computer Aided Verification, pages 3--27, Cham, 2025. Springer Nature Switzerland. [ PDF | Abstract ]
[3] Lucas Silver, Paul He, Ethan Cecchetti, Andrew K. Hirsch, and Steve Zdancewic. Semantics for Noninterference with Interaction Trees. In Proceedings of the 37th Annual European Conference on Object-Oriented Programming (ECOOP 2023), 2023. [ PDF | Abstract ]
[4] Stephen Mell, Favyen Bastani, Steve Zdancewic, and Osbert Bastani. Synthesizing Trajectory Queries from Examples. In Computer Aided Verification - 35th International Conference, CAV, 2023. [ PDF | Abstract ]
[5] Lawrence Dunn, Val Tannen, and Steve Zdancewic. Syntax Monads for the Working Formal Metatheorist. In Proceedings of the 6th International Conference on Applied Category Theory (ACT), 2023. [ PDF | Abstract ]
[6] Lawrence Dunn, Val Tannen, and Steve Zdancewic. Tealeaves: Structured Monads for Generic First-Order Abstract Syntax Infrastructure. In 14th International Conference on Interactive Theorem Proving (ITP), 2023. [ PDF | Abstract ]
[7] George Tolkachev, Stephen Mell, Steve Zdancewic, and Osbert Bastani. Counterfactual Explanations for Natural Language Interfaces. In 60th Annual Meeting of the Association for Computational Linguistics (ACL), 2022. (short paper). [ PDF | Abstract ]
[8] Stephen Mell, Osbert Bastani, and Steve Zdancewic. Ideograph: A Language for Expressing and Manipulating Structured Data. In Proceedings Twelfth International Workshop on Computing with Terms and Graphs (TERMGRAPH 2022), pages 65--84. Electronic Proceedings in Theoretical Computer Science, 2022. [ PDF | Abstract ]
[9] Hengchu Zhang, Wolf Honoré, Nicolas Koh, Yao Li, Yishuai Li, Li-Yao Xia, Lennart Beringer, William Mansky, Benjamin Pierce, and Steve Zdancewic. Verifying an HTTP Key-Value Server with Interaction Trees and VST. In Liron Cohen and Cezary Kaliszyk, editors, 12th International Conference on Interactive Theorem Proving (ITP 2021), volume 193 of Leibniz International Proceedings in Informatics (LIPIcs), pages 32:1--32:19, Dagstuhl, Germany, 2021. Schloss Dagstuhl -- Leibniz-Zentrum für Informatik. [ DOI | PDF | http | Abstract ]
[10] Yishuai Li, Benjamin Pierce, and Steve Zdancewic. Model-Based Testing of Networked Applications. In The ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA), 2021. [ Abstract ]
[11] Yannick Zakowski, Paul He, Chung-Kil Hur, and Steve Zdancewic. An Equational Theory for Weak Bisimulation via Generalized Parameterized Coinduction. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP), January 2020. [ PDF | Abstract ]
[12] Nicolas Koh, Yao Li, Yishuai Li, Li yao Xia, Lennart Beringer, Wolf Honoré, William Mansky, Benjamin C. Pierce, and Steve Zdancewic. From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server. In Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP), January 2019. [ PDF | Abstract ]
[13] Marcella Hastings, Brett Hemenway, Daniel Noble, and Steve Zdancewic. SoK: General Purpose Compilers for Secure Multi-Party Computation. In IEEE 2019 Symposium on Security and Privacy (Oakland), 2019. [ PDF | Abstract ]
[14] Jennifer Paykin and Steve Zdancewic. A HoTT Quantum Equational Theory. In The 16th International Conference on Quantum Physics and Logic (QPL), 2019. extended version available on arXiv. [ http | Abstract ]
[15] Christine Rizkallah, Dmitri Garbuzov, and Steve Zdancewic. A Formal Equational Theory for Call-By-Push-Value. In 9th International Conference on Interactive Theorem Proving (ITP), 2018. [ PDF | Abstract ]
[16] Robert Rand, Jennifer Paykin, Dong-Ho Lee, and Steve Zdancewic. REQUIRE: Reasoning about Reversible Quantum Circuits. In The 15th International Conference on Quantum Physics and Logic (QPL), 2018. [ PDF ]
[17] Jennifer Paykin, Robert Rand, and Steve Zdancewic. QWire: A Core Language for Quantum Circuits. In Proc. of the ACM Symposium on Principles of Programming Languages (POPL), 2017. [ PDF | Abstract ]
[18] William Mansky, Yuanfeng Peng, Steve Zdancewic, and Joseph Devietti. Verifying Dynamic Race Detection. In The 6th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP 2017), 2017. [ PDF | Abstract ]
[19] Robert Rand, Jennifer Paykin, and Steve Zdancewic. Qwire Practice: Formal Verification of Quantum Circuits in Coq. In The 14th International Conference on Quantum Physics and Logic (QPL), 2017. [ PDF | Abstract ]
[20] Jennifer Paykin and Steve Zdancewic. The Linearity Monad. In Proceedings of the 10th ACM SIGPLAN International Haskell Symposium, 2017. [ PDF | Abstract ]
[21] Jonathan Frankle, Peter-Michael Osera, David Walker, and Steve Zdancewic. Example-Directed Synthesis: A Type-Theoretic Interpretation. In Proc. of the ACM Symposium on Principles of Programming Languages (POPL), 2016. [ PDF | Abstract ]
[22] Jennifer Paykin and Steve Zdancewic. Linear λμ is CP (more or less). In A List of Successes to Change the World (Wadlerfest), 2016. [ PDF | Abstract ]
[23] Peter-Michael Osera and Steve Zdancewic. Type-and-Example-Directed Program Synthesis. In Proc. 2015 ACM SIGPLAN Conference on Programming Languages Design and Implementation (PLDI), 2015. [ PDF | Abstract ]
[24] Jeehoon Kang, Chung-Kil Hur, William Mansky, Dmitri Garbuzov, Steve Zdancewic, and Viktor Vafeiadis. A Formal C Memory Model Supporting Integer-Pointer Casts. In Proc. 2015 ACM SIGPLAN Conference on Programming Languages Design and Implementation (PLDI), 2015. [ PDF | Abstract ]
[25] William Mansky, Dmitri Garbuzov, and Steve Zdancewic. An Axiomatic Specification for Sequential Memory Models. In Computer Aided Verification - 27th International Conference, CAV 2015, 2015. [ PDF | Abstract ]
[26] Santosh Nagarakatte, Milo M. K. Martin, and Steve Zdancewic. Everything You Want to Know About Pointer-Based Checking. In 1st Summit on Advances in Programming Languages, SNAPL 2015, May 3-6, 2015, Asilomar, California, USA, pages 190--208, 2015. [ DOI | PDF | http | Abstract ]
[27] Robert Rand and Steve Zdancewic. VPHL: A Verified Partial-Correctness Logic for Probabilistic Programs. In Mathematical Foundations of Program Semantics (MFPS), 2015. [ PDF | Abstract ]
[28] Santosh Nagarakatte, Milo M. K. Martin, and Steve Zdancewic. WatchdogLite: Hardware-Accelerated Compiler-Based Pointer Checking. In Proceedings of Annual IEEE/ACM International Symposium on Code Generation and Optimization, CGO '14, pages 175:175--175:184. ACM, 2014. [ DOI | PDF | http | Abstract ]
[29] Aloïs Brunel, Marco Gaboardi, Damiano Mazza, and Steve Zdancewic. A Core Quantitative Coeffect Calculus. In Proc. of the 23rd European Symposium on Programming (ESOP), volume 8410, pages 351--370, 2014. [ PDF | Abstract ]
[30] Benoît Valiron and Steve Zdancewic. Finite vector spaces as model of simply-typed lambda-calculi. In Proceedings of the 11th International Colloquium on Theoretical Aspects of Computing (ICTAC 14), 2014. [ PDF | Abstract ]
[31] Santosh Nagarakatte, Milo M K Martin, and Steve Zdancewic. Hardware-enforced Comprehensive Memory Safety. IEEE MICRO's "Top Picks of Architecture Conferences of 2012" Issue (Micro Top Picks'2013), May/June 2013. [ PDF | Abstract ]
[32] Jianzhou Zhao, Santosh Nagarakatte, Milo M. K. Martin, and Steve Zdancewic. Formal Verification of SSA-Based Optimizations for LLVM. In Proc. 2013 ACM SIGPLAN Conference on Programming Languages Design and Implementation (PLDI), 2013. [ PDF | Abstract ]
[33] Christian DeLozier, Richard Eisenberg, Santosh Nagarakatte, Peter-Michael Osera, Milo M. K. Martin, and Steve Zdancewic. Ironclad C++: A Library-Augmented Type-Safe Subset of C++. In Proceedings of the 28th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, (OOPSLA), 2013. [ PDF | Abstract ]
[34] Santosh Nagarakatte, Milo M. K. Martin, and Steve Zdancewic. Watchdog: Hardware for Safe and Secure Manual Memory Management and Full Memory Safety. In Proceedings of the 39th International Symposium on Computer Architecture (ISCA), June 2012. [ PDF | Abstract ]
[35] Jianzhou Zhao, Santosh Nagarakatte, Milo M. K. Martin, and Steve Zdancewic. Formalizing the LLVM Intermediate Representation for Verified Program Transformations. In Proc. of the ACM Symposium on Principles of Programming Languages (POPL), 2012. [ PDF | Abstract ]
[36] Jianzhou Zhao and Steve Zdancewic. Mechanized Verification of Computing Dominators for Formalizing Compilers. In The Second International Conference on Certified Programs and Proofs (CPP), Lecture Notes in Computer Science, pages 27--42, 2012. [ PDF | Abstract ]
[37] Stephanie Weirich, Dimitrios Vytiniotis, Simon Peyton Jones, and Steve Zdancewic. Generative Type Abstraction and Type-level Computation. In Proc. of the ACM Symposium on Principles of Programming Languages (POPL), 2011. [ PDF | Abstract ]
[38] Karl Mazurak and Steve Zdancewic. Lolliproc: to Concurrency from Classical Linear Logic via Curry-Howard and Control. In Proc. of the 15th ACM SIGPLAN International Conference on Functional Programming (ICFP), 2010. [ PDF | Abstract ]
[39] Santosh Nagarakatte, Jianzhou Zhao, Milo M. K. Martin, and Steve Zdancewic. CETS: Compiler-Enforced Temporal Safety for C. In Proceedings of the ACM International Symposium on Memory Management (ISMM), 2010. [ PDF | Abstract ]
[40] Jianzhou Zhao, Qi Zhang, and Steve Zdancewic. Relational Parametricity for Polymorphic Linear Lambda Calculus. In Proceedings of the Eighth ASIAN Symposium on Programming Languages and Systems (APLAS), 2010. [ PDF | Abstract ]
[41] Santosh Nagarakatte, Jianzhou Zhao, Milo M. K. Martin, and Steve Zdancewic. SoftBound: Highly Compatible and Complete Spatial Memory Safety for C. In Proc. 2009 ACM SIGPLAN Conference on Programming Languages Design and Implementation (PLDI), 2009. [ PDF | Abstract ]
[42] J. Nathan Foster, Benjamin C. Pierce, and Steve Zdancewic. Updatable Security Views. In Proc. of 22nd IEEE Computer Security Foundations Symposium (CSF), 2009. [ PDF | Abstract ]
[43] Aaron Bohannon, Benjamin C. Pierce, Vilhelm Sjöberg, Stephanie Weirich, and Steve Zdancewic. Reactive Noninterference. In ACM Computer and Communications Security Conference (CCS), 2009. [ PDF | Abstract ]
[44] Limin Jia, Jeffrey A. Vaughan, Karl Mazurak, Jianzhou Zhao, Luke Zarko, Joseph Schorr, and Steve Zdancewic. AURA: A Programming Language for Authorization and Audit. In Proc. of the 13th ACM SIGPLAN International Conference on Functional Programming (ICFP), Victoria, British Columbia, Canada, September 2008. [ PDF | Abstract ]
[45] Joe Devietti, Colin Blundell, Milo M.K. Martin, and Steve Zdancewic. HardBound: Architectural Support for Spatial Safety of the C Programming Language. In International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), March 2008. [ PDF | Abstract ]
[46] Jeffrey A. Vaughan, Limin Jia, Karl Mazurak, and Steve Zdancewic. Evidence-based Audit. In Proc. of 21st IEEE Computer Security Foundations Symposium (CSF), pages 177--191. IEEE Computer Society Press, 2008. [ PDF | Abstract ]
[47] Peng Li and Steve Zdancewic. Combining Events And Threads For Scalable Network Services. In Proc. 2007 ACM SIGPLAN Conference on Programming Languages Design and Implementation (PLDI), pages 189--199, 2007. [ PS | Abstract ]
[48] Jeffrey A. Vaughan and Steve Zdancewic. A Cryptographic Decentralized Label Model. In IEEE 2007 Symposium on Security and Privacy (Oakland), pages 192--206, 2007. [ PDF | PS | Abstract ]
[49] Nikhil Swamy, Michael Hicks, Stephen Tse, and Steve Zdancewic. Managing Policy Updates in Security-Typed Languages. In Proc. of 19th IEEE Computer Security Foundations Workshop (CSFW), pages 202--216. IEEE Computer Society Press, 2006. [ PDF | Abstract ]
[50] Peng Li and Steve Zdancewic. Encoding Information Flow in Haskell. In Proc. of 19th IEEE Computer Security Foundations Workshop (CSFW), pages 16--27. IEEE Computer Society Press, 2006. [ PDF | Abstract ]
[51] Rajeev Alur, Pavol Černý, and Steve Zdancewic. Preserving Secrecy under Refinement. In Proc. of 33rd International Colloquium on Automata, Languages and Programming (ICALP), pages 107--118, 2006. [ PDF | Abstract ]
[52] Peng Li and Steve Zdancewic. Downgrading Policies and Relaxed Noninterference. In Proc. 32nd ACM Symp. on Principles of Programming Languages (POPL), pages 158--170, January 2005. [ PDF | Abstract ]
[53] Peng Li and Steve Zdancewic. Practical Information-flow Control in Web-based Information Systems. In Proc. of 18th IEEE Computer Security Foundations Workshop (CSFW), pages 2--15, 2005. [ PDF | Abstract ]
[54] Stephen Tse and Steve Zdancewic. Designing a Security-typed Language with Certificate-based Declassification. In Proc. of the 14th European Symposium on Programming (ESOP), volume 3444, pages 279--294, 2005. [ PDF | Abstract ]
[55] Brian E. Aydemir, Aaron Bohannon, Matthew Fairbairn, J. Nathan Foster, Benjamin C. Pierce, Peter Sewell, Dimitrios Vytiniotis, Geoffrey Washburn, Stephanie Weirich, and Steve Zdancewic. Mechanized Metatheory for the Masses: The POPLMark Challenge. In International Conference on Theorem Proving in Higher Order Logics (TPHOLs), pages 50--65, 2005. [ PDF | Abstract ]
[56] Peng Li and Steve Zdancewic. Advanced Control Flow in Java Card Programming. In Proceedings of the 2004 ACM SIGPLAN/SIGBED Conference on Languages, Compilers, and Tools for Embedded Systems (LCTES), pages 165--174, June 2004. [ PDF | Abstract ]
[57] Stephen Tse and Steve Zdancewic. Run-time Principals in Information-flow Type Systems. In IEEE 2004 Symposium on Security and Privacy (Oakland), pages 179--193. IEEE Computer Society Press, May 2004. [ PDF | PS | Abstract ]
[58] Stephen Tse and Steve Zdancewic. Translating Dependency into Parametricity. In Proc. of the 9th ACM SIGPLAN International Conference on Functional Programming (ICFP), 2004. [ PDF | PS | Abstract ]
[59] Andrew C. Myers, Andrei Sabelfeld, and Steve Zdancewic. Enforcing Robust Declassification. In Proc. of 17th IEEE Computer Security Foundations Workshop (CSFW), pages 172--186, 2004. [ PDF | Abstract ]
[60] David Walker, Steve Zdancewic, and Jay Ligatti. A Theory of Aspects. In Proc. of the 8th ACM SIGPLAN International Conference on Functional Programming (ICFP), pages 127--139, Upsala, Sweden, August 2003. [ PDF | PS | Abstract ]
[61] Steve Zdancewic and Andrew C. Myers. Observational Determinism for Concurrent Program Security. In Proc. of 16th IEEE Computer Security Foundations Workshop (CSFW), pages 29--45, Asilomar, CA, July 2003. [ PDF | PS | Abstract ]
[62] Lantian Zheng, Stephen Chong, Steve Zdancewic, and Andrew C. Myers. Building Secure Distributed Systems Using Replication and Partitioning. In IEEE 2003 Symposium on Security and Privacy (Oakland), pages 236--250. IEEE Computer Society Press, 2003. [ PDF | PS | Abstract ]
[63] Steve Zdancewic, Lantian Zheng, Nathaniel Nystrom, and Andrew C. Myers. Untrusted Hosts and Confidentiality: Secure Program Partitioning. In Proc. 18th ACM Symp. on Operating System Principles (SOSP), volume 35(5) of Operating Systems Review, pages 1--14, Banff, Canada, October 2001. [ PDF | PS | Abstract ]
[64] Steve Zdancewic and Andrew C. Myers. Robust Declassification. In Proc. of 14th IEEE Computer Security Foundations Workshop (CSFW), pages 15--23, Cape Breton, Canada, June 2001. [ PDF | PS | Abstract ]
[65] Steve Zdancewic and Andrew C. Myers. Secure Information Flow and CPS. In Proc. of the 10th European Symposium on Programming (ESOP), volume 2028 of Lecture Notes in Computer Science, pages 46--61, April 2001. [ PDF | PS | Abstract ]
[66] Steve Zdancewic, Dan Grossman, and Greg Morrisett. Principals in Programming Languages: A Syntactic Proof Technique. In Proc. of the 4th ACM SIGPLAN International Conference on Functional Programming (ICFP), pages 197--207, Paris, France, September 1999. [ PDF | PS | Abstract ]

Workshop Papers

[1] Neelakantan R. Krishnaswami, Jennifer Paykin, and Steve Zdancewic. Curry-Howard for GUIs. In POPL Off the Beaten Track (OBT), 2015. [ PDF ]
[2] Jennifer Paykin and Steve Zdancewic. A Linear/Producer/Consumer model of Classical Linear Logic (extended abstract). In Third International Workshop on Linearity, LINEARITY, 2014. [ PDF | Abstract ]
[3] Peter-Michael Osera, Vilhelm Sjöberg, and Steve Zdancewic. Dependent Ineroperability. In The Sixth ACM SIGPLAN Workshop on Programming Languages meets Program Verification (PLPV), 2012. [ PDF | Abstract ]
[4] Karl Mazurak, Jianzhou Zhao, and Steve Zdancewic. Lightweight linear types in System Fo. In ACM SIGPLAN International Workshop on Types in Languages Design and Implementation (TLDI), pages 77--88, 2010. [ PDF | Abstract ]
[5] Limin Jia and Steve Zdancewic. Encoding information flow in Aura. In Proceedings of the 2009 Workshop on Programming Languages and Analysis for Security (PLAS), pages 17--29, 2009. [ PDF | Abstract ]
[6] Michael J. May, Carl A. Gunter, Insup Lee, and Steve Zdancewic. Strong and Weak Policy Relations. In POLICY 2009, IEEE International Symposium on Policies for Distributed Systems and Networks, pages 33--36, 2009.
[7] Karl Mazurak and Steve Zdancewic. ABash: Finding Bugs in Bash Scripts. In ACM SIGPLAN Workshop on Programming Languages and Analysis for Security (PLAS), June 2007. [ PDF | Abstract ]
[8] Peng Li and Steve Zdancewic. Unifying Confidentiality and Integrity in Downgrading Policies. In Proc. of Foundations of Computer Security Workshop (FCS), 2005. [ PDF | Abstract ]
[9] Michael Hicks, Stephen Tse, Boniface Hicks, and Steve Zdancewic. Dynamic updating of information-flow policies. In Proc. of Foundations of Computer Security Workshop (FCS), 2005. [ PDF | Abstract ]
[10] Peng Li, Yun Mao, and Steve Zdancewic. Information Integrity Policies. In Proceedings of the Workshop on Formal Aspects in Security & Trust (FAST), September 2003. [ PDF | PS | Abstract ]
[11] Usa Sammapun, Raman Sharykin, Margaret Delap, Myong Kim, and Steve Zdancewic. Formalizing Java-MaC. In Proceedings of the Third Runtime Verification Workshop, pages 171--190. Electronic Notes in Theoretical Computer Science, July 2003. [ PDF | PS | Abstract ]
[12] Michael Greenwald, Carl A. Gunter, Björn Knutsson, Andre Scedrov, Jonathan M. Smith, and Steve Zdancewic. Computer Security is Not a Science (but it should be). In Proceedings of the Large-Scale Network Security Workshop, March 2003. [ PDF | PS ]
[13] Greg Morrisett, Karl Crary, Neal Glew, Dan Grossman, Richard Samuels, Frederick Smith, David Walker, Stephanie Weirich, and Steve Zdancewic. TALx86: A Realistic Typed Assembly Language. In 2nd ACM SIGPLAN Workshop on Compiler Support for System Software, pages 25--35, 1999. [ PDF | PS | Abstract ]

Edited Volumes

[1] Pierpaolo Degano, Ralf Küsters, Luca Viganò, and Steve Zdancewic, editors. Joint workshop on foundations of computer security and automated reasoning for security protocol analysis (FCS-ARSPA '06), volume 206 of Information and Computation. Elsevier, 2008.
[2] Vugranam C. Shreedhar and Steve Zdancewic, editors. Proceedings of the 2006 Workshop on Programming Languages and Analysis for Security (PLAS). ACM, 2006.

Technical Reports, Work in Progress, and Unpublished Papers

[1] Vadim Zaliva, Yannick Zakowski, Ilia Zaichuk, Valerii Huhnin, Calvin Beck, Irene Yoon, and Steve Zdancewic. HELIX: Verified compilation of cyber-physical control systems to LLVM IR, 2026. [ arXiv | http ]
[2] Jennifer Paykin and Steve Zdancewic. A HoTT Quantum Equational Theory (Extended Version). available on arXiv, 2019. [ http | Abstract ]
[3] Dmitri Garbuzov, William Mansky, Christine Rizkallah, and Steve Zdancewic. Structural Operational Semantics for Control Flow Graph Machines, 2018. [ arXiv | PDF | Abstract ]
[4] Jennifer Paykin and Steve Zdancewic. A Linear/Producer/Consumer model of Classical Linear Logic. Technical report, University of Pennsylvania, 2014. [ PDF | Abstract ]
[5] Christian DeLozier, Richard Eisenberg, Santosh Nagarakatte, Peter-Michael Osera, Milo M.K. Martin, and Steve Zdancewic. Ironclad C++: A library-Augmented Type-Safe Subset of C++. Technical Report MS-CIS-13-05, University of Pennsylvania, March 2013. [ PDF ]
[6] Jianzhou Zhao, Qi Zhang, and Steve Zdancewic. Relational Parametricity for Polymorphic Linear Lambda Calculus (Extended TR). 2010. [ PDF | Abstract ]
[7] Jeffrey C. Vaughan, Limin Jia, Karl Mazurak, and Steve Zdancewic. Evidence-based Audit, Technical Appendix. Technical Report MS-CIS-08-09, University of Pennsylvania, 2008. [ PDF ]
[8] Limin Jia, Jeffrey A. Vaughan, Karl Mazurak, Jianzhou Zhao, Luke Zarko, Joseph Schorr, and Steve Zdancewic. AURA:Preliminary Technical Results. Technical Report MS-CIS-08-10, University of Pennsylvania, 2008. [ PDF ]
[9] Stephen Tse and Steve Zdancewic. Concise Concrete Syntax. Technical Report MS-CIS-08-11, University of Pennsylvania, 2008. [ PDF ]
[10] Brian Aydemir, Stephanie Weirich, and Steve Zdancewic. Abstracting Syntax. (15 pages), 2008.
[11] Stephen Tse and Steve Zdancewic. Translating Dependency into Parametricity. (33 pages) Accepted to Journal of Functional Programming, pending revisions, 2006.
[12] Stephen Tse and Steve Zdancewic. Translating Dependency into Parametricity. Technical Report MIS-CIS-04-01, University of Pennsylvania, 2004. [ PDF | Abstract ]
[13] Stephen Tse and Steve Zdancewic. Designing a Security-typed Language with Certificate-based Declassification. Technical Report MIS-CIS-04-16, University of Pennsylvania, 2004. [ PDF | Abstract ]
[14] Stephen Tse and Steve Zdancewic. Run-time Principals in Information-flow Type Systems. Technical Report MS-CIS-03-39, University of Pennsylvania, 2003. The conference version appears in IEEE Security and Privacy 2004. [ PDF | PS | Abstract ]
[15] Stephan A. Zdancewic. Programming Languages for Information Security. PhD thesis, Cornell University, August 2002. [ PDF | PS | Abstract ]
[16] Steve Zdancewic, Lantian Zheng, Nathaniel Nystrom, and Andrew C. Myers. Secure Program Partitioning. Technical Report 2001-1846, Computer Science Dept., Cornell University, 2001. [ PDF | PS | Abstract ]
[17] Steve Zdancewic and Andrew C. Myers. Confidentiality and Integrity with Untrusted Hosts. Technical Report 2000-1810, Computer Science Dept., Cornell University, 2000. [ PDF | PS | Abstract ]
[18] Steve Zdancewic and Dan Grossman. Principals in Programming Languages: Technical Results. Technical Report TR99-1752, Computer Science Dept., Cornell University, June 1999. [ PDF | PS | Abstract ]