Propositional quantifiers for intuitionistic logic mechanized in Coq.

This is an old version (published in CPP 2023), which is no longer maintained, but kept online for archival purposes. The next version of the project (published in IJCAR 2024) is here: https://hferee.github.io/UIML/demo.html.

Table of Contents

Source code

Accompanying paper (pre-print of the paper published in CPP 2023)