CMTT: Contextual Modal Type Theory

This is a prototype implementation of Contextual Modal Type Theory (CMTT), developed for academic use. It includes a bidirectional typechecker and an interpreter, along with a REPL interface for loading and evaluating CMTT programs.

Features

• A bidirectional typechecker for CMTT
• A call-by-value interpreter
• A REPL for interactive use
• A collection of example programs in the examples/ directory

Disclaimer

This is a research prototype, developed to support formal and experimental work with CMTT. It is not intended for production use. Error handling is minimal, and the focus is on clarity and fidelity to the theory.

Installation

You’ll need GHC and Cabal. Then:

    git clone https://github.com/kevinlopaq/cmtt
    cd cmtt
    cabal build

Usage

Run the REPL with:

    cabal run cmtt

Inside the REPL, the following commands are available:

• typecheck <filename> — Typeheck a program in the file
• run <filename> — Typecheck and evaluate the file
• parse <filename> — Parse and print the abstract syntax tree
• quit — Exit the REPL

Directory Overview

• src/ — Parser, typechecker, interpreter
• Main.hs — REPL entry point
• examples/ — Sample programs

References and Related Work

Nanevski, A., Pfenning, F., & Pientka, B. (2008). Contextual Modal Type Theory.

Pfenning, F., & Davies, R. (2001). A Judgmental Reconstruction of Modal Logic.

mtt-lang: An implementation of Pfenning and Davies' modal type theory.

License

MIT License