Translation certification for smart contracts

DOI10.1007/978-3-030-99461-7_6OpenAlexW4285217460MaRDI QIDQ2163161

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

Publication date: 10 August 2022

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

Mathematics Subject Classification ID

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

Uses Software

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

Cites Work

• Unnamed Item
• 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
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Computer aided verification. 32nd international conference, CAV 2020, Los Angeles, CA, USA, July 21--24, 2020. Proceedings. Part I
• Unraveling recursion: compiling an IR with recursion to System F
• The \textsc{MetaCoq} project
• Mathematics of program construction. 13th international conference, MPC 2019, Porto, Portugal, October 7--9, 2019. Proceedings
• Ready,Set, Verify! Applyinghs-to-coqto real-world Haskell code
• Cogent: uniqueness types and certifying compilation
• CakeML
• Probabilistic relational verification for cryptographic implementations
• Programming Languages and Systems

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