June 2023 (flexible)
Good mathematical background; Functional programming skills; Basic Coq programming/proving
Go 1.18  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 is any type (
Featherweight Generic Go (FGG) is a small subset of Go with generics that has been formalised in , 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  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 ).
The projects will be jointly supervised by Julien Lange (lead), Francisco Ferreira, and Reuben Rowe.
 Featherweight Go (https://dl.acm.org/doi/10.1145/3428217)