Good mathematical background; Functional programming skills; Basic Coq programming/proving

No

Go 1.18 [1] has recently been released. This new version includes generics and more flexible interfaces.

Generics allow programmers to define data structures and functions that work safely for several types, e.g., like `List<E>`

in Java which defines lists that can store any value of type `E`

, where `E`

is any type (`String`

, `Boolean`

, etc).

Featherweight Generic Go (FGG) is a small subset of Go with generics that has been formalised in [2], where it is notably proved that FGG is type safe (i.e., well-typed programs never go wrong). One may wonder whether the more flexible interfaces recently introduced still validate type safety.

A good definition of subtyping is key to prove type safety as it specifies when a datatype can be safely replaced by another, e.g., `integer`

is a subtype of `floating point`

(you can use an `integer`

whenever a `floating point`

is expected).

Building on FGG, the core objective of the project is to mechanise, using Coq, a definition of subtyping between interfaces [3] for (a subset of) the most recent version of Go (including ‘type lists’). Then we shall prove different properties of this subtyping relation (e.g., transitivity).

Next, we will design subtyping algorithms, and prove them correct wrt. the mechanised specification.

NB: For this project, you don’t need to know much about Go, but you should have some basic knowledge of programming with Coq (i.e., Chapters 1-6 of Software Foundations [4]).

The projects will be jointly supervised by Julien Lange (lead), Francisco Ferreira, and Reuben Rowe.

[1] https://go.dev/blog/go1.18

[2] Featherweight Go (https://dl.acm.org/doi/10.1145/3428217)

[3] https://go.dev/ref/spec#Interface_types

[4] https://softwarefoundations.cis.upenn.edu/lf-current/toc.html