A Formal Treatment of Bidirectional Typing

Introduction

This is the repository for the development, including formal proofs and tex code, presented in the paper A formal treatment of bidirectional typing.

Abstract from the paper

There has been much progress in designing bidirectional type systems and associated type synthesis algorithms, but mainly on a case- by-case basis. To remedy the situation, this paper develops a general and formal theory of bidirectional typing and as a by-product of our formalism provides a verified generator of proof-relevant type synthesisers for simply typed languages: for every signature that specifies a mode- correct bidirectionally typed language, there exists a proof-relevant type synthesiser that for an input abstract syntax tree constructs a typing derivation if any, gives its refutation if not, or reports that the input does not have enough type annotations. Soundness, completeness, and mode- correctness are studied universally for all signatures, which are sufficient conditions for deriving a type synthesiser. We propose a preprocessing step called mode decoration, which helps the user to deal with missing type annotations in a given abstract syntax tree. The entire development is formalised in Agda and can be further integrated with other language- formalisation frameworks.

Repository organisation

This repository consists of the following directories and files.

• README.agda is a walkthrough of the formal implementation with mappings to the paper.
• src/ is the formal implementation in Agda.
  • src/Example/STLC.agda contains the example of simply typed lambda calculus presented in the Appendix Demonstration of the paper.
• tex/ is the tex code for the paper including all submissions, reviews, and our reponses.
  • In particular, tex/ESOP24/ contains the accepted ESOP'24 submission.
• docs/ is the listing of source code published here
• agda-stdlib/ is the Agda standard library v2.0 as a Git submodule.

Requirements

To type-check the formal implementation, you need

• Agda version 2.6.4.1

Agda

An earlier version such as 2.6.4 compatible with the standard library v2.0 may work. Should you have no Agda installed or fail to check README.agda with an earlier version of Agda, you may

• Install Agda 2.6.4.1 or
• Use the Docker image for Agda 2.6.4.1, i.e. containerised Agda.

Instructions

To browse and check this repository locally, please follow the instructions below.

0. Open a terminal emulator.

   For example, you may use the application Terminal on macOS or Windows Terminal on Windows 10 (or later).

1. Clone this repository (in the terminal)

   git clone --depth 1 --recurse-submodules --shallow-submodules https://github.com/L-TChen/BiSig.git

   This repository contains the Agda standard library as a Git submodule, so it is necessary to clone this repository with the submodule.

2. Change the working directory to the local repository

   cd [the location of your copy of this repo]

3. (Optional) If you have no Agda, you may install Docker and use containerised Agda as follow:

   docker run -it --mount type=bind,source"=${PWD}",destination=/BiSig -w /BiSig ltchentw/agda:2.6.4.1

   This command pulls the pre-built image, which contains Agda 2.6.4.1, from Docker Hub and runs the image as a container with the current working directory mounted at /BiSig/ internally.

4. Type-check the walkthrough file

   agda README.agda

   The option --safe has been specified additionally in the BiSig.agda-lib and README.agda to ensure that no definitions are postulated.

5. Finally, use an editor that supports the Agda development, such as Emacs with the Agda mode or VS Code with the extension for Agda, to play with this repo.

   If you use the docker image for Agda, then Emacs with Agda mode is already available to use inside the container.

   Hint. Start with README.agda or try to normalise the term ⊢S? in src/Example/STLC.agda.