The geometry of types

DOI10.1145/2429069.2429090MaRDI QIDQ2931793zbMATH OpenOpenAlexFDO

Authors Ugo Dal Lago, Barbara Petit

Publication date 27 November 2014

Published in Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1210.6857

zbMATH Keywords

complexity analysisfunctional programminghigher-order typeslinear logicresource consumption

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Analysis of algorithms and problem complexity (68Q25) Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65)

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 latter can then be put in a format suitable for automatic or semi-automatic verification by external solvers. Ongoing experimental evaluation has produced encouraging results, which are briefly presented in the paper.

Recommendations

• scientific article; zbMATH DE number 177794
• Implementation of Functional Languages
• Linear dependent types in a call-by-value scenario
• Linear dependent types and relative completeness
• Complexity analysis in presence of control operators and higher-order functions

Cited in

(15)

• Combining linear logic and size types for implicit complexity
• Implicit computational complexity of subrecursive definitions and applications to cryptographic proofs
• Linear dependent types in a call-by-value scenario
• Implementing Euclid's straightedge and compass constructions in type theory
• Context dependent procedures and computed types in \texttt{VeriFun}
• Types et contragrédientes
• Linear dependent types and relative completeness
• Combining linear logic and size types for implicit complexity
• lambda!-calculus, Intersection Types, and Involutions
• scientific article; zbMATH DE number 7204445 (Why is no real title available?)
• Tight typings and split bounds, fully developed
• scientific article; zbMATH DE number 7178075 (Why is no real title available?)
• Geometry of synthesis III
• Implicit computation complexity in higher-order programming languages
• Type-based complexity analysis of probabilistic functional programs

This page was built for publication: The geometry of types

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2931793)