Translation certification for smart contracts

DOI10.1007/978-3-030-99461-7_6MaRDI QIDQ2163161zbMATH OpenOpenAlexFDO

Authors Jacco O. G. Krijnen, Manuel M. T. Chakravarty, Gabriele Keller, Wouter Swierstra

Publication date 10 August 2022

Full work available at URL https://arxiv.org/abs/2201.04919

Mathematics Subject Classification ID

Logic programming (68N17) Functional programming and lambda calculus (68N18)

Recommendations

• Certificate Translation for Optimizing Compilers
• An Introduction to Certificate Translation
• Verification-Led Smart Contracts
• SSCalc: a calculus for Solidity smart contracts
• Formal verification of Ethereum smart contracts using Isabelle/HOL

Cites work

• CakeML
• Cogent: uniqueness types and certifying compilation
• Computer aided verification. 32nd international conference, CAV 2020, Los Angeles, CA, USA, July 21--24, 2020. Proceedings. Part I
• scientific article; zbMATH DE number 3768948 (Why is no real title available?)
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Mathematics of program construction. 13th international conference, MPC 2019, Porto, Portugal, October 7--9, 2019. Proceedings
• Principles of security and trust. 6th international conference, POST 2017, held as part of the European joint conferences on theory and practice of software, ETAPS 2017, Uppsala, Sweden, April 22--29, 2017. Proceedings
• Probabilistic relational verification for cryptographic implementations
• Programming Languages and Systems
• Ready, set, verify! Applying hs-to-coq to real-world Haskell code
• The \textsc{MetaCoq} project
• Unraveling recursion: compiling an IR with recursion to System F

Cited in

(3)

• A lightweight approach to smart contracts supporting safety, security, and privacy
• Trusted Translation Services
• Certificate Translation for Optimizing Compilers

Describes a project that uses

Uses Software

• Coq
• Haskell
• CakeML
• CompCert
• CertiCoq
• MetaCoq

This page was built for publication: Translation certification for smart contracts

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