Principal types of BCK-lambda-terms

DOI10.1016/0304-3975(93)90171-OzbMath0770.03006MaRDI QIDQ1208417

Sachio Hirokawa

Publication date: 16 May 1993

Published in: Theoretical Computer Science (Search for Journal in Brave)

zbMATH Keywords

principal type schemeBCK-\(\lambda\)-termBCK-implicational logicBCK-minimal typeBCK-typenormalized proofstype assignments

Mathematics Subject Classification ID

Theory of programming languages (68N15) Combinatory logic and lambda calculus (03B40)

Related Items (10)

Uniqueness of normal proofs of minimal formulas ⋮ Principal type-schemes of BCI-lambda-terms ⋮ Unnamed Item ⋮ Unnamed Item ⋮ 2000 European Summer Meeting of the Association for Symbolic Logic. Logic Colloquium 2000 ⋮ Most general first order theorems are not recursively enumerable ⋮ The converse principal type-scheme theorem in lambda calculus ⋮ Studying provability in implicational intuitionistic logic ⋮ Computing interpolants in implicational logics ⋮ On principal types of combinators

Uses Software

• ML

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Linear logic
• Combinatory logic. With two sections by William Craig.
• Principal type scheme and unification for intersection type discipline
• BCK-combinators and linear \(\lambda\)-terms have types
• Condensed detachment is complete for relevance logic: A computer-aided proof
• Implementing the `Fool's model' of combinatory logic
• Intersection types for combinatory logic
• Fully abstract models of typed \(\lambda\)-calculi
• A theory of type polymorphism in programming
• BCK and BCI logics, condensed detachment and the 2-property
• Combinatory logic. Vol. II
• Principal type-schemes and condensed detachment
• Logics without the contraction rule
• Why commutative diagrams coincide with equivalent proofs
• Coherence and valid isomorphism in closed categories applications of proof theory to category theory in a computer sclentist perspective
• The Principal Type-Scheme of an Object in Combinatory Logic
• Über Tautologien, in Welchen Keine Variable Mehr Als Zweimal Vorkommt

This page was built for publication: Principal types of BCK-lambda-terms