Thorin 1.9.0
The Higher ORder INtermediate representation

Support Documentation Discord
License License
Requirements CMake C++ LLVM/Clang Submodules
Tests Linux Windows MacOS Doxygen

Thorin is an extensible compiler intermediate representation that is based upon the Calculus of Constructions (CoC). This means:

In contrast to other CoC-based program representations such as Coq or Lean, Thorin is not a theorem prover but focuses on generating efficient code. For this reason, Thorin explicitly features mutable state and models imperative control flow with continuation-passing style (CPS).

You can use Thorin either via it's C++-API or the command-line utility.


If you have a GitHub account setup with SSH, just do this:

git clone --recurse-submodules

Otherwise, clone via HTTPS:

git clone --recurse-submodules

Then, build with:

cd thorin2
mkdir build
cmake -S . -B build -DCMAKE_BUILD_TYPE=Debug
cmake --build build -j $(nproc)

For a Release build simply use -DCMAKE_BUILD_TYPE=Release.


If you want to install Thorin, specify an install prefix and build the target install:

cmake -S . -B build -DCMAKE_BUILD_TYPE=Debug -DCMAKE_INSTALL_PREFIX=/my/local/install/prefix
cmake --build build -j $(nproc) -t install

Build Switches

CMake Switch Options Default Comment
CMAKE_BUILD_TYPE Debug | Release | RelWithDebInfo Debug Build type.
CMAKE_INSTALL_PREFIX /usr/local Install prefix.
THORIN_BUILD_DOCS ON | OFF OFF If ON, Thorin will build the documentation
(requires Doxygen).
THORIN_BUILD_TESTING ON | OFF OFF If ON, Thorin will build all of Thorin's own tests.
THORIN_ENABLE_CHECKS ON | OFF ON If ON, enables expensive runtime checks
(requires CMAKE_BUILD_TYPE=Debug).


In addition to the provided submodules:

  • Recent version of CMake
  • A C++20-compatible C++ compiler.
  • While Thorin emits LLVM, it does not link against LLVM.

    Simply toss the emitted *.ll file to your system's LLVM toolchain. But techincally, you don't need LLVM.