A Step-indexed Kripke Model of Hidden State
(pdf)
Jan Schwinghammer, Lars Birkedal, François Pottier, Bernhard Reus, Kristian Støvring, Hongseok Yang
Mathematical Structures in Computer Science
Nested Hoare Triples and Frame Rules for Higher-order Store
Jan Schwinghammer, Lars Birkedal, Bernhard Reus, Hongseok Yang
Logical Methods in Computer Science
Step-indexed Kripke Models over Recursive Worlds
(pdf)
Lars Birkedal, Bernhard Reus, Jan Schwinghammer, Kristian Støvring, Jacob Thamsborg, Hongseok Yang
Principles of Programming Languages (POPL'11)
A Semantic Foundation for Hidden State
(pdf)
Jan Schwinghammer, Hongseok Yang, Lars Birkedal, François Pottier, Bernhard Reus
Foundations of Software Science and Computation Structures (FOSSACS 2010)
Nested Hoare Triples and Frame Rules for Higher-Order Store
(pdf)
Jan Schwinghammer, Lars Birkedal, Bernhard Reus, Hongseok Yang
Computer Science Logic (CSL'09)
A Simple Model of Separation Logic for Higher-order Store
(pdf)
Lars Birkedal, Bernhard Reus, Jan Schwinghammer, Hongseok Yang
Int. Conference Automata Logic and Programming (ICALP'08)