Translating Scala programs to Isabelle/HOL. System description

DOI10.1007/978-3-319-40229-1_38MaRDI QIDQ2817953zbMATH OpenOpenAlexWikidataFDO

Authors Lars Hupel, Viktor Kuncak

Publication date 5 September 2016

Published in Automated Reasoning (Search for Journal in Brave)

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

zbMATH Keywords

HOLIsabellecompilerScalaLeon

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Abstract: We present a trustworthy connection between the Leon verification system and the Isabelle proof assistant. Leon is a system for verifying functional Scala programs. It uses a variety of automated theorem provers (ATPs) to check verification conditions (VCs) stemming from the input program. Isabelle, on the other hand, is an interactive theorem prover used to verify mathematical specifications using its own input language Isabelle/Isar. Users specify (inductive) definitions and write proofs about them manually, albeit with the help of semi-automated tactics. The integration of these two systems allows us to exploit Isabelle's rich standard library and give greater confidence guarantees in the correctness of analysed programs.

Recommendations

• Scallina: translating verified programs from Coq to Scala
• A verified compiler from Isabelle/HOL to CakeML
• Scalable LCF-style proof translation
• Imperative Functional Programming with Isabelle/HOL
• The Isabelle Framework

Cites work

• Asynchronous user interaction and tool integration in Isabelle/PIDE
• Code generation via higher-order rewrite systems
• Concrete semantics. With Isabelle/HOL
• Isabelle as document-oriented proof assistant
• Isabelle/jEdit – A Prover IDE within the PIDE Framework
• Partial and nested recursive function definitions in higher-order logic
• Truly modular (co)datatypes for Isabelle/HOL

Cited in

(2)

• Scallina: translating verified programs from Coq to Scala
• Scala to the Power of Z3: Integrating SMT and Programming

Describes a project that uses

Uses Software

• Apache Spark
• CVC4
• Leon
• Isabelle/PIDE
• Scala
• Isabelle/jEdit
• PIDE
• HOL
• z3
• Isar
• Isabelle/Isar
• Isabelle

This page was built for publication: Translating Scala programs to Isabelle/HOL. System description

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