Eastern Canada Logic and Programming Seminar 2023

Metatheory of Proto-Quipper in Hybrid: Context Relations Revisited

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

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

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

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

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

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

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

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

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

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.