POPL 2019
77 papers
- A calculus for Esterel: if can, can. if no can, no can
- A domain theory for statistical probabilistic programming
- A separation logic for concurrent randomized programs
- A true positives theorem for a static race detector
- A verified, efficient embedding of a verifiable assembly language
- Abstracting algebraic effects
- Abstracting extensible data types: or, rows by any other name
- Abstraction-safe effect handlers via tunneling
- Adventures in monitorability: from branching to linear time and back again
- An abstract domain for certifying neural networks
- An abstract stack based approach to verified compositional compilation to machine code
- A²I: abstract² interpretation
- Bayesian synthesis of probabilistic programs for automatic data modeling
- Better late than never: a fully-abstract semantics for classical processes
- Bindings as bounded natural functors
- Bisimulation as path type for guarded recursive types
- Bounded model checking of signal temporal logic properties using syntactic separation
- Bridging the gap between programming languages and hardware weak memory models
- CT-wasm: type-driven secure cryptography for the web ecosystem
- Categorical combinatorics of scheduling and synchronization in game semantics
- Closed forms for numerical loops
- Concerto: a framework for combined concrete and abstract interpretation
- Constructing quotient inductive-inductive types
- Context-, flow-, and field-sensitive data-flow analysis using synchronized Pushdown systems
- Decidable verification of uninterpreted programs
- Decision procedures for path feasibility of string-manipulating programs with complex operations
- Decoupling lock-free data structures from memory reclamation for static analysis
- Definitional proof-irrelevance without K
- Diagrammatic algebra: from linear to concurrent systems
- Distributed programming using role-parametric session types in go: statically-typed endpoint APIs for dynamically-instantiated communication structures
- Dynamic type inference for gradual Hindley-Milner typing
- Efficient automated repair of high floating-point errors in numerical libraries
- Efficient parameterized algorithms for data packing
- Exceptional asynchronous session types: session types without tiers
- Exploring C semantics and pointer provenance
- Familial monads and structural operational semantics
- Fast and exact analysis for LRU caches
- Fixpoint games on continuous lattices
- Formal verification of higher-order probabilistic programs: reasoning about approximation, convergence, Bayesian inference, and optimization
- FrAngel: component-based synthesis with control structures
- From fine- to coarse-grained dynamic information flow control and back
- Fully abstract module compilation
- Game semantics for quantum programming
- Gradual parametricity, revisited
- Gradual type theory
- Gradual typing: a new perspective
- Grounding thin-air reads with event structures
- Hamsaz: replication coordination analysis and synthesis
- Higher inductive types in cubical computational type theory
- ISA semantics for ARMv8-a, RISC-v, and CHERI-MIPS
- Inferring frame conditions with static correlation analysis
- Intersection types and runtime errors in the pi-calculus
- Iron: managing obligations in higher-order concurrent separation logic
- JaVerT 2.0: compositional symbolic execution for JavaScript
- LWeb: information flow security for multi-tier web applications
- Less is more: multiparty session types revisited
- Live functional programming with typed holes
- Modalities, cohesion, and information flow
- Modular quantitative monitoring
- On library correctness under weak memory consistency: specifying and verifying concurrent libraries under declarative consistency models
- Polymorphic symmetric multiple dispatch with variance
- Pretend synchrony: synchronous verification of asynchronous distributed programs
- Principality and approximation under dimensional bound
- Probabilistic programming with densities in SlicStan: efficient, flexible, and deterministic
- Quantitative robustness analysis of quantum programs
- Quantitative separation logic: a logic for reasoning about probabilistic pointer programs
- Quantum relational Hoare logic
- Refinement of path expressions for static analysis
- Skeletal semantics and their interpretations
- Sound and complete bidirectional typechecking for higher-rank polymorphism with existentials and indexed types
- StkTokens: enforcing well-bracketed control flow and stack encapsulation using linear capabilities
- Structuring the synthesis of heap-manipulating programs
- Trace abstraction modulo probability
- Two sides of the same coin: session types and game semantics: a synchronous side and an asynchronous side
- Type-guided worst-case input generation
- Weak-consistency specification via visibility relaxation
- code2vec: learning distributed representations of code