scientific article

zbMath0753.03008MaRDI QIDQ4012884

Lincoln Wallen, David J. Pym

Publication date: 27 September 1992

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

unificationcut-eliminationsubformula propertyintrinsic well-typingreduction of search spacesystem for proof-search in the \(\lambda\Pi\)- calculus

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Combinatory logic and lambda calculus (03B40)

Related Items (7)

A note on the proof theory of the \(\lambda \Pi\)-calculus ⋮ Proof-terms for classical and intuitionistic resolution ⋮ On the intuitionistic force of classical search (Extended abstract) ⋮ Using typed lambda calculus to implement formal systems on a machine ⋮ Permutability of proofs in intuitionistic sequent calculi ⋮ On the intuitionistic force of classical search ⋮ Proof-search in type-theoretic languages: An introduction

This page was built for publication: