Go Code Generation for Isabelle

Terru Stübinger 🌐 and Lars Hupel 🌐

January 22, 2024

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

Abstract

This entry contains a standalone code generation target for the Go programming language. Unlike the previous targets, Go is not a functional language and encourages code in an imperative style, thus many of the features of Isabelle's language (particularly data types, pattern matching, and type classes) have to be emulated using imperative language constructs in Go. To generate Go code, users can simply import this entry, which makes the Go target available.

License

BSD License

Topics

Related publications

  • Stübinger, T., & Hupel, L. (2023). Extending Isabelle/HOL's Code Generator with support for the Go programming language. ArXiv. https://doi.org/10.48550/ARXIV.2310.02704
  • Lars Hupel, & terru. (2024). isabelle-prover/isabelle-go-codegen: v0.3.1 (Version v0.3.1) [Computer software]. Zenodo. https://doi.org/10.5281/ZENODO.8401392

Session Go

Session Go_Test_Quick

Session Go_Test_Slow

Cite

× 
@article{Go-AFP,
  author  = {Terru Stübinger and Lars Hupel},
  title   = {Go Code Generation for Isabelle},
  journal = {Archive of Formal Proofs},
  month   = {January},
  year    = {2024},
  note    = {\url{https://isa-afp.org/entries/Go.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest

Older releases: