Conference

Recursion Schemes and Logical Reflection

Abstract:

Let ℛ be a class of generators of node-labelled infinite trees, and ℒ be a logical language for describing correctness properties of these trees. Given R ∈ R and φ ∈ ℒ, we say that Rφ is a φ-reflection of R just if (i) R and Rφ generate the same underlying tree, and (ii) suppose a node u of the tree [R] generated by R has label f, then the label of the node u of [Rφ] is f if u in [R] satisfies φ; it is f otherwise. Thus if [R] is the computation tree of a program R, we may regard Rφ as a tran...

Publication status:
Published

Access Document

Publisher copy:
10.1109/LICS.2010.40

Authors

Pages:
120-129
Publication date:
2010-01-01
DOI:
ISSN:
1043-6871
URN:
uuid:ca0a84ee-b355-4108-943b-429df16d11b6
Source identifiers:
328281
Local pid:
pubs:328281
ISBN:
9780769541143