next up previous contents
Next: The Main Points Up: Logical and Programming Style Previous: Logical and Programming Style

Logical Style

The Mark2 prover has been affected from the outset by certain decisions of logical style. These are motivated by the theoretical origins of the project in untyped synthetic combinatory logic, motivated by Curry's program of untyped combinatory logic without bound variables on the one hand, and the untyped set theory ``New Foundations'' (NF) of Quine on the other.

Randall Holmes
Fri Sep 5 16:28:58 MDT 1997