William Bowman

Prospective Graduate Students / Postdocs

This faculty member is currently not actively recruiting graduate students or Postdoctoral Fellows, but might consider co-supervision together with another faculty member.

Assistant Professor

Research Interests

programming languages

Relevant Thesis-Based Degree Programs

Research Options

I am available and interested in collaborations (e.g. clusters, grants).
I am interested in and conduct interdisciplinary research.
I am interested in working with undergraduate students on research projects.

Graduate Student Supervision

Master's Student Supervision

Theses completed in 2010 or later are listed below. Please note that there is a 6-12 month delay to add the latest theses.

Sized dependent types via extensional type theory (2022)

Many contemporary proof assistants based on dependent type theories such as Coq and Agda are founded on the types-as-propositions paradigm where type checking a program corresponds to verifying a proof of some proposition in a higher-order predicate logic. To ensure decidability of type checking and consistency of the logic, these proof assistants forbid nonterminating recursive functions using guard predicates that only allow structurally recursive functions recurring on syntactically smaller arguments. However, these guard predicates are sometimes too restrictive and reject simple terminating functions that aren't otherwise structurally recursive.An alternative is to use type-based termination checking such as sized types, where inductively-defined types are annotated with sizes. Successful type checking guarantees that functions recur only on arguments whose types have smaller sizes, rather than merely on syntactic subarguments. Some existing models of sized dependent type theories support features for more expressive sized types, namely higher-rank size quantification (which allows for passing around size-preserving functions) and bounded size quantification (which eliminates the need for complex semi-continuity checks), but unfortunately none support both simultaneously. Meanwhile, the only implementation of sized types in a major proof assistant, Agda, does support these features, but is unfortunately logically inconsistent.In this thesis, I design a sized dependent type theory with higher-rank and bounded sizes (STT), and show that it's suitable for theorem proving by proving its consistency with a syntactic model: by compiling STT into the Extensional Calculus of Inductive Constructions (CICᴇ), a variant of Coq's core type theory, and showing that this translation is type preserving, the consistency of STT follows from the consistency of CICᴇ.This approach refutes the existence of an infinite size strictly greater than all sizes, which is present in prior sized type systems to overcome the limitations of finitary size expressions, meaning that some infinitary constructs unfortunately aren't definable in STT. Even so, STT provides a valid foundation for sized types in a proof assistant, opening the way for future work on recovering expressivity lost from the lack of an infinite size and on restricting sized types in Agda to be consistent.

View record

ANF preserves dependent types up to extensional equality (2021)

A growing number of programmers use dependently typed languagessuch as Coq to machine-verify important properties of high-assurance software.However, existing compilers for these languages provide no guarantees after compiling, nor when linking after compilation.Type-preserving compilers preserve guarantees encodedin types, then use type checking to verify compiled code and ensuresafe linking with external code.Unfortunately, standard compiler passes do not preserve the dependent typing of commonly used (intensional) type theories.This is because assumptions valid in simpler type systems no longer hold,and intensional dependent type systems are highly sensitive tosyntactic changes, including compilation.We develop an A-normal form (ANF) translation with join-point optimization, a standard translation for making control flow explicit in functional languages, from the Extended Calculus of Constructions (ECC)with dependent elimination of booleans and natural numbers(a representative subset of Coq). Our dependently typed target language has equality reflection,allowing the type system to encode semantic equality of terms.This is key to proving type preservation and correctness of separate compilationfor this translation.This is the first ANF translation for dependent types.Unlike related translations, it supports the universe hierarchy,and does not rely on parametricity or impredicativity.

View record

An indexed type system for (2020)

Downloading and executing untrusted code is inherently unsafe, but also something that happens often on the internet. Therefore, untrusted code often requires run-time checks to ensure safety during execution. These checks compromise performance and may be unnecessary. We present the Wasm-prechk language, an assembly language based on WebAssembly that is intended to ensure safety while justifying the static elimination of run-time checks.

View record


If this is your researcher profile you can log in to the Faculty & Staff portal to update your details and provide recruitment preferences.


Explore our wide range of course-based and research-based program options!