Translating Scala Programs to Isabelle/HOL

DOI10.1007/978-3-319-40229-1_38zbMath1475.68437arXiv1607.01539OpenAlexW3125694439WikidataQ57955182 ScholiaQ57955182MaRDI QIDQ2817953

Viktor Kuncak, Lars Hupel

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)

Uses Software

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

Cites Work

• Partial and nested recursive function definitions in higher-order logic
• Truly Modular (Co)datatypes for Isabelle/HOL
• Asynchronous User Interaction and Tool Integration in Isabelle/PIDE
• Isabelle/jEdit – A Prover IDE within the PIDE Framework
• Concrete Semantics
• Code Generation via Higher-Order Rewrite Systems
• Isabelle as Document-Oriented Proof Assistant

This page was built for publication: Translating Scala Programs to Isabelle/HOL