Highly-Assured PLDI using Dependent Types.

These notes complement my contributed talk at SPLV ’26. The course, entitled: Highly-Assured Programming Language Design and Implementation using Dependent Types.

The contributed talks will be over three sessions, in which we will introduce students to mechanising a simple programming language that combines core features from both functional and imperative languages.

The language of instruction will be Idris, and more information about installing the language is available online.

Although we do not require students to have a background in dependently-typed programming, or functional programming, we outline some high-level guides and links to reference material within these notes.

Please send comments and questions to Jan de Muijnck-Hughes (WWW).

Aims

The lecture series has the following high-level learning objectives:

1. provide students with a grounding in mechanised verification of programming language and type system design using dependent types;
2. show how to (re)utilise mechanised proofs of type-safety and type checking to form the core of a working language implementation;

To support student learning, we will frame the entire lecture series towards giving students the ability to realise a fully specified language: ‘Olaf’. The lecture series itself will concentrate on a smaller complete subset called ‘Ola’.

More information about ‘Olaf & Ola’ is available.

‘Take-home’ exercises will be provided that complement the lecture material, and further guide students towards realising Olaf in their own time.

In addition, we will provide a project stub containing a partial implementation of Olaf that students can use as a base project to complete.

These notes will provide the full specification and the exercises themselves.

Student Assumptions

The language of instruction will be Idris, and more information about installing the language is available online.

Although we do not require students to have a background in dependently-typed programming, or functional programming, we outline some high-level guides and links to reference material within these notes.

Learning Outcomes

The learning outcomes are such that after the course, students will be able to:

1. discuss, explain, and illustrate the benefits and restrictions of highly-assured programming language design and implementation;

2. associate formal specifications with dependently-typed representations;

3. create the mechanised components for a highly-assured language implementation in Idris:

   • imperative languages with typed references;
   • well-shaped abstract syntax trees;
   • intrinsically-typed intermediate representations for terms;
   • type-safe evaluation of terms; and
   • sound and complete elaboration of core terms from abstract syntax trees;

Topics

This contributed talk is split into three topics, and each topic should correspond to a reasonable chunk of learning. Each subsection, within each topic, should represent some ‘bitesized’ learning.

We will guide you through the basics, and provide some miniexercises to help stimulate your learning.

Lecture 1 Intrinsically-Typed Encoding of Terms

In which we will discuss the construction of core term representations that are intrinsically-typed, ensuring that only well-typed terms (including variables) are constructed. We will also show efficient encoding of nameless representation of binders.

Lecture 2 Type-Safe Evaluation of Terms

In which we will discuss type-safe evaluation of terms using using definitional interpreters, capturing our language’s evaluation as small-step operational semantics. As Olaf is imperative with a heap, We will also introduce working with intrinsically-typed heaps.

Lecture 3 Correct-by-Construction Elaboration of Syntax into Terms

In which we will discuss the mechanisation, as well as proving soundness and completeness, of type checking, We will see how dependent types enables our proposition for type-checking informs the construction of a working type checker that produces intrinsically typed terms.

Olaf

To support student learning, we will frame the entire lecture series towards giving students the ability to realise a fully specified language: ‘Olaf’. The lecture series itself will concentrate on a smaller complete subset called ‘Ola’.

More information about ‘Olaf & Ola’ is available.

‘Take-home’ exercises will be provided that complement the lecture material, and further guide students towards realising Olaf in their own time.

Git Repository

In addition, we will provide a project stub containing a partial implementation of Olaf that students can use as a base project to complete.

These notes will provide the full specification and the exercises themselves.

Thanks

Thanks to Bob Atkey for delivering a set of very impressive interactive notes for CS208. I have stolen many a good idea from them!