This is the Coq formalization of the core calculus for oblivious algebraic data types.
- coq (8.18)
- coq-stdpp (>= 1.9.0)
- coq-smpl (>= 8.18)
- coq-hammer-tactics (>= 1.3.2)
- coq-idt (>= 1.1)
See coq-oadt.opam for more details.
The easiest way to install the dependencies and build the project is via OPAM.
opam repo add coq-released https://coq.inria.fr/opam/released
opam update
cd path/to/oadt
opam install . --deps-onlyRun make in the top-level directory.
- Qianchuan Ye and Benjamin Delaware. 2022. Oblivious Algebraic Data Types. Proc. ACM Program. Lang. 6, POPL, Article 51 (January 2022), 29 pages. https://doi.org/10.1145/3498713
- Qianchuan Ye and Benjamin Delaware. 2021. Oblivious Algebraic Data Types: POPL22 Artifact. Zenodo. https://doi.org/10.5281/zenodo.5652106
- Qianchuan Ye and Benjamin Delaware. 2023. Taype: A Policy-Agnostic Language for Oblivious Computation. Proc. ACM Program. Lang. 7, PLDI, Article 147 (June 2023), 25 pages. https://doi.org/10.1145/3591261
- Qianchuan Ye and Benjamin Delaware. 2023. Taype: A Policy-Agnostic Language for Oblivious Computation: PLDI23 Artifact. Zenodo. https://doi.org/10.5281/zenodo.7806981