TYPO is a type checker which implements typed lambda calculus with the purpose of formalizing mathematical proofs. TYPO has been constructed with the following design objectives: (1) Easy installation. In order to obtain this goal the program has been written in portable C. The program has modest memory demands. (2) Access to the proof terms. A formalized theory is represented as an ASCII file containing the definitions/theorems and proofs as lambda terms. (3) Maintainability. In order to obtain this goal the program has not been optimized for speed.

Mathematical Logic (acm F.4.1)
Higher-order logic and type theory (msc 03B15), Combinatory logic and lambda-calculus (msc 03B40), Applications of logic (msc 16B70)
Information Systems [INS]

de Nivelle, H. (1998). Manual of the TYPO type checker. Information Systems [INS]. CWI.