2 papers
cs.PL2026
Logical Relations for Session-Typed Concurrency
Stephanie Balzer, Farzaneh Derakhshan, Robert Harper +1
Program equivalence is the fulcrum for reasoning about and proving properties of programs. For noninterference, for example, program equivalence up to the secrecy level of an obser…
cs.PL2025
Mechanizing Synthetic Tait Computability in Istari
Runming Li, Yue Yao, Robert Harper
Categorical gluing is a powerful technique for proving meta-theorems of type theories such as canonicity and normalization. Synthetic Tait Computability (STC) provides an abstract…