A terminating type checker for the smart contract language Plutus in Rocq
Publication date
Authors
DOI
Document Type
Master Thesis
Metadata
Show full item recordCollections
License
CC-BY-NC-ND
Abstract
Using the Rocq proof assistant, Krijnen et al. prove semantic equivalence for compiler passes of the smart contract language Plutus, assuming that input programs are well-typed. Bugs in the compiler's type checker, dumping mechanism, or pretty-printing algorithms can invalidate this assumption.
This assumption is unnecessary: we decide type correctness within Rocq by implementing a sound and complete terminating type checker. Type-level computation requires proving strong normalization of the type language, which uses a named variable representation. We reason up to alpha-equivalence and present an embedding technique that lifts the strong normalization argument to richer languages.
Keywords
type checker; typechecker; Plutus; smart contract; proof verification; program verification; Rocq; Coq; Proof assistant; formal verification; System F; type system; progress and preservation; soundness; completeness; type safety; Plutus Intermediate Representation; verifying blockchains; Strong normalization; named representation; alpha equivalence; normalization; kind system; non-deterministic reduction relation; terminating normalizer; termination proof; dependent types; Plutus type checker; translation certification; compiler verification; verified type checker; verified compiler