Loading...
Please wait, while we are loading the content...
Similar Documents
Temporal Refinements for Guarded Recursive Types
| Content Provider | Semantic Scholar |
|---|---|
| Author | Jaber, Guilhem Riba, Colin |
| Copyright Year | 2020 |
| Abstract | We propose a framework to reason on temporal properties of higher-order programs with coinductive types. It extends guarded recursive types with temporal refinements, which are formulae of the modal μ-calculus. Its semantics is given inside the topos of trees, and corresponds to the standard semantics for safety properties (defined as greatest fixpoints). For more general properties involving least fixpoints, we accommodate an external semantics, whose interaction with the internal one is regulated when restricting to the flat μcalculus, in which fixpoints can be computed by iteration over N, and thus can be unfolded syntactically. |
| File Format | PDF HTM / HTML |
| Alternate Webpage(s) | http://perso.ens-lyon.fr/colin.riba/papers/reftrees.pdf |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |
