POPL 2023 SRC
2023-01-18
Boston, United States
POPL ·
[POPL 2021, POPL 2022, POPL 2022 Virtual Workshop, POPL 2023, POPL 2023 SRC, POPL 2024, POPL 2025, POPL 2026]
who it's for
programming language researchers, compiler engineers, program synthesis researchers, formal verification engineers, testing and QA engineers, python library developers, quantum programming language developers
topics
vectorized Python loop synthesis; SMT-checked synthesis of combinators; property-based verifier testing; gradual verifier soundness; CPS-calculus metatheory; Coq mechanized proofs; Bayesian probabilistic assertions; branch-probability based monitoring; regular-expression synthesis ranking; beam search for synthesis; Silq to HQIR compilation; automatic quantum uncomputation
| title | author | length |
|---|---|---|
| Synthesizing Vectorized Code via Verified Lifting | Jeremy Ferguson | 14m |
A toolchain translates small, fixed‑size Python loops into vectorized NumPy by unrolling loops, emitting C/C++/LLVM, and using Metalift to synthesize programs… | ||
| Evaluating Soundness of a Gradual Verifier with Property Based Testing | Jan-Paul Ramos-Davila | 15m |
An empirical checker implements Gradual C0 and a fully dynamic Dynamic C0 verifier, runs both on mutated versions of a dozen large benchmarks, and asserts… | ||
| On the metatheory of IRs and the CPS-calculus | Paulo Torrens | 12m |
Formalizes Thielecke’s CPS-calculus with an equational theory driven by real compiler optimizations and proves the new reduction relation admits a theory of… | ||
| Wisening Assertions: A live Bayesian reasoning system for probabilistic co... | Joshua Turcotti | 14m |
Claims a practical system that turns expensive runtime assertions into a scalable, probabilistic monitor by computing a blame as probabilistic event per… | ||
| Scalable Synthesis of Regular Expressions From Only Positive Examples | Elizaveta Pertseva, Mark Barbone | 16m |
Synthesis system extends Regex+ with a pragmatic ranking function (Bayesian simplicity vs. specificity) and three search modes: VSA enumeration (complete)… | ||
| Compiling and Running High-level Quantum Programs | Hristo Venev | 16m |
Claims a working compilation framework from Silq to a new graph IR called HQIR that preserves Silq semantics and is physically realizable; implements automatic… | ||
| nothing matches | ||