Generics in Go and lambda lifting

Abstract

This thesis examines the history of generics in the Go programming language, and analyses two specific issues that arise: local type declarations inside generic functions, and embedded type parameters.

This work includes a novel algorithm for lambda lifting, a problem closely related to the handling of local types inside generic functions in Go. The correctness of this algorithm is proven with respect to both a specification from the literature and additional specifications. Parts of these proofs are formalised using the Lean 4 theorem prover.

For embedded type parameters, this thesis proposes sound member promotion rules for type parameters embedded in struct types in Go.

The testing methodology used in this thesis centres around "checking", which strikes a middle ground between formal verification and testing.