Cargando…
Temporal Refinements for Guarded Recursive Types
We propose a logic for temporal properties of higher-order programs that handle infinite objects like streams or infinite trees, represented via coinductive types. Specifications of programs use safety and liveness properties. Programs can then be proven to satisfy their specification in a compositi...
| Autores principales: | , |
|---|---|
| Formato: | Online Artículo Texto |
| Lenguaje: | English |
| Publicado: |
2021
|
| Materias: | |
| Acceso en línea: | https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7984570/ http://dx.doi.org/10.1007/978-3-030-72019-3_20 |