POPL 2024
100 videos • 3,503 views • by ACM SIGPLAN
POPL Research Papers
1
[POPL'24] Welcome To POPL 2024
ACM SIGPLAN
Download
2
[POPL'24] A New Perspective on Commutativity in Verification
ACM SIGPLAN
Download
3
[POPL'24] Implementation and Synthesis of Math Library Functions
ACM SIGPLAN
Download
4
[POPL'24] Enhanced Enumeration Techniques for Syntax-Guided Synthesis of Bit-Vector Manipu...
ACM SIGPLAN
Download
5
[POPL'24] Efficient Bottom-Up Synthesis for Programs with Local Variables
ACM SIGPLAN
Download
6
[POPL'24] Optimal Program Synthesis via Abstract Interpretation
ACM SIGPLAN
Download
7
[POPL'24] Generating Well-Typed Terms that are not "Useless"
ACM SIGPLAN
Download
8
[POPL'24] Indexed Types for a Statically Safe WebAssembly
ACM SIGPLAN
Download
9
[POPL'24] The Essence of Generalized Algebraic Data Types
ACM SIGPLAN
Download
10
[POPL'24] Ill-Typed Programs Don't Evaluate
ACM SIGPLAN
Download
11
[POPL'24] An Infinite Needle in a Finite Haystack: Finding Infinite Counter-Models in Dedu...
ACM SIGPLAN
Download
12
[POPL'24] Mostly Automated Verification of Liveness Properties for Distributed Protocols w...
ACM SIGPLAN
Download
13
[POPL'24] Decision and Complexity of Dolev-Yao Hyperproperties
ACM SIGPLAN
Download
14
[POPL'24] Soundly Handling Linearity
ACM SIGPLAN
Download
15
[POPL'24] Answer Refinement Modification: Refinement Type System for Algebraic Effects and...
ACM SIGPLAN
Download
16
[POPL'24] Effectful Software Contracts
ACM SIGPLAN
Download
17
[POPL'24] Algebraic Effects Meet Hoare Logic in Cubical Agda
ACM SIGPLAN
Download
18
[POPL'24] An Iris Instance for Verifying CompCert C Programs
ACM SIGPLAN
Download
19
[POPL'24] The Logical Essence of Well-Bracketed Control Flow
ACM SIGPLAN
Download
20
[POPL'24] Asynchronous Probabilistic Couplings in Higher-Order Separation Logic
ACM SIGPLAN
Download
21
[POPL'24] Thunks and Debits in Separation Logic with Time Credits
ACM SIGPLAN
Download
22
[POPL'24] Parikh's Theorem Made Symbolic
ACM SIGPLAN
Download
23
[POPL'24] Efficient Matching of Regular Expressions with Lookaround Assertions
ACM SIGPLAN
Download
24
[POPL'24] The Complex(ity) Landscape of Checking Infinite Descent
ACM SIGPLAN
Download
25
[POPL'24] Positive Almost-Sure Termination – Complexity and Proof Rules
ACM SIGPLAN
Download
26
[POPL'24] EasyBC: A Cryptography-Specific Language for Security Analysis of Block Ciphers ...
ACM SIGPLAN
Download
27
[POPL'24] A Core Calculus for Documents: Or, Lambda: The Ultimate Document
ACM SIGPLAN
Download
28
[POPL'24] Validation of Modern JSON Schema: Formalization and Complexity
ACM SIGPLAN
Download
29
[POPL'24] Shoggoth - A Formal Foundation for Strategic Rewriting
ACM SIGPLAN
Download
30
[POPL'24] A Universal, Sound, and Complete Forward Reasoning Technique for Machine-Verifie...
ACM SIGPLAN
Download
31
[POPL'24] Predictive Monitoring against Pattern Regular Languages
ACM SIGPLAN
Download
32
[POPL'24] Commutativity Simplifies Proofs of Parameterized Programs
ACM SIGPLAN
Download
33
[POPL'24] Coarser Equivalences for Causal Concurrency
ACM SIGPLAN
Download
34
[POPL'24] On Model-Checking Higher-Order Effectful Programs
ACM SIGPLAN
Download
35
[POPL'24] Explicit Effects and Effect Constraints in ReML
ACM SIGPLAN
Download
36
[POPL'24] Decalf: A Directed, Effectful Cost-Aware Logical Framework
ACM SIGPLAN
Download
37
[POPL'24] Modular Denotational Semantics for Effects with Guarded Interaction Trees
ACM SIGPLAN
Download
38
[POPL'24] Semantic Code Refactoring for Abstract Data Types
ACM SIGPLAN
Download
39
[POPL'24] API-driven Program Synthesis for Testing Static Typing Implementations
ACM SIGPLAN
Download
40
[POPL'24] Programmatic Strategy Synthesis: Resolving Nondeterminism in Probabilistic Progr...
ACM SIGPLAN
Download
41
[POPL'24] A Case for Synthesis of Recursive Quantum Unitary Programs
ACM SIGPLAN
Download
42
[POPL'24] Quotient Haskell: Lightweight Quotient Types for All
ACM SIGPLAN
Download
43
[POPL'24] Focusing on Refinement Typing (TOPLAS)
ACM SIGPLAN
Download
44
[POPL'24] Polymorphic Reachability Types: Tracking Freshness, Aliasing, and Separation in ...
ACM SIGPLAN
Download
45
[POPL'24] Capturing Types (TOPLAS)
ACM SIGPLAN
Download
46
[POPL'24] Probabilistic programming interfaces for random graphs: Markov categories, graph...
ACM SIGPLAN
Download
47
[POPL'24] Inference of Probabilistic Programs with Moment-Matching Gaussian Mixtures
ACM SIGPLAN
Download
48
[POPL'24] Higher Order Bayesian Networks, Exactly
ACM SIGPLAN
Download
49
[POPL'24] Strong Invariants Are Hard: On the Hardness of Strongest Polynomial Invariants f...
ACM SIGPLAN
Download
50
[POPL'24] With a Few Square Roots, Quantum Computing is as Easy as Pi
ACM SIGPLAN
Download
51
[POPL'24] Quantum Bisimilarity via Barbs and Contexts: Curbing the Power of Non-Determinis...
ACM SIGPLAN
Download
52
[POPL'24] SimuQ: A Framework for Programming Quantum Hamiltonian Simulation with Analog Co...
ACM SIGPLAN
Download
53
[POPL'24] Enriched Presheaf Model of Quantum FPC
ACM SIGPLAN
Download
54
[POPL'24] How Hard is Weak-Memory Testing?
ACM SIGPLAN
Download
55
[POPL'24] An Axiomatic Basis for Computer Programming on the Relaxed Arm-A Architecture: T...
ACM SIGPLAN
Download
56
[POPL'24] Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intension...
ACM SIGPLAN
Download
57
[POPL'24] Deadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-O...
ACM SIGPLAN
Download
58
[POPL'24] Polyregular functions on unordered trees of bounded height
ACM SIGPLAN
Download
59
[POPL'24] Solving Infinite-State Games via Acceleration
ACM SIGPLAN
Download
60
[POPL'24] Ramsey Quantifiers in Linear Arithmetics
ACM SIGPLAN
Download
61
[POPL'24] Reachability in Continuous Pushdown VASS
ACM SIGPLAN
Download
62
[POPL'24] Pipelines and Beyond: Graph Types for ADTs with Futures
ACM SIGPLAN
Download
63
[POPL'24] Disentanglement with Futures, State, and Interaction
ACM SIGPLAN
Download
64
[POPL'24] DisLog: A Separation Logic for Disentanglement
ACM SIGPLAN
Download
65
[POPL'24] Automatic Parallelism Management
ACM SIGPLAN
Download
66
[POPL'24] SIGPLAN Awards, PC Chair's Report, and Business Meeting
ACM SIGPLAN
Download
67
[POPL'24] Extraordinary Meeting: The Publicity Chairs Reflect on the Peer-Review Process
ACM SIGPLAN
Download
68
[POPL'24] The Network is the Computer: A Programming Language Perspective
ACM SIGPLAN
Download
69
[POPL'24] Solvable Polynomial Ideals: The Ideal Reflection for Program Analysis
ACM SIGPLAN
Download
70
[POPL'24] On-The-Fly Static Analysis via Dynamic Bidirected Dyck Reachability
ACM SIGPLAN
Download
71
[POPL'24] Monotonicity and the Precision of Program Analysis
ACM SIGPLAN
Download
72
[POPL'24] Flan: An Expressive and Efficient Datalog Compiler for Program Analysis
ACM SIGPLAN
Download
73
[POPL'24] Internal parametricity, without an interval
ACM SIGPLAN
Download
74
[POPL'24] Internal and Observational Parametricity for Cubical Agda
ACM SIGPLAN
Download
75
[POPL'24] Internalizing Indistinguishability with Dependent Types
ACM SIGPLAN
Download
76
[POPL'24] Polynomial Time and Dependent types
ACM SIGPLAN
Download
77
[POPL'24] Guided Equality Saturation
ACM SIGPLAN
Download
78
[POPL'24] Fusing Direct Manipulations into Functional Programs
ACM SIGPLAN
Download
79
[POPL'24] Inference of Robust Reachability Constraints
ACM SIGPLAN
Download
80
[POPL'24] Nominal Recursors as Epi-Recursors
ACM SIGPLAN
Download
81
[POPL'24] When Subtyping Constraints Liberate: A Novel Type Inference Approach for First-C...
ACM SIGPLAN
Download
82
[POPL'24] Parametric Subtyping for Structural Parametric Polymorphism
ACM SIGPLAN
Download
83
[POPL'24] Unboxed data constructors -- or, how cpp decides a halting problem
ACM SIGPLAN
Download
84
[POPL'24] Polymorphic Type Inference for Dynamic Languages
ACM SIGPLAN
Download
85
[POPL'24] Efficient CHAD
ACM SIGPLAN
Download
86
[POPL'24] ReLU Hull Approximation
ACM SIGPLAN
Download
87
[POPL'24] On Learning Polynomial Recursive Programs
ACM SIGPLAN
Download
88
[POPL'24] Programming-by-Demonstration for Long-Horizon Robot Tasks
ACM SIGPLAN
Download
89
[POPL'24] Mechanizing Refinement Types
ACM SIGPLAN
Download
90
[POPL'24] VST-A: A Foundationally Sound Annotation Verifier
ACM SIGPLAN
Download
91
[POPL'24] Fully Composable and Adequate Verified Compilation with Direct Refinements betwe...
ACM SIGPLAN
Download
92
[POPL'24] A Formalization of Core Why3 in Coq
ACM SIGPLAN
Download
93
[POPL'24] Securing Verified IO Programs Against Unverified Code in F*
ACM SIGPLAN
Download
94
[POPL'24] Sound Gradual Verification with Symbolic Execution
ACM SIGPLAN
Download
95
[POPL'24] Type-based Gradual Typing Performance Optimization
ACM SIGPLAN
Download
96
[POPL'24] Total Type Error Localization and Recovery with Holes
ACM SIGPLAN
Download
97
[POPL'24] Orthologic with Axioms
ACM SIGPLAN
Download
98
[POPL'24] Deciding Asynchronous Hyperproperties for Recursive Programs
ACM SIGPLAN
Download
99
[POPL'24] Calculational Design of [In]Correctness Transformational Program Logics by Abstr...
ACM SIGPLAN
Download
100
[POPL'24] Concluding Remarks
ACM SIGPLAN
Download