PLDI 2023
2023-06-17..2023-06-21
-- online --
[PLDI 2020, PLDI 2022, PLDI 2023, PLDI 2024, PLDI 2024 Workshop Honoring Andreas Podelski, PLDI 2025, PLDI 2026, PLDI 2026 Student Research Competition]
as the organisers put it
PLDI echoes FCRC’s statement regarding recent legislation in Florida. Anyone, from any background, should feel encouraged to participate and contribute to PLDI. Differences – in age, race, gender and sexual orientation, nationality, physical ability, thinking style and experience – bring richness to our efforts in providing quality programs and services for the global computing community. Thus, PLDI is committed to creating an environment that welcomes new ideas and perspectives, and where hostility or other antisocial behaviors are not tolerated. Welcome to the home page of the 44th ACM ...
who it's for
programming language researchers, compiler engineers, formal verification engineers, systems engineers, machine learning engineers, security and privacy engineers, parallel and concurrency engineers
topics
dynamic partial order reduction for transactions; region inference for parallelism; homomorphic encryption compiler optimizations; neural network verification and repair; equality saturation with Datalog; WebAssembly program verification; CUDA memory safety debugging; probabilistic programming density compilation; modal and separation logics for concurrency; tensor algebra compiler interoperability; program synthesis for batch image processing; register tiling for unstructured sparsity
| title | author | length |
|---|---|---|
| Dynamic Partial Order Reduction for Checking Correctness Against Transaction Isolation(…) | Ahmed Bouajjani, Constantin Enea, Enrique Román-Calvo | 16m |
First DPOR-based stateless model checking algorithm for transactional apps that is sound, complete and optimal and runs in polynomial memory. It is parametric… | ||
| Efficient Parallel Functional Programming with Effects | Jatin Arora, Sam Westrick, Umut A. Acar | 21m |
Extends the MPL/Maple compiler for Parallel ML to track and pin entangled objects and install read barriers on mutable objects, proving entanglement management… | ||
| Context Sensitivity without Contexts: A Cut-Shortcut Approach to Fast and Precise(…) | Wenjie Ma, Shengyuan Yang, Tian Tan, Xiaoxing Ma, Chang Xu, Yue Li | 21m |
Proposes Cut-Shortcut that cuts PFG edges causing merged flows and adds direct shortcut edges to simulate context sensitivity without cloning; implements two… | ||
| Fuzzing Loop Optimizations in Compilers for C++ and Data-Parallel Languages | Vsevolod Livinskii, Dmitry Babokin, John Regehr | 17m |
An open-source reimplementation of YARPGen reimplementation generates C/C++ and data-parallel tests that statically avoid undefined behavior using a… | ||
| Better Together: Unifying Datalog and Equality Saturation | Yihong Zhang, Yisu Remy Wang, Oliver Flatt, David Cao, Philip Zucker, Eli Rosenthal, Zachary Tatlock, Max Willsey | 17m |
egglog claims a single system that combines Datalog-style declarative analyses with equality-saturation rewriting by introducing functional dependency repair… | ||
| A Lineage-Based Referencing DSL for Computer-Aided Design | Dan Cascaval, Rastislav Bodík, Adriana Schulz | 18m |
Proposes a semantics that records fine‑grained element lineage and exposes it as first‑class queries so references remain stable across parameterized… | ||
| Parallelism in a Region Inference Context | Martin Elsman, Troels Henriksen | 18m |
Implements a fork‑join parallel construct for a region‑inference compiler, embeds an effect-based region-protection inference that flags regions needing… | ||
| Prompting Is Programming: A Query Language for Large Language Models | Luca Beurer-Kellner, Marc Fischer, Martin Vechev | 30m |
Introduces LMQL, a small query language that combines templated prompts, Python control flow and constraint decoding to steer off‑the‑shelf LLMs by masking… | ||
| Architecture-Preserving Provable Repair of Deep Neural Networks | Zhe Tao, Stephanie Nawas, Jacqueline Mitchell, Aditya V. Thakur | 21m |
Presents an algorithm that modifies only network parameters to yield architecture-preserving fixes that are provably correct on entire V-polytopes, encoding… | ||
| Better Defunctionalization through Lambda Set Specialization | William Brandon, Benjamin Driscoll, Frank Dai, Wilson Berkow, Mae Milano | 23m |
Claims a compiler pass called Lambda set specialization that turns defunctionalization into type monomorphization, implemented as a polymorphic internal type… | ||
| Incremental Verification of Neural Networks | Shubham Ugare, Debangshu Banerjee, Sasa Misailovic, Gagandeep Singh | 20m |
Complete, verifier-agnostic method IVAN reuses branch-and-bound work by saving a specification tree of partitioned subproblems and then avoids costly analyzer… | ||
| Responsive Parallelism with Synchronization | Stefan K. Muller, Kyle Singer, Devyn Terra Keeney, Andrew Neth, Kunal Agrawal, I-Ting Angelina Lee, Umut A. Acar | 25m |
Claims a static type system plus runtime priority-ceiling prevents priority inversions across mutexes and condition variables, with a formal soundness proof… | ||
| Cutting the Cake: A Language for Fair Division | Noah Bertram, Alex Levinson, Justin Hsu | 18m |
A domain-specific language called Slice DSL encodes cake-cutting protocols and compiles them to logical constraints that are sound and complete with respect to… | ||
| Loop Rerolling for Hardware Decompilation | Zachary D. Sisco, Jonathan Balkind, Timothy Sherwood, Ben Hardekopf | 19m |
Defines hardware loop rerolling to recover syntactic loops from netlists by combining clone detection with sketch-based program synthesis using Rosette, and… | ||
| HEaaN.MLIR: An Optimizing Compiler for Fast Ring-Based Homomorphic Encryption | Sunjae Park, Woosung Song, Seunghyeon Nam, Hyeongyu Kim, Junbum Shin, Juneyoung Lee | 20m |
A compiler that lowers ring HE programs into CPU machine code and two custom IRs Poly and ModArith IRs perform cross‑polynomial optimizations: optimized… | ||
| Sound Dynamic Deadlock Prediction in Linear Time | Hünkar Can Tunç, Umang Mathur, Andreas Pavlogiannis, Mahesh Viswanathan | 15m |
Introduces a new class called sync-preserving deadlocks and two algorithms SPDOffline and SPDOnline that detect only those deadlocks but do so with overall… | ||
| Performal: Formal Verification of Latency Properties for Distributed Systems | Tony Nuda Zhang, Upamanyu Sharma, Manos Kapritsos | 20m |
PerforMal gives a concrete method to prove worst case latency for real distributed code by modeling programs as state machines in Daphne, attaching ghost… | ||
| Reliable Actors with Retry Orchestration | Olivier Tardieu, David Grove, Gheorghe-Teodor Bercea, Paul Castro, Jaroslaw Cwiklik, Edward Epstein | 18m |
Proposes retry orchestration that guarantees failed actor invocations are retried, completed invocations never repeat, and strict happen‑before ordering across… | ||
| Modular Hardware Design with Timeline Types | Rachit Nigam, Adrian Sampson | 20m |
Filament implements timeline types to encode when signals are produced and consumed, enforcing timing and structural constraints for statically scheduled… | ||
| Memento: A Framework for Detectable Recoverability in Persistent Memory | Kyeongmin Cho, Seungmin Jeon, Azalea Raad, Jeehoon Kang | 19m |
Memento is a programming framework that proves and enforces detectable recoverability for persistent memory by using a timestamp-based recovery strategy plus… | ||
| Beyond Backtracking: Connections in Fine-Grained Concurrent Separation Logic | Ike Mulder, Łukasz Czajka, Robbert Krebbers | 19m |
Proposes a connection-based multi-succedent calculus that reduces blind backtracking for disjunctive invariants in fine-grained concurrent separation logic… | ||
| Abstract Interpretation of Fixpoint Iterators with Applications to Neural Networks | Mark Niklas Müller, Marc Fischer, Robin Staab, Martin Vechev | 15m |
A new abstract-interpretation framework abstracts the concrete fixpoints of numerical fixpoint iterators and implements it in CRAFT, introducing the… | ||
| Collecting Cyclic Garbage across Foreign Function Interfaces: Who Takes the Last Piece(…) | Tetsuro Yamazaki, Tomoki Nakamaru, Ryota Shioya, Tomoharu Ugawa, Shigeru Chiba | 17m |
Refgraph GC coordinates two independent tracing collectors by copying a compressed reference graph from Ruby into an unmodified JavaScript runtime so the JS… | ||
| Scallop: A Language for Neurosymbolic Programming | Ziyang Li, Jiani Huang, Mayur Naik | 17m |
Scallop is a differentiable neurosymbolic language that compiles Datalog-style programs to a relational algebra machine and plugs into PyTorch, using a… | ||
| Register Tiling for Unstructured Sparsity in Neural Network Inference | Lucas Wilkinson, Kazem Cheshmi, Maryam Mehri Dehnavi | 16m |
Introduces Sparse Register Tiling that uses an unroll-and-sparse-jam compile-time transformation plus compression to shrink SpMM code size and improve register… | ||
| Don't Look UB: Exposing Sanitizer-Eliding Compiler Optimizations | Raphael Isemann, Cristiano Giuffrida, Herbert Bos, Erik van der Kouwe, Klaus von Gleissenthall | 18m |
Differential-testing framework LookUB compiles programs with sanitizers on with and without optimization to expose optimizer transformations that remove… | ||
| cuCatch: A Debugging Tool for Efficiently Catching Memory Safety Violations in CUDA(…) | Mohamed Tarek Ibn Ziad, Sana Damani, Aamer Jaleel, Stephen W. Keckler, Mark Stephenson | 23m |
cuCatch implements compiler-added read-metadata and safety-check instructions plus a runtime PST and two-level shadow map to retrieve per-allocation base, size… | ||
| Indexed Streams: A Formal Intermediate Representation for Fused Contraction Programs | Scott Kovach, Praneeth Kolichala, Tiancheng Gu, Fredrik Kjolstad | 16m |
A formal operational IR called index streams models sparse tensors and relations as transition systems with index, value, ready and skip functions… | ||
| Type-Checking CRDT Convergence | George Zakhour, Pascal Weisenburger, Guido Salvaneschi | 16m |
Propel is a Scala-embedded language and type system that encodes CRDT merge laws as types and automatically proves them by case analysis, induction, and… | ||
| A Type System for Safe Intermittent Computing | Milijana Surbatovich, Naomi Spargo, Limin Jia, Brandon Lucia | 20m |
Curricle is a Rust-based information-flow type system that classifies variables as item-potent or non-item-potent, adds access-mode inference to decide when… | ||
| ImageEye: Batch Image Processing using Program Synthesis | Celeste Barnaby, Qiaochu Chen, Roopsha Samanta, Işıl Dillig | 20m |
A synthesis pipeline that learns programs in a neuro-symbolic DSL uses Amazon recognition detectors and an enumerative synthesizer with equivalence-reduction… | ||
| Derivative Based Nonbacktracking Real-World Regex Matching with Backtracking Semantics | Dan Moseley, Mario Nishio, Jose Perez Rodriguez, Olli Saarikivi, Stephen Toub, Margus Veanes, Tiki Wan, Eric Xu | 19m |
A derivative-based algorithm produces input-linear matching without actual backtracking while preserving PC (backtracking) semantics and supporting anchors and… | ||
| Mosaic: An Interoperable Compiler for Tensor Algebra | Manya Bansal, Olivia Hsu, Kunle Olukotun, Fredrik Kjolstad | 19m |
Mosaic is a Taco-based compiler that binds tensor expressions to external library or compiler functions via a scheduling API, substitutes bound subexpressions… | ||
| Flux: Liquid Types for Rust | Nico Lehmann, Adam T. Geller, Niki Vazou, Ranjit Jhala | 20m |
Flux implements a novel refined type system for Rust as a plug-in to the Rust compiler that indexes mutable locations, introduces strong references for precise… | ||
| Automated Expected Value Analysis of Recursive Programs | Martin Avanzini, Georg Moser, Michael Schaper | 17m |
Defines infer[.], a term representation that translates weakest pre-expectation semantics for recursive, imperative probabilistic programs into first-order… | ||
| PureCake: A Verified Compiler for a Lazy Functional Language | Hrutvik Kanabar, Samuel Vivien, Oskar Abrahamsson, Magnus O. Myreen, Michael Norrish, Johannes Åman Pohjola, Riccardo Zanetti | 17m |
PureCake is a mechanically verified compiler built in HOL4 that translates a Haskell-like lazy language, PureLang, down to machine code by targeting and… | ||
| VMSL: A Separation Logic for Mechanised Robust Safety of Virtual Machines Communicating(…) | Zongyuan Liu, Sergei Stepanenko, Jean Pichon-Pharabod, Amin Timany, Aslan Askarov, Lars Birkedal | 18m |
Formalises a substantial fragment of Arm FF‑A as a toy ISA with hypercalls and develops VMSL separation logic to reason about VM-to-VM shared pages and handoff… | ||
| CryptOpt: Verified Compilation with Randomized Program Search for Cryptographic Primitives | Joel Kuepper, Andres Erbsen, Jason Gross, Owen Conoly, Chuyue Sun, Samuel Tian, David Wu, Adam Chlipala, Chitchanok Chuengsatiansup, Daniel Genkin, Markus Wagner, Yuval Yarom | 19m |
CryptOpt turns Fiat Cryptography IR into x86-64 assembly by running a random local search over instruction selection and scheduling, auto-benchmarking… | ||
| Merging Inductive Relations | Jacob Prinz, Leonidas Lampropoulos | 19m |
Algorithm takes two inductive relations over the same data type and produces a single relation provably equivalent to their conjunction by constructor-pair… | ||
| Synthesizing MILP Constraints for Efficient and Robust Optimization | Jingbo Wang, Aarti Gupta, Chao Wang | 17m |
Proposes a syntax-guided synthesis pipeline that generates MILP encodings from arbitrary Boolean-linear specs, implementing an extensible DSL, iterative… | ||
| Fair Operational Semantics | Dongjae Lee, Minki Cho, Jinwoo Kim, Soonwon Moon, Youngju Song, Chung-Kil Hur | 20m |
Proposes FOS, an operational semantics that can encode arbitrary fairness notions and gives a concrete proof technique: a fairness counter that drops on bad… | ||
| Formally Verified Samplers from Probabilistic Programs with Loops and Conditioning | Alexander Bagnall, Gordon Stewart, Anindya Banerjee | 20m |
Zar compiles cpGCL programs with unbounded loops and conditioning into proved-correct samplers in the random bit model, implemented and fully verified in Coq… | ||
| Verified Density Compilation for a Probabilistic Programming Language | Joseph Tassarotti, Jean-Baptiste Tristan | 20m |
Provides a mechanized semantics for a Stan subset and verifies three density-compilation passes in Coq, producing ProbCompCert that connects to CompCert down… | ||
| Generalized Policy-Based Noninterference for Efficient Confidentiality-Preservation | Shamiek Mangipudi, Pavel Chuprikov, Patrick Eugster, Malte Viering, Savvas Savvides | 20m |
Hydra implements a mechanism‑independent language and a type system that enforces a generalized noninterference property called S non-interference and… | ||
| Trace-Guided Inductive Synthesis of Recursive Functional Programs | Yongwei Yuan, Arjun Radhakrishna, Roopsha Samanta | 20m |
A method augments program search with explicit recursion traces and a new version space algebra that represents pairs of traces and programs under angelic… | ||
| Taype: A Policy-Agnostic Language for Oblivious Computation | Qianchuan Ye, Benjamin Delaware | 20m |
Taype provides a policy-agnostic language and a compiler that implements oblivious algebraic data types and tape semantics, translating λOADT+ concepts into a… | ||
| Recursive State Machine Guided Graph Folding for Context-Free Language Reachability | Yuxiang Lei, Yulei Sui, Shin Hwei Tan, Qirun Zhang | 15m |
An algorithm called graph folding GF identifies adjacent node pairs that are provably removable for CFL‑reachability by examining only their incoming and… | ||
| Covering All the Bases: Type-Based Verification of Test Input Generators | Zhe Zhou, Ashish Mishra, Benjamin Delaware, Suresh Jagannathan | 19m |
Claims a new coverage types system that interprets refinements as underapproximate reasoning and verifies whether generators actually produce every value in a… | ||
| Modular Control Plane Verification via Temporal Invariants | Timothy Alberdingk Thijm, Ryan Beckett, Aarti Gupta, David Walker | 21m |
Timepiece implements a temporal model and an SMT-backed verifier (C library plus harness) that replaces unsafe stable-state modular checks with temporal… | ||
| Obtaining Information Leakage Bounds via Approximate Model Counting | Seemanta Saha, Surendra Ghentiyala, Shihua Lu, Lucas Bang, Tevfik Bultan | 14m |
Provides a method that produces sound upper and lower bounds on Shannon entropy when symbolic execution fails to explore all paths or model counters return… | ||
| Automated Detection of Under-Constrained Circuits in Zero-Knowledge Proofs | Shankara Pailoor, Yanju Chen, Franklyn Wang, Clara Rodríguez, Jacob Van Geffen, Jason Morton, Michael Chu, Brian Gu, Yu Feng, Işıl Dillig | 19m |
Tool QED2 performs semantic reasoning over Circom-generated polynomial equations by combining SMT solving with lightweight uniqueness inference in an… | ||
| Psym: Efficient Symbolic Exploration of Distributed Systems | Lauren Pick, Ankush Desai, Aarti Gupta | 18m |
Psym implements a symbolic explorer for P programs that merges frontier states using composite value summaries and canonical BDD-backed SECI guards so… | ||
| Inductive Program Synthesis via Iterative Forward-Backward Abstract Interpretation | Yongho Yoon, Woosuk Lee, Kwangkeun Yi | 17m |
Implements a synthesis tool, Shimba, that uses iterative forward-backward abstract interpretation plus a reduced product domain and selective finite… | ||
| WasmRef-Isabelle: A Verified Monadic Interpreter and Industrial Fuzzing Oracle for(…) | Conrad Watt, Maja Trela, Peter Lammich, Florian Märkl | 17m |
A verified monadic interpreter for WebAssembly implemented in Isabelle/HOL and proven via a two-step refinement proof against WasmCert-Isabelle, extracted to… | ||
| Extensible Metatheory Mechanization via Family Polymorphism | Ende Jin, Nada Amin, Yizhou Zhang | 19m |
Claims a language-layer for family polymorphism inside Coq that reuses code and proofs via late binding and generates a Coq plugin plus a core dependent type… | ||
| Leveraging Rust Types for Program Synthesis | Jonáš Fiala, Shachar Itzhaky, Peter Müller, Nadia Polikarpova, Ilya Sergey | 21m |
First deductive synthesizer for safe Rust that uses Rust types to both shrink specifications and prune search, extracting programs from proofs and guaranteeing… | ||
| Cakes That Bake Cakes: Dynamic Computation in CakeML | Thomas Sewell, Magnus O. Myreen, Yong Kiam Tan, Ramana Kumar, Alexander Mihajlovic, Oskar Abrahamsson, Scott Owens | 24m |
Extends the verified CakeML compiler with an Eval primitive that compiles and executes new CakeML code at runtime, letting original and dynamic code share… | ||
| Parameterized Algebraic Protocols | Andreia Mordido, Janek Spaderna, Peter Thiemann, Vasco T. Vasconcelos | 20m |
The work defines algebraic session types that name recursion like algebraic datatypes and claim type equivalence becomes linear-time nominal check instead of… | ||
| Optimal Reads-From Consistency Checking for C11-Style Memory Models | Hünkar Can Tunç, Parosh Aziz Abdulla, Soham Chakraborty, Krishna Shankaranarayanan, Umang Mathur, Andreas Pavlogiannis | 15m |
Characterizes reads-from consistency for C11 variants and gives concrete algorithms and hardness results: introduces a minimal coherence witness to avoid… | ||
| Putting Weak Memory in Order via a Promising Intermediate Representation | Sung-Hwan Lee, Minki Cho, Roy Margalit, Chung-Kil Hur, Ori Lahav | 17m |
Claims an in-order source semantics for C/C++ that preserves all common compiler optimizations for non-atomics by compiling to an out-of-order IR with… | ||
| Search-Based Regular Expression Inference on a GPU | Mojtaba Valizadeh, Martin Berger | 20m |
Enumerative RE inference runs as a cost-ordered search over languages encoded as contiguous matrix of bitvectors built from the infix-closure of the example… | ||
| An Automata-Based Framework for Verification and Bug Hunting in Quantum Circuits | Yu-Fang Chen, Kai-Min Chung, Ondřej Lengál, Jyun-Ao Lin, Wei-Lun Tsai, Di-De Yen | 18m |
Introduces an automata-based verification engine that encodes sets of quantum states as tree automata and implements gate semantics as automata transformers… | ||
| Feature-Sensitive Coverage for Conformance Testing of Programming Language Implementations | Jihyeok Park, Dongjun Youn, Kanguk Lee, Sukyoung Ryu | 19m |
Presents a new coverage refinement that distinguishes identical CFG nodes by their innermost language features and by feature-call paths (with k-limiting)… | ||
| Probabilistic Programming with Stochastic Probabilities | Alexander K. Lew, Matin Ghavamizadeh, Martin C. Rinard, Vikash K. Mansinghka | 20m |
Claims a compiler and runtime that let expressive probabilistic programs use noisy density estimates while preserving sound inference by design. It introduces… | ||
| CommCSL: Proving Information Flow Security for Concurrent Programs using Abstract(…) | Marco Eilers, Thibault Dardinier, Peter Müller | 21m |
Claims a verification method that proves non‑interference for concurrent programs without any timing assumptions by requiring commutativity of updates only on… | ||
| Synthesizing Quantum-Circuit Optimizers | Amanda Xu, Abtin Molavi, Lauren Pick, Swamit Tannu, Aws Albarghouthi | 24m |
Synthesizes a device-specific quantum-circuit optimizer from a gate-set spec in 1.2 minutes and outputs 7,001 symbolic rewrite rules for IBM’s gate set, giving… | ||
| Mostly Automated Proof Repair for Verified Libraries | Kiran Gopinathan, Mayank Keoliya, Ilya Sergey | 19m |
Tool Sisyphus takes an old Coq-verified OCaml function, a changed OCaml implementation, and emits a mostly-automated Coq proof by combining dynamic program… | ||
| Garbage-Collection Safety for Region-Based Type-Polymorphic Programs | Martin Elsman | 18m |
Region-inference plus polymorphism produces a real soundness hole that yields dangling pointers during reference-tracing (and generational) collection; the… | ||
| One Pixel Adversarial Attacks via Sketched Programs | Tom Yuviler, Dana Drachsler Cohen | 19m |
Claims a method called OPPSLA that synthesizes a sketch-based prioritization program to find one-pixel (or few-pixel) adversarial examples for CIFAR-10 and… | ||
| Repairing Regular Expressions for Extraction | Nariyoshi Chida, Tachio Terauchi | 17m |
A tool called R3 implements the first PBE-based synthesis and repair for extraction, supporting real-world extensions like backreferences and lookarounds. It… | ||
| Embedding Hindsight Reasoning in Separation Logic | Roland Meyer, Thomas Wies, Sebastian Wolff | 21m |
The work embeds hindsight reasoning into separation logic via a new proof rule called temporal interpolation, implemented in an automated tool that proves… | ||
| Proving and Disproving Equivalence of Functional Programming Assignments | Dragana Milovančević, Viktor Kuncak | 20m |
A tool implemented on top of the Stainless verifier automatically proves or disproves student Scala submissions by generating inductive equivalence proofs or… | ||
| Compound Memory Models | Andrés Goens, Soham Chakraborty, Susmit Sarkar, Sukarn Agarwal, Nicolai Oswald, Vijay Nagarajan | 16m |
Defines a compositional operational specification that composes distinct device models into a x86TSO/PTX compound model and proves C-to-architecture compiler… | ||
| Absynthe: Abstract Interpretation-Guided Synthesis | Sankha Narayan Guria, Jeffrey S. Foster, David Van Horn | 20m |
Framework uses user-defined abstract domains to prune families of candidate programs during enumerative search, infers abstract values for intermediate holes… | ||
| Lilac: A Modal Separation Logic for Conditional Probability | John M. Li, Amal Ahmed, Steven Holtzen | 19m |
Lilac presents a separation logic that models probability spaces as heap-like resources and defines an independent combination operator that interprets… | ||
| Conflict-Driven Synthesis for Layout Engines | Junrui Liu, Yanju Chen, Eric Atkinson, Yu Feng, Rastislav Bodík | 22m |
Medea synthesizes incremental layout engines from an attribute grammar specification plus a traversal sketch, using symbolic execution to produce concrete… | ||
| Iris-Wasm: Robust and Modular Verification of WebAssembly Programs | Xiaojia Rao, Aina Linn Georges, Maxime Legoupil, Conrad Watt, Jean Pichon-Pharabod, Philippa Gardner, Lars Birkedal | 16m |
Iris-Wasm mechanizes Wasm 1.0 in Coq on top of the Iris framework and claims modular, higher-order verification that composes across host boundaries. It builds… | ||
| nothing matches | ||