# Papers

Toward Type Preserving Compilation of Coq.

William J. Bowman.

POPL 2017 Student Research Competition

Extended Abstract |
Poster

Growing a Proof Assistant.

William J. Bowman.

Unpublished

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 |
PDF ((Very preliminary) draft as of Apr 20, 2017) |
HOPE 2016 Presentation
GitHub

Fully Abstract Compilation via Universal Embedding.

Max New, William J. Bowman, Amal Ahmed.

To appear in Proc. of the 21st 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, Amal Ahmed.

In Proc. of the 20th 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 |
PDF (Author-Izer) |
PDF (Preprint) |
Technical Appendix
(Draft) |
ICFP 2015 Presentation

Profile-Guided Meta-Programming.

William J. Bowman, Swaha Miller, Vincent St-Amour, and R. Kent Dybvig.

In Proc. of the 36th 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—

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

PDF |
Code