A Temporal Logic for Higher-Order Functional Programs

Abstract

We propose an extension of linear temporal logic that we call Linear Temporal Logic of Calls (LTLC) for describing temporal properties of higher-order functions, such as “the function calls its first argument before any call of the second argument.” A distinguishing feature of LTLC is a new modal operator, the call modality, that checks if the function specified by the operator is called in the current step and, if so, describes how the arguments are used in the subsequent computation. We demonstrate expressiveness of the logic, by giving examples of LTLC formulas describing interesting properties. Despite its high expressiveness, the model checking problem is decidable for deterministic programs with finite base types.