Conference item

### 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
Host title:
25TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS 2010)
Publication date:
2010-01-01
DOI:
ISSN:
1043-6871
Source identifiers:
328281
ISBN:
9780769541143
Pubs id:
pubs:328281
UUID:
uuid:ca0a84ee-b355-4108-943b-429df16d11b6
Local pid:
pubs:328281
Deposit date:
2012-12-19