POPL（CCF A）（共 609 篇）
202692 篇 · 10(POPL)
A Modular Static Cost Analysis for GPU Warp-Level Parallelism
POPL 10(POPL)2026
Extensible Data Types with Ad-Hoc Polymorphism
POPL 10(POPL)2026
Parameterized Infinite-State Reactive Synthesis
POPL 10(POPL)2026
A Verified High-Performance Composable Object Library for Remote Direct Memory Access
POPL 10(POPL)2026
The Relative Monadic Metalanguage
POPL 10(POPL)2026
Characterizing Sets of Theories That Can Be Disjointly Combined
POPL 10(POPL)2026
ArchSem: Reusable Rigorous Semantics of Relaxed Architectures
POPL 10(POPL)2026
ChiSA: Static Analysis for Lightweight Chisel Verification
POPL 10(POPL)2026
Qudit Quantum Programming with Projective Cliffords
POPL 10(POPL)2026
JAX Autodiff from a Linear Logic Perspective
POPL 10(POPL)2026
Higher-Order Behavioural Conformances via Fibrations
POPL 10(POPL)2026
Determination Problems for Orbit Closures and Matrix Groups
POPL 10(POPL)2026
Hyperfunctions: Communicating Continuations
POPL 10(POPL)2026
Coco: Corecursion with Compositional Heterogeneous Productivity
POPL 10(POPL)2026
A Synthetic Reconstruction of Multiparty Session Types
POPL 10(POPL)2026
Di- is for Directed: First-Order Directed Type Theory via Dinaturality
POPL 10(POPL)2026
A Lazy, Concurrent Convertibility Checker
POPL 10(POPL)2026
Canonicity for Indexed Inductive-Recursive Types
POPL 10(POPL)2026
A Complementary Approach to Incorrectness Typing
POPL 10(POPL)2026
Local Contextual Type Inference
POPL 10(POPL)2026
The Complexity of Testing Message-Passing Concurrency
POPL 10(POPL)2026
A Relational Separation Logic for Effect Handlers
POPL 10(POPL)2026
Separating the Wheat from the Chaff: Understanding (In-)Completeness of Proof Mechanisms for Separation Logic with Inductive Definitions
POPL 10(POPL)2026
TypeDis: A Type System for Disentanglement
POPL 10(POPL)2026
An Expressive Assertion Language for Quantum Programs
POPL 10(POPL)2026
RapunSL: Untangling Quantum Computing with Separation, Linear Combination and Mixing
POPL 10(POPL)2026
Algorithmic Conversion with Surjective Pairing: A Syntactic and Untyped Approach
POPL 10(POPL)2026
Big-Stop Semantics: Small-Step Semantics in a Big-Step Judgment
POPL 10(POPL)2026
Context-Free-Language Reachability for Almost-Commuting Transition Systems
POPL 10(POPL)2026
Hadamard-Pi: Equational Quantum Programming
POPL 10(POPL)2026
Rows and Capabilities as Modal Effects
POPL 10(POPL)2026
Stateful Differential Operators for Incremental Computing
POPL 10(POPL)2026
Bounded Treewidth, Multiple Context-Free Grammars, and Downward Closures
POPL 10(POPL)2026
Tropical Mathematics and the Lambda-Calculus II: Tropical Geometry of Probabilistic Programming Languages
POPL 10(POPL)2026
Accelerating Syntax-Guided Program Synthesis by Optimizing Domain-Specific Languages
POPL 10(POPL)2026
Bayesian Separation Logic: A Logical Foundation and Axiomatic Semantics for Probabilistic Programming
POPL 10(POPL)2026
Probabilistic Programming with Vectorized Programmable Inference
POPL 10(POPL)2026
Abstraction Functions as Types: Modular Verification of Cost and Behavior in Dependent Type Theory
POPL 10(POPL)2026
DafnyMPI: A Dafny Library for Verifying Message-Passing Concurrent Programs
POPL 10(POPL)2026
Parameterized Verification of Quantum Circuits
POPL 10(POPL)2026
Handling Higher-Order Effectful Operations with Judgemental Monadic Laws
POPL 10(POPL)2026
Compiling to Linear Neurons
POPL 10(POPL)2026
Generating Compilers for Qubit Mapping and Routing
POPL 10(POPL)2026
Domain-Theoretic Semantics for Functional Logic Programming
POPL 10(POPL)2026
Zoo: A Framework for the Verification of Concurrent OCaml 5 Programs using Separation Logic
POPL 10(POPL)2026
Normalisation for First-Class Universe Levels
POPL 10(POPL)2026
A Logic for the Imprecision of Abstract Interpretations
POPL 10(POPL)2026
Lazy Linearity for a Core Functional Language
POPL 10(POPL)2026
Counting and Sampling Traces in Regular Languages
POPL 10(POPL)2026
Towards Pen-and-Paper-Style Equational Reasoning in Interactive Theorem Provers by Equality Saturation
POPL 10(POPL)2026
Foundational Multi-Modal Program Verifiers
POPL 10(POPL)2026
Let Generalization, Polymorphic Recursion, and Variable Minimization in Boolean-Kinded Type Systems
POPL 10(POPL)2026
Network Change Validation with Relational NetKAT
POPL 10(POPL)2026
Quantum Circuits Are Just a Phase
POPL 10(POPL)2026
Consistent Updates for Scalable Microservices
POPL 10(POPL)2026
Dependent Coeffects for Local Sensitivity Analysis
POPL 10(POPL)2026
Encode the Cake and Eat It Too: Controlling Computation in Type Theory, Locally
POPL 10(POPL)2026
Classical Notions of Computation and the Hasegawa-Thielecke Theorem
POPL 10(POPL)2026
AdapTT: Functoriality for Dependent Type Casts
POPL 10(POPL)2026
Nice to Meet You: Synthesizing Practical MLIR Abstract Transformers
POPL 10(POPL)2026
Recurrence Sets for Proving Fair Non-termination under Axiomatic Memory Consistency Models
POPL 10(POPL)2026
All for One and One for All: Program Logics for Exploiting Internal Determinism in Parallel Programs
POPL 10(POPL)2026
Inductive Program Synthesis by Meta-Analysis-Guided Hole Filling
POPL 10(POPL)2026
ChopChop: A Programmable Framework for Semantically Constraining the Output of Language Models
POPL 10(POPL)2026
Typing Strictness
POPL 10(POPL)2026
Parametrised Verification of Intel-x86 Programs
POPL 10(POPL)2026
Endangered by the Language But Saved by the Compiler: Robust Safety via Semantic Back-Translation
POPL 10(POPL)2026
General Decidability Results for Systems with Continuous Counters
POPL 10(POPL)2026
Fuzzing Guided by Bayesian Program Analysis
POPL 10(POPL)2026
Verifying Almost-Sure Termination for Randomized Distributed Algorithms
POPL 10(POPL)2026
Quotient Polymorphism
POPL 10(POPL)2026
Formal Verification for JavaScript Regular Expressions: A Proven Mechanized Semantics and Its Applications
POPL 10(POPL)2026
From Semantics to Syntax: A Type Theory for Comprehension Categories
POPL 10(POPL)2026
Oriented Metrics for Bottom-Up Enumerative Synthesis
POPL 10(POPL)2026
What Is a Monoid?
POPL 10(POPL)2026
An Equational Axiomatization of Dynamic Threads via Algebraic Effects: Presheaves on Finite Relations, Labelled Posets, and Parameterized Algebraic Theories
POPL 10(POPL)2026
A Family of Sims with Diverging Interests
POPL 10(POPL)2026
Probabilistic Concurrent Reasoning in Outcome Logic: Independence, Conditioning, and Invariants
POPL 10(POPL)2026
Corrigendum: Unrealizability Logic
POPL 10(POPL)2026
Handling Scope Checks: A Comparative Framework for Dynamic Scope Extrusion Checks
POPL 10(POPL)2026
Cryptis: Cryptographic Reasoning in Separation Logic
POPL 10(POPL)2026
Bounded Sort Polymorphism with Elimination Constraints
POPL 10(POPL)2026
The Simple Essence of Boolean-Algebraic Subtyping: Semantic Soundness for Algebraic Union, Intersection, Negation, and Equi-recursive Types
POPL 10(POPL)2026
Piecewise Analysis of Probabilistic Programs via 𝑘-Induction
POPL 10(POPL)2026
Miri: Practical Undefined Behavior Detection for Rust
POPL 10(POPL)2026
Optimising Density Computations in Probabilistic Programs via Automatic Loop Vectorisation
POPL 10(POPL)2026
On Circuit Description Languages, Indexed Monads, and Resource Analysis
POPL 10(POPL)2026
The Ghosts of Empires: Extracting Modularity from Interleaving-Based Proofs
POPL 10(POPL)2026
Security Reasoning via Substructural Dependency Tracking
POPL 10(POPL)2026
Arbitration-Free Consistency Is Available (and Vice Versa)
POPL 10(POPL)2026
Welterweight Go: Boxing, Structural Subtyping, and Generics
POPL 10(POPL)2026
U-Turn: Enhancing Incorrectness Analysis by Reversing Direction
POPL 10(POPL)2026
202579 篇 · 9(POPL)
On Extending Incorrectness Logic with Backwards Reasoning
POPL 9(POPL)2025
Affect: An Affine Type and Effect System
POPL 9(POPL)2025
Derivative-Guided Symbolic Execution
POPL 9(POPL)2025
Biparsers: Exact Printing for Data Synchronisation
POPL 9(POPL)2025
Data Race Freedom à la Mode
POPL 9(POPL)2025
A Demonic Outcome Logic for Randomized Nondeterminism
POPL 9(POPL)2025
Verifying Quantum Circuits with Level-Synchronized Tree Automata
POPL 9(POPL)2025
Coinductive Proofs for Temporal Hyperliveness
POPL 9(POPL)2025
A Modal Deconstruction of Löb Induction
POPL 9(POPL)2025
TensorRight: Automated Verification of Tensor Graph Rewrites
POPL 9(POPL)2025
Archmage and CompCertCast: End-to-End Verification Supporting Integer-Pointer Casting
POPL 9(POPL)2025
Maximal Simplification of Polyhedral Reductions
POPL 9(POPL)2025
Interaction Equivalence
POPL 9(POPL)2025
SNIP: Speculative Execution and Non-Interference Preservation for Compiler Transformations
POPL 9(POPL)2025
Model Checking C/C++ with Mixed-Size Accesses
POPL 9(POPL)2025
Consistency of a Dependent Calculus of Indistinguishability
POPL 9(POPL)2025
Bidirectional Higher-Rank Polymorphism with Intersection and Union Types
POPL 9(POPL)2025
A Verified Foreign Function Interface between Coq and C
POPL 9(POPL)2025
Avoiding Signature Avoidance in ML Modules with Zippers
POPL 9(POPL)2025
Translation of Temporal Logic for Efficient Infinite-State Reactive Synthesis
POPL 9(POPL)2025
Approximate Relational Reasoning for Higher-Order Probabilistic Programs
POPL 9(POPL)2025
Calculational Design of Hyperlogics by Abstract Interpretation
POPL 9(POPL)2025
Automating Equational Proofs in Dirac Notation
POPL 9(POPL)2025
BiSikkel: A Multimode Logical Framework in Agda
POPL 9(POPL)2025
CF-GKAT: Efficient Validation of Control-Flow Transformations
POPL 9(POPL)2025
Preservation of Speculative Constant-Time by Compilation
POPL 9(POPL)2025
Program Analysis via Multiple Context Free Language Reachability
POPL 9(POPL)2025
Fulminate: Testing CN Separation-Logic Specifications in C
POPL 9(POPL)2025
Grove: A Bidirectionally Typed Collaborative Structure Editor Calculus
POPL 9(POPL)2025
RE#: High Performance Derivative-Based Regex Matching with Intersection, Complement, and Restricted Lookarounds
POPL 9(POPL)2025
Guaranteed Bounds on Posterior Distributions of Discrete Probabilistic Programs with Loops
POPL 9(POPL)2025
Flexible Type-Based Resource Estimation in Quantum Circuit Description Languages
POPL 9(POPL)2025
Symbolic Automata: Omega-Regularity Modulo Theories
POPL 9(POPL)2025
A Quantitative Probabilistic Relational Hoare Logic
POPL 9(POPL)2025
A Dependent Type Theory for Meta-programming with Intensional Analysis
POPL 9(POPL)2025
Linear and Non-linear Relational Analyses for Quantum Program Optimization
POPL 9(POPL)2025
Bluebell: An Alliance of Relational Lifting and Independence for Probabilistic Reasoning
POPL 9(POPL)2025
Reachability Analysis of the Domain Name System
POPL 9(POPL)2025
Simple Linear Loops: Algebraic Invariants and Applications
POPL 9(POPL)2025
Semantic Logical Relations for Timed Message-Passing Protocols
POPL 9(POPL)2025
Algebras for Deterministic Computation Are Inherently Incomplete
POPL 9(POPL)2025
Do You Even Lift? Strengthening Compiler Security Guarantees against Spectre Attacks
POPL 9(POPL)2025
Sound and Complete Proof Rules for Probabilistic Termination
POPL 9(POPL)2025
Flo: A Semantic Foundation for Progressive Stream Processing
POPL 9(POPL)2025
Axe ’Em: Eliminating Spurious States with Induction Axioms
POPL 9(POPL)2025
Formalising Graph Algorithms with Coinduction
POPL 9(POPL)2025
Barendregt Convenes with Knaster and Tarski: Strong Rule Induction for Syntax with Bindings
POPL 9(POPL)2025
On Decidable and Undecidable Extensions of Simply Typed Lambda Calculus
POPL 9(POPL)2025
Unifying Compositional Verification and Certified Compilation with a Three-Dimensional Refinement Algebra
POPL 9(POPL)2025
An Incremental Algorithm for Algebraic Program Analysis
POPL 9(POPL)2025
Qurts: Automatic Quantum Uncomputation by Affine Types with Lifetime
POPL 9(POPL)2025
Automated Program Refinement: Guide and Verify Code Large Language Model with Refinement Calculus
POPL 9(POPL)2025
Finite-Choice Logic Programming
POPL 9(POPL)2025
Compositional Imprecise Probability: A Solution from Graded Monads and Markov Categories
POPL 9(POPL)2025
Modelling Recursion and Probabilistic Choice in Guarded Type Theory
POPL 9(POPL)2025
Top-Down or Bottom-Up? Complexity Analyses of Synchronous Multiparty Session Types
POPL 9(POPL)2025
Generic Refinement Types
POPL 9(POPL)2025
Pantograph: A Fluid and Typed Structure Editor
POPL 9(POPL)2025
QuickSub: Efficient Iso-Recursive Subtyping
POPL 9(POPL)2025
Algebraic Temporal Effects: Temporal Verification of Recursively Typed Higher-Order Programs
POPL 9(POPL)2025
A Taxonomy of Hoare-Like Logics: Towards a Holistic View using Predicate Transformers and Kleene Algebras with Top and Tests
POPL 9(POPL)2025
Inference Plans for Hybrid Particle Filtering
POPL 9(POPL)2025
Generically Automating Separation Logic by Functors, Homomorphisms, and Modules
POPL 9(POPL)2025
The Decision Problem for Regular First Order Theories
POPL 9(POPL)2025
Relaxed Memory Concurrency Re-executed
POPL 9(POPL)2025
VeriRT: An End-to-End Verification Framework for Real-Time Distributed Systems
POPL 9(POPL)2025
MimIR: An Extensible and Type-Safe Intermediate Representation for the DSL Age
POPL 9(POPL)2025
The Duality of λ-Abstraction
POPL 9(POPL)2025
RELINCHE: Automatically Checking Linearizability under Relaxed Memory Consistency
POPL 9(POPL)2025
A Primal-Dual Perspective on Program Verification Algorithms
POPL 9(POPL)2025
Program Logics à la Carte
POPL 9(POPL)2025
Dis/Equality Graphs
POPL 9(POPL)2025
Abstract Operational Methods for Call-by-Push-Value
POPL 9(POPL)2025
All Your Base Are Belong to Us: Sort Polymorphism for Proof Assistants
POPL 9(POPL)2025
Progressful Interpreters for Efficient WebAssembly Mechanisation
POPL 9(POPL)2025
Denotational Semantics of Gradual Typing using Synthetic Guarded Domain Theory
POPL 9(POPL)2025
Tail Modulo Cons, OCaml, and Relational Separation Logic
POPL 9(POPL)2025
Formal Foundations for Translational Separation Logic Verifiers
POPL 9(POPL)2025
The Best of Abstract Interpretations
POPL 9(POPL)2025
202493 篇 · 8(POPL)
Solving Infinite-State Games via Acceleration
POPL 8(POPL)2024
API-Driven Program Synthesis for Testing Static Typing Implementations
POPL 8(POPL)2024
Ramsey Quantifiers in Linear Arithmetics
POPL 8(POPL)2024
Deciding Asynchronous Hyperproperties for Recursive Programs
POPL 8(POPL)2024
Predictive Monitoring against Pattern Regular Languages
POPL 8(POPL)2024
Mechanizing Refinement Types
POPL 8(POPL)2024
A Universal, Sound, and Complete Forward Reasoning Technique for Machine-Verified Proofs of Linearizability
POPL 8(POPL)2024
Parametric Subtyping for Structural Parametric Polymorphism
POPL 8(POPL)2024
Validation of Modern JSON Schema: Formalization and Complexity
POPL 8(POPL)2024
Polyregular Functions on Unordered Trees of Bounded Height
POPL 8(POPL)2024
Quantum Bisimilarity via Barbs and Contexts: Curbing the Power of Non-deterministic Observers
POPL 8(POPL)2024
Parikh’s Theorem Made Symbolic
POPL 8(POPL)2024
Unboxed Data Constructors: Or, How cpp Decides a Halting Problem
POPL 8(POPL)2024
On-the-Fly Static Analysis via Dynamic Bidirected Dyck Reachability
POPL 8(POPL)2024
Thunks and Debits in Separation Logic with Time Credits
POPL 8(POPL)2024
An Iris Instance for Verifying CompCert C Programs
POPL 8(POPL)2024
Orthologic with Axioms
POPL 8(POPL)2024
Inference of Probabilistic Programs with Moment-Matching Gaussian Mixtures
POPL 8(POPL)2024
Higher Order Bayesian Networks, Exactly
POPL 8(POPL)2024
Coarser Equivalences for Causal Concurrency
POPL 8(POPL)2024
Automatic Parallelism Management
POPL 8(POPL)2024
Implementation and Synthesis of Math Library Functions
POPL 8(POPL)2024
Polynomial Time and Dependent Types
POPL 8(POPL)2024
Sound Gradual Verification with Symbolic Execution
POPL 8(POPL)2024
Optimal Program Synthesis via Abstract Interpretation
POPL 8(POPL)2024
Monotonicity and the Precision of Program Analysis
POPL 8(POPL)2024
Internal Parametricity, without an Interval
POPL 8(POPL)2024
Effectful Software Contracts
POPL 8(POPL)2024
Mostly Automated Verification of Liveness Properties for Distributed Protocols with Ranking Functions
POPL 8(POPL)2024
Efficient Matching of Regular Expressions with Lookaround Assertions
POPL 8(POPL)2024
Pipelines and Beyond: Graph Types for ADTs with Futures
POPL 8(POPL)2024
Flan: An Expressive and Efficient Datalog Compiler for Program Analysis
POPL 8(POPL)2024
Disentanglement with Futures, State, and Interaction
POPL 8(POPL)2024
ReLU Hull Approximation
POPL 8(POPL)2024
Soundly Handling Linearity
POPL 8(POPL)2024
Regular Abstractions for Array Systems
POPL 8(POPL)2024
Efficient CHAD
POPL 8(POPL)2024
Internalizing Indistinguishability with Dependent Types
POPL 8(POPL)2024
Enhanced Enumeration Techniques for Syntax-Guided Synthesis of Bit-Vector Manipulations
POPL 8(POPL)2024
Positive Almost-Sure Termination: Complexity and Proof Rules
POPL 8(POPL)2024
Generating Well-Typed Terms That Are Not “Useless”
POPL 8(POPL)2024
Indexed Types for a Statically Safe WebAssembly
POPL 8(POPL)2024
Asynchronous Probabilistic Couplings in Higher-Order Separation Logic
POPL 8(POPL)2024
Fully Composable and Adequate Verified Compilation with Direct Refinements between Open Modules
POPL 8(POPL)2024
Calculational Design of [In]Correctness Transformational Program Logics by Abstract Interpretation
POPL 8(POPL)2024
On Learning Polynomial Recursive Programs
POPL 8(POPL)2024
The Complex(ity) Landscape of Checking Infinite Descent
POPL 8(POPL)2024
Solvable Polynomial Ideals: The Ideal Reflection for Program Analysis
POPL 8(POPL)2024
Strong Invariants Are Hard: On the Hardness of Strongest Polynomial Invariants for (Probabilistic) Programs
POPL 8(POPL)2024
Deadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-Order Message Passing
POPL 8(POPL)2024
VST-A: A Foundationally Sound Annotation Verifier
POPL 8(POPL)2024
Fusing Direct Manipulations into Functional Programs
POPL 8(POPL)2024
Algebraic Effects Meet Hoare Logic in Cubical Agda
POPL 8(POPL)2024
Type-Based Gradual Typing Performance Optimization
POPL 8(POPL)2024
When Subtyping Constraints Liberate: A Novel Type Inference Approach for First-Class Polymorphism
POPL 8(POPL)2024
The Logical Essence of Well-Bracketed Control Flow
POPL 8(POPL)2024
Semantic Code Refactoring for Abstract Data Types
POPL 8(POPL)2024
Quotient Haskell: Lightweight Quotient Types for All
POPL 8(POPL)2024
A Formalization of Core Why3 in Coq
POPL 8(POPL)2024
Enriched Presheaf Model of Quantum FPC
POPL 8(POPL)2024
DisLog: A Separation Logic for Disentanglement
POPL 8(POPL)2024
A Core Calculus for Documents: Or, Lambda: The Ultimate Document
POPL 8(POPL)2024
How Hard Is Weak-Memory Testing?
POPL 8(POPL)2024
With a Few Square Roots, Quantum Computing Is as Easy as Pi
POPL 8(POPL)2024
Probabilistic Programming Interfaces for Random Graphs: Markov Categories, Graphons, and Nominal Sets
POPL 8(POPL)2024
Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement
POPL 8(POPL)2024
Reachability in Continuous Pushdown VASS
POPL 8(POPL)2024
SimuQ: A Framework for Programming Quantum Hamiltonian Simulation with Analog Compilation
POPL 8(POPL)2024
Modular Denotational Semantics for Effects with Guarded Interaction Trees
POPL 8(POPL)2024
Polymorphic Type Inference for Dynamic Languages
POPL 8(POPL)2024
Efficient Bottom-Up Synthesis for Programs with Local Variables
POPL 8(POPL)2024
Guided Equality Saturation
POPL 8(POPL)2024
Inference of Robust Reachability Constraints
POPL 8(POPL)2024
Securing Verified IO Programs Against Unverified Code in F*
POPL 8(POPL)2024
Decision and Complexity of Dolev-Yao Hyperproperties
POPL 8(POPL)2024
Polymorphic Reachability Types: Tracking Freshness, Aliasing, and Separation in Higher-Order Generic Programs
POPL 8(POPL)2024
Internal and Observational Parametricity for Cubical Agda
POPL 8(POPL)2024
Explicit Effects and Effect Constraints in ReML
POPL 8(POPL)2024
Decalf: A Directed, Effectful Cost-Aware Logical Framework
POPL 8(POPL)2024
Total Type Error Localization and Recovery with Holes
POPL 8(POPL)2024
Programmatic Strategy Synthesis: Resolving Nondeterminism in Probabilistic Programs
POPL 8(POPL)2024
On Model-Checking Higher-Order Effectful Programs
POPL 8(POPL)2024
The Essence of Generalized Algebraic Data Types
POPL 8(POPL)2024
An Axiomatic Basis for Computer Programming on the Relaxed Arm-A Architecture: The AxSL Logic
POPL 8(POPL)2024
Commutativity Simplifies Proofs of Parameterized Programs
POPL 8(POPL)2024
Programming-by-Demonstration for Long-Horizon Robot Tasks
POPL 8(POPL)2024
Nominal Recursors as Epi-Recursors
POPL 8(POPL)2024
Ill-Typed Programs Don’t Evaluate
POPL 8(POPL)2024
An Infinite Needle in a Finite Haystack: Finding Infinite Counter-Models in Deductive Verification
POPL 8(POPL)2024
Answer Refinement Modification: Refinement Type System for Algebraic Effects and Handlers
POPL 8(POPL)2024
EasyBC: A Cryptography-Specific Language for Security Analysis of Block Ciphers against Differential Cryptanalysis
POPL 8(POPL)2024
A Case for Synthesis of Recursive Quantum Unitary Programs
POPL 8(POPL)2024
Shoggoth: A Formal Foundation for Strategic Rewriting
POPL 8(POPL)2024
202374 篇 · 7(POPL)
Stratified Commutativity in Verification Algorithms for Concurrent Programs
POPL 7(POPL)2023
Type-Preserving, Dependence-Aware Guide Generation for Sound, Effective Amortized Probabilistic Inference
POPL 7(POPL)2023
Statically Resolvable Ambiguity
POPL 7(POPL)2023
When Less Is More: Consequence-Finding in a Weak Theory of Arithmetic
POPL 7(POPL)2023
Single-Source-Single-Target Interleaved-Dyck Reachability via Integer Linear Programming
POPL 7(POPL)2023
Optimal CHC Solving via Termination Proofs
POPL 7(POPL)2023
Reconciling Shannon and Scott with a Lattice of Computable Information
POPL 7(POPL)2023
FlashFill++: Scaling Programming by Example by Cutting to the Chase
POPL 7(POPL)2023
A Calculus for Amortized Expected Runtimes
POPL 7(POPL)2023
SSA Translation Is an Abstract Interpretation
POPL 7(POPL)2023
Higher-Order Leak and Deadlock Free Locks
POPL 7(POPL)2023
Tail Recursion Modulo Context: An Equational Approach
POPL 7(POPL)2023
Deconstructing the Calculus of Relations with Tape Diagrams
POPL 7(POPL)2023
MSWasm: Soundly Enforcing Memory-Safe Execution of Unsafe Code
POPL 7(POPL)2023
A High-Level Separation Logic for Heap Space under Garbage Collection
POPL 7(POPL)2023
Higher-Order MSL Horn Constraints
POPL 7(POPL)2023
Context-Bounded Verification of Context-Free Specifications
POPL 7(POPL)2023
Unrealizability Logic
POPL 7(POPL)2023
The Geometry of Causality: Multi-token Geometry of Interaction and Its Causal Unfolding
POPL 7(POPL)2023
A Compositional Theory of Linearizability
POPL 7(POPL)2023
Grisette: Symbolic Compilation as a Functional Programming Library
POPL 7(POPL)2023
Executing Microservice Applications on Serverless, Correctly
POPL 7(POPL)2023
A Core Calculus for Equational Proofs of Cryptographic Protocols
POPL 7(POPL)2023
HFL(Z) Validity Checking for Automated Program Verification
POPL 7(POPL)2023
Witnessability of Undecidable Problems
POPL 7(POPL)2023
Quantitative Inhabitation for Different Lambda Calculi in a Unifying Framework
POPL 7(POPL)2023
An Algebra of Alignment for Relational Verification
POPL 7(POPL)2023
You Only Linearize Once: Tangents Transpose to Gradients
POPL 7(POPL)2023
Kater: Automating Weak Memory Model Metatheory and Consistency Checking
POPL 7(POPL)2023
Dargent: A Silver Bullet for Verified Data Layout Refinement
POPL 7(POPL)2023
DimSum: A Decentralized Approach to Multi-language Semantics and Verification
POPL 7(POPL)2023
Efficient Dual-Numbers Reverse AD via Well-Known Program Transformations
POPL 7(POPL)2023
Top-Down Synthesis for Library Learning
POPL 7(POPL)2023
Qunity: A Unified Language for Quantum and Classical Computing
POPL 7(POPL)2023
Choice Trees: Representing Nondeterministic, Recursive, and Impure Programs in Coq
POPL 7(POPL)2023
Proto-Quipper with Dynamic Lifting
POPL 7(POPL)2023
Fast Coalgebraic Bisimilarity Minimization
POPL 7(POPL)2023
Towards a Higher-Order Mathematical Operational Semantics
POPL 7(POPL)2023
Elements of Quantitative Rewriting
POPL 7(POPL)2023
CoqQ: Foundational Verification of Quantum Programs
POPL 7(POPL)2023
Recursive Subtyping for All
POPL 7(POPL)2023
A Partial Order View of Message-Passing Communication Models
POPL 7(POPL)2023
Taking Back Control in an Intermediate Representation for GPU Computing
POPL 7(POPL)2023
Dynamic Race Detection with O(1) Samples
POPL 7(POPL)2023
Temporal Verification with Answer-Effect Modification: Dependent Temporal Type-and-Effect System with Delimited Continuations
POPL 7(POPL)2023
CN: Verifying Systems C Code with Separation-Logic Refinement Types
POPL 7(POPL)2023
ADEV: Sound Automatic Differentiation of Expected Values of Probabilistic Programs
POPL 7(POPL)2023
Inductive Synthesis of Structurally Recursive Functional Programs from Non-recursive Expressions
POPL 7(POPL)2023
Admissible Types-to-PERs Relativization in Higher-Order Logic
POPL 7(POPL)2023
From SMT to ASP: Solver-Based Approaches to Solving Datalog Synthesis-as-Rule-Selection Problems
POPL 7(POPL)2023
babble: Learning Better Abstractions with E-Graphs and Anti-unification
POPL 7(POPL)2023
Locally Nameless Sets
POPL 7(POPL)2023
Why Are Proofs Relevant in Proof-Relevant Models?
POPL 7(POPL)2023
Smoothness Analysis for Probabilistic Programs with Application to Optimised Variational Inference
POPL 7(POPL)2023
Making a Type Difference: Subtraction on Intersection Types as Generalized Record Operations
POPL 7(POPL)2023
Modular Primal-Dual Fixpoint Logic Solving for Temporal Verification
POPL 7(POPL)2023
An Operational Approach to Library Abstraction under Relaxed Memory Concurrency
POPL 7(POPL)2023
Combining Functional and Automata Synthesis to Discover Causal Reactive Programs
POPL 7(POPL)2023
Step-Indexed Logical Relations for Countable Nondeterminism and Probabilistic Choice
POPL 7(POPL)2023
A General Noninterference Policy for Polynomial Time
POPL 7(POPL)2023
Probabilistic Resource-Aware Session Types
POPL 7(POPL)2023
A Robust Theory of Series Parallel Graphs
POPL 7(POPL)2023
The Path to Durable Linearizability
POPL 7(POPL)2023
Comparative Synthesis: Learning Near-Optimal Network Designs by Query
POPL 7(POPL)2023
The Fine-Grained Complexity of CFL Reachability
POPL 7(POPL)2023
An Order-Theoretic Analysis of Universe Polymorphism
POPL 7(POPL)2023
Formally Verified Native Code Generation in an Effectful JIT: Turning the CompCert Backend into a Formally Verified JIT Compiler
POPL 7(POPL)2023
Conditional Contextual Refinement
POPL 7(POPL)2023
On the Expressive Power of String Constraints
POPL 7(POPL)2023
Hefty Algebras: Modular Elaboration of Higher-Order Algebraic Effects
POPL 7(POPL)2023
Impredicative Observational Equality
POPL 7(POPL)2023
A Type-Based Approach to Divide-and-Conquer Recursion in Coq
POPL 7(POPL)2023
A Bowtie for a Beast: Overloading, Eta Expansion, and Extensible Data Types in F⋈
POPL 7(POPL)2023
Affine Monads and Lazy Structures for Bayesian Programming
POPL 7(POPL)2023
202265 篇 · 6(POPL)
On incorrectness logic and Kleene algebra with top and tests
POPL 6(POPL)2022
Mœbius: metaprogramming using contextual types: the stage where system f can pattern match on itself
POPL 6(POPL)2022
Efficient algorithms for dynamic bidirected Dyck-reachability
POPL 6(POPL)2022
A cost-aware logical framework
POPL 6(POPL)2022
From enhanced coinduction towards enhanced induction
POPL 6(POPL)2022
Symmetries in reversible programming: from symmetric rig groupoids to reversible programming languages
POPL 6(POPL)2022
Extending Intel-x86 consistency and persistency: formalising the semantics of Intel-x86 memory types and non-temporal stores
POPL 6(POPL)2022
Relational e-matching
POPL 6(POPL)2022
The decidability and complexity of interleaved bidirected Dyck reachability
POPL 6(POPL)2022
Verified compilation of C programs with a nominal memory model
POPL 6(POPL)2022
Type-level programming with match types
POPL 6(POPL)2022
Software model-checking as cyclic-proof search
POPL 6(POPL)2022
VIP: verifying real-world C idioms with integer-pointer casts
POPL 6(POPL)2022
Property-directed reachability as abstract interpretation in the monotone theory
POPL 6(POPL)2022
Semantics for variational Quantum programming
POPL 6(POPL)2022
The leaky semicolon: compositional semantic dependencies for relaxed-memory concurrency
POPL 6(POPL)2022
Subcubic certificates for CFL reachability
POPL 6(POPL)2022
Reasoning about “reasoning about reasoning”: semantics and contextual equivalence for probabilistic programs with nested queries and recursion
POPL 6(POPL)2022
Provably correct, asymptotically efficient, higher-order reverse-mode automatic differentiation
POPL 6(POPL)2022
Interval universal approximation for neural networks
POPL 6(POPL)2022
PRIMA: general and precise neural network certification via scalable convex hull approximations
POPL 6(POPL)2022
Return of CFA: call-site sensitivity can be superior to object sensitivity even for object-oriented programs
POPL 6(POPL)2022
Formal metatheory of second-order abstract syntax
POPL 6(POPL)2022
A separation logic for heap space under garbage collection
POPL 6(POPL)2022
Twist: sound reasoning for purity and entanglement in Quantum programs
POPL 6(POPL)2022
What’s decidable about linear loops?
POPL 6(POPL)2022
Truly stateless, optimal dynamic partial order reduction
POPL 6(POPL)2022
Effectful program distancing
POPL 6(POPL)2022
Pirouette: higher-order typed functional choreographies
POPL 6(POPL)2022
A fine-grained computational interpretation of Girard’s intuitionistic proof-nets
POPL 6(POPL)2022
Oblivious algebraic data types
POPL 6(POPL)2022
Fair termination of binary sessions
POPL 6(POPL)2022
A relational theory of effects and coeffects
POPL 6(POPL)2022
Solving string constraints with Regex-dependent functions through transducers with priorities and variables
POPL 6(POPL)2022
A separation logic for negative dependence
POPL 6(POPL)2022
Safe, modular packet pipeline programming
POPL 6(POPL)2022
On type-cases, union elimination, and occurrence typing
POPL 6(POPL)2022
A Quantum interpretation of separating conjunction for local reasoning of Quantum programs based on separation logic
POPL 6(POPL)2022
Linked visualisations via Galois dependencies
POPL 6(POPL)2022
SolType: refinement types for arithmetic overflow in solidity
POPL 6(POPL)2022
Certifying derivation of state machines from coroutines
POPL 6(POPL)2022
Layered and object-based game semantics
POPL 6(POPL)2022
Solving constrained Horn clauses modulo algebraic data types and recursive functions
POPL 6(POPL)2022
Context-bounded verification of thread pools
POPL 6(POPL)2022
Fully abstract models for effectful λ-calculi via category-theoretic logical relations
POPL 6(POPL)2022
Simuliris: a separation logic framework for verifying concurrent program optimizations
POPL 6(POPL)2022
Learning formulas in finite variable logics
POPL 6(POPL)2022
Connectivity graphs: a method for proving deadlock freedom based on separation logic
POPL 6(POPL)2022
Dependently-typed data plane programming
POPL 6(POPL)2022
Bottom-up synthesis of recursive functional programs using angelic execution
POPL 6(POPL)2022
Static prediction of parallel computation graphs
POPL 6(POPL)2022
Profile inference revisited
POPL 6(POPL)2022
Staging with class: a specification for typed template Haskell
POPL 6(POPL)2022
Partial (In)Completeness in abstract interpretation: limiting the imprecision in program analysis
POPL 6(POPL)2022
A dual number abstraction for static analysis of Clarke Jacobians
POPL 6(POPL)2022
Verified tensor-program optimization via high-level scheduling rewrites
POPL 6(POPL)2022
Isolation without taxation: near-zero-cost transitions for WebAssembly and SFI
POPL 6(POPL)2022
Quantum information effects
POPL 6(POPL)2022
Concurrent incorrectness separation logic
POPL 6(POPL)2022
A formal foundation for symbolic evaluation with merging
POPL 6(POPL)2022
Visibility reasoning for concurrent snapshot algorithms
POPL 6(POPL)2022
Induction duality: primal-dual search for invariants
POPL 6(POPL)2022
Observational equality: now for good
POPL 6(POPL)2022
Logarithm and program testing
POPL 6(POPL)2022
One polynomial approximation to produce correctly rounded results of an elementary function for multiple representations and rounding modes
POPL 6(POPL)2022
202161 篇 · 5(POPL)
A unifying type-theory for higher-order (amortized) cost analysis
POPL 5(POPL)2021
Context-bounded verification of liveness properties for multithreaded shared-memory programs
POPL 5(POPL)2021
Fully abstract from static to gradual
POPL 5(POPL)2021
Intersection types and (positive) almost-sure termination
POPL 5(POPL)2021
On the semantic expressiveness of recursive types
POPL 5(POPL)2021
On algebraic abstractions for concurrent separation logics
POPL 5(POPL)2021
Intrinsically typed compilation with nameless labels
POPL 5(POPL)2021
Combining the top-down propagation and bottom-up enumeration for inductive program synthesis
POPL 5(POPL)2021
Learning the boundary of inductive invariants
POPL 5(POPL)2021
Automata and fixpoints for asynchronous hyperproperties
POPL 5(POPL)2021
An approach to generate correctly rounded math libraries for new floating point variants
POPL 5(POPL)2021
A computational interpretation of compact closed categories: reversible programming with negative and fractional types
POPL 5(POPL)2021
Paradoxes of probabilistic programming: and how to condition on events of measure zero with infinitesimal probabilities
POPL 5(POPL)2021
Abstracting gradual typing moving forward: precise and space-efficient
POPL 5(POPL)2021
Deciding accuracy of differential privacy schemes
POPL 5(POPL)2021
Distributed causal memory: modular specification and verification in higher-order distributed separation logic
POPL 5(POPL)2021
Precise subtyping for asynchronous multiparty sessions
POPL 5(POPL)2021
Dijkstra monads forever: termination-sensitive specifications for interaction trees
POPL 5(POPL)2021
Taming x86-TSO persistency
POPL 5(POPL)2021
The taming of the rew: a type theory with computational assumptions
POPL 5(POPL)2021
Semantics-guided synthesis
POPL 5(POPL)2021
Relatively complete verification of probabilistic programs: an expressive language for expectation-based reasoning
POPL 5(POPL)2021
Verified code generation for the polyhedral model
POPL 5(POPL)2021
Formally verified speculation and deoptimization in a JIT compiler
POPL 5(POPL)2021
𝜆ₛ: computable semantics for differentiable programming with higher-order functions and datatypes
POPL 5(POPL)2021
Corpse reviver: sound and efficient gradual typing via contract verification
POPL 5(POPL)2021
Data flow refinement type inference
POPL 5(POPL)2021
Petr4: formal foundations for p4 data planes
POPL 5(POPL)2021
A verified optimizer for Quantum circuits
POPL 5(POPL)2021
Mechanized logical relations for termination-insensitive noninterference
POPL 5(POPL)2021
On the complexity of bidirected interleaved Dyck-reachability
POPL 5(POPL)2021
Giving semantics to program-counter labels via secure effects
POPL 5(POPL)2021
Simplifying dependent reductions in the polyhedral model
POPL 5(POPL)2021
Intensional datatype refinement: with application to scalable verification of pattern-match safety
POPL 5(POPL)2021
Diamonds are not forever: liveness in reactive programming with guarded recursion
POPL 5(POPL)2021
The (In)Efficiency of interaction
POPL 5(POPL)2021
An abstract interpretation for SPMD divergence on reducible control flow graphs
POPL 5(POPL)2021
Deciding reachability under persistent x86-TSO
POPL 5(POPL)2021
Verifying observational robustness against a c11-style memory model
POPL 5(POPL)2021
A pre-expectation calculus for probabilistic sensitivity
POPL 5(POPL)2021
Efficient and provable local capability revocation using uninitialized capabilities
POPL 5(POPL)2021
Modeling and analyzing evaluation cost of CUDA kernels
POPL 5(POPL)2021
Internalizing representation independence with univalence
POPL 5(POPL)2021
Optimal prediction of synchronization-preserving races
POPL 5(POPL)2021
Asynchronous effects
POPL 5(POPL)2021
A separation logic for effect handlers
POPL 5(POPL)2021
Provably space-efficient parallel functional programming
POPL 5(POPL)2021
Cyclic proofs, system t, and the power of contraction
POPL 5(POPL)2021
Deciding ω-regular properties on linear recurrence sequences
POPL 5(POPL)2021
Automatic differentiation in PCF
POPL 5(POPL)2021
Transfinite step-indexing for termination
POPL 5(POPL)2021
PerSeVerE: persistency semantics for verification under ext4
POPL 5(POPL)2021
Probabilistic programming semantics for name generation
POPL 5(POPL)2021
A graded dependent type system with a usage-aware semantics
POPL 5(POPL)2021
Automatically eliminating speculative leaks from cryptographic code with blade
POPL 5(POPL)2021
The fine-grained and parallel complexity of andersen’s pointer analysis
POPL 5(POPL)2021
A practical mode system for recursive definitions
POPL 5(POPL)2021
Verifying correct usage of context-free API protocols
POPL 5(POPL)2021
Functorial semantics for partial theories
POPL 5(POPL)2021
Generating collection transformations from proofs
POPL 5(POPL)2021
egg: Fast and extensible equality saturation
POPL 5(POPL)2021
2019145 篇 · 3(POPL)
Modular quantitative monitoring
POPL 3(POPL)2019
From fine- to coarse-grained dynamic information flow control and back
POPL 3(POPL)2019
Concerto: a framework for combined concrete and abstract interpretation
POPL 3(POPL)2019
Probabilistic programming with densities in SlicStan: efficient, flexible, and deterministic
POPL 3(POPL)2019
Principality and approximation under dimensional bound
POPL 3(POPL)2019
StkTokens: enforcing well-bracketed control flow and stack encapsulation using linear capabilities
POPL 3(POPL)2019
Gradual type theory
POPL 3(POPL)2019
Fully abstract module compilation
POPL 3(POPL)2019
Modalities, cohesion, and information flow
POPL 3(POPL)2019
Polymorphic symmetric multiple dispatch with variance
POPL 3(POPL)2019
Hamsaz: replication coordination analysis and synthesis
POPL 3(POPL)2019
An abstract stack based approach to verified compositional compilation to machine code
POPL 3(POPL)2019
Formal verification of higher-order probabilistic programs: reasoning about approximation, convergence, Bayesian inference, and optimization
POPL 3(POPL)2019
CT-wasm: type-driven secure cryptography for the web ecosystem
POPL 3(POPL)2019
Two sides of the same coin: session types and game semantics: a synchronous side and an asynchronous side
POPL 3(POPL)2019
Abstracting algebraic effects
POPL 3(POPL)2019
Type-guided worst-case input generation
POPL 3(POPL)2019
Exceptional asynchronous session types: session types without tiers
POPL 3(POPL)2019
A true positives theorem for a static race detector
POPL 3(POPL)2019
Efficient parameterized algorithms for data packing
POPL 3(POPL)2019
Weak-consistency specification via visibility relaxation
POPL 3(POPL)2019
Context-, flow-, and field-sensitive data-flow analysis using synchronized Pushdown systems
POPL 3(POPL)2019
Decoupling lock-free data structures from memory reclamation for static analysis
POPL 3(POPL)2019
Bridging the gap between programming languages and hardware weak memory models
POPL 3(POPL)2019
Abstraction-safe effect handlers via tunneling
POPL 3(POPL)2019
Better late than never: a fully-abstract semantics for classical processes
POPL 3(POPL)2019
Sound and complete bidirectional typechecking for higher-rank polymorphism with existentials and indexed types
POPL 3(POPL)2019
On library correctness under weak memory consistency: specifying and verifying concurrent libraries under declarative consistency models
POPL 3(POPL)2019
Gradual parametricity, revisited
POPL 3(POPL)2019
Bisimulation as path type for guarded recursive types
POPL 3(POPL)2019
Bounded model checking of signal temporal logic properties using syntactic separation
POPL 3(POPL)2019
Categorical combinatorics of scheduling and synchronization in game semantics
POPL 3(POPL)2019
Skeletal semantics and their interpretations
POPL 3(POPL)2019
Familial monads and structural operational semantics
POPL 3(POPL)2019
A separation logic for concurrent randomized programs
POPL 3(POPL)2019
Higher inductive types in cubical computational type theory
POPL 3(POPL)2019
JaVerT 2.0: compositional symbolic execution for JavaScript
POPL 3(POPL)2019
Pretend synchrony: synchronous verification of asynchronous distributed programs
POPL 3(POPL)2019
FrAngel: component-based synthesis with control structures
POPL 3(POPL)2019
Bindings as bounded natural functors
POPL 3(POPL)2019
Abstracting extensible data types: or, rows by any other name
POPL 3(POPL)2019
A domain theory for statistical probabilistic programming
POPL 3(POPL)2019
Fast and exact analysis for LRU caches
POPL 3(POPL)2019
Game semantics for quantum programming
POPL 3(POPL)2019
Refinement of path expressions for static analysis
POPL 3(POPL)2019
Adventures in monitorability: from branching to linear time and back again
POPL 3(POPL)2019
Quantitative separation logic: a logic for reasoning about probabilistic pointer programs
POPL 3(POPL)2019
An abstract domain for certifying neural networks
POPL 3(POPL)2019
Quantitative robustness analysis of quantum programs
POPL 3(POPL)2019
Intersection types and runtime errors in the pi-calculus
POPL 3(POPL)2019
A calculus for Esterel: if can, can. if no can, no can.
POPL 3(POPL)2019
Trace abstraction modulo probability
POPL 3(POPL)2019
Live functional programming with typed holes
POPL 3(POPL)2019
Fixpoint games on continuous lattices
POPL 3(POPL)2019
ISA semantics for ARMv8-a, RISC-v, and CHERI-MIPS
POPL 3(POPL)2019
Definitional proof-irrelevance without K
POPL 3(POPL)2019
Exploring C semantics and pointer provenance
POPL 3(POPL)2019
A²I: abstract² interpretation
POPL 3(POPL)2019
LWeb: information flow security for multi-tier web applications
POPL 3(POPL)2019
code2vec: learning distributed representations of code
POPL 3(POPL)2019
Distributed programming using role-parametric session types in go: statically-typed endpoint APIs for dynamically-instantiated communication structures
POPL 3(POPL)2019
Diagrammatic algebra: from linear to concurrent systems
POPL 3(POPL)2019
Grounding thin-air reads with event structures
POPL 3(POPL)2019
Efficient automated repair of high floating-point errors in numerical libraries
POPL 3(POPL)2019
Bayesian synthesis of probabilistic programs for automatic data modeling
POPL 3(POPL)2019
Iron: managing obligations in higher-order concurrent separation logic
POPL 3(POPL)2019
Dynamic type inference for gradual Hindley–Milner typing
POPL 3(POPL)2019
A verified, efficient embedding of a verifiable assembly language
POPL 3(POPL)2019
Closed forms for numerical loops
POPL 3(POPL)2019
Less is more: multiparty session types revisited
POPL 3(POPL)2019
Quantum relational Hoare logic
POPL 3(POPL)2019
Decision procedures for path feasibility of string-manipulating programs with complex operations
POPL 3(POPL)2019
Decidable verification of uninterpreted programs
POPL 3(POPL)2019
Structuring the synthesis of heap-manipulating programs
POPL 3(POPL)2019
Gradual typing: a new perspective
POPL 3(POPL)2019
Constructing quotient inductive-inductive types
POPL 3(POPL)2019
Inferring frame conditions with static correlation analysis
POPL 3(POPL)2019
Program synthesis by type-guided abstraction refinement
POPL 4(POPL)2019
CompCertM: CompCert with C-assembly linking and lightweight modular verification
POPL 4(POPL)2019
Backpropagation in the simply typed lambda-calculus with linear negation
POPL 4(POPL)2019
A probabilistic separation logic
POPL 4(POPL)2019
Recurrence extraction for functional programs through call-by-push-value
POPL 4(POPL)2019
The high-level benefits of low-level sandboxing
POPL 4(POPL)2019
Kind inference for datatypes
POPL 4(POPL)2019
Spy game: verifying a local generic solver in Iris
POPL 4(POPL)2019
Abstract interpretation of distributed network control planes
POPL 4(POPL)2019
Liquidate your assets: reasoning about resource usage in liquid Haskell
POPL 4(POPL)2019
Trace types and denotational semantics for sound programmable inference in probabilistic languages
POPL 4(POPL)2019
Proving expected sensitivity of probabilistic programs with randomized variable-dependent termination time
POPL 4(POPL)2019
Seminaïve evaluation for a higher-order functional language
POPL 4(POPL)2019
Abstract extensionality: on the properties of incomplete abstract interpretations
POPL 4(POPL)2019
Semantics of higher-order probabilistic programs with conditioning
POPL 4(POPL)2019
Deductive verification with ghost monitors
POPL 4(POPL)2019
Visualization by example
POPL 4(POPL)2019
Synthesis of coordination programs from linear temporal specifications
POPL 4(POPL)2019
Synthesizing replacement classes
POPL 4(POPL)2019
Relational proofs for quantum programs
POPL 4(POPL)2019
Parameterized verification under TSO is PSPACE-complete
POPL 4(POPL)2019
A language for probabilistically oblivious computation
POPL 4(POPL)2019
A simple differentiable programming language
POPL 4(POPL)2019
Decidable subtyping for path dependent types
POPL 4(POPL)2019
Partial type constructors: or, making ad hoc datatypes less ad hoc
POPL 4(POPL)2019
Binders by day, labels by night: effect instances via lexically scoped handlers
POPL 4(POPL)2019
Mechanized semantics and verified compilation for a dataflow synchronous language with reset
POPL 4(POPL)2019
Pointer life cycle types for lock-free data structures with memory reclamation
POPL 4(POPL)2019
Detecting floating-point errors via atomic conditions
POPL 4(POPL)2019
Fast, sound, and effectively complete dynamic race prediction
POPL 4(POPL)2019
What is decidable about gradual types?
POPL 4(POPL)2019
Deterministic parallel fixpoint computation
POPL 4(POPL)2019
The future is ours: prophecy variables in separation logic
POPL 4(POPL)2019
Reduction monads and their signatures
POPL 4(POPL)2019
Actris: session-type based reasoning in separation logic
POPL 4(POPL)2019
Aiming low is harder: induction for lower bounds in probabilistic program verification
POPL 4(POPL)2019
Label-dependent session types
POPL 4(POPL)2019
Persistency semantics of the Intel-x86 architecture
POPL 4(POPL)2019
Undecidability of
<i>
d
<sub><:</sub>
</i>
and its decidable fragments
POPL 4(POPL)2019
Graduality and parametricity: together again for the first time
POPL 4(POPL)2019
Deciding memory safety for single-pass heap-manipulating programs
POPL 4(POPL)2019
Taylor subsumes Scott, Berry, Kahn and Plotkin
POPL 4(POPL)2019
Guarded Kleene algebra with tests: verification of uninterpreted programs in nearly linear time
POPL 4(POPL)2019
Incorrectness logic
POPL 4(POPL)2019
Reductions for safety proofs
POPL 4(POPL)2019
Towards verified stochastic variational inference for probabilistic programs
POPL 4(POPL)2019
The weak call-by-value λ-calculus is reasonable for both time and space
POPL 4(POPL)2019
Interaction trees: representing recursive and impure programs in Coq
POPL 4(POPL)2019
Decomposition diversity with symmetric data and codata
POPL 4(POPL)2019
Optimal approximate sampling from discrete probability distributions
POPL 4(POPL)2019
Virtual timeline: a formal abstraction for verifying preemptive schedulers with temporal isolation
POPL 4(POPL)2019
Provenance-guided synthesis of Datalog programs
POPL 4(POPL)2019
Executable formal semantics for the POSIX shell
POPL 4(POPL)2019
Complexity and information in invariant inference
POPL 4(POPL)2019
Par means parallel: multiplicative linear logic proofs as concurrent functional programs
POPL 4(POPL)2019
The fire triangle: how to mix substitution, dependent elimination, and effects
POPL 4(POPL)2019
Augmented example-based synthesis using relational perturbation properties
POPL 4(POPL)2019
PλωNK: functional probabilistic NetKAT
POPL 4(POPL)2019
Stacked borrows: an aliasing model for Rust
POPL 4(POPL)2019
The next 700 relational program logics
POPL 4(POPL)2019
Dependent type systems as macros
POPL 4(POPL)2019
Does blame shifting work?
POPL 4(POPL)2019
Formal verification of a constant-time preserving C compiler
POPL 4(POPL)2019
SyTeCi: automating contextual equivalence for higher-order programs with references
POPL 4(POPL)2019
Disentanglement in nested-parallel programs
POPL 4(POPL)2019
Full abstraction for the quantum lambda-calculus
POPL 4(POPL)2019
RustBelt meets relaxed memory
POPL 4(POPL)2019
Coq Coq correct! verification of type checking and erasure for Coq, in Coq
POPL 4(POPL)2019