Mechanizing proofs with logical relations - Kripke-style

Cave, A; Pientka, B

Cave, A (reprint author), McGill Univ, Sch Comp Sci, Montreal, PQ, Canada.

MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE, 2018; 28 (9): 1606

Abstract

Proofs with logical relations play a key role to establish rich properties such as normalization or contextual equivalence. They are also challenging ......

Full Text Link