这样的类型检查器被称为证明辅助器（Proof Assistant）。比较常见的证明辅助器有 Agda, Arend, Coq, Lean, F* 等。一个语言能用作辅助证明，最基本要拥有依赖类型（Dependent Type），例如对于上面的简单证明 <code>p</code> 的类型 <code>parallel ( a, b )</code> 也会依赖 <code>a, b</code> 。不过构造演算的类型系统足够表述上面的证明：</p>
<pre><code>parallelAxiom = Axiom (
    (<span class="hljs-selector-tag">a</span>: Line) → 