William Bowman

 
Prospective Graduate Students / Postdocs

This faculty member is currently not looking for graduate students or Postdoctoral Fellows. Please do not contact the faculty member with any such requests.

Assistant Professor

Research Classification

Research Interests

programming languages

Relevant 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 (2010 - 2021)
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.

 
 

Discover the amazing research that is being conducted at UBC!