Cube is an experimental interactive theorem prover for the formalization of constructive mathematics as developed in the informal cubically-flavored style advocated by Bentzen [1]. It implements a version of the cubical type theory with reflection-free extensional equality proposed by Sterling, Angiuli, and Gratzer [2][3], facilitating formalization with proof irrelevance while maintaining core cubical features.
To install and use Cube, you need OCaml version 4.14.2 or greater. We also recommend relying on the opam package manager for installation. You will also need menhir for the LR(1) parser generator, and dune for building the project. Both can be installed using opam. It is best to ensure that your opam is up-to-date before installing the dependencies:
$ opam update && opam upgrade
$ opam install menhir dune base
Next, clone the repository and build the project using dune:
$ git clone https://github.com/bbentzen/cube.git
$ cd cube
$ dune build
This will create the executable main.exe which you can run on any .cube file to typecheck its contents with Cube. Since this compiled executable is typically be found under a subfolder such as _build/default/bin, you can run it as follows:
$ dune exec _build/default/bin/main.exe <filename>.cube
However, we recommend using the cube-vscode extension for verification support. More information can be found at cube-vscode/README.md.
Please see the reference manual on doc/README.md.
This work was partly supported by the US Air Force Office of Scientific Research (AFOSR) grant FA9550-18-1-0120. Any opinions, findings and conclusions, or recommendations expressed in this material are those of the author and do not necessarily reflect the views of the AFOSR.
[1] Bruno Bentzen. Naive cubical type theory. Mathematical Structures in Computer Science, 31, pp. 1205–1231, 2021. doi:10.1017/S096012952200007X, arXiv:1911.05844.
[2] Jonathan Sterling, Carlo Angiuli, Daniel Gratzer. Cubical syntax for reflection-free extensional equality. In Herman Geuvers (ed.), 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019), volume 131 of Leibniz International Proceedings in Informatics (LIPIcs), pages 31:1-31:25. doi:10.4230/LIPIcs.FSCD.2019.31, arXiv:1904.08562.
[3] Jonathan Sterling, Carlo Angiuli, Daniel Gratzer. A Cubical Language for Bishop Sets. Logical Methods in Computer Science, 18 (1), 2022. doi:10.46298/lmcs-18(1:43)2022, arXiv:2003.01491.