William J. Bowman | Home

A headshot of me

wjb

William J. Bowman is finishing his Ph.D. in computer science (studying programming languages) at Northeastern University, and will be starting as an Assistant Professor at University of British Columbia in Spring 2019. Broadly speaking, he is interested in making it easier for programmers to communicate their intent to machines, and preserving that intent through the stages of compilation. More specifically, his research interests include secure and verified compilation, dependently typed programming, verification, meta-programming, and interoperability. His recent work examines type-preserving compilation of dependently typed programming language like Coq, a technique that can enable preserving security and correctness invariants of verified software through compilation and statically enforcing those invariants in the low-level (assembly-like) code generated by compilers.

Manuscripts

Dependent Type Systems as Macros.
Stephen Chang, Michael Ballantyne, Marcela Poffald, William J. Bowman
2018.
Increasingly, programmers want the power of dependent types, yet significant expertise is still required to write realistic dependently-typed programs. Domain-specific languages (DSLs) attempting to tame dependent types have proliferated, adding notation and tools tailored to a problem domain, but these only shift the problem, as implementing such languages requires at least as much expertise as using dependent types.

We show how to lower the burden for implementing dependently-typed languages and DSLs, using a classic approach to DSL implementation not typically associated with typed languages— macros— which allows programmers to reuse all of a host language’s infrastructure when implementing a new, dependently-typed, language or DSL, reducing the overall effort. We also extend the Turnstile language, a meta-DSL for typed DSL implementation using syntax resembling “pen and paper” models, with support for dependent types. Using macros not only simplifies the initial language implementation, but simplifies adding extensions like notation or tactic languages— all but required features for dependently-typed languages.

We evaluate our approach by building three languages in different parts of the design space: first, a video-editing DSL with a Dependent ML-like type system, demonstrating that our approach accommodates “lightweight” dependent types; second, we gradually extend MLTT to the Calculus of Inductive Constructions, demonstrating that our approach is modular, and scales to “heavyweight” dependent type systems; and, finally, Cur, a prototype proof assistant with a similar design to Coq, which supports new notation and an extensible tactic language, demonstrating that our approach scales to creating realistic dependently-typed proof assistants.
AbstractAbstract (Hide) | Paper

Compiling Dependent Types Without Continuations.
William J. Bowman and Amal Ahmed
2018.
Type-preserving compilation of dependently typed languages preserves the correctness specifications (encoded in types) and proofs from languages such as Coq through compilation. This enables checking that programs still meet their specification after compilation, and allows enforcing specifications at link time via type checking. Unfortunately, the standard approach to making control flow explicit in a type-preserving compiler is the continuation-passing style (CPS) transformation, which does not work well in dependent type theory. In fact, until recently, preserving dependent types through CPS translation was thought impossible, and even recent successful approaches do not scale well in general. For example, they require eliding types like strong dependent pairs from the source language, require non-standard typed target languages, do not support an infinite predicative universe hierarchy, or do not have decidable type checking in the target language.

In this work, we present a type-preserving A-normal form (ANF) transformation— a common alternative to CPS— from the Extended Calculus of Constructions (ECC) to a syntactically restricted subset of ECC. We also prove correctness of separate compilation for this translation. Unlike the existing CPS translations, we show that ANF translation does scale well— in particular, our type-preserving ANF translation does not require a custom typed intermediate language to ensure type preservation, does support general dependent elimination of positive types (such as dependent projection of dependent pairs), does support an infinite predicative universe hierarchy, and does have decidable type checking in the target language. We also demonstrate how ANF provides insight into the commonality between problems (and solutions) in work on CPS, dependent sequent calculus, dependent call-by-push-value, dependent pattern matching, and commutative cuts in dependently typed languages.
AbstractAbstract (Hide) | Paper | Technical Appendix

Conference Publications

Typed Closure Conversion of the Calculus of Constructions.
William J. Bowman and Amal Ahmed
In Proc. of the Conference on Programming Language Implementation and Design (PLDI 2018).
Dependently typed languages such as Coq are used to specify and verify the full functional correctness of source programs. Type-preserving compilation can be used to preserve these specifications and proofs of correctness through compilation into the generated target-language programs. Unfortunately, type-preserving compilation of dependent types is hard. In essence, the problem is that dependent type systems are designed around high-level compositional abstractions to decide type checking, but compilation interferes with the type-system rules for reasoning about run-time terms.

We develop a type-preserving closure-conversion translation from the Calculus of Constructions (CC) with strong dependent pairs (Σ types)— a subset of the core language of Coq— to a type-safe, dependently typed compiler intermediate language named CC-CC. The central challenge in this work is how to translate the source type-system rules for reasoning about functions into target type-system rules for reasoning about closures. To justify these rules, we prove soundness of CC-CC by giving a model in CC. In addition to type preservation, we prove correctness of separate compilation.
AbstractAbstract (Hide) | Paper | Technical Appendix | PLDI 2018 Talk (by me) | Slides

Type-Preserving CPS Translation of Σ and Π Types is Not Not Possible.
William J. Bowman, Youyou Cong, Nick Rioux, and Amal Ahmed
In Proc. of the Symposium on Principles of Programming Languages (POPL 2018)
Dependently typed languages such as Coq are used to specify and prove functional correctness of source programs, but what we ultimately need are guarantees about correctness of compiled code. By preserving dependent types through each compiler pass, we could preserve source-level specifications and correctness proofs into the generated target-language programs. Unfortunately, type-preserving compilation of dependent types is a challenging problem. In 2002, Barthe and Uustalu showed that type-preserving CPS is \emph{not possible} for languages such as Coq. Specifically, they showed that for strong dependent pairs ($\Sigma$ types), the standard typed call-by-name CPS is \emph{not type preserving}. They further proved that for dependent case analysis on sums, a class of typed CPS translations— including the standard translation— is \emph{not possible}. In 2016, Morrisett noticed a similar problem with the standard call-by-value CPS translation for dependent functions ($\Pi$ types). In essence, the problem is that the standard typed CPS translation by double-negation, in which computations are assigned types of the form $(A \rightarrow \bot) \rightarrow \bot$, disrupts the term/type equivalence that is used during type checking in a dependently typed language.

In this paper, we prove that type-preserving CPS translation for dependently typed languages is \emph{not} not possible. We develop both call-by-name and call-by-value CPS translations from the Calculus of Constructions with both $\Pi$ and $\Sigma$ types (CC) to a dependently typed target language, and prove type preservation and compiler correctness of each translation. Our target language is CC extended with an additional equivalence rule and an additional typing rule, which we prove consistent by giving a model in the extensional Calculus of Constructions. Our key observation is that we can use a CPS translation that employs \emph{answer-type polymorphism}, where CPS-translated computations have type $\forall \alpha. (A \rightarrow \alpha) \rightarrow \alpha$. This type justifies, by a \emph{free theorem}, the new equality rule in our target language and allows us to recover the term/type equivalences that CPS translation disrupts. Finally, we conjecture that our translation extends to dependent case analysis on sums, despite the impossibility result, and provide a proof sketch.
AbstractAbstract (Hide) | Paper | Technical Appendix | POPL 2018 Talk (by me) | POPL 2018 Lightning Talk (by me) | Slides | Supplementary Materials

Fully Abstract Compilation via Universal Embedding.
Max New, William J. Bowman, and Amal Ahmed.
In Proc. of the International Conference on Functional Programming (ICFP 2016)
A fully abstract compiler guarantees that two source components are observationally equivalent in the source language if and only if their translations are observationally equivalent in the target. Full abstraction implies the translation is secure: target-language attackers can make no more observations of a compiled component than a source-language attacker interacting with the original source component. Proving full abstraction for realistic compilers is challenging because realistic target languages contain features (such as control effects) unavailable in the source, while proofs of full abstraction require showing that every target context to which a compiled component may be linked can be back-translated to a behaviorally equivalent source context.

We prove the first full abstraction result for a translation whose target language contains exceptions, but the source does not. Our translation— specifically, closure conversion of simply typed λ-calculus with recursive types— uses types at the target level to ensure that a compiled component is never linked with attackers that have more distinguishing power than source-level attackers. We present a new back-translation technique based on a deep embedding of the target language into the source language at a dynamic type. Then boundaries are inserted that mediate terms between the untyped embedding and the strongly-typed source. This technique allows back-translating non-terminating programs, target features that are untypeable in the source, and well-bracketed effects.
AbstractAbstract (Hide) | Paper | Technical Appendix | ICFP 2016 Talk (by Max New) | Author-Izer

Noninterference for Free.
William J. Bowman, and Amal Ahmed.
In Proc. of the International Conference on Functional Programming (ICFP 2015)
Abadi et. al. (1999) introduced the dependency core calculus (DCC) as a framework for studying a variety of dependency analyses (e.g., secure information flow). The key property provided by DCC is noninterference, which guarantees that a low-level observer (attacker) cannot distinguish high-level (protected) computations. The proof of noninterference for DCC suggests a connection to parametricity in System F, which suggests that it should be possible to implement dependency analyses in languages with parametric polymorphism.

In this paper, we present a translation from DCC into Fω and prove that the translation preserves noninterference. To express noninterference in Fω we define a notion of observer-sensitive equivalence that makes essential use of both first-order and higher-order polymorphism. Our translation provides insights into DCC’s type system and shows how DCC can be implemented in a polymorphic language without loss of the security/noninterference guarantees available in DCC. Our contributions include proof techniques that should be valuable when proving other secure compilation or full abstraction results.
AbstractAbstract (Hide) | Paper | Technical Appendix | ICFP 2015 Talk (by me) | Slides | Author-Izer


Profile-Guided Meta-Programming.
William J. Bowman, Swaha Miller, Vincent St-Amour, and R. Kent Dybvig.
In Proc. of the Conference on Programming Language Implementation and Design (PLDI 2015).
Contemporary compiler systems such as GCC, .NET, and LLVM incorporate profile-guided optimizations (PGOs) on low-level intermediate code and basic blocks, with impressive results over purely static heuristics. Recent work shows that profile information is also useful for performing source-to-source optimizations via meta-programming. For example, using profiling information to inform decisions about data structures and algorithms can potentially lead to asymptotic improvements in performance.

We present a design for profile-guided meta-programming in a general-purpose meta-programming system. Our design is parametric over the particular profiler and meta-programming system. We implement this design in two different meta-programming systems— the syntactic extensions systems of Chez Scheme and Racket— and provide several profile-guided meta-programs as usability case studies.
AbstractAbstract (Hide) | Paper | Slides | GitHub | Author-Izer

Workshop Publications

Dependently Typed Assembly and Secure Linking (short talk)
William J. Bowman.
Talk at the Workshop on Principles of Secure Compilation (PriSC 2018).
Type-preserving compilation is used to statically enforce safety and security properties through type checking. The idea is to design strongly typed compiler target languages, preserve type information through the compiler, then use the types in the target language to enforce invariants when linking with untrusted code. Unfortunately, this technique is limited by the expressiveness of the target type system, and existing simple and polymorphic typed assembly languages cannot express all security invariants we wish to enforce. Dependent types could be used to express safety, security, and full functional correctness invariants. In this talk, I briefly describe work-in-progress on developing a dependently typed assembly, and how it could be used to statically enforce security guarantees when linking.AbstractAbstract (Hide) | Slides

Only Control Effects and Dependent Types.
Youyou Cong, William J. Bowman.
Talk at the Workshop on Higher-order Programming with Effects (HOPE 2017).
Abstract | GitHub

Growing a Proof Assistant.
William J. Bowman.
Talk at the Workshop on Higher-order Programming with Effects (HOPE 2016).
Sophisticated domain-specific and user-defined notation is widely used in formal models, but is poorly supported by proof assistants. Many proof assistants support simple notation definitions, but no proof assistant enables users to conveniently define sophisticated notation. For instance, in modeling a programming language, we often define infix relations such as Γ  e : t and use BNF notation to specify the syntax of the language. In a proof assistant like Coq or Agda, users can easily define the notation for Γ  e : t, but to use BNF notation the user must use a preprocessing tool external to the proof assistant, which is cumbersome.

To support sophisticated user-defined notation, we propose to use language extension as a fundamental part of the design of a proof assistant. We describe how to design a language-extension systems that support safe, convenient, and sophisticated user-defined extensions, and how to design a proof assistant based on language extension. We evaluate this design by building a proof assistant that features a small dependent type theory as the core language and implementing the following extensions in small user-defined libraries: pattern matching for inductive types, dependently-typed staged meta-programming, a tactic-based proof language, and BNF and inference-rule notation for inductive type definitions.
AbstractAbstract (Hide) | Draft Paper | HOPE 2016 Talk (by me) | GitHub

Dagger Traced Symmetric Monoidal Categories and Reversible Programming.
William J. Bowman, Roshan P. James, and Amr Sabry.
In Proc. of the 4th Workshop on Reversible Computation (RC 2011).
Paper | Code

Talks

Do Compilers Respect Programmers?
William J. Bowman
Video | Keynote | PDF

Other

Toward Type Preserving Compilation of Coq.
William J. Bowman.
POPL 2017 Student Research Competition
Extended Abstract | Poster