William J. Bowman | Home

William J. Bowman is an Assistant Professor of computer science in the Software Practices Lab at University of British Columbia. Broadly speaking, he is interested in making it easier for programmers to communicate their intent to machines, and preserving that intent through 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.

Coordinates

• In Cyberspace:

  As a person or researcher:

  As UBC faculty:

  wilbowma

• In Space:

  ICICS/CS Building Room 389

  201 Main Mall

  Vancouver, BC V6T 1Z4 Canada

• In Time: My Free/Busy Calendar

Group

• Paulette Koronkevich – MSc (toward PhD)

  Dependent-type-preserving compilation.

• Adam Geller – PhD.

  Index-typed Web Assembly for safety and performance.

• Jonathan Chan – MSc.

  Sized types for Coq.

• Aarti Kashyap – PhD.

  Secure compilation for ISA semantics.

  Co-supervised with Margo Seltzer.

• Lily Bryant – MSc (toward PhD)

  Dependent-type-preserving compilation.

• Junfeng Xu – MSc.

  Formal semantics of PL meta-notation.

  Co-supervised with Margo Seltzer.

• Ramon Rakow – BSc.

  Dependent-type-preserving compilation with Paulette.

• Justin Frank – Post-BSc.

  Index-typed Web Assembly for safety and performance with Adam.

• "Michael" Yufeng Li – BSc.

  Sized types for Coq with Jonathan.

Manuscripts

Practical Sized Types for Coq.

Jonathan Chan and William J. Bowman

2019.

AbstractAbstract (Hide) | arXiv | Artifact | GitHub

Compiling Dependent Types Without Continuations.

William J. Bowman and Amal Ahmed

2019.

AbstractAbstract (Hide) | Proofs incomplete, but draft available on request.

Conference Publications

Dependent Type Systems as Macros.

Stephen Chang, Michael Ballantyne, Milo Turner, William J. Bowman

To appear In Proc. of the Symposium on Principles of Programming Languages (POPL 2020).

AbstractAbstract (Hide) | Paper | Artifact | GitHub (Turnstile+) | GitHub (Cur)

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).

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)

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)

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)

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).

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).

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).

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

Cur: Designing a Less Devious Proof Assistant

William J. Bowman

AbstractAbstract (Hide) | Video | Slides (ODP) | Slides (Google Slides) | Demo Code | Cur GitHub

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

Dissertation

Compiling with Dependent Types.

William J. Bowman.

Northeastern University, Feb. 2019.

AbstractAbstract (Hide) | PDF | Slides (keynote) | Slides (PDF)