Computer Science on Cambridge Core4/8/2026

A practical formalization of monadic equational reasoning in dependent-type theory