POPL 2021
61 papers
- A computational interpretation of compact closed categories: reversible programming with negative and fractional types
- A graded dependent type system with a usage-aware semantics
- A practical mode system for recursive definitions
- A pre-expectation calculus for probabilistic sensitivity
- A separation logic for effect handlers
- A unifying type-theory for higher-order (amortized) cost analysis
- A verified optimizer for Quantum circuits
- Abstracting gradual typing moving forward: precise and space-efficient
- An abstract interpretation for SPMD divergence on reducible control flow graphs
- An approach to generate correctly rounded math libraries for new floating point variants
- Asynchronous effects
- Automata and fixpoints for asynchronous hyperproperties
- Automatic differentiation in PCF
- Automatically eliminating speculative leaks from cryptographic code with blade
- Combining the top-down propagation and bottom-up enumeration for inductive program synthesis
- Context-bounded verification of liveness properties for multithreaded shared-memory programs
- Corpse reviver: sound and efficient gradual typing via contract verification
- Cyclic proofs, system t, and the power of contraction
- Data flow refinement type inference
- Deciding accuracy of differential privacy schemes
- Deciding reachability under persistent x86-TSO
- Deciding ω-regular properties on linear recurrence sequences
- Diamonds are not forever: liveness in reactive programming with guarded recursion
- Dijkstra monads forever: termination-sensitive specifications for interaction trees
- Distributed causal memory: modular specification and verification in higher-order distributed separation logic
- Efficient and provable local capability revocation using uninitialized capabilities
- Formally verified speculation and deoptimization in a JIT compiler
- Fully abstract from static to gradual
- Functorial semantics for partial theories
- Generating collection transformations from proofs
- Giving semantics to program-counter labels via secure effects
- Intensional datatype refinement: with application to scalable verification of pattern-match safety
- Internalizing representation independence with univalence
- Intersection types and (positive) almost-sure termination
- Intrinsically typed compilation with nameless labels
- Learning the boundary of inductive invariants
- Mechanized logical relations for termination-insensitive noninterference
- Modeling and analyzing evaluation cost of CUDA kernels
- On algebraic abstractions for concurrent separation logics
- On the complexity of bidirected interleaved Dyck-reachability
- On the semantic expressiveness of recursive types
- Optimal prediction of synchronization-preserving races
- Paradoxes of probabilistic programming: and how to condition on events of measure zero with infinitesimal probabilities
- PerSeVerE: persistency semantics for verification under ext4
- Petr4: formal foundations for p4 data planes
- Precise subtyping for asynchronous multiparty sessions
- Probabilistic programming semantics for name generation
- Provably space-efficient parallel functional programming
- Relatively complete verification of probabilistic programs: an expressive language for expectation-based reasoning
- Semantics-guided synthesis
- Simplifying dependent reductions in the polyhedral model
- Taming x86-TSO persistency
- The (In)Efficiency of interaction
- The fine-grained and parallel complexity of andersen's pointer analysis
- The taming of the rew: a type theory with computational assumptions
- Transfinite step-indexing for termination
- Verified code generation for the polyhedral model
- Verifying correct usage of context-free API protocols
- Verifying observational robustness against a c11-style memory model
- egg: Fast and extensible equality saturation
- 𝜆ₛ: computable semantics for differentiable programming with higher-order functions and datatypes