Mica: Automated Differential Testing for OCaml Modulesin-person
This program is tentative and subject to change.
Suppose we are given two OCaml modules implementing the same signature. How do we check that they are observationally equivalent—that is, that they behave the same on all inputs? One established technique is to use a property-based testing (PBT) tool such as QuickCheck. Currently, however, this can require significant amounts of boilerplate code and ad-hoc test harnesses.
To address this issue, We present Mica, an automated tool for testing observational equivalence of OCaml modules. Mica is implemented as a PPX compiler extension, allowing users to supply minimal annotations to a module signature. These annotations guide Mica to automatically derive specialized PBT code that checks observational equivalence. We discuss the design of Mica and demonstrate its efficacy as a testing tool on various modules taken from real-world OCaml libraries.
Paper (ocaml2024-final8.pdf) | 528KiB |
This program is tentative and subject to change.
Sat 7 SepDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
11:00 - 12:30 | |||
11:00 22mTalk | Structured diagnostics for the OCaml compilerin-person OCaml Florian Angeletti Inria Pre-print File Attached | ||
11:22 22mTalk | Project-wide occurrences for OCaml, a progress reportin-person OCaml Ulysse Gérard Tarides Pre-print File Attached | ||
11:45 22mTalk | Mica: Automated Differential Testing for OCaml Modulesin-person OCaml Ernest Ng Cornell University, Harrison Goldstein University of Pennsylvania, Benjamin C. Pierce University of Pennsylvania Pre-print File Attached | ||
12:07 22mTalk | First-Class Windows: Building a Roadmap for OCaml on Windowsin-person OCaml Pre-print File Attached |