This project provides a soundness proof for a lambda calculus with an extrinsic concept, subtyping. The calculus is equipped with call-by-name structural operational semantics. The proof is formalized in Cubical Agda.
Features:
- The
Toptype - Record types