Sciweavers

Share
POPL
2010
ACM

A Relational Modal Logic for Higher-Order Stateful ADTs

9 years 8 months ago
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....
Derek Dreyer, Georg Neis, Andreas Rossberg, Lars B
Added 01 Mar 2010
Updated 02 Mar 2010
Type Conference
Year 2010
Where POPL
Authors Derek Dreyer, Georg Neis, Andreas Rossberg, Lars Birkedal
Comments (0)
books