An Investigation of Kripke-style Modal Type Theories

This homepage contains the investigation of properties of Kripke-style modal type theories, normalization in particular.

Please find the technical report for more detailed development. Most of our development has been mechanized in safe Agda with standard extensions. The normalization algorithm for our dependent type theory, Mint is extracted and can be executed in Haskell.

Papers

  1. Jason Z. S. Hu and Brigitte Pientka. A Categorical Normalization Proof for the Modal Lambda-Calculus (MFPS 22)

    See the code

  2. Jason Z. S. Hu, Junyoung Jang and Brigitte Pientka. Normalization by Evaluation for Modal Dependent Type Theory (JFP 23)

    See the code

Installing Agda

It is recommended to build Agda from source. To do so, one would need to install stack. This can be done via

curl -sSL https://get.haskellstack.org/ | sh

Then the following script will use stack to install Agda in ~/.local/bin/.

git clone https://github.com/agda/agda
cd agda
git checkout release-2.6.2.2
cp stack-8.4.4.yaml stack.yaml # choose your favourite Haskell version
stack install # it is going to take a while
cp ~/.local/bin/agda ~/.local/bin/agda-2.6.2.2
cp ~/.local/bin/agda-mode ~/.local/bin/agda-mode-2.6.2.2

If Agda does not run, please check to make sure it is in your PATH.