![]() |
![]() |
University of Birmingham > Talks@bham > Theoretical computer science seminar > Temporal Refinements for Guarded Recursive Types
Temporal Refinements for Guarded Recursive TypesAdd to your list(s) Download to your calendar using vCal
If you have a question about this talk, please contact George Kaye. Zoom details
Abstract We propose a logic for temporal properties of higher-order programs that handle infinite objects like streams or infinite trees, rep- resented via coinductive types. Specifications of programs use safety and liveness properties. Programs can then be proven to satisfy their specifi- cation in a compositional way, our logic being based on a type system. The logic is presented as a refinement type system over the guarded λ-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. j.w.w. Guilhem Jaber. This talk is part of the Theoretical computer science seminar series. This talk is included in these lists:
Note that ex-directory lists are not shown. |
Other listsContemporary History EPS - College Research Teas Type the title of a new list hereOther talksTBA Ultrafast Spectroscopy and Microscopy as probes of Energy Materials The tragic destiny of Mileva Marić Einstein TBA Life : it’s out there, but what and why ? TBC |