A decidable theory of type assignment

DOI10.1007/s00153-013-0335-xzbMath1303.03036OpenAlexW1972202041MaRDI QIDQ365669

William R. Stirton

Publication date: 9 September 2013

Published in: Archive for Mathematical Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00153-013-0335-x

zbMATH Keywords

lambda calculustype reconstructionprimitive recursive functionalsreduction sequencestypabilitytype assignmenttype checking

Mathematics Subject Classification ID

Functionals in proof theory (03F10) Combinatory logic and lambda calculus (03B40)

Related Items

Combinatory logic with polymorphic types

Uses Software

• Automath

Cites Work

• How to assign ordinal numbers to combinatory terms with polymorphic types
• Combinatory logic. With two sections by William Craig.
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Typability and type checking in System F are equivalent and undecidable
• Combinatory logic. Vol. II
• An upper bound for reduction sequences in the typed \(\lambda\)-calculus
• Exact bounds for lengths of reductions in typed λ-calculus
• ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item