This thesis presents a framework aimed at significantly reducing the cost of proving functional correctness for low-level operating systems components, designed around a new programming language, Cogent. This language is total, polymorphic, higher-order, and purely functional, including features such as algebraic data types and type inference. Crucially, Cogent is equipped with a uniqueness type system, which eliminates the need for a trusted runtime or garbage collector, and allows us to assign two semantics to the language: one imperative, suitable for efficient C code generation; and one functional, suitable for equational reasoning and verification. We prove that the functional semantics is a valid abstraction of the imperative semantics for all well-typed programs. Cogent is designed to easily interoperate with existing C code, to enable Cogent software to interact with existing C systems, and also to provide an escape hatch of sorts, for when the restrictions of Cogent's type system are too onerous. This interoperability extends to Cogent's verification framework, which composes with existing C verification frameworks to enable whole systems to be verified. Cogent's verification framework is based on certifying compilation: For a well-typed Cogent program, the compiler produces C code, a high-level representation of its semantics in Isabelle/HOL, and a proof that the C code correctly refines this embedding. Thus one can reason about the full semantics of real-world systems code productively and equationally, while retaining the interoperability and leanness of C. The compiler certificate is a series of language-level proofs and per-program translation validation phases, combined into one coherent top-level theorem in Isabelle/HOL. To evaluate the effectiveness of this framework, two realistic file systems were implemented as a case study, and key operations for one file system were formally verified on top of Cogent specifications. These studies demonstrate that verification effort is drastically reduced for proving higher-level properties of file system implementations, by reasoning about the generated formal specification from Cogent, rather than low-level C code.

Existing proof assistants such as Isabelle or Coq are geared towards large-scale, complicated verification projects, and are not ideal educational tools for topics of a fairly formal nature, such as the theoretical foundations of programming languages. In particular, they opt for a proof language that resembles a programming language, rather than the structure typically seen in pen-and-paper proofs. Gentzen is a simple theorem prover we are developing in Haskell, which will be tightly integrated with its user interface, using a structural editor for graphically presented proofs. This allows proof scripts to resemble pen-and-paper proofs, and assists students to focus on the proof, rather than the proof assistant. This report outlines the current state of Gentzen development, and gives a formal treatment of its proof checker semantics.

GHC, a Haskell compiler, offers numerous extensions to the standard Haskell type system. Each of these extensions is usually specified only semi-formally, and only in isolation. Very little work has been done examining type system properties when multiple type system extensions are combined, which is the scenario actually being faced by GHC developers. To address this, the GHC team published OutsideIn(X), a mostly-rigorous formulation of GHC's type inference system, which encompasses every type system extension developed for GHC to date.

We formalise OutsideIn(X) in a mechanical proof assistant, in order to provide a body of formal work upon which future extensions can be developed. By using a mechanical proof assistant we not only ensure correctness of our proofs and complete rigor in our definitions, but also make possible the incremental development of the formal work alongside the more practically-minded type checker implementation in GHC. This additional accessibility will hopefully prevent further extensions from being developed without regard to the effect such an extension may have on other parts of the type system.

Our formalisation is developed in Agda. As a dependently typed programming language which enforces totality, Agda doubles as a proof assistant. It is still under heavy development, and is quite experimental. By formalising OutsideIn(X) in Agda, we demonstrate its readiness for type system work, and also provide an example to encourage further type systems research in Agda.