Temporal Refinements for Guarded Recursive Types (full version)

We propose a logic to reason on temporal properties of higher-order programs that handle infinite objects like streams or infinite trees, represented via coinductive types. Specifications of programs are defined using safety and liveness properties. A given program can then be proven to satisfy its specification, in a compositional way, our logic being based on a type system.The logic is presented as a refinement type system over the guarded lambda-calculus, a λ-calculus with guarded recursive types. The refinements are formulae of a modal μ-calculus which embeds usual temporal modal logics such as LTL and CTL.The semantics of our system is given within a rich structure, the topos of trees, in which we build a realizability model of the temporal refinement type system. We use in a crucial way the connection with set-theoretic semantics to handle liveness properties