Intuitionistic Metric Temporal Logic

Luiz de Sá, Bernardo Toninho, Frank Pfenning

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

16 Downloads (Pure)

Abstract

We develop Intuitionistic Metric Temporal Logic (IMTL) that extends prior work on intuitionistic temporal logics in two ways: (1) it generalizes discrete time to dense time with intervals so it can, for example, express the duration of signals, and (2) every proof corresponds to a temporal computation. Our main technical result is a syntactic proof of cut elimination for IMTL, which entails logical consistency and ensures that every proof executes while respecting the flow of time. Cut reductions in IMTL correspond to temporal interactions, although we do not fully develop a programming language in this paper. Beyond the metatheory of IMTL, we illustrate the computational meaning of IMTL proofs by developing examples and a small case study where we apply IMTL to well-timed digital circuit design.
Original languageEnglish
Title of host publicationPPDP '23
Subtitle of host publicationProceedings of the 25th International Symposium on Principles and Practice of Declarative Programming
Place of PublicationNew York
PublisherACM - Association for Computing Machinery
Number of pages13
ISBN (Print)979-8-4007-0812-1
DOIs
Publication statusPublished - 22 Oct 2023
Event25th International Symposium on Principles and Practice of Declarative Programming, PPDP 2023 - As part of the ACM SIGPLAN conference on Systems, Programming, Languages, and Applications: Software for Humanity, SPLASH 2023, including LOPSTR 2023 - Lisbon, Portugal
Duration: 22 Oct 202323 Oct 2023

Publication series

NamePPDP: Principles and Practice of Declarative Programming
PublisherACM - Association for Computing Machinery

Conference

Conference25th International Symposium on Principles and Practice of Declarative Programming, PPDP 2023 - As part of the ACM SIGPLAN conference on Systems, Programming, Languages, and Applications: Software for Humanity, SPLASH 2023, including LOPSTR 2023
Country/TerritoryPortugal
CityLisbon
Period22/10/2323/10/23

Fingerprint

Dive into the research topics of 'Intuitionistic Metric Temporal Logic'. Together they form a unique fingerprint.

Cite this