Manual of the TYPO type checker

de Nivelle, H.

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.

Additional Metadata
ACM	Mathematical Logic (acm F.4.1)
MSC	Higher-order logic and type theory (msc 03B15), Combinatory logic and lambda-calculus (msc 03B40), Applications of logic (msc 16B70)
Publisher	CWI
Series	Information Systems [INS]
Citation APA Style AAA Style APA Style Cell Style Chicago Style Harvard Style IEEE Style MLA Style Nature Style Vancouver Style American-Institute-of-Physics Style Council-of-Science-Editors Style BibTex Format Endnote Format RIS Format CSL Format DOIs only Format	de Nivelle, H. (1998). Manual of the TYPO type checker. Information Systems [INS]. CWI.

Free Full Text ( Final Version , 248kb )

Manual of the TYPO type checker

Publication

Publication

Address

CWI researchers

Questions or comments?

Manual of the TYPO type checker

Publication

Publication

Workflow

Workflow

Add Content