A terminating type checker for the smart contract language Plutus in Rocq

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.