Step-indexed kripke models over recursive worlds

Birkedal, Lars, Reus, Bernhard, Schwinghammer, Jan, Stovring, Kristian, Thamsborg, Jacob and Yang, Hongseok (2011) Step-indexed kripke models over recursive worlds. In: Thomas, B and Mooly, S (eds.) POPL '11 Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages. ACM, pp. 119-132. ISBN 978-1-4503-0490-0

[img] PDF
Restricted to SRO admin only

Download (739kB)

Abstract

Over the last decade, there has been extensive research on modelling challenging features in programming languages and program logics, such as higher-order store and storable resource invariants. A recent line of work has identified a common solution to some of these challenges: Kripke models over worlds that are recursively defined in a category of metric spaces. In this paper, we broaden the scope of this technique from the original domain-theoretic setting to an elementary, operational one based on step indexing. The resulting method is widely applicable and leads to simple, succinct models of complicated language features, as we demonstrate in our semantics of Charguraud and Pottier's type-and-capability system for an ML-like higher-order language. Moreover, the method provides a high-level understanding of the essence of recent approaches based on step indexing.

Item Type: Book Section
Additional Information: DOI: 10.1145/1926385.1926401
Schools and Departments: School of Engineering and Informatics > Informatics
Depositing User: Bernhard Reus
Date Deposited: 06 Feb 2012 21:07
Last Modified: 13 Nov 2013 15:23
URI: http://sro.sussex.ac.uk/id/eprint/29613

View download statistics for this item

📧 Request an update