William Bowman

When defining the syntax and semantics of programming languages, computer scientists often use some kind of computer science metanotations. These metanotations are often informal or under-defined: human readers can understand them intuitively, but they are unsuitable for use in rigorous formal proofs. The aim of this project is to develop a tool that bridges the gap between the intuitive metanotations for defining programming languages, and proof assistant languages in which properties of the languages defined can be formally proven.In this thesis, I present Redex-Plus, an implementation of a computer science metanotation based on the Racket language Redex, which is used to define programming language models. Redex-Plus is a compiler that translates language models defined in the Redex language to corresponding definitions in various proof assistant languages. Redex-Plus also generates boilerplate such as binding operations, saving the users from the tedious job of writing boilerplate by hand. Redex-Plus supports Coq, Agda, SMT-LIB, and Beluga as translation targets; it can faithfully translate language models with multiple types of bound variables; and it gives users the choice between multiple ways to represent variable binding when using the Coq or Agda targets. I evaluate Redex-Plus by formalizing a variant of Simply Typed Lambda Calculus and proving some important properties of the language model in both Coq and Agda, and by formalizing a variant of System F and attempting to prove the same properties in Coq.The source code repository of Redex-Plus is publicly available at https://gitlab.com/xujunfeng/redex-plus , and on Zenodo.

View record

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

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

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