ICFP 2021 (series) / ML 2021 (series) / ML 2021 /
Hobbit: A Tool for Contextual Equivalence Checking Using Bisimulation Up-to Techniques
We present a bounded equivalence verification tool called Hobbit for higher-order programs with local state—based on a subset of OCaml—that combines fully abstract symbolic environmental bisimulations, novel up-to techniques, and lightweight invariant annotations. The tool reports no false positives or negatives, can automatically detect all inequivalences, and is able to automatically or semi-automatically prove many equivalences, including all classical Meyer and Sieber equivalences.
presentation_slides (presentation.pdf) | 938KiB |
extended_abstract (main.pdf) | 303KiB |
Thu 26 AugDisplayed time zone: Seoul change
Thu 26 Aug
Displayed time zone: Seoul change
18:00 - 19:30 | |||
18:00 30mTalk | Composing UNIX with Effect Handlers: A Case Study in Effect Handler Oriented Programming ML Daniel Hillerström The University of Edinburgh Pre-print Media Attached | ||
18:30 30mTalk | Cameleer: a Deductive Verification Tool for OCaml ML Mário Pereira NOVA LINCS & DI -- Nova School of Science and Technology, António Ravara Department of Informatics, Faculty of Sciences and Technology, NOVA University of Lisbon and NOVA LINCS File Attached | ||
19:00 30mTalk | Hobbit: A Tool for Contextual Equivalence Checking Using Bisimulation Up-to Techniques ML Vasileios Koutavas Trinity College Dublin, Yu-Yang Lin Trinity College Dublin, Nikos Tzevelekos Queen Mary University of London File Attached |