Extending Isabelle/HOL's Code Generator with support for the Go programming language
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2023
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866917779650641920 |
|---|---|
| author | Stübinger, Terru Hupel, Lars |
| author_facet | Stübinger, Terru Hupel, Lars |
| contents | The Isabelle proof assistant includes a small functional language, which allows users to write and reason about programs. So far, these programs could be extracted into a number of functional languages: Standard ML, OCaml, Scala, and Haskell. This work adds support for Go as a fifth target language for the Code Generator. 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. The developed Code Generation is provided as an add-on library that can be simply imported into existing theories. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2310_02704 |
| institution | arXiv |
| publishDate | 2023 |
| record_format | arxiv |
| spellingShingle | Extending Isabelle/HOL's Code Generator with support for the Go programming language Stübinger, Terru Hupel, Lars Programming Languages Logic in Computer Science The Isabelle proof assistant includes a small functional language, which allows users to write and reason about programs. So far, these programs could be extracted into a number of functional languages: Standard ML, OCaml, Scala, and Haskell. This work adds support for Go as a fifth target language for the Code Generator. 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. The developed Code Generation is provided as an add-on library that can be simply imported into existing theories. |
| title | Extending Isabelle/HOL's Code Generator with support for the Go programming language |
| topic | Programming Languages Logic in Computer Science |
| url | https://arxiv.org/abs/2310.02704 |