79 citations · 126 across the 4 of their papers we have counts for
4 papers
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. Be…
First steps in synthetic guarded domain theory: step-indexing in the topos of trees
Lars Birkedal, Rasmus Ejlers Møgelberg, Jan Schwinghammer +1
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 pred…
Nested Hoare Triples and Frame Rules for Higher-order Store
Jan Schwinghammer, Lars Birkedal, Bernhard Reus +1
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 language…
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…