Discussion: LTL types FRP
Today we'll discuss LTL types FRP: Linear-time Temporal Logic Propositions as Types Proofs as Functional Reactive Programs by Alan Jeffrey.
Add your questions or comments about here.
From section 2.3, what does it mean
"LTL is usually presented as a classical logic, in which there are derived modalities"?
Specifically, what does it mean to present one form of logic as another and how does that give rise to derived modalities?
It also confuses me how the derivations for reactive types expressed in classical logic uses new connectives. For instance, the modality for Future A requires Until, which isn't given a derivation.
I am confused about the interpretation of implication in 2.3.
Has there been any work looking at other temporal logics (e.g. CTL) and how they correspond to functional (reactive?) programming?