File(s) under permanent embargo
Step-indexed kripke models over recursive worlds
chapter
posted on 2023-06-08, 08:51 authored by Lars Birkedal, Bernhard ReusBernhard Reus, Jan Schwinghammer, Kristian Stovring, Jacob Thamsborg, Hongseok YangOver 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.
History
Publication status
- Published
Publisher
ACMPublisher URL
Volume
38Page range
119-132Pages
11.0Event name
Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languagesEvent location
Austin (Texas)Event type
conferenceBook title
POPL '11 Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languagesISBN
978-1-4503-0490-0Department affiliated with
- Informatics Publications
Notes
DOI: 10.1145/1926385.1926401Full text available
- No
Peer reviewed?
- Yes
Editors
S Mooly, B ThomasLegacy Posted Date
2012-02-06Usage metrics
Categories
No categories selectedKeywords
Licence
Exports
RefWorks
BibTeX
Ref. manager
Endnote
DataCite
NLM
DC