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

Autor: Lars Birkedal, Rasmus Ejlers Møgelberg, Jan Schwinghammer, Kristian Støvring

Publikováno v: Logical Methods in Computer Science, Vol Volume 8, Issue 4 (2012)

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 te

Externí odkaz: https://doaj.org/article/5bc5287ee86c491ca6b70f696b4b6227

The category-theoretic solution of recursive metric-space equations

Autor: Jacob Thamsborg, Kristian Støvring, Lars Birkedal

Publikováno v: Theoretical Computer Science. 411(47):4102-4122

It is well known that one can use an adaptation of the inverse-limit construction to solve recursive equations in the category of complete ultrametric spaces. We show that this construction generalizes to a large class of categories with metric-space

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::57ba21e375b0a0160afc847b9cb585a6

A step-indexed Kripke Model of Hidden State

Autor: Kristian Støvring, François Pottier, Hongseok Yang, Lars Birkedal, Bernhard Reus, Jan Schwinghammer

Publikováno v: Mathematical Structures in Computer Science
Mathematical Structures in Computer Science, Cambridge University Press (CUP), 2013, 23 (1), pp.1--54
Mathematical Structures in Computer Science, 2013, 23 (1), pp.1--54

Frame and anti-frame rules have been proposed as proof rules for modular reasoning about programs. Frame rules allow the hiding of irrelevant parts of the state during verification, whereas the anti-frame rule allows the hiding of local state from th

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::9acf64bd5d93c8ef19c0cd3892d94344
https://hal.inria.fr/hal-00772757/document

A Step-Indexed Kripke Model of Hidden State via Recursive Properties on Recursively Defined Metric Spaces

Autor: Kristian Støvring, Lars Birkedal, Jan Schwinghammer

Publikováno v: Foundations of Software Science and Computational Structures ISBN: 9783642198045
FoSSaCS

Frame and anti-frame rules have been proposed as proof rules for modular reasoning about programs. Frame rules allow one to hide irrelevant parts of the state during verification, whereas the anti-frame rule allows one to hide local state from the co

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::1dfb790e9a6dec1bc92f161290430da8
https://doi.org/10.1007/978-3-642-19805-2_21

A Complete, Co-inductive Syntactic Theory of Sequential Control and State

Autor: Kristian Støvring, Soren Lassen

Publikováno v: Semantics and Algebraic Specification ISBN: 9783642041631
Semantics and Algebraic Specification

We present a co-inductive syntactic theory, eager normal form bisimilarity, for the untyped call-by-value lambda calculus extended with continuations and mutable references. We demonstrate that the associated bisimulation proof principle is easy to u

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::4c448d0a6d9c3dcc29b7f4034834068d
https://doi.org/10.1007/978-3-642-04164-8_17