The Geometry of Types (Long Version)
Ugo Dal Lago, Barbara Petit

TL;DR
This paper introduces an efficient method for analyzing the time complexity of higher-order functional programs by translating the problem into first-order inequalities, enabling automated verification with promising initial results.
Contribution
It presents a novel inference algorithm for linear dependent types that simplifies complexity analysis to first-order inequality verification, ensuring accuracy and facilitating automation.
Findings
Algorithm produces valid type judgments iff proof obligations are valid
Method simplifies complexity analysis to first-order inequalities
Initial experiments show promising results
Abstract
We show that time complexity analysis of higher-order functional programs can be effectively reduced to an arguably simpler (although computationally equivalent) verification problem, namely checking first-order inequalities for validity. This is done by giving an efficient inference algorithm for linear dependent types which, given a PCF term, produces in output both a linear dependent type and a cost expression for the term, together with a set of proof obligations. Actually, the output type judgement is derivable iff all proof obligations are valid. This, coupled with the already known relative completeness of linear dependent types, ensures that no information is lost, i.e., that there are no false positives or negatives. Moreover, the procedure reflects the difficulty of the original problem: simple PCF terms give rise to sets of proof obligations which are easy to solve. The…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Real-Time Systems Scheduling · Parallel Computing and Optimization Techniques
