Static prediction of heap space usage for first-order functional programs

DOI10.1145/604131.604148zbMath1321.68180OpenAlexW2068055184MaRDI QIDQ2942925

Martin Hofmann, Steffen Jost

Publication date: 11 September 2015

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

Full work available at URL: https://doi.org/10.1145/604131.604148

zbMATH Keywords

program analysisfunctional programmingresourcesheapgarbage collection

Mathematics Subject Classification ID

Searching and sorting (68P10) Linear programming (90C05) Theory of compilers and interpreters (68N20) Functional programming and lambda calculus (68N18) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17)

Related Items

ATLAS: automated amortised complexity analysis of self-adjusting data structures, Calculating Statically Maximum Log Memory Used by Multi-threaded Transactional Programs, A type-based complexity analysis of object oriented programs, Formal Certification of a Resource-Aware Language Implementation, Type-based cost analysis for lazy functional languages, Space-aware ambients and processes, Machine-Checked Verification of the Correctness and Amortized Complexity of an Efficient Union-Find Implementation, Amortized Complexity Verified, Trends in trends in functional programming 1999/2000 versus 2007/2008, Denotational semantics as a foundation for cost recurrence extraction for functional languages, Linear types and non-size-increasing polynomial time computation., Closed-form upper bounds in static cost analysis, Tight typings and split bounds, fully developed, Automatic Inference of Upper Bounds for Recurrence Relations in Cost Analysis, A resource semantics and abstract machine for \textit{Safe}: a functional language with regions and explicit deallocation, Type-based amortized resource analysis with integers and arrays, Exception handling for copyless messaging, Types for complexity of parallel computation in pi-calculus, Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits, Amortized complexity verified, A program logic for resources, Combining linear logic and size types for implicit complexity, A type system for counting instances of software components, Unnamed Item, Structural recursion as a query language on lists and ordered trees, A Coq Library for Internal Verification of Running-Times, Attribute-Based Signatures for Circuits from Bilinear Map, A type system with usage aspects, A Transformational Approach to Resource Analysis with Typed-norms Inference, An Inference Algorithm for Guaranteeing Safe Destruction, Light types for polynomial time computation in lambda calculus, Unnamed Item, A Heterogeneous Pushout Approach to Term-Graph Transformation, A Type System for Usage of Software Components, Efficient Type-Checking for Amortised Heap-Space Analysis, Cost analysis of object-oriented bytecode programs, Two decades of automatic amortized resource analysis, Type-based analysis of logarithmic amortised complexity

Uses Software

• TREX

Cites Work

• Regular expression pattern matching for XML
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item