Ready,Set, Verify! Applyinghs-to-coqto real-world Haskell code

DOI10.1017/S0956796820000283MaRDI QIDQ5018778

Christine Rizkallah, Joachim Breitner, Unnamed Author, Stephanie Weirich, Yao Li, John Wiegley, Antal Spector-Zabusky

Publication date: 22 December 2021

Published in: Journal of Functional Programming (Search for Journal in Brave)

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

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Related Items (2)

Translation certification for smart contracts ⋮ Cogent: uniqueness types and certifying compilation

Uses Software

• Coq

Cites Work

• Unnamed Item
• Unnamed Item
• The calculus of constructions
• Isabelle/HOL. A proof assistant for higher-order logic
• Refinement types for Haskell
• How to keep your neighbours in order
• Dependent types and multi-monadic effects in F*
• Automatic Functional Correctness Proofs for Functional Search Trees
• A Framework for the Automatic Formal Verification of Refinement from Cogent to C
• Proof-producing translation of higher-order logic into pure and stateful ML
• HALO
• Refinement through restraint: bringing down the cost of verification
• Balancing weight-balanced trees
• A Brief Overview of Agda – A Functional Language with Dependent Types
• Fast Reflexive Arithmetic Tactics the Linear Case and Beyond
• Partial Recursive Functions in Higher-Order Logic
• Purely Functional Data Structures
• Program verification through characteristic formulae
• Programming Languages and Systems
• Abstract Refinement Types
• CakeML
• The Optimal Fixed Point Combinator

This page was built for publication: Ready,Set, Verify! Applyinghs-to-coqto real-world Haskell code