大部分定理证明系统都依赖于对形式化语言的解析，生成抽象语法树（Abstract Syntax Tree，AST）并进行类型检查。通常，符号绑定在作用域内进行，每个作用域都是通过解析特定编程语言编写的程序而得到的。
然而，为了实现一个命令式且不依赖特定语言的证明系统，我们需要以某种方式存储“作用域”的信息。通过语言解析获得的作用域类似于依赖类型论的范畴语义中的上下文范畴的对象，即上下文。本文通过类比上下文范畴的定义设计了上下文结构，并用该结构存储某个上下文中已经构造出来的项。
系统的主要功能通过操作上下文结构来实现。这极大地提高了构造证明的灵活性，但同时也增加了书写的复杂性