A Relational Modal Logic for Higher-Order Stateful ADTs

The method of logical relations is a classic technique for proving the equivalence of higher-order programs that implement the same observable behavior but employ different internal data representations. Although it was originally studied for pure, strongly normalizing languages like System F, it has been extended over the past two decades to reason about increasingly realistic languages. In particular, Appel and McAllester's idea of step-indexing has been used recently to develop syntactic Kripke logical relations for MLlike languages that mix functional and imperative forms of data abstraction. However, while step-indexed models are powerful tools, reasoning with them directly is quite painful, as one is forced to engage in tedious step-index arithmetic to derive even simple results. In this paper, we propose a logic LADR for equational reasoning about higher-order programs in the presence of existential type abstraction, general recursive types, and higher-order mutable state....

• Type: Conference
• Year: 2010
• Where: POPL
• Authors: Derek Dreyer, Georg Neis, Andreas Rossberg, Lars Birkedal
• Keywords: Kripke Logical Relations, Modal Logic, POPL 2010, Programming Languages, Relational Separation Logic