A resource semantics and abstract machine for \textit{Safe}: a functional language with regions and explicit deallocation

DOI10.1016/j.ic.2014.01.003zbMath1358.68059OpenAlexW2033746349MaRDI QIDQ2437794

Clara Segura, Ricardo Peña, Manuel Montenegro

Publication date: 13 March 2014

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.ic.2014.01.003

zbMATH Keywords

functional languagesmemory managementcode generationabstract machinescertifying compilers

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20) Functional programming and lambda calculus (68N18)

Uses Software

• Isabelle/HOL
• LLVM

Cites Work

• Unnamed Item
• Unnamed Item
• Region-based memory management
• Isabelle/HOL. A proof assistant for higher-order logic
• Abstract computing machines. A lambda calculus perspective.
• Verified bytecode verifiers.
• A program logic for resources
• A formally verified compiler back-end
• Static prediction of heap space usage for first-order functional programs
• π-RED⁺ An interactive compiling graph reduction system for an applied λ-calculus
• Formal Certification of a Resource-Aware Language Implementation
• Amortized Resource Analysis with Polynomial Potential
• An Inference Algorithm for Guaranteeing Safe Destruction
• Polynomial Size Analysis of First-Order Shapely Functions
• From operational semantics to abstract machines
• Deriving a lazy abstract machine
• A Resource-Aware Semantics and Abstract Machine for a Functional Language with Explicit Deallocation
• Static determination of quantitative resource usage for higher-order programs
• From natural semantics to C: A formal derivation of two STG machines
• Formal certification of a compiler back-end or
• The Mechanical Evaluation of Expressions
• A Space Consumption Analysis by Abstract Interpretation
• Programming Languages and Systems