00:00:00 / 00:00:00
3 5

Graded modalities have been proposed in recent work on programming languages as a general framework for refining type systems with intensional properties. In particular, continuous endomaps of the discrete time scale, or time warps, can be used to quantify the growth of information in the course of program execution. Time warps form a complete residuated lattice, with the residuals playing an important role in potential programming applications. In this paper, we study the algebraic structure of time warps, and prove that their equational theory is decidable, a necessary condition for their use in real-world compilers. We also describe how our universal-algebraic proof technique lends itself to a constraint-based implementation, establishing a new link between universal algebra and verification technology.

Information about the video

Citation data

  • DOI 10.24350/CIRM.V.19828203
  • Cite this video Santschi, Simon (03/11/2021). Time warps, from algebra to algorithms. CIRM. Audiovisual resource. DOI: 10.24350/CIRM.V.19828203
  • URL https://dx.doi.org/10.24350/CIRM.V.19828203

Domain(s)

Bibliography

  • GUATTO, Adrien. A generalized modality for recursion. In : Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science. 2018. p. 482-491. - https://doi.org/10.1145/3209108.3209148
  • HOLLAND, W. Charles and McCLEARLY, Stephen H. Solvability of the Word Problem in Free Lattice-Ordered Groups. Houston Journal of Mathematics. 1979, vol. 5, no 1, p. 99-105. - https://www.math.uh.edu/~hjm/vol05-1.html
  • LÄUCHLI, H., and LEONARD, J.. On the elementary theory of linear order. Fundamenta Mathematicae 59.1 (1966): 109-116. - http://eudml.org/doc/213884
  • SANTOCANALE, Luigi. The involutive quantaloid of completely distributive lattices. Relational and Algebraic Methods in Computer Science, 2020, vol. 12062, p. 286-301. - https://arxiv.org/abs/1911.01085

Last related questions on MathOverflow

You have to connect your Carmin.tv account with mathoverflow to add question

Ask a question on MathOverflow




Register

  • Bookmark videos
  • Add videos to see later &
    keep your browsing history
  • Comment with the scientific
    community
  • Get notification updates
    for your favorite subjects
Give feedback