## Talk abstracts

**Invited talk: Systems Programming with Dependent Types**

*Edwin Brady*

*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**

*Bob Atkey*

*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**

*Venanzio Capretta*

*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**

*Cezar Ionescu*

*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**

*Steven Keuchel*

*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**

*Josh Ko*

*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**

*Conor McBride*

*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**

*Duckki Oe*

*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**

*Brigitte Pientka*

*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**

*Maciej Pirog*

*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**

*Kai Trojahner*

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