Abstracts
Metatheory of Proto-Quipper in Hybrid: Context
Relations Revisited
Amy Felty
University of Ottawa
We revisit our formalization of the metatheory of
Proto-Quipper in the Hybrid logical framework.
Proto-Quipper contains the core of Quipper, which is a
programming language designed to express quantum circuits
and allow them to be treated as data. Hybrid is a system
that is designed to support the use of higher-order
abstract syntax (also called lambda-tree syntax) for
representing and reasoning about formal systems,
implemented in the Coq Proof Assistant. Hybrid follows a
two-level approach, where a specification logic (SL) is
defined as an inductive type in Coq, and reasoning about
an object logic (OL) such as Proto-Quipper is carried out
using the SL. In this work, we adopt a linear SL, which
provides infrastructure for reasoning directly about the
linear type system of Proto-Quipper.
In two-level systems, statements of theorems often relate
two or more OL judgments, and a "context relation" is
often needed to specify the constraints between them. In
this work, we carry out a more careful study of context
relations in a linear setting. Other goals of revisiting
our formalization include: extending the use of
higher-order syntax to encode the notion of bound
variables in circuits, and improving the representation of
subtyping so that it is closer to the original formulation
of Proto-Quipper. The latter allowed us to find an error
in one of the on-paper proofs.
A Logical Framework with Higher-Order Rational (Circular) Terms
Zhibo Chen
Carnegie Mellon University
Logical frameworks provide natural and direct ways of
specifying and reasoning within deductive systems. The
logical framework LF and subsequent developments focus on
finitary proof systems, making the formalization of
circular proof systems in such logical frameworks a
cumbersome and awkward task. To address this issue, we
propose CoLF, a conservative extension of LF with
higher-order rational terms and mixed inductive and
coinductive definitions. In this framework, two terms are
equal if they unfold to the same infinite regular Böhm
tree. Both term equality and type checking are decidable
in CoLF. We illustrate the elegance and expressive power
of the framework with several small case studies.
Higher Order Mechanization of Session Typed Process Calculus
Chuta Sano
McGill University
We describe an encoding of a session typed process
calculus based on classical linear logic in the Beluga
proof assistant. Session types employ a linear type
system, where variables cannot be implicitly copied or
dropped, and therefore, most mechanizations of these
systems require modeling the context and carefully
ensuring that its variables are handled linearly. We take
advantage of (weak) higher order abstract syntax and
express the linear constraints in session types as an
additional logical predicate baked inside the usual type
judgment rules, leading to an elegant mechanization of
session typed process calculus. We prove the usual type
preservation theorem in this setting.
Layered Modal Type Theory
Jason Hu
McGill University
In this talk, we introduce a novel approach of layering to
meta-programming, which enables a modular way to extend type theories
with capability of intensional analysis. In a layered type theory, we
begin with a core type theory, e.g. simply typed lambda-calculus
(STLC), which cannot do meta-programming. Then we extend STLC with a
layer of modality. In this layer, due to the modality, we obtain the
power to do pattern matching on code of STLC. By extending more
layers, the type theory supports meta-programs with arbitrarily high
stages. We use a presheaf model to justify a 2-layered modal type
theory, giving not only a type-theoretical foundation to
meta-programming with intensional analysis, but also a concrete
normalization algorithm which can be implemented in a conventional
programming language.
Modal crash types for intermittent computing
Farzaneh Derakshan
Carnegie Mellon University
Energy Harvesting Devices (EHDs) experience arbitrary
power failures during program execution. To make progress,
programs require system support to checkpoint state and
re-execute after power failure by restoring the last saved
state. This re-execution should be ``correct/consistent",
i.e., simulated by a continuously-powered execution. We
study the logical underpinning of intermittent computing
and model checkpoint, crash, restore, and re-execution
operations as computation on Crash types. We draw
inspiration from adjoint logic and define Crash types by
introducing two adjoint modality operators to model
persistent and transient memory values of partial
(re-)executions and the transitions between them caused by
checkpoints and restoration. We define a Crash type system
for a core calculus. We prove the correctness of
intermittent systems by defining a novel logical relation
for Crash types.
Multi-modal Programming with Resource Guarantees
Clare Jang
McGill University
Various modalities have been applied to a wide range of
applications: Meta-programming, binding-time analysis,
resource availability, resource privacy, etc. However, at
the same time, it has been challenging to combine multiple
modalities into a single system because of the difficulty
and complexity of their logical behaviour. In particular,
we do not have a clear answer to how to reason about
resource availability and privacy in meta-programming,
which are essential requirements for a secure program. In
this talk, we will describe a multi-modal logical
foundation parametrized by a generic structure of various
modalities. Based on adjoint logic, this formulation
allows us to capture modalities for meta-programming,
resource availability, privacy, and combinations of those
in a single system. We show that this system is a
conservative extension to prior meta-programming systems
based on modal logic S4, yet allows more fine-grained
control over when to generate and store code. Thus, this
system provides a rich logical foundation for capturing
and reasoning about guarantees for meta-programs.
Closure Converting the Universes
Jean-Alexandre Barszcz
Université de Montréal
Type preserving closure conversion of languages with
dependent types has proved difficult. One problem is that
it requires some form of impredicativity, since a
function's free variables can belong to a universe higher
than its own. One solution developed for the Calculus of
Constructions uses a construct custom-made for closure
conversion. As an alternative, we propose a more general
construct and a new form of impredicativity based on
existential quantification over universe levels. With it,
we define a type preserving closure conversion for a
dependently-typed language with a tower of universes.
Explicit locally nameless
Vincent Archambault
Université de Montréal
The locally nameless representation of variables uses
names for free variables and de Bruijn indices for bound
variables and allows for a simpler definition of
substitution and a simpler way of weakening. We give an
explicit substitutions calculus for this representation so
it can be reliably implemented in a compiler for a
dependently typed language.
Static Prediction of Parallel Computation Graphs
Stefan Muller
Illinois Institute of Technology
Many algorithms for analyzing parallel programs, for
example to detect deadlocks or data races or to calculate
the execution cost, are based on a model variously known
as a cost graph, computation graph, or dependency graph,
which captures the parallel structure of threads in a
program. In modern parallel programs, computation graphs
are highly dynamic and depend greatly on the program
inputs and execution details. As such, most analyses that
use these graphs are either dynamic analyses or are
specialized static analyses that gather a subset of
dependency information for a specific purpose.
In this talk, I'll briefly discuss my work on graph types,
which compactly represent all of the graphs that could
arise from program execution and can be inferred from a
parallel program using a graph type system. The graph type
system introduces unique names for vertices in the graph;
uniqueness is ensured using an affine type system. One
major restriction of the existing graph type system is
that it is unable to assign types to data structures
containing, or built using, thread handles. I will present
ongoing work in which we relax this restriction by
indexing types in the graph type system with corecursive
structures of vertex names.
Bounding the Execution Cost of WebAssembly Functions
John Shortt
University of Ottawa
WebAssembly is a programming language and virtual machine
architecture that allows code to be executed in any
environment that implements a WebAssembly
runtime. WebAssembly has been formally specified using an
abstract syntax and formal semantics, and a soundness
proof of this specification has been written and
mechanized. We build on this to create a system that
determines a bound on the runtime cost of a WebAssembly
function. We show that for a broad class of real-world
programs this cost can be computed efficiently and we
develop a software tool called WANALYZE that does so. The
software tool is comprised of a set of algorithms that
perform a series of transformations on the raw WebAssembly
bytecode into forms that are more suitable for
analysis. We test WANALYZE against a suite of programs of
varying size and complexity and find that WANALYZE is able
to successfully analyze over 99.9% of the functions in
these programs at a typical rate of 5K to 13K lines of
code per second.