OOPSLA 2021
71 papers
- A derivative-based parser generator for visibly Pushdown grammars
- A multiparty session typing discipline for fault-tolerant event-driven distributed programming
- A type system for extracting functional specifications from memory-safe imperative programs
- APIfix: output-oriented program synthesis for combating breaking changes in libraries
- Automatic migration from synchronous to asynchronous JavaScript APIs
- Coarsening optimization for differentiable programming
- Compacting points-to sets through object clustering
- Compilation of sparse array programming models
- Compiling with continuations, correctly
- Copy-and-patch compilation: a fast compilation algorithm for high-level languages and bytecode
- Data-driven abductive inference of library specifications
- Durable functions: semantics for stateful serverless
- Dynaplex: analyzing program complexity using dynamically inferred recurrence relations
- ECROs: building global scale systems from sequential code
- Efficient automatic scheduling of imaging and vision pipelines for the GPU
- Efficient compilation of algebraic effect handlers
- FPL: fast Presburger arithmetic through transprecision
- Formal verification of high-level synthesis
- Fully automated functional fuzzing of Android apps for detecting non-crashing logic bugs
- Gauss: program synthesis by reasoning over graphs
- Generalizable synthesis through unification
- Generative type-aware mutation for testing SMT solvers
- Gradually structured data
- How statically-typed functional programmers write code
- Interpretable noninterference measurement and its application to processor designs
- JavaDL: automatically incrementalizing Java bug pattern detection
- LXM: better splittable pseudorandom number generators (and almost as fast)
- Label dependent lambda calculus and gradual typing
- LooPy: interactive program synthesis with control structures
- Making pointer analysis more precise by unleashing the power of selective context sensitivity
- Making weak memory models fair
- Modular specification and verification of closures in Rust
- MonkeyDB: effectively testing correctness under weak isolation levels
- Much ADO about failures: a fault-aware model for compositional verification of strongly consistent distributed systems
- Multi-modal program inference: a marriage of pre-trained language models and component-based synthesis
- Not so fast: understanding and mitigating negative impacts of compiler optimizations on code reuse gadget sets
- One down, 699 to go: or, synthesising compositional desugarings
- Permchecker: a toolchain for debugging memory managers with typestate
- Program analysis via efficient symbolic abstraction
- Programming and execution models for parallel bounded exhaustive testing
- Promises are made to be broken: migrating R to strict semantics
- QuickSilver: modeling and parameterized verification for distributed agreement-based systems
- Reachability types: tracking aliasing and separation in higher-order functional programs
- Reconciling optimization with secure compilation
- Relational nullable types with Boolean unification
- Rewrite rule inference using equality saturation
- Rich specifications for Ethereum smart contract verification
- Safer at any speed: automatic context-aware safety enhancement for Rust
- Scalability and precision by combining expressive type systems and deductive verification
- SecRSL: security separation logic for C11 release-acquire concurrency
- Semantic programming by example with pre-trained models
- SimTyper: sound type inference for Ruby using type equality prediction
- Solver-based gradual type migration
- SpecSafe: detecting cache side channels in a speculative world
- Specifying and testing GPU workgroup progress models
- Static detection of silent misconfigurations with deep interaction analysis
- Statically bounded-memory delayed sampling for probabilistic streams
- Study of the subtyping machine of nominal subtyping with variance
- Symbolic value-flow static analysis: deep, precise, complete modeling of Ethereum smart contracts
- Synbit: synthesizing bidirectional programs using unidirectional sketches
- Synthesizing contracts correct modulo a test generator
- The reads-from equivalence for the TSO and PSO memory models
- The semantics of shared memory in Intel CPU/FPGA systems
- Transitioning from structural to nominal code with efficient gradual typing
- Translating C to safer Rust
- Type stability in Julia: avoiding performance pathologies in JIT compilation
- UDF to SQL translation through compositional lazy inductive synthesis
- VESPA: static profiling for binary optimization
- Verifying concurrent multicopy search structures
- Well-typed programs can go wrong: a study of typing-related bugs in JVM compilers
- What we eval in the shadows: a large-scale study of eval in R programs