Tog⁺

Tog⁺ (pronounced tog-tee) is a prototype of a dependent type checker using twin types.

It is a variant/extension of Tog

Short technical description:
Víctor López Juan, Nils Anders Danielsson. Practical Dependent Type Checking Using Twin Types Paper (Accepted at TyDe'20)

Extended description:
Víctor López Juan, Practical Unification for Dependent Type Checking Licentiate thesis (October 2, 2020)

Source code releases

Compilation and usage instructions

  1. Download the latest release and unpack.
  2. Open the directory in a terminal/command-line prompt.

  3. Download and install stack

    In Unix-y sytems:

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

    For Windows systems and others, check the Stack user manual.

  4. In the directory containing the README.md file, run:

    stack install alex happy
stack build

    This will take a while.

  5. To run Tog⁺, use:

    stack exec -- tog [OPTIONS] [FILE]

    Use --help for a list of possible flags. 

    stack exec -- tog --help

Examples

The examples/ directory of the release contains some examples and benchmarks:

To run them, open the folder containing the README.md file in a terminal, after having compiled Tog⁺, and run:

stack exec tog -- [OPTIONS] [FILE]

…where [FILE] is the path to one of the above files, and [OPTIONS] corresponds to one of the following configurations:

For instance, when running the Setoid example from the main directory:

stack exec tog -- --synEquality 2 --physicalEquality --solver W --noCheckElaborated --fastElaborate --termType HC4 examples/Language_test6_Setoid.agda

To compare with Agda (tested with v2.6.0.1), install Agda and run:

agda -iexamples -iagda-prelude --type-in-type --without-K --no-termination-check --ignore-interfaces --no-positivity-check [FILE]

Helper scripts

Alternatively, if you are in a Unix-y system, you can run the examples using one of the included shell scripts.

These scripts also enable the “-s” flag in the Haskell RTS so that CPU and memory usage statistics will be output.