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.