Foundational certified code in the Twelf metalogical framework

DOI10.1145/1352582.1352584MaRDI QIDQ5277805zbMATH OpenOpenAlexFDO

Authors Karl Crary, Susmit Sarkar

Publication date 12 July 2017

Published in ACM Transactions on Computational Logic (Search for Journal in Brave)

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

zbMATH Keywords

foundational certified codelogic programmingmetalogic

Mathematics Subject Classification ID

Logic in computer science (03B70) Logic programming (68N17) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Automated Deduction – CADE-19
• Term Rewriting and Applications
• A syntactic approach to foundational proof-carrying code
• Tutorial examples of the semantic approach to foundational proof-carrying code
• Typed Lambda Calculi and Applications

Cited in

(7)

• TWAM: a certifying abstract machine for logic programs
• Formalizing the SAFECode type system
• Verified software toolchain (invited talk)
• A Certified Distributed Security Logic for Authorizing Code
• scientific article; zbMATH DE number 1949628 (Why is no real title available?)
• A type system for expressive security policies
• Automated Deduction – CADE-19

This page was built for publication: Foundational certified code in the Twelf metalogical framework

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