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.

翻译：伊莎贝尔证明助手包含一个函数式小语言，允许用户编写程序并对其进行推理。迄今为止，这些程序可被提取到多种函数式语言中：标准ML、OCaml、Scala和Haskell。本工作新增了Go作为代码生成器的第五个目标语言。与先前的目标语言不同，Go并非函数式语言，而是鼓励使用命令式风格编写代码，因此伊莎贝尔语言的许多特性（特别是数据类型、模式匹配和类型类）必须通过Go中的命令式语言结构进行模拟。所开发的代码生成器作为附加库提供，可简单地导入到现有理论中。