Verified functional programming of an abstract interpreter

DOI10.1007/978-3-030-88806-0_6zbMath1497.68102arXiv2107.09472MaRDI QIDQ2145322

David Pichardie, Jean-Pierre Talpin, Lucas Franceschino

Publication date: 17 June 2022

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

Mathematics Subject Classification ID

68N20: Theory of compilers and interpreters

68N18: Functional programming and lambda calculus

68V15: Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)

Uses Software

• z3
• Verasco
• HACL*

Cites Work

• Abstract Interpretation of Annotated Commands
• Programming Languages and Systems
• A Certified Denotational Abstract Interpreter