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

DOI10.1016/J.IC.2014.01.003MaRDI QIDQ2437794zbMATH OpenOpenAlexFDO

Authors Manuel Montenegro, Ricardo Peña, Clara Segura

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

abstract machinescertifying compilerscode generationfunctional languagesmemory management

Mathematics Subject Classification ID

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

Recommendations

• A Resource-Aware Semantics and Abstract Machine for a Functional Language with Explicit Deallocation
• A space consumption analysis by abstract interpretation
• Typing Safe Deallocation
• Safety Guarantees from Explicit Resource Management
• Safe manual memory management in Cyclone

Cites work

• A formally verified compiler back-end
• A program logic for resources
• A Resource-Aware Semantics and Abstract Machine for a Functional Language with Explicit Deallocation
• A space consumption analysis by abstract interpretation
• Abstract computing machines. A lambda calculus perspective.
• Amortized resource analysis with polynomial potential. A static inference of polynomial bounds for functional programs
• An Inference Algorithm for Guaranteeing Safe Destruction
• Deriving a lazy abstract machine
• Formal certification of a compiler back-end or: programming a compiler with a proof assistant
• Formal Certification of a Resource-Aware Language Implementation
• From natural semantics to C: A formal derivation of two STG machines
• From operational semantics to abstract machines
• scientific article; zbMATH DE number 2081101 (Why is no real title available?)
• scientific article; zbMATH DE number 2090288 (Why is no real title available?)
• Isabelle/HOL. A proof assistant for higher-order logic
• Polynomial Size Analysis of First-Order Shapely Functions
• Programming Languages and Systems
• Region-based memory management
• Static determination of quantitative resource usage for higher-order programs
• Static prediction of heap space usage for first-order functional programs
• The Mechanical Evaluation of Expressions
• Verified bytecode verifiers.
• π-RED⁺ An interactive compiling graph reduction system for an applied λ-calculus

Cited in

(10)

• Reasoning about a machine with local capabilities. Provably safe stack and return pointer management
• The meaning of memory safety
• Safe manual memory management in Cyclone
• Semantics of memory management for polymorphic languages
• Safety Guarantees from Explicit Resource Management
• An Inference Algorithm for Guaranteeing Safe Destruction
• scientific article; zbMATH DE number 1955913 (Why is no real title available?)
• A Resource-Aware Semantics and Abstract Machine for a Functional Language with Explicit Deallocation
• Typing Safe Deallocation
• A space consumption analysis by abstract interpretation

Describes a project that uses

Uses Software

• Isabelle/HOL
• LLVM

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

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