The coq-uplc library provides a Coq-based implementation of the Cardano CEK machine—the virtual
machine responsible for evaluating UPLC programs (validators), which serve as the on-chain
components of Cardano smart contracts.
The implementation of the library is funded by Project Catalyst.
- Catalyst page: https://milestones.projectcatalyst.io/projects/1200028
- Codebase: https://github.com/Anastasia-Labs/coq-uplc
- Completion video for milestone 1: https://www.youtube.com/watch?v=srEPiyU8jQI