19th International Conference on Relational and Algebraic Methods in Computer Science / 19ème Conférence internationale de méthodes relationnelles et algébriques en informatique

Collection 19th International Conference on Relational and Algebraic Methods in Computer Science / 19ème Conférence internationale de méthodes relationnelles et algébriques en informatique

Organizer(s) Fahrenberg, Uli ; Gehrke, Mai ; Santocanale, Luigi ; Winter, Michael

Date(s) 02/11/2021 - 06/11/2021

linked URL https://conferences.cirm-math.fr/2398.html

00:00:00 / 00:00:00

3 5

Time warps, from algebra to algorithms

By Simon Santschi

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

Date of recording 03/11/2021
Date of publication 26/11/2021
Institution CIRM
Licence CC BY NC ND
Language English
Audience Researchers
Director(s) Luca Recanzone
Format MP4

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)

Logic

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

MSC codes

Document(s)

https://www.cirm-math.fr/RepOrga/2398/Slides/Santschi.pdf

Last related questions on MathOverflow

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

Ask a question on MathOverflow

All the collection videos

01:03:09

published on November 26, 2021

Relational tight field bounds for distributed analysis of programs

By Marcelo Frias

44:23

published on November 26, 2021

Quantified constraint satisfaction problem: towards the classification of complexity

By Dmitriy Zhuk

25:24

published on November 26, 2021

Time warps, from algebra to algorithms

By Simon Santschi

01:00:52

published on November 26, 2021

Fixpoint games

By Barbara König

29:45

published on November 26, 2021

Relational models for the Lambek calculus with intersection and unit

By Stepan Kuznetsov

Copyright Carmin.tv 2024

Give feedback