Extending Isabelle/HOL's Code Generator with support for the Go programming language

Terru Stübinger, Lars Hupel

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…