Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Go Code Generation for Isabelle


view this post on Zulip Email Gateway (Mar 11 2024 at 11:00):

From: Peter Lammich <cl-isabelle-users@lists.cam.ac.uk>
Go Code Generation for Isabelle

by Terru Stübinger and Lars Hupel

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.

https://www.isa-afp.org/entries/Go.html

Enjoy!


Last updated: Apr 28 2024 at 20:16 UTC