[Agda] LTL Types FRP: Linear-time Temporal Logic Propositions as Types, Proofs as Functional Reactive Programs

[Peter Hancock]

On 10/11/2011 15:17, Alan Jeffrey wrote:

> LTL Types FRP: Linear-time Temporal Logic Propositions as Types,

This seems very interesting.  I've looked a bit through it.

Do you have any sense of what would happen if you dropped the "O" (next state)
modality from LTL? Would that be a disaster?

There are fragments of LTL which are "invariant under stuttering": Lamport is
very insistent on the importance of this notion.
http://research.microsoft.com/en-us/um/people/lamport/pubs/pubs.html
Have you encountered anything bearing on this?

Hank