Formal Certification of a Resource-Aware Language Implementation

DOI10.1007/978-3-642-03359-9_15MaRDI QIDQ3183530zbMATH OpenOpenAlexFDO

Authors Javier de Dios, Ricardo Peña

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

compiler verificationfunctional languagesmemory management

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Theory of compilers and interpreters (68N20) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Formal certification of a compiler back-end or: programming a compiler with a proof assistant
• scientific article; zbMATH DE number 1980940
• A formally verified compiler back-end
• Theorem Proving in Higher Order Logics
• scientific article; zbMATH DE number 2090288

Cites work

• A formally verified compiler back-end
• A Resource-Aware Semantics and Abstract Machine for a Functional Language with Explicit Deallocation
• An Inference Algorithm for Guaranteeing Safe Destruction
• Certificate Translation for Optimizing Compilers
• Formal certification of a compiler back-end or: programming a compiler with a proof assistant
• 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
• Static prediction of heap space usage for first-order functional programs
• Structure of a Proof-Producing Compiler for a Subset of Higher Order Logic
• Verified bytecode verifiers.

Cited in

(12)

• A formal, resource consumption-preserving translation of actors to Haskell
• A resource semantics and abstract machine for \textit{Safe}: a functional language with regions and explicit deallocation
• A program logic for resources
• A formal, resource consumption-preserving translation from actors with cooperative scheduling to Haskell
• A certified framework for compiling and executing garbage-collected languages
• Resource bound certification
• Formal certification of a compiler back-end or: programming a compiler with a proof assistant
• Theorem Proving in Higher Order Logics
• Formalizing the Edmonds-Karp Algorithm
• Flow Networks and the Min-Cut-Max-Flow Theorem
• Formalizing Push-Relabel Algorithms
• Verified Efficient Implementation of Gabow's Strongly Connected Components Algorithm

Describes a project that uses

Uses Software

• Coq
• Isabelle/HOL
• Isabelle

This page was built for publication: Formal Certification of a Resource-Aware Language Implementation

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