BCK-combinators and linear \(\lambda\)-terms have types

DOI10.1016/0304-3975(89)90100-XzbMath0671.03010OpenAlexW1968532969MaRDI QIDQ1119620

J. Roger Hindley

Publication date: 1989

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

Full work available at URL: https://doi.org/10.1016/0304-3975(89)90100-x

zbMATH Keywords

typesBCK-combinatorlinear \(\lambda\)-term

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Related Items

Principal type-schemes of BCI-lambda-terms ⋮ A type-assignment of linear erasure and duplication ⋮ Unnamed Item ⋮ The proofs of α → α in P – W ⋮ Unnamed Item ⋮ Filter models with polymorphic types ⋮ Compact bracket abstraction in combinatory logic ⋮ Gödel's system \(\mathcal T\) revisited ⋮ Abstract Families of Abstract Categorial Languages ⋮ Principal types of BCK-lambda-terms ⋮ On the reification of semantic linearity ⋮ Phase semantics and Petri net interpretation for resource-sensitive strong negation ⋮ Perpetual reductions in \(\lambda\)-calculus ⋮ Weak linearization of the lambda calculus ⋮ On principal types of combinators ⋮ The number of proofs for a BCK-formula

Cites Work

• Linear logic
• Combinatory Reductions and Lambda Reductions Compared
• Unnamed Item
• Unnamed Item
• Unnamed Item