Erasure enriches type theory with a distinction between runtime relevant and irrelevant data, allowing the compilation step to safely erase the latter. Versions of this feature are implemented by many systems, including Agda, Idris, and Rocq. We present a structural version of type theory with erasure, formulated as a second-order generalised algebraic theory (SOGAT). Erasure is encoded as a phase distinction between runtime and erased terms, in the form of a proposition that can appear in a context. This formulation has several advantages: it has models based on categories with families, is compatible with other structural features such as staging, and provides a better guideline for implementation. Through the model theory of SOGATs, we study the semantics of type theory with erasure in families of sets, which generalises to any Grothendieck topos equipped with a tiny proposition. We establish conservativity over Martin-Löf type theory (MLTT) in both phases. For code extraction, we construct a presheaf model that produces untyped lambda calculus programs and prove its correctness through gluing. Our results are formalised in Agda and we provide a toy elaborator implementation.

Typed functional programming languages like Haskell and OCaml make heavy use of the heap at run-time. This makes them largely unsuitable for systems programming, where resources are limited and programs are often expected to run on bare-metal. This paper demonstrates how a (slightly restricted) high-level, pure, functional language can be compiled to machine code which does not use the heap at all. Despite usually requiring a heap at run-time, features such as higher-order functions, polymorphism and typeclasses are all supported by the surface language. This is made possible through partial evaluation [12]: by carefully reducing the program at compile-time, we can eliminate these highlevel features entirely, resulting in a residual program which is trivial to compile to stack-based machine code. This paper describes the operation of this partial evaluator, justifies its design, and introduces a novel type system which guarantees that the partial evaluator will always succeed in removing all heap-using features.

Inductive families provide a convenient way of programming with dependent types. Yet, when it comes to compilation, their default linked-tree runtime representations, as well as the need to convert between different indexed views of the same data, can lead to unsatisfactory runtime performance. In this paper, we introduce a language with dependent types, and inductive families with customisable representations. Representations are a version of Wadler's views, refined to inductive families like in Epigram, but with compilation guarantees: a represented inductive family will not leave any runtime traces behind, without relying on heuristics such as deforestation. This way, we can build a library of convenient inductive families based on a minimal set of primitives, whose re-indexing and conversion functions are erased during compilation. We show how we can express optimisation techniques such as representing Nat-like types as GMP-style big integers, without special casing in the compiler. With dependent types, reasoning about data representations is also possible through a provided modality. This yields computationally irrelevant isomorphisms between the original and represented data.

We present a new design for an algebraic simplification library structured around concepts from universal algebra: theories, models, homomorphisms, and universal properties of free algebras and free extensions of algebras. The library's dependently typed interface guarantees that both built-in and user-defined simplification modules are terminating, sound, and complete with respect to a well-specified class of equations. We have implemented the design in the Idris 2 and Agda dependently typed programming languages and shown that it supports modular extension to new theories, proof extraction and certification, goal extraction via reflection, and interactive development.

We present an automated framework for solidifying the cohesion between software specifications, their dependently typed models, and implementation at compile time. Model Checking and type checking are currently separate techniques for automatically verifying the correctness of programs. Using Property Based Testing (PBT), Indexed State Monads (ISMs), and dependent types, we are able to model several interesting systems and network protocols, have the type checker verify that our implementation behaves as specified, and test that our model matches the specification's semantics; a step towards combining model and type checking.

Language Workbenches offer language designers an expressive environment in which to create their DSLs. Similarly, research into mechanised meta-theory has shown how dependently typed languages provide expressive environments to formalise and study DSLs and their meta-theoretical properties. But can we claim that dependently typed languages qualify as language workbenches? We argue yes! We have developed an exemplar DSL called Velo that showcases not only dependently typed techniques to realise and manipulate IRs, but that dependently typed languages make fine language workbenches. Velo is a simple verified language with well-typed holes and comes with a complete compiler pipeline: parser, elaborator, REPL, evaluator, and compiler passes. Specifically, we describe our design choices for well-typed IRs design that includes support for well-typed holes, how CSE is achieved in a well-typed setting, and how the mechanised type-soundness proof for Velo is the source of the evaluator.

Dependent types allow us to express precisely what a function is intended to do. Recent work on Quantitative Type Theory (QTT) extends dependent type systems with linearity, also allowing precision in expressing when a function can run. This is promising, because it suggests the ability to design and reason about resource usage protocols, such as we might find in distributed and concurrent programming, where the state of a communication channel changes throughout program execution. As yet, however, there has not been a full-scale programming language with which to experiment with these ideas. Idris 2 is a new version of the dependently typed language Idris, with a new core language based on QTT, supporting linear and dependent types. In this paper, we introduce Idris 2, and describe how QTT has influenced its design. We give examples of the benefits of QTT in practice including: expressing which data is erased at run time, at the type level; and, resource tracking in the type system leading to type-safe concurrent programming with session types.

We report about the ongoing development of a library for dependently-typed programming with computations in index positions. Such indexing leads to notoriously difficult unification problems. Here we combine the established ‘fording’ technique (§2) with our work on free extensions (frex) developed for staged optimisation in OCaml and Haskell [22]. In brief, fording improves the judgmental-propositional communication channel for equations while Frex provides an extensible collection of algebraic solvers for discharging these equations. We present our design in Idris2; we would like to pursue similar development in other type theories.

Idris' Effects library demonstrates how to embed resource dependent algebraic effect handlers into a dependently typed host language, providing run-time and compile-time based reasoning on type-level resources. Building upon this work, Resources is a framework for realising Embedded Domain Specific Languages (EDSLs) with type systems that contain domain specific substructural properties. Differing from Effects, Resources allows a language’s substructural properties to be encoded within type-level resources that are associated with language variables. Such an association allows for multiple effect instances to be reasoned about autonomically and without explicit type-level declaration. Type-level predicates are used as proof that the language’s substructural properties hold. Several exemplar EDSLs are presented that illustrates our framework’s operation and how dependent types provide correctness-by-construction guarantees that substructural properties of written programs hold.

Session Types offer a typing discipline that allows protocol specifications to be used during type-checking, ensuring that implementations adhere to a given specification. When looking to realise global session types in a dependently typed language care must be taken that values introduced in the description are used by roles that know about the value. We present Sessions, a Resource Dependent EDSL for describing global session descriptions in the dependently typed language Idris. As we construct session descriptions the values parameterising the EDSLs' type keeps track of roles and messages they have encountered. We can use this knowledge to ensure that message values are only used by those who know the value. Sessions supports protocol descriptions that are computable, composable, higher-order, and value-dependent. We demonstrate Sessions expressiveness by describing the TCP Handshake, a multi-modal server providing echo and basic arithmetic operations, and a Higher-Order protocol that supports an authentication interaction step.

Implementing security protocols correctly is hard; verifying them is too. However, we also implement them in languages different to those we verify them in. With dependent types we can reason on software with greater precision and link specifications to implementations. In this talk we examine how state-of-the-art programming language research can help us to verify and implement protocols in the same language.

The conference proceeding CICM 2018 focus on computer based systems for computer algebra, automated deduction, and mathematical publishing as well as novel user interfaces. The conference consisted of three tracks: Mathematical knowledge management, calculemus, and systems and projects.

Verification projects on industrial code have required reasoning about functional programming constructs in Java 8. General functional programming requires reasoning about how the specifications of function objects that are inputs to a method combine to produce the specifications of output function objects. This short paper describes our in-progress experience in adapting prior work (Kassios & Müller) to Java 8, JML, OpenJML, and to ACSL++, a specification language for C++ built on ACSL.

Our overall research goal is to develop ways to systematically relate the non-functional properties of a program, such as its time and energy usage, directly to its source code. This will enable source-level reasoning about important software properties, enabling them as first-class citizens. Unfortunately, as processors and compiler optimizations continue to increase in complexity, so modelling such properties is becoming increasingly difficult. Even simple high-level language constructs can be difficult to understand and may require a detailed understanding of the compilation process, ISA and microarchitectural details such as cache, pipeline, memory layout and memory buffers. To exemplify the problem, consider a simple multiplication in C: y = x * 5. With no optimization on an x86 machine, the compiler might produce a simple imul instruction; however, an optimised version might be lea rcx, [rax+rax*4]. This may change which hardware components are used, and so have an impact on execution time, energy usage and other properties. In this paper, we propose to use a type-directed, statistical approach. We aim to mitigate error by developing a mechanism for mechanically reasoning about both the accuracy and the confidence of a probabilistic cost (time,

We present a computer-checked generic implementation for solving finite-horizon sequential decision problems. This is a wide class of problems, including inter-temporal optimizations, knapsack, optimal bracketing, scheduling, etc. The implementation can handle time-step dependent control and state spaces, and monadic representations of uncertainty (such as stochastic, non-deterministic, fuzzy, or combinations thereof). This level of genericity is achievable in a programming language with dependent types (we have used both Idris and Agda). Dependent types are also the means that allow us to obtain a formalization and computer-checked proof of the central component of our implementation: Bellman's principle of optimality and the associated backwards induction algorithm. The formalization clarifies certain aspects of backwards induction and, by making explicit notions such as viability and reachability, can serve as a starting point for a theory of controllability of monadic dynamical systems, commonly encountered in, e.g., climate impact research.

Modern software systems rely on communication; for example, mobile applications communicating with a central server, distributed systems coordinating a telecommunications network, or concurrent systems handling events and processes in a desktop application. However, reasoning about concurrent programs is hard since we must reason about each process and the order in which communication might happen between processes. In this paper, I describe a type-driven approach to implementing communicating concurrent programs using the dependently typed programming language Idris. I show how the type system can be used to describe resource access protocols (such as controlling access to a file handle) and verify that the programs correctly follow those protocols. Finally, I show how to use the type system to reason about the order of communication between concurrent processes, ensuring that each end of a communication channel follows a defined protocol.

One difficulty with reasoning and programming with dependent types is that proof obligations arise naturally once programs become even moderately sized. For example, implementing an adder for binary numbers indexed over their natural number equivalents naturally leads to proof obligations for equalities of expressions over natural numbers. The need for these equality proofs comes, in intensional type theories, from the fact that the propositional equality enables us to prove as equal terms that are not judgementally equal, which means that the typechecker can’t always obtain equalities by reduction. As far as possible, we would like to solve such proof obligations automatically. In this paper, we show one way to automate these proofs by reflection in the dependently typed programming language Idris. We show how defining reflected terms indexed by the original Idris expression allows us to construct and manipulate proofs. We build a hierarchy of tactics for proving equivalences in semi-groups, monoids, commutative monoids, groups, commutative groups, semi-rings and rings. We also show how each tactic reuses those from simpler structures, thus avoiding duplication of code and proofs.

Modern software systems rely on communication, for example mobile applcations communicating with a central server, distributed systems coordinaing a telecommunications network, or concurrent systems handling events and processes in a desktop application. However, reasoning about concurrent prgrams is hard, since we must reason about each process and the order in which communication might happen between processes. In this paper, I describe a type-driven approach to implementing communicating concurrent programs, using the dependently typed programming language Idris. I show how the type system can be used to describe resource access protocols (such as controlling access to a file handle) and verify that programs correctly follow those prtools. Finally, I show how to use the type system to reason about the order of communication between concurrent processes, ensuring that each end of a communication channel follows a defined protocol.

Many programming languages and proof assistants are defined by elaboration from a high-level language with a great deal of implicit information to a highly explicit core language. In many advanced languages, these elaboration facilities contain powerful tools for program construction, but these tools are rarely designed to be repurposed by users. We describe elaborator reflection , a paradigm for metaprogramming in which the elaboration machinery is made directly available to metaprograms, as well as a concrete realization of elaborator reflection in Idris, a functional language with full dependent types. We demonstrate the applicability of Idris’s reflected elaboration framework to a number of realistic problems, we discuss the motivation for the specific features of its design, and we explore the broader meaning of elaborator reflection as it can relate to other languages.

Modern software is often designed to run on a virtual machine, such as the JVM or .NET’s CLR. Increasingly, even the web browser is considered a target platform with the Javascript engine as its virtual machine. The choice of programming language for a project is therefore restricted to the languages which target the desired platform. As a result, an important consideration for a programming language designer is the platform to be targetted. For a language to be truly cross-platform, it must not only support different operating systems (e.g. Windows, OSX and Linux) but it must also target different virtual machine environments such as JVM, .NET, Javascript and others. In this paper, I describe how this problem is addressed in the Idris programming language. The overall compilation process involves a number of intermediate representations and Idris exposes an interface to each of these representations, allowing back ends for different target platforms to decide which is most appropriate. I show how to use these representations to retarget Idris for multiple platforms, and further show how to build a generic foreign function interface supporting multiple platforms.