POPL 2022
65 papers
- A Quantum interpretation of separating conjunction for local reasoning of Quantum programs based on separation logic
- A cost-aware logical framework
- A dual number abstraction for static analysis of Clarke Jacobians
- A fine-grained computational interpretation of Girard's intuitionistic proof-nets
- A formal foundation for symbolic evaluation with merging
- A relational theory of effects and coeffects
- A separation logic for heap space under garbage collection
- A separation logic for negative dependence
- Bottom-up synthesis of recursive functional programs using angelic execution
- Certifying derivation of state machines from coroutines
- Concurrent incorrectness separation logic
- Connectivity graphs: a method for proving deadlock freedom based on separation logic
- Context-bounded verification of thread pools
- Dependently-typed data plane programming
- Effectful program distancing
- Efficient algorithms for dynamic bidirected Dyck-reachability
- Extending Intel-x86 consistency and persistency: formalising the semantics of Intel-x86 memory types and non-temporal stores
- Fair termination of binary sessions
- Formal metatheory of second-order abstract syntax
- From enhanced coinduction towards enhanced induction
- Fully abstract models for effectful λ-calculi via category-theoretic logical relations
- Induction duality: primal-dual search for invariants
- Interval universal approximation for neural networks
- Isolation without taxation: near-zero-cost transitions for WebAssembly and SFI
- Layered and object-based game semantics
- Learning formulas in finite variable logics
- Linked visualisations via Galois dependencies
- Logarithm and program testing
- Mœbius: metaprogramming using contextual types: the stage where system f can pattern match on itself
- Oblivious algebraic data types
- Observational equality: now for good
- On incorrectness logic and Kleene algebra with top and tests
- On type-cases, union elimination, and occurrence typing
- One polynomial approximation to produce correctly rounded results of an elementary function for multiple representations and rounding modes
- PRIMA: general and precise neural network certification via scalable convex hull approximations
- Partial (In)Completeness in abstract interpretation: limiting the imprecision in program analysis
- Pirouette: higher-order typed functional choreographies
- Profile inference revisited
- Property-directed reachability as abstract interpretation in the monotone theory
- Provably correct, asymptotically efficient, higher-order reverse-mode automatic differentiation
- Quantum information effects
- Reasoning about "reasoning about reasoning": semantics and contextual equivalence for probabilistic programs with nested queries and recursion
- Relational e-matching
- Return of CFA: call-site sensitivity can be superior to object sensitivity even for object-oriented programs
- Safe, modular packet pipeline programming
- Semantics for variational Quantum programming
- Simuliris: a separation logic framework for verifying concurrent program optimizations
- Software model-checking as cyclic-proof search
- SolType: refinement types for arithmetic overflow in solidity
- Solving constrained Horn clauses modulo algebraic data types and recursive functions
- Solving string constraints with Regex-dependent functions through transducers with priorities and variables
- Staging with class: a specification for typed template Haskell
- Static prediction of parallel computation graphs
- Subcubic certificates for CFL reachability
- Symmetries in reversible programming: from symmetric rig groupoids to reversible programming languages
- The decidability and complexity of interleaved bidirected Dyck reachability
- The leaky semicolon: compositional semantic dependencies for relaxed-memory concurrency
- Truly stateless, optimal dynamic partial order reduction
- Twist: sound reasoning for purity and entanglement in Quantum programs
- Type-level programming with match types
- VIP: verifying real-world C idioms with integer-pointer casts
- Verified compilation of C programs with a nominal memory model
- Verified tensor-program optimization via high-level scheduling rewrites
- Visibility reasoning for concurrent snapshot algorithms
- What's decidable about linear loops?