plutus-cert

Translation certification of Plutus compiler passes in Coq.

Status

Work in progress

Reading

• Translation Certification for Smart Contracts (Krijnen, J.O.G, Chakravarty, M.M., Keller, G. and Swierstra, W., FLOPS 2022): Translation relations for certifying Plutus compilations
• Verified Compiler Optimisations (Joris Dral, 2022 MSc thesis): Using step-indexed logical relations for verifying translation relations
• Automatically Deriving Checkers for Compilation Verification (Bart Remmers, 2023 MSc thesis): Generating decision procedures for translation relations