Typed Operational Semantics for Dependent Record Types

Yangyue Feng, Zhaohui Luo

Typed operational semantics is a method developed by H. Goguen to prove meta-theoretic properties of type systems. This paper studies the metatheory of a type system with dependent…