Mechanizing proofs with logical relations – Kripke-style

Proofs with logical relations play a key role to establish rich properties such as normalization or contextual equivalence. They are also challenging to mechanize. In this paper, we describe two case studies using the proof environment Beluga : First, we explain the mechanization of the weak normali...

Full description

Bibliographic Details
Published in:Mathematical Structures in Computer Science
Main Authors: CAVE, ANDREW, PIENTKA, BRIGITTE
Format: Article in Journal/Newspaper
Language:English
Published: Cambridge University Press (CUP) 2018
Subjects:
Computer Science Applications
Mathematics (miscellaneous)
Lambda
Beluga
Beluga*
Online Access:http://dx.doi.org/10.1017/s0960129518000154
https://www.cambridge.org/core/services/aop-cambridge-core/content/view/S0960129518000154

Similar Items