Search

• < Previous
• 1
• Next >

---

A Step-indexed Semantics of Imperative Objects

Catalin Hritcu ; Jan Schwinghammer.

Step-indexed semantic interpretations of types were proposed as an alternative to purely syntactic proofs of type safety using subject reduction. The types are interpreted as sets of values indexed by the number of computation steps for which these values are guaranteed to behave like proper&nbsp;[&hellip;]

---

Step-Indexed Relational Reasoning for Countable Nondeterminism

Lars Birkedal ; Aleš Bizjak ; Jan Schwinghammer.

Programming languages with countable nondeterministic choice are computationally interesting since countable nondeterminism arises when modeling fairness for concurrent systems. Because countable choice introduces non-continuous behaviour, it is well-known that developing semantic models for&nbsp;[&hellip;]

---

Nested Hoare Triples and Frame Rules for Higher-order Store

Jan Schwinghammer ; Lars Birkedal ; Bernhard Reus ; Hongseok Yang.

Separation logic is a Hoare-style logic for reasoning about programs with heap-allocated mutable data structures. As a step toward extending separation logic to high-level languages with ML-style general (higher-order) storage, we investigate the compatibility of nested Hoare triples with several&nbsp;[&hellip;]

---

First steps in synthetic guarded domain theory: step-indexing in the topos of trees

Lars Birkedal ; Rasmus Ejlers Møgelberg ; Jan Schwinghammer ; Kristian Støvring.

We present the topos S of trees as a model of guarded recursion. We study the internal dependently-typed higher-order logic of S and show that S models two modal operators, on predicates and types, which serve as guards in recursive definitions of terms, predicates, and types. In particular, we show&nbsp;[&hellip;]

---