Intuitionistic Metric Temporal Logic

Luiz de Sá; Bernardo Toninho; Frank Pfenning

doi:10.1145/3610612.3610621

Intuitionistic Metric Temporal Logic

Luiz de Sá, Bernardo Toninho, Frank Pfenning

NOVALincs

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

1 Citation (Scopus)

25 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 language	English
Title of host publication	PPDP '23
Subtitle of host publication	Proceedings of the 25th International Symposium on Principles and Practice of Declarative Programming
Place of Publication	New York
Publisher	ACM - Association for Computing Machinery
Number of pages	13
ISBN (Print)	979-8-4007-0812-1
DOIs	https://doi.org/10.1145/3610612.3610621
Publication status	Published - 22 Oct 2023
Event	25th 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 2023 → 23 Oct 2023

Publication series

Name	PPDP: Principles and Practice of Declarative Programming
Publisher	ACM - Association for Computing Machinery

Conference

Conference	25th 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/Territory	Portugal
City	Lisbon
Period	22/10/23 → 23/10/23

Access to Document

10.1145/3610612.3610621Licence: CC BY

Intuitionistic Metric Temporal LogicFinal published version, 820 KBLicence: CC BY

Cite this

@inproceedings{19e59dd6eee042a6b9ce7b7f1ff2d356,

title = "Intuitionistic Metric Temporal Logic",

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.",

author = "S{\'a}, {Luiz de} and Bernardo Toninho and Frank Pfenning",

note = "Publisher Copyright: {\textcopyright} 2023 Owner/Author.; 25th 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 ; Conference date: 22-10-2023 Through 23-10-2023",

year = "2023",

month = oct,

day = "22",

doi = "10.1145/3610612.3610621",

language = "English",

isbn = "979-8-4007-0812-1",

series = "PPDP: Principles and Practice of Declarative Programming",

publisher = "ACM - Association for Computing Machinery",

booktitle = "PPDP '23",

address = "United States",

}

Sá, LD, Toninho, B & Pfenning, F 2023, Intuitionistic Metric Temporal Logic. in PPDP '23: Proceedings of the 25th International Symposium on Principles and Practice of Declarative Programming., 9, PPDP: Principles and Practice of Declarative Programming, ACM - Association for Computing Machinery, New York, 25th 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, 22/10/23. https://doi.org/10.1145/3610612.3610621

Intuitionistic Metric Temporal Logic. / Sá, Luiz de; Toninho, Bernardo; Pfenning, Frank.
PPDP '23: Proceedings of the 25th International Symposium on Principles and Practice of Declarative Programming. New York: ACM - Association for Computing Machinery, 2023. 9 (PPDP: Principles and Practice of Declarative Programming).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Intuitionistic Metric Temporal Logic

AU - Sá, Luiz de

AU - Toninho, Bernardo

AU - Pfenning, Frank

PY - 2023/10/22

Y1 - 2023/10/22

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=85175491056&partnerID=8YFLogxK

U2 - 10.1145/3610612.3610621

DO - 10.1145/3610612.3610621

M3 - Conference contribution

AN - SCOPUS:85175491056

SN - 979-8-4007-0812-1

T3 - PPDP: Principles and Practice of Declarative Programming

BT - PPDP '23

PB - ACM - Association for Computing Machinery

CY - New York

T2 - 25th 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

Y2 - 22 October 2023 through 23 October 2023

ER -

Intuitionistic Metric Temporal Logic

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this