# Publications

## Manuscripts

Practical Sized Types for Coq.

Jonathan Chan and William J. Bowman

2019.

Termination of recursive functions and productivity of corecursive functions are important for maintaining logical consistency in proof assistants. However, contemporary proof assistants, such as Coq, rely on syntactic criteria that prevent users from easily writing obviously terminating or productive programs, such as quicksort. This is troublesome, since there exist theories for type-based termination- and productivity-checking.

In this paper, we present a design and implementation of sized type checking and inference for Coq. We extend past work on sized types for the Calculus of (Co)\-Inductive Constructions (CIC) with support for global definitions found in Gallina, and extend the sized-type inference algorithm to support completely unannotated Gallina terms. This allows our design to maintain complete backwards compatibility with existing Coq developments. We provide an implementation that extends the Coq kernel with optional support for sized types.Abstract |
arXiv |
Artifact |
GitHub

Compiling Dependent Types Without Continuations.

William J. Bowman and Amal Ahmed

2019.

Programmers rely on dependently typed languages, such as Coq, to machine-verify
high-assurance software, but get no guarantees after compiling or when linking
after compilation.
We could provide guarantees after compiling and linking by building
type-preserving compilers, which preserve specifications encoded
in types and use type checking to verify code after compilation and to ensure
safety when linking with unverified code.
Unfortunately, standard type-preserving translations do not scale to dependently
typed languages for two key reasons: assumptions valid in simpler type systems
no longer hold, and checking dependent types relies strongly on the syntax
of programs, which compilers change.

We extend the A-normal form (ANF) translation—

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

We present Turnstile+, a high-level, macros-based metaDSL for building
dependently typed languages.
With it, programmers may rapidly prototype and iterate on the design of new
dependently typed features and extensions.
Or they may create entirely new DSLs whose dependent type “power” is tailored
to a specific domain.
Our framework’s support of language-oriented programming also makes it suitable
for experimenting with systems of interacting components, e.g., a proof
assistant and its companion DSLs.
This paper explains the implementation details of Turnstile+, as well as how it
may be used to create a wide-variety of dependently typed languages, from a
lightweight one with indexed types, to a full spectrum proof assistant, complete
with a tactic system and extensions for features like sized types and SMT
interaction.Abstract |
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).

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

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—

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.

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—

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.Abstract |
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—

## 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.Abstract |
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.Abstract |
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

Dijkstra said that our tools can have a profound and devious influence on our
thinking. I find this especially true of modern proof assistants, with "devious"
out-weighing "profound". Cur is an experiment in design that aims to be less
devious. The design emphasizes language extension, syntax manipulation, and DSL
construction and integration. This enables the user to be in charge of how they
think, rather than requiring the user to contort their thinking to that of the
proof assistant. In this talk, my goal is to convince you that you want similar
capabilities in a proof assistant, and explain and demonstrate Cur’s attempt at
solving the problem.Abstract
Video |
Slides (ODP) |
Slides (Google Slides) |
Demo Code

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.

Dependently typed languages have proven useful for developing large-scale fully
verified software, but we do not have any guarantees after compiling that
verified software.
A verified program written in a dependently typed language, such as Coq, can be
type checked to ensure that the program meets its specification.
Similarly, type checking prevents us from importing a library and
violating the specification declared by its types.
Unfortunately, we cannot perform either of these checks after compiling a
dependently typed program, since all current implementations erase types before
compiling the program.
Instead, we must trust the compiler to not introduce errors into the
verified code, and, after compilation, trust the programmer to never introduce
errors by linking two incompatible program components.
As a result, the compiled and linked program is
not verified—

In this dissertation, I develop a theory for preserving dependent types through
compilation so that we can use type checking after compilation to check that no
errors are introduced by the compiler or by linking.
Type-preserving compilation is a well-known technique that has been used to
design compilers for non-dependently typed languages, such as ML, that
statically enforce safety and security guarantees in compiled code.
But there are many open challenges in scaling type preservation to dependent
types.
The key problems are adapting syntactic type systems to interpret low-level
representations of code, and breaking the complex mutually recursive structure
of dependent type systems to make proving type preservation and compiler
correctness feasible.
In this dissertation, I explain the concepts required to scale type preservation
to dependent types, present a proof architecture and language design that
support type preservation, and prove type preservation and compiler correctness
for four early-stage compiler translations of a realistic dependently typed
calculus.
These translations include an A-normal form (ANF), a continuation-passing style
(CPS), an abstract closure conversion, and a parametric closure conversion
translation.