Interesting paper, I happened to do something very similar for my master's thesis around a decade ago. I did not prove the soundness of the type system due to lack of time but had the feeling that should not be a major obstacle, probably in my naivete.

I skimmed through this thing and found no way to define clocked feedback circuits. This was something I was conceptually struggling with that at the time. The pipelined combination of timing definitions seems straightforward enough as its just adding integers together. Maybe someone who is actually up to date can correct me or provide some more info.

Interesting but this paper is very poorly named.

Interesting but a bit limited. It assumes you entire design is clocked from the same clock, and doesn't seem to allow you to account for the fact that some buses might be long enough to require their inputs to be ready in <1 clock period.