Last change
on this file was
2394,
checked in by campbell, 7 years ago

I've kept the odd note on bits of CerCo? work I've been doing. James suggested
that it might be useful if these were recorded in the repository just in case
they contain some useful information that doesn't get recorded elsewhere.

File size:
970 bytes

Line  

1  The idea was to flatten the structured traces and show that these are the same 

2  as the original trace. This looks like it could work out OK, but with the 

3  caveats that: 

4  

5  1. flattening is a notquite trivial operations  we need to define a type 

6  of finite flat traces to get out of the finite structured traces, get the 

7  executable parts from Prop into Type[0] using their executability, then 

8  define a careful pair of mutual cofixpoints to satisfy the guardedness 

9  conditions; 

10  

11  2. we can't show the usual equality on coinductive data, so we need to define 

12  a specialised coinductive equality predicate for flat traces; and 

13  

14  3. define a cofixpoint proof for that tediously going through all of the 

15  structure I defined at 1 (this is the point that I'm at). 

16  

17  After all of this, we get a corrollary saying the the flattened result of 

18  making a structured trace must be the same as the original trace because all 

19  traces from the same place are. 

Note: See
TracBrowser
for help on using the repository browser.