Invited talk: Systems Programming with Dependent Types
Abstract: Systems software, such as an operating system or a network stack, underlies everything we do on a computer, whether that computer is a desktop machine, a server, a mobile phone, or any embedded device. It is therefore vital that such software operates correctly in all situations. In recent years, dependent types have emerged as a promising approach to ensuring program correctness using languages and verification tools such as Agda and Coq. However, these tools operate at a high level of abstraction and so it can be difficult to map these verified programs to efficient low level code, working with bit-level operations and interacting directly with system services.
In this talk I will describe Idris, a dependently typed programming language implemented with systems programming in mind. I will show how it may be used to implement programs which interact safely with the operating system, in particular how to give precise APIs for verifiable systems programming with external C libraries such as the POSIX socket library and OpenSSL.Reifying Parametricity
Abstract: I'll talk about a method for reifying parametricity principles for a sub-theory of a larger type theory. For instance, for the simply-typed lambda-calculus over a single base type inside some Martin-Lof type theory, one has a new construct:
param : (Γ : Ctxt) →
(τ : Ty) →
(x : (α : Set) → ctxt-sem Γ α → ty-sem τ α) →
(α : Set) →
(Φ : α → Set) →
(γ : ctxt-sem Γ α) →
ctxt-pred Γ α Φ γ →
ty-pred τ α Φ (x α γ)
where Ctxt is the type of simply-typed contexts, Ty is the type of simple types, ctxt-sem and ty-sem embed these in the outer theory, and ctxt-pred, ty-pred describe the (unary) relational lifting of contexts and types. The idea is that "param Γ τ e" reduces to a proof of the abstraction theorem for this type. Thus many theorems for free can be proved inside a given theory.
This construct is more powerful than the translation-based technique proposed by Bernardy, since we are able to quantify over all types that we wish to deduce parametricity principles for.
I will describe an implementation technique for this construct, based on normalisation by evaluation, and also report on progress towards a proof of correctness.The Polymorphic Representation of Induction-recursion
Abstract: Inductive-recursive definitions originated as a way of defining universes in type theory. They turn out to be useful in other contexts, like the definition of data types with recursive constraints and the characterisation of general recursion in a total setting. In fact, they are very common in algorithmics, although this fact is not often noticed. Many advanced data structures are defined as inductive types, often trees, with side conditions guaranteeing their correctness and efficiency. these conditions are recursively defined on the data itself. I will illustrate this by showing how leftist heaps, an optimal implementation of priority queues, are in fact an inductive-recursive type. If these definitions are not provided by our type theory, we must find a way to encode them. In a polymorphic lambda calculus, we can define them by universally quantifying over the type and the functions on it. This idea can be abstracted and we can see inductive-recursive structures as the initial objects of a comma category. I will illustrate this in the specific case of leftist trees.Dependently-typed Programming in Economic Modelling
Abstract: Economic models are often used to estimate the first-order consequences of policies, for example in the context of investments in green energy, or carbon taxes. Most of these models work by computing an ``equilibrium'', but there are many kinds of equilibria in economic theory and their precise nature can puzzle the non-specialist. We use Martin-LÃ¶f type theory to express the relationships between several such equilibria: Pareto, Walrasian, Nash, and correlated Nash. The Agda implementation can be seen as a tool for choosing and assembling the correct components for computing the desired kind of equilibrium.Generic Programming with Binders and Scope
Abstract: In this talk we present a datatype-generic approach to syntax with variable binding. A universe specifies the the binding and scoping structure of languages, including binders that bind multiple variables as well as sequential and recursive scoping. Two interpretations of the universe are given: one based on parametric higher-order abstract syntax and one on well-scoped de Bruijn indices. We show how to generically convert from the former to the latter and present generic operations such as capture-avoiding substitutions on the de Bruijn representations.Modularising Inductive Families
Abstract: Dependently typed programmers are encouraged to use inductive families to integrate constraints with data construction. Different constraints are used in different contexts, leading to different versions of datatypes for the same data structure. Modular implementation of common operations for these structurally similar datatypes has been a longstanding problem. We propose a datatype-generic solution based on McBride's datatype ornaments, exploiting an isomorphism whose interpretation borrows ideas from realisability. Relevant properties of the operations are separately proven for each constraint, and after the programmer selects several constraints to impose on a basic datatype and synthesises an inductive family incorporating those constraints, the operations can be routinely upgraded to work with the synthesised inductive family.Formally Comparing Approaches to Datatype-generic Programming, using Agda
José Pedro Magalhães
Abstract: Datatype-generic programming increases program abstraction and reuse by making functions operate uniformly across different types. To reach this goal, the common structure of inductive datatypes is exploited. Many approaches to generic programming have been proposed over the years, most of them for Haskell, but recently also for dependently typed languages such as Agda. Different approaches vary in expressiveness, ease of use, and implementation techniques.
Some work has been done in comparing the different approaches informally, by looking at example code or comparing lists of features. However, to our knowledge there have been no attempts to formally prove relations between different approaches. On the other hand, it is relatively obvious that some approaches subsume others, sometimes sacrificing ease of use for increased expressiveness. A constructive proof of inclusion of an approach in another can be used to convert between approaches, potentially reducing code duplication between different approaches. Furthermore, such proofs help in providing a clear picture of the potential of each approach, especially in relating different generic views and their expressiveness.
We thus present a formal comparison between several approaches to generic programming by encoding them in Agda and then establishing theorems that relate the approaches to each other.Crude but Effective Stratification
Abstract: I propose a bidirectional type system for a dependent type theory with a predicative hierarchy of universes. Set0 : Set1 : Set2 ... Cumulativity is added via structural subtyping, and a simple form of explicit universe polymorphism is induced by the property that judgments are preserved by constant "upward" displacements. What you build for Set0, you can shift to Set1, and so on. I shall explore how much is possible in a simple system without universe variables or constraint solving and draw comparisons with Coq, Agda and Lego.versat: A Verified Modern SAT Solver
Abstract: "versat" is a formally verified SAT solver incorporating the essential features of modern SAT solvers, including clause learning, watched literals, optimized conflict analysis, non-chronological backtracking, and backjumping. Unlike previous related work on SAT-solver verification, versat is implemented using efficient low-level data structures like mutable arrays for clauses and other solver state, and machine integers for literals. The implementation and proofs are written in GURU, a verified-programming language. The soundness of versat is statically verified: whenever the solver reports a set of input clauses unsatisfiable, then there exists a resolution proof of the empty clause from those input clauses. This proof is not constructed at run-time. Rather, our verification confirms statically that it exists, for all formulas versat reports unsatisfiable. Dependent types are used not only for the consistency and correctness of the resolution proof, but also for static bounds-checking of array accesses and passing along various invariants across functions. An empirical evaluation shows that versat can solve SAT problems on the modern scale.Covering all Bases: Design and Implementation of a Coverage Checker for Contextual Objects
Abstract: We consider the question: Does a set of patterns cover all objects of a given type? This is straightforward in the simply-typed setting, but undecidable in the presence of dependent types. We discuss the question in the setting of Beluga, a dependently-typed programming and reasoning environment which supports programming with contextual objects and contexts. We describe the design and implementation of a coverage algorithm for Beluga programs and provide an in-depth comparison to closely related systems such as Twelf and Delphin. Our experience with coverage checking Beluga programs shows that many problems and difficulties are avoided. Beluga's coverage algorithm has been used on a wide range of standard examples, including the POPLmark challenge and examples from the Twelf repository.Interactive Programs in Coq, Coinductively
Abstract: In this talk I present a model of the IO monad which allows to write interactive, possibly non-terminating programs in Coq. The execution of such a program in an initial state of the world is represented by a stream of all the subsequent states that are present during the execution. To reconcile the monad laws and the Coq requirement of productivity of the execution, all monadic expressions are, by construction, in a particular (but still flexible) shape.Qube: Array Programming with Dependent Types
Abstract: Array programming languages such as APL, or MATLAB use multidimen- sional arrays as the primary data structures. Rank-generic array operations are applicable to vectors, matrices, and other arrays with an even higher number of axes. This flexibility introduces structural constraints between the operands that can neither be expressed nor statically enforced with con- ventional type systems. For example, the APL inner product computes vector-vector, vector-matrix, matrix-vector, matrix-matrix products and so forth, provided that both arrays have at least one axis and that the last axis of the first array is as long as the first axis of the second array.
This talk presents QUBE, a functional array programming language that employs dependent types to intuitively express such constraints. As de- pendent types distinguish between arrays of different shapes, function sig- natures precisely specify the allowed arguments and how the type of the function's result depends on the arguments. For example, the type of the inner product in QUBE is:val ip : m:nat. n:nat. r:(natvec m). s:nat. t:(natvec n). [int|r,[s]]. [int|[s],t] → [int|r,t]
The type checker uses the fine-grained types to verify that functions are only applied to legitimate arguments and to statically rule out array bound- ary violations. Technically, type checking proceeds by converting the con- straints to be checked into first-order formulas that are verified by an auto- matic theorem prover for the Satisfiability Modulo Theories (SMT) problem.
The QUBE compiler exploits the dependent types to compile array pro- grams into efficient executables, even when the array shapes are not compile- time constants. Since QUBE programs do not need to perform dynamic checks such as shape checks or array boundary checks, multidimensional arrays are represented as mere sequences of data without additional type tags or shape descriptors.