![]() |
![]() |
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 listsSchool of Metallurgy and Materials Colloquia Theoretical Physics Journal Club and Group Meeting 'Roles' Postgraduate Gender and Sexuality Network DiscussionOther talksTest talk Geometry of alternating projections in metric spaces with bounded curvature Sylow branching coefficients for symmetric groups TBC Extending the Lax type operator for finite W-algebras Modelling uncertainty in image analysis. |