Starting Date: June 2023 (flexible)
Prerequisites: Good mathematical background; Functional programming skills; Basic Coq programming/proving
Will results be assigned to University: 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