Formal Certification of a Resource-Aware Language Implementation

DOI10.1007/978-3-642-03359-9_15zbMath1252.68070MaRDI QIDQ3183530

Ricardo Peña, Javier de Dios

Publication date: 20 October 2009

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-03359-9_15

zbMATH Keywords

functional languages; memory management; compiler verification

Mathematics Subject Classification ID

68N20: Theory of compilers and interpreters

68N18: Functional programming and lambda calculus

68Q60: Specification and verification (program logics, model checking, etc.)

Related Items

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

Uses Software

• Coq
• Isabelle
• Isabelle/HOL

Cites Work

• Unnamed Item
• Unnamed Item
• Isabelle/HOL. A proof assistant for higher-order logic
• Verified bytecode verifiers.
• A formally verified compiler back-end
• Static prediction of heap space usage for first-order functional programs
• Certificate Translation for Optimizing Compilers
• An Inference Algorithm for Guaranteeing Safe Destruction
• A Resource-Aware Semantics and Abstract Machine for a Functional Language with Explicit Deallocation
• Formal certification of a compiler back-end or
• Structure of a Proof-Producing Compiler for a Subset of Higher Order Logic