Principal types of BCK-lambda-terms
From MaRDI portal
Publication:1208417
DOI10.1016/0304-3975(93)90171-OzbMath0770.03006MaRDI QIDQ1208417
Publication date: 16 May 1993
Published in: Theoretical Computer Science (Search for Journal in Brave)
principal type schemeBCK-\(\lambda\)-termBCK-implicational logicBCK-minimal typeBCK-typenormalized proofstype assignments
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
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