Agda Implementors' Meeting XXXVII

• Program
  • Planning
  • Talks Proposals
  • Discussion Proposals
  • Code Sprint Proposals
• Organisation
  • Location
    • Suggested Way to arrive at Academia Sinica from the TPE airport
  • Registration
  • Accommodation
  • Excursion
  • Participants
• Wrap-up Notes
  • Monday, 20 Nov
  • Tuesday, 21 Nov
  • Thursday, 23 Nov
  • Friday, 24 Nov

The CompCert project produced a verified compiler for a large fragment of the C programming language. The CompCert compiler is implemented in the type-theoretic proof assistant Coq, and is fully verified: there is a proof that the semantics of the source program matches the semantics of the target program. However, full verification comes with a price: the majority of the formalization is concerned not with the runnable code of the compiler, but with the properties of its components and proofs of these properties. If we are not willing to pay the price of full verification, can we nevertheless profit from the technology of type-theoretic proof assistants to make our compilers safer and less likely to contain bugs?

In this talk, I am presenting a compiler for a small fragment of the C language using dependently-typed syntax. A typical compiler is proceeding in phases: parsing, type checking, code generation, and finally, object/binary file creation. Parsing and type checking make up the front end, which may report syntax and type errors to the user; the other phases constitute the back end that should only fail in exceptional cases. After type checking succeeded, we have to deal only with well-typed source programs, whose abstract syntax trees can be captured with the indexed data types of dependently-typed proof assistants and programming languages like Agda, Coq, Idris, Lean etc. More concisely, we shall by dependently-typed syntax refers to the technique of capturing well-typedness invariants of syntax trees. Representing also typed assembly language via dependently-typed syntax, we can write a type-preserving compiler whose type soundness is given *by construction*. In the talk, the target of compilation is a fragment of the Java Virtual Machine (JVM) enriched by some *administrative instructions* that declare the types of local variables. With JVM being a stack machine, instructions are indexed not only by the types of the local variables, but also by the types of the stack entries before and after the instruction. However for instructions that change the control flow, such as unconditional and conditional jumps, we need an additional structure to ensure type safety. Jumps are safe if the jump target has the same machine typing than the jump source. By machine typing we mean the pair of the types of the local variables and the types of the stack entries. Consequently, each label (i.e., jump target) needs to be assigned a machine type and can only be targeted from a program point with the same machine type. We then distinguish two types of labels:

• Join points, e.g., labels of statements following an if-else statement. Join points can be represented by a let binding in the abstract JVM syntax.
• Looping points, e.g., labels at the beginning of a while statement that allows back jumps to iterate the loop. Those are represented by fix (recursion).

Using dependently-typed machine syntax, we ensure that well-typed jumps do not miss. As a result, we obtain a type-preserving compiler by construction, with a good chance of full correctness, since many compiler faults already break typing invariants. Intrinsic well-typedness also allows us to write the compiler as a total function from well-typed source to typed assembly, and totality can be automatically verified by the Agda type and termination checker.

• bugfixes
  • a lot of entry-level bugs currently on the issue tracker
  • happy to help anyone interested in getting started with agda2hs, show them around the codebase, fix bugs together, etc...
• better error reporting
  • there are currently situations where agda2hs can produce invalid Haskell (e.g. when using identifiers supported by Agda, but not by Haskell)
  • these appear to the user at a later phase when invoking GHC
  • it would be nicer to catch them early on in our backend and have faster/better error messages
• new Haskell features
  • GADTs
  • extract property-based tests from (erased) proofs
• Prelude completeness
  • agda2hs comes with a port of Haskell's prelude written in Agda
    • ...but it is currently incomplete
    • ...and there are not many properties proven about these definitions
• new application for agda2hs -- simplistic barebones blockchain
  • Within IOG, there is currently some potential for using agda2hs for a blockchain ledger formalisation in Agda.
  • To begin with, I would like personally to start a prototype solution for a "toy" blockchain that will be easier to work with.
    • this would be good for newcomers to get acquainted with agda2hs and how to use it for a simple application
    • moreover, I expect a lot of bug-finding to arise from this endeavour, so the plan is to start prototyping and see where we get stuck!
• theoretical investigation, proving the compilation correct
  1. prototype featherweight Haskell and featherweight Agda (agda-core maybe?)
  2. decide on the methodology to use (piggyback on nad's work on erasure perhaps?)

In the same spirits as extensible backends (where we use Agda as a library and provide a new Haskell package), I would like to discuss the possibility for extensible frontends. For instance, `agda2hs` currently copy-pastes thousands LOC related to Emacs from the Agda codespace in order to be able to interactively call the backend from Emacs (+ possibly provide some backend-specific commands).

Another example from my own projects is the agda2train backend for generating training data for machine-learning purposes. These data cannot really be utilised in an interactive fashion (once we have a machine-learned model trained on those data), unless the backend can also provide Emacs functionality specific to this backend.

Currently backends use Agda as a library, but it would be nice to be able to dynamically provide them as plugins to an existing Agda installation.

• e.g. if I have two backends there is no easy way to use both at the same time, other than writing a new Haskell package that imports them and provides a "merged" backend
• more of a discussion than a code sprint at this stage

• discuss feasibility with Liang-Ting & Cas
• compare & contrast deriving solution (e.g. for decidable equality DecEq)

Make the prototype from AIMXXXVI (using the kind2 solver) more robust/general

• either to include more Agda datatypes and more capabilities
• ...or to use other solvers apart from `kind2`
• ...or to write a solver within Agda

This code sprint is a step towards a usable Agda inside a browser. As Agda is used as a library for implementing a language server, it is required to compile Agda into WASM. However, many parts of Agda assume it will be running on an actual OS instead of a browser. For example, a full file system does not exist and libraries cannot be imported.

We will first need to make sure that Agda can be compiled with the latest GHC WebAssembly backend.

• Name:
• Online or In person:
• Affiliation:
• If you wish to give a talk:
  • Title
  • Short Abstract (Optional)
• If you wish to suggest a talk topic:
  • Topic
  • Short Description (Optional)
• If you wish to suggest a code sprint:
  • Proposal
  • Short Description (Optional)
• Other comments:
• Will you require on-campus accommodation? (Yes / No)
  • If so, please indicate your preferred dates of stay between 18–25 Nov:
• Please indicate any special requests or dietary restrictions.