Skip to main content
3 of 5
added 363 characters in body
Dave Clarke
  • 16.7k
  • 3
  • 61
  • 106

I know of work adding temporal modalities to linear logic. This is quite interesting: a formula (without a modality) is interpreted as resources being available now. The next time modality ($\circ$) is interpreted as resources being available in the next time step. The box modality $\Box$ means that the resources can be consumed at any point in the future, determined by the holder of the resources, whereas $\diamond$ means that the resources can be consumed at any point in time determined by the system. Notice the duality.

There are a few papers adding all sorts of modalities to linear and affine logic:

The work on temporal linear logic has been applied in agent-oriented programming and coordination, making essential use of the interpretation of the modalities described above:

Dave Clarke
  • 16.7k
  • 3
  • 61
  • 106