ICFP 2021
Sun 22 - Sat 28 August 2021
Thu 26 Aug 2021 19:00 - 19:30 at ML - Semantics & Verification Chair(s): Martin Elsman

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 Aug

Displayed time zone: Seoul change

18:00 - 19:30
Semantics & VerificationML at ML
Chair(s): Martin Elsman University of Copenhagen, Denmark
18:00
30m
Talk
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
30m
Talk
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
30m
Talk
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