POPL 2023
74 papers
- A Bowtie for a Beast: Overloading, Eta Expansion, and Extensible Data Types in F⋈
- A Calculus for Amortized Expected Runtimes
- A Compositional Theory of Linearizability
- A Core Calculus for Equational Proofs of Cryptographic Protocols
- A General Noninterference Policy for Polynomial Time
- A High-Level Separation Logic for Heap Space under Garbage Collection
- A Partial Order View of Message-Passing Communication Models
- A Robust Theory of Series Parallel Graphs
- A Type-Based Approach to Divide-and-Conquer Recursion in Coq
- ADEV: Sound Automatic Differentiation of Expected Values of Probabilistic Programs
- Admissible Types-to-PERs Relativization in Higher-Order Logic
- Affine Monads and Lazy Structures for Bayesian Programming
- An Algebra of Alignment for Relational Verification
- An Operational Approach to Library Abstraction under Relaxed Memory Concurrency
- An Order-Theoretic Analysis of Universe Polymorphism
- CN: Verifying Systems C Code with Separation-Logic Refinement Types
- Choice Trees: Representing Nondeterministic, Recursive, and Impure Programs in Coq
- Combining Functional and Automata Synthesis to Discover Causal Reactive Programs
- Comparative Synthesis: Learning Near-Optimal Network Designs by Query
- Conditional Contextual Refinement
- Context-Bounded Verification of Context-Free Specifications
- CoqQ: Foundational Verification of Quantum Programs
- Dargent: A Silver Bullet for Verified Data Layout Refinement
- Deconstructing the Calculus of Relations with Tape Diagrams
- DimSum: A Decentralized Approach to Multi-language Semantics and Verification
- Dynamic Race Detection with O(1) Samples
- Efficient Dual-Numbers Reverse AD via Well-Known Program Transformations
- Elements of Quantitative Rewriting
- Executing Microservice Applications on Serverless, Correctly
- Fast Coalgebraic Bisimilarity Minimization
- FlashFill++: Scaling Programming by Example by Cutting to the Chase
- Formally Verified Native Code Generation in an Effectful JIT: Turning the CompCert Backend into a Formally Verified JIT Compiler
- From SMT to ASP: Solver-Based Approaches to Solving Datalog Synthesis-as-Rule-Selection Problems
- Grisette: Symbolic Compilation as a Functional Programming Library
- HFL(Z) Validity Checking for Automated Program Verification
- Hefty Algebras: Modular Elaboration of Higher-Order Algebraic Effects
- Higher-Order Leak and Deadlock Free Locks
- Higher-Order MSL Horn Constraints
- Impredicative Observational Equality
- Inductive Synthesis of Structurally Recursive Functional Programs from Non-recursive Expressions
- Kater: Automating Weak Memory Model Metatheory and Consistency Checking
- Locally Nameless Sets
- MSWasm: Soundly Enforcing Memory-Safe Execution of Unsafe Code
- Making a Type Difference: Subtraction on Intersection Types as Generalized Record Operations
- Modular Primal-Dual Fixpoint Logic Solving for Temporal Verification
- On the Expressive Power of String Constraints
- Optimal CHC Solving via Termination Proofs
- Probabilistic Resource-Aware Session Types
- Proto-Quipper with Dynamic Lifting
- Quantitative Inhabitation for Different Lambda Calculi in a Unifying Framework
- Qunity: A Unified Language for Quantum and Classical Computing
- Reconciling Shannon and Scott with a Lattice of Computable Information
- Recursive Subtyping for All
- SSA Translation Is an Abstract Interpretation
- Single-Source-Single-Target Interleaved-Dyck Reachability via Integer Linear Programming
- Smoothness Analysis for Probabilistic Programs with Application to Optimised Variational Inference
- Statically Resolvable Ambiguity
- Step-Indexed Logical Relations for Countable Nondeterminism and Probabilistic Choice
- Stratified Commutativity in Verification Algorithms for Concurrent Programs
- Tail Recursion Modulo Context: An Equational Approach
- Taking Back Control in an Intermediate Representation for GPU Computing
- Temporal Verification with Answer-Effect Modification: Dependent Temporal Type-and-Effect System with Delimited Continuations
- The Fine-Grained Complexity of CFL Reachability
- The Geometry of Causality: Multi-token Geometry of Interaction and Its Causal Unfolding
- The Path to Durable Linearizability
- Top-Down Synthesis for Library Learning
- Towards a Higher-Order Mathematical Operational Semantics
- Type-Preserving, Dependence-Aware Guide Generation for Sound, Effective Amortized Probabilistic Inference
- Unrealizability Logic
- When Less Is More: Consequence-Finding in a Weak Theory of Arithmetic
- Why Are Proofs Relevant in Proof-Relevant Models?
- Witnessability of Undecidable Problems
- You Only Linearize Once: Tangents Transpose to Gradients
- babble: Learning Better Abstractions with E-Graphs and Anti-unification