zbMATH — the first resource for mathematics

A proof-theoretic account of programming and the role of reduction rules. (English) Zbl 0676.03007
The author tries to find out the role of rules (introduction, elimination, reduction) in the explicit description of logical connectives. He considers the introduction and reduction rules to be the specifications of the meaning of a connective because they describe when and how the connective can be used. On the other hand, the elimination rule is responsible for the computation of an expression.
Martin-Löf’s intuitionistic type theory is suggested as a suitable background for this approach. The author defines an extension of this theory by the equality rules. This allows him to prove that the elimination rules are derivable from the introduction rules.
Reviewer: O.Štěpánková

03B40 Combinatory logic and lambda calculus
03F35 Second- and higher-order arithmetic and fragments
03B30 Foundations of classical theories (including reverse mathematics)
68Q60 Specification and verification (program logics, model checking, etc.)
Full Text: DOI