path was initially based on the calculus described in A tutorial implementation of a dependently typed lambda calculus. It has been extended with the quantitative type theory described in Syntax and Semantics of Quantitative Type Theory.
Development of path typically uses cabal new-build:
cabal new-build # build the library and pathc
cabal new-repl # load the library in GHCI
Path’s REPL can be run from GHCI:
λ import Path.REPL
λ repl (packageSources basePackage)
λ: …or from the CLI:
cabal new-run pathc -- -i src/Base/*.path