Steve Zdancewic

Osbert Bastani

Proc. ACM Program. Lang., January, 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.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2024

Structural temporal logic for mechanized program verification.

[BibT_eX]

[DOI]

Eleftherios Ioannidis

Yannick Zakowski

Sebastian Angel

CoRR, 2024

An Opportunistically Parallel Lambda Calculus for Performant Composition of Large Language Models.

[BibT_eX]

[DOI]

Stephen Mell

Osbert Bastani

CoRR, 2024

A Two-Phase Infinite/Finite Low-Level Memory Model.

[BibT_eX]

[DOI]

CoRR, 2024

2023

A Bowtie for a Beast: Overloading, Eta Expansion, and Extensible Data Types in F⋈.

[BibT_eX]

[DOI]

Nick Rioux

Xuejing Huang

Bruno C. d. S. Oliveira

Proc. ACM Program. Lang., January, 2023

Choice Trees: Representing Nondeterministic, Recursive, and Impure Programs in Coq.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., January, 2023

Semantics for Noninterference with Interaction Trees (Artifact).

[BibT_eX]

[DOI]

Dagstuhl Artifacts Ser., 2023

Syntax Monads for the Working Formal Metatheorist.

[BibT_eX]

[DOI]

Lawrence Dunn

Val Tannen

Proceedings of the Sixth International Conference on Applied Category Theory 2023, 2023

Tealeaves: Structured Monads for Generic First-Order Abstract Syntax Infrastructure.

[BibT_eX]

[DOI]

Lawrence Dunn

Val Tannen

Proceedings of the 14th International Conference on Interactive Theorem Proving, 2023

Semantics for Noninterference with Interaction Trees.

[BibT_eX]

[DOI]

Proceedings of the 37th European Conference on Object-Oriented Programming, 2023

Synthesizing Trajectory Queries from Examples.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 35th International Conference, 2023

2022

Formal reasoning about layered monadic interpreters.

[BibT_eX]

[DOI]

Irene Yoon

Yannick Zakowski

Proc. ACM Program. Lang., 2022

C4: verified transactional objects.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2022

Ideograph: A Language for Expressing and Manipulating Structured Data.

[BibT_eX]

[DOI]

Stephen Mell

Osbert Bastani

Proceedings of the Proceedings Twelfth International Workshop on Computing with Terms and Graphs, 2022

Counterfactual Explanations for Natural Language Interfaces.

[BibT_eX]

[DOI]

Proceedings of the 60th Annual Meeting of the Association for Computational Linguistics (Volume 2: Short Papers), 2022

2021

Replication Package for Article: Model-Based Testing of Networked Applications.

[BibT_eX]

[DOI]

Yishuai Li

Benjamin C. Pierce

Dataset, May, 2021

Modular, compositional, and executable formal semantics for LLVM IR.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2021

Dijkstra monads forever: termination-sensitive specifications for interaction trees.

[BibT_eX]

[DOI]

Lucas Silver

Proc. ACM Program. Lang., 2021

A type system for extracting functional specifications from memory-safe imperative programs.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2021

Verifying an HTTP Key-Value Server with Interaction Trees and VST.

[BibT_eX]

[DOI]

Proceedings of the 12th International Conference on Interactive Theorem Proving, 2021

Model-based testing of networked applications.

[BibT_eX]

[DOI]

Yishuai Li

Benjamin C. Pierce

Proceedings of the ISSTA '21: 30th ACM SIGSOFT International Symposium on Software Testing and Analysis, 2021

2020

Interaction trees: representing recursive and impure programs in Coq.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2020

Computation focusing.

[BibT_eX]

[DOI]

Nick Rioux

Proc. ACM Program. Lang., 2020

An equational theory for weak bisimulation via generalized parameterized coinduction.

[BibT_eX]

[DOI]

Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2020

2019

Synthesizing symmetric lenses.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2019

Interaction Trees: Representing Recursive and Impure Programs in Coq (Work In Progress).

[BibT_eX]

[DOI]

CoRR, 2019

A HoTT Quantum Equational Theory (Extended Version).

[BibT_eX]

[DOI]

CoRR, 2019

SoK: General Purpose Compilers for Secure Multi-Party Computation.

[BibT_eX]

[DOI]

Proceedings of the 2019 IEEE Symposium on Security and Privacy, 2019

From C to interaction trees: specifying, verifying, and testing a networked server.

[BibT_eX]

[DOI]

Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2019

2018

Synthesizing bijective lenses.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2018

Synthesizing quotient lenses.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2018

ReQWIRE: Reasoning about Reversible Quantum Circuits.

[BibT_eX]

[DOI]

Proceedings of the Proceedings 15th International Conference on Quantum Physics and Logic, 2018

Structural Operational Semantics for Control Flow Graph Machines.

[BibT_eX]

[DOI]

CoRR, 2018

Technical perspective: Building bug-free compilers.

[BibT_eX]

[DOI]

Commun. ACM, 2018

A Formal Equational Theory for Call-By-Push-Value.

[BibT_eX]

[DOI]

Christine Rizkallah

Dmitri Garbuzov

Proceedings of the Interactive Theorem Proving - 9th International Conference, 2018

2017

QWIRE Practice: Formal Verification of Quantum Circuits in Coq.

[BibT_eX]

[DOI]

Robert Rand

Proceedings of the Proceedings 14th International Conference on Quantum Physics and Logic, 2017

QWIRE: a core language for quantum circuits.

[BibT_eX]

[DOI]

Robert Rand

Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, 2017

The linearity Monad.

[BibT_eX]

[DOI]

Proceedings of the 10th ACM SIGPLAN International Symposium on Haskell, 2017

Verifying dynamic race detection.

[BibT_eX]

[DOI]

Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, 2017

2016

Example-directed synthesis: a type-theoretic interpretation.

[BibT_eX]

[DOI]

Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2016

Linear λμ is CP (more or less).

[BibT_eX]

[DOI]

Proceedings of the A List of Successes That Can Change the World, 2016

2015

VPHL: A Verified Partial-Correctness Logic for Probabilistic Programs.

[BibT_eX]

[DOI]

Robert Rand

Proceedings of the 31st Conference on the Mathematical Foundations of Programming Semantics, 2015

Everything You Want to Know About Pointer-Based Checking.

[BibT_eX]

[DOI]

Proceedings of the 1st Summit on Advances in Programming Languages, 2015

Type-and-example-directed program synthesis.

[BibT_eX]

[DOI]

Peter-Michael Osera

Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2015

A formal C memory model supporting integer-pointer casts.

[BibT_eX]

[DOI]

Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2015

An Axiomatic Specification for Sequential Memory Models.

[BibT_eX]

[DOI]

William Mansky

Dmitri Garbuzov

Proceedings of the Computer Aided Verification - 27th International Conference, 2015

2014

Modeling Simply-Typed Lambda Calculi in the Category of Finite Vector Spaces.

[BibT_eX]

[DOI]

Benoît Valiron

Sci. Ann. Comput. Sci., 2014

A Linear/Producer/Consumer Model of Classical Linear Logic.

[BibT_eX]

[DOI]

Proceedings of the Proceedings Third International Workshop on Linearity, 2014

Finite Vector Spaces as Model of Simply-Typed Lambda-Calculi.

[BibT_eX]

[DOI]

Benoît Valiron

Proceedings of the Theoretical Aspects of Computing - ICTAC 2014, 2014

A Core Quantitative Coeffect Calculus.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems, 2014

WatchdogLite: Hardware-Accelerated Compiler-Based Pointer Checking.

[BibT_eX]

[DOI]

Proceedings of the 12th Annual IEEE/ACM International Symposium on Code Generation and Optimization, 2014

2013

Hardware-Enforced Comprehensive Memory Safety.

[BibT_eX]

[DOI]

IEEE Micro, 2013

Formal verification of SSA-based optimizations for LLVM.

[BibT_eX]

[DOI]

Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, 2013

Ironclad C++: a library-augmented type-safe subset of c++.

[BibT_eX]

[DOI]

Proceedings of the 2013 ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages & Applications, 2013

2012

Formalizing the LLVM intermediate representation for verified program transformations.

[BibT_eX]

[DOI]

Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2012

Dependent interoperability.

[BibT_eX]

[DOI]

Peter-Michael Osera

Vilhelm Sjöberg

Proceedings of the sixth workshop on Programming Languages meets Program Verification, 2012

Watchdog: Hardware for safe and secure manual memory management and full memory safety.

[BibT_eX]

[DOI]

Proceedings of the 39th International Symposium on Computer Architecture (ISCA 2012), 2012

Mechanized Verification of Computing Dominators for Formalizing Compilers.

[BibT_eX]

[DOI]

Jianzhou Zhao

Proceedings of the Certified Programs and Proofs - Second International Conference, 2012

2011

Generative type abstraction and type-level computation.

[BibT_eX]

[DOI]

Stephanie Weirich

Dimitrios Vytiniotis

Simon L. Peyton Jones

Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2011

2010

Arrows for secure information flow.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2010

Lightweight linear types in system fdegree.

[BibT_eX]

[DOI]

Karl Mazurak

Jianzhou Zhao

Proceedings of TLDI 2010: 2010 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, 2010

CETS: compiler enforced temporal safety for C.

[BibT_eX]

[DOI]

Proceedings of the 9th International Symposium on Memory Management, 2010

Lolliproc: to concurrency from classical linear logic via curry-howard and control.

[BibT_eX]

[DOI]

Karl Mazurak

Proceedings of the Proceeding of the 15th ACM SIGPLAN international conference on Functional programming, 2010

Relational Parametricity for a Polymorphic Linear Lambda Calculus.

[BibT_eX]

[DOI]

Jianzhou Zhao

Qi Zhang

Proceedings of the Programming Languages and Systems - 8th Asian Symposium, 2010

2009

An overview of the Oregon programming languages summer school.

[BibT_eX]

[DOI]

ACM SIGPLAN Notices, 2009

Strong and Weak Policy Relations.

[BibT_eX]

[DOI]

Proceedings of the POLICY 2009, 2009

SoftBound: highly compatible and complete spatial memory safety for c.

[BibT_eX]

[DOI]

Proceedings of the 2009 ACM SIGPLAN Conference on Programming Language Design and Implementation, 2009

Encoding information flow in Aura.

[BibT_eX]

[DOI]

Limin Jia

Proceedings of the 2009 Workshop on Programming Languages and Analysis for Security, 2009

Updatable Security Views.

[BibT_eX]

[DOI]

J. Nathan Foster

Benjamin C. Pierce

Proceedings of the 22nd IEEE Computer Security Foundations Symposium, 2009

Reactive noninterference.

[BibT_eX]

[DOI]

Proceedings of the 2009 ACM Conference on Computer and Communications Security, 2009

2008

Joint workshop on foundations of computer security and automated reasoning for security protocol analysis (FCS-ARSPA '06).

[BibT_eX]

[DOI]

Inf. Comput., 2008

AURA: a programming language for authorization and audit.

[BibT_eX]

[DOI]

Proceedings of the Proceeding of the 13th ACM SIGPLAN international conference on Functional programming, 2008

Evidence-Based Audit.

[BibT_eX]

[DOI]

Proceedings of the 21st IEEE Computer Security Foundations Symposium, 2008

Hardbound: architectural support for spatial safety of the C programming language.

[BibT_eX]

[DOI]

Proceedings of the 13th International Conference on Architectural Support for Programming Languages and Operating Systems, 2008

2007

Run-time principals in information-flow type systems.

[BibT_eX]

[DOI]

Stephen Tse

ACM Trans. Program. Lang. Syst., 2007

A Cryptographic Decentralized Label Model.

[BibT_eX]

[DOI]

Jeffrey A. Vaughan

Proceedings of the 2007 IEEE Symposium on Security and Privacy (S&P 2007), 2007

Application-level concurrency: combining events and treads: invited talk.

[BibT_eX]

[DOI]

Proceedings of the POPL 2007 Workshop on Declarative Aspects of Multicore Programming, 2007

Combining events and threads for scalable network services implementation and evaluation of monadic, application-level concurrency primitives.

[BibT_eX]

[DOI]

Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation, 2007

2006

A type-theoretic interpretation of pointcuts and advice.

[BibT_eX]

[DOI]

Jay Ligatti

David Walker

Sci. Comput. Program., 2006

Enforcing Robust Declassification and Qualified Robustness.

[BibT_eX]

[DOI]

Andrei Sabelfeld

J. Comput. Secur., 2006

Preserving Secrecy Under Refinement.

[BibT_eX]

[DOI]

Rajeev Alur

Pavol Cerný

Proceedings of the Automata, Languages and Programming, 33rd International Colloquium, 2006

Managing Policy Updates in Security-Typed Languages.

[BibT_eX]

[DOI]

Proceedings of the 19th IEEE Computer Security Foundations Workshop, 2006

Encoding Information Flow in Haskell.

[BibT_eX]

[DOI]

Proceedings of the 19th IEEE Computer Security Foundations Workshop, 2006

2005

It Is Time to Mechanize Programming Language Metatheory.

[BibT_eX]

[DOI]

Proceedings of the Verified Software: Theories, 2005

Mechanized Metatheory for the Masses: The PoplMark Challenge.

[BibT_eX]

[DOI]

Proceedings of the Theorem Proving in Higher Order Logics, 18th International Conference, 2005

Downgrading policies and relaxed noninterference.

[BibT_eX]

[DOI]

Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2005

A Design for a Security-Typed Language with Certificate-Based Declassification.

[BibT_eX]

[DOI]

Stephen Tse

Proceedings of the Programming Languages and Systems, 2005

Practical Information-flow Control in Web-Based Information Systems.

[BibT_eX]

[DOI]

Proceedings of the 18th IEEE Computer Security Foundations Workshop, 2005

2004

Advanced control flow in Java card programming.

[BibT_eX]

[DOI]

Proceedings of the 2004 ACM SIGPLAN/SIGBED Conference on Languages, 2004

Translating dependency into parametricity.

[BibT_eX]

[DOI]

Stephen Tse

Proceedings of the Ninth ACM SIGPLAN International Conference on Functional Programming, 2004

Enforcing Robust Declassification.

[BibT_eX]

[DOI]

Andrei Sabelfeld

Proceedings of the 17th IEEE Computer Security Foundations Workshop, 2004

2003

Formalizing Java-MaC.

[BibT_eX]

[DOI]

Proceedings of the Third Workshop on Run-time Verification, 2003

Using Replication and Partitioning to Build Secure Distributed Systems.

[BibT_eX]

[DOI]

Proceedings of the 2003 IEEE Symposium on Security and Privacy (S&P 2003), 2003

A Type System for Robust Declassification.

[BibT_eX]

[DOI]

Proceedings of 19th Conference on the Mathematical Foundations of Programming Semantics, 2003

A theory of aspects.

[BibT_eX]

[DOI]

David Walker

Jay Ligatti

Proceedings of the Eighth ACM SIGPLAN International Conference on Functional Programming, 2003

Observational Determinism for Concurrent Program Security.

[BibT_eX]

[DOI]

Proceedings of the 16th IEEE Computer Security Foundations Workshop (CSFW-16 2003), 30 June, 2003

2002

Programming Languages for Information Security.

[BibT_eX]

PhD thesis, 2002

Secure program partitioning.

[BibT_eX]

[DOI]

ACM Trans. Comput. Syst., 2002

Secure Information Flow via Linear Continuations.

[BibT_eX]

[DOI]

High. Order Symb. Comput., 2002

2001

Untrusted Hosts and Confidentiality: Secure Program Partitioning.

[BibT_eX]

[DOI]

Proceedings of the 18th ACM Symposium on Operating System Principles, 2001

Secure Information Flow and CPS.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems, 2001

Robust Declassification.

[BibT_eX]

[DOI]

Proceedings of the 14th IEEE Computer Security Foundations Workshop (CSFW-14 2001), 2001

2000

Syntactic type abstraction.

[BibT_eX]

[DOI]

Dan Grossman

J. Gregory Morrisett

ACM Trans. Program. Lang. Syst., 2000

1999

Principals in Programming Languages: A Syntactic Proof Technique.

[BibT_eX]

[DOI]