Formalization for Article "Deciding not to Decide: Sound and Complete Effect Inference in the Presence of Higher-Rank Polymorphism"

Zenodo (CERN European Organization for Nuclear Research) 2026 Open access

Read full text
Authors: Patrycja Balik, Szymon Jędras, Piotr Polesiuk
DOI: 10.5281/zenodo.18197463
Cited by: 0

Abstract

This is the Rocq formalization accompanying the paper “Deciding not to Decide: Sound and Complete Effect Inference in the Presence of Higher-Rank Polymorphism”. The archive eff-infer.tar.gz contains the sources and a README.md file, while eff-infer-docker-img.tar.gz is a Docker image that can be loaded and launched in a new container as follows. docker load -i eff-infer-docker-img.tar.gz docker run -it eff-infer

Publication details

Journal / source
Zenodo (CERN European Organization for Nuclear Research)
Publication date
9 January 2026
Language
EN