POPL 2024
93 papers
- A Case for Synthesis of Recursive Quantum Unitary Programs
- A Core Calculus for Documents: Or, Lambda: The Ultimate Document
- A Formalization of Core Why3 in Coq
- A Universal, Sound, and Complete Forward Reasoning Technique for Machine-Verified Proofs of Linearizability
- API-Driven Program Synthesis for Testing Static Typing Implementations
- Algebraic Effects Meet Hoare Logic in Cubical Agda
- An Axiomatic Basis for Computer Programming on the Relaxed Arm-A Architecture: The AxSL Logic
- An Infinite Needle in a Finite Haystack: Finding Infinite Counter-Models in Deductive Verification
- An Iris Instance for Verifying CompCert C Programs
- Answer Refinement Modification: Refinement Type System for Algebraic Effects and Handlers
- Asynchronous Probabilistic Couplings in Higher-Order Separation Logic
- Automatic Parallelism Management
- Calculational Design of [In]Correctness Transformational Program Logics by Abstract Interpretation
- Coarser Equivalences for Causal Concurrency
- Commutativity Simplifies Proofs of Parameterized Programs
- Deadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-Order Message Passing
- Decalf: A Directed, Effectful Cost-Aware Logical Framework
- Deciding Asynchronous Hyperproperties for Recursive Programs
- Decision and Complexity of Dolev-Yao Hyperproperties
- DisLog: A Separation Logic for Disentanglement
- Disentanglement with Futures, State, and Interaction
- EasyBC: A Cryptography-Specific Language for Security Analysis of Block Ciphers against Differential Cryptanalysis
- Effectful Software Contracts
- Efficient Bottom-Up Synthesis for Programs with Local Variables
- Efficient CHAD
- Efficient Matching of Regular Expressions with Lookaround Assertions
- Enhanced Enumeration Techniques for Syntax-Guided Synthesis of Bit-Vector Manipulations
- Enriched Presheaf Model of Quantum FPC
- Explicit Effects and Effect Constraints in ReML
- Flan: An Expressive and Efficient Datalog Compiler for Program Analysis
- Fully Composable and Adequate Verified Compilation with Direct Refinements between Open Modules
- Fusing Direct Manipulations into Functional Programs
- Generating Well-Typed Terms That Are Not "Useless"
- Guided Equality Saturation
- Higher Order Bayesian Networks, Exactly
- How Hard Is Weak-Memory Testing?
- Ill-Typed Programs Don't Evaluate
- Implementation and Synthesis of Math Library Functions
- Indexed Types for a Statically Safe WebAssembly
- Inference of Probabilistic Programs with Moment-Matching Gaussian Mixtures
- Inference of Robust Reachability Constraints
- Internal Parametricity, without an Interval
- Internal and Observational Parametricity for Cubical Agda
- Internalizing Indistinguishability with Dependent Types
- Mechanizing Refinement Types
- Modular Denotational Semantics for Effects with Guarded Interaction Trees
- Monotonicity and the Precision of Program Analysis
- Mostly Automated Verification of Liveness Properties for Distributed Protocols with Ranking Functions
- Nominal Recursors as Epi-Recursors
- On Learning Polynomial Recursive Programs
- On Model-Checking Higher-Order Effectful Programs
- On-the-Fly Static Analysis via Dynamic Bidirected Dyck Reachability
- Optimal Program Synthesis via Abstract Interpretation
- Orthologic with Axioms
- Parametric Subtyping for Structural Parametric Polymorphism
- Parikh's Theorem Made Symbolic
- Pipelines and Beyond: Graph Types for ADTs with Futures
- Polymorphic Reachability Types: Tracking Freshness, Aliasing, and Separation in Higher-Order Generic Programs
- Polymorphic Type Inference for Dynamic Languages
- Polynomial Time and Dependent Types
- Polyregular Functions on Unordered Trees of Bounded Height
- Positive Almost-Sure Termination: Complexity and Proof Rules
- Predictive Monitoring against Pattern Regular Languages
- Probabilistic Programming Interfaces for Random Graphs: Markov Categories, Graphons, and Nominal Sets
- Programmatic Strategy Synthesis: Resolving Nondeterminism in Probabilistic Programs
- Programming-by-Demonstration for Long-Horizon Robot Tasks
- Quantum Bisimilarity via Barbs and Contexts: Curbing the Power of Non-deterministic Observers
- Quotient Haskell: Lightweight Quotient Types for All
- Ramsey Quantifiers in Linear Arithmetics
- ReLU Hull Approximation
- Reachability in Continuous Pushdown VASS
- Regular Abstractions for Array Systems
- Securing Verified IO Programs Against Unverified Code in F
- Semantic Code Refactoring for Abstract Data Types
- Shoggoth: A Formal Foundation for Strategic Rewriting
- SimuQ: A Framework for Programming Quantum Hamiltonian Simulation with Analog Compilation
- Solvable Polynomial Ideals: The Ideal Reflection for Program Analysis
- Solving Infinite-State Games via Acceleration
- Sound Gradual Verification with Symbolic Execution
- Soundly Handling Linearity
- Strong Invariants Are Hard: On the Hardness of Strongest Polynomial Invariants for (Probabilistic) Programs
- The Complex(ity) Landscape of Checking Infinite Descent
- The Essence of Generalized Algebraic Data Types
- The Logical Essence of Well-Bracketed Control Flow
- Thunks and Debits in Separation Logic with Time Credits
- Total Type Error Localization and Recovery with Holes
- Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement
- Type-Based Gradual Typing Performance Optimization
- Unboxed Data Constructors: Or, How cpp Decides a Halting Problem
- VST-A: A Foundationally Sound Annotation Verifier
- Validation of Modern JSON Schema: Formalization and Complexity
- When Subtyping Constraints Liberate: A Novel Type Inference Approach for First-Class Polymorphism
- With a Few Square Roots, Quantum Computing Is as Easy as Pi