A decidable theory of type assignment

DOI10.1007/S00153-013-0335-XMaRDI QIDQ365669zbMATH OpenOpenAlexFDO

Authors 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

type reconstructionlambda calculusprimitive recursive functionalsreduction sequencestypabilitytype assignmenttype checking

Mathematics Subject Classification ID

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

Recommendations

• PRINCIPAL TYPE ASSIGNMENT TO LAMBDA TERMS
• scientific article; zbMATH DE number 814613
• Typing untyped \(\lambda\)-terms, or reducibility strikes again!
• Positive recursive type assignment
• Typability and type checking in System F are equivalent and undecidable

Cites work

• scientific article; zbMATH DE number 1722646 (Why is no real title available?)
• scientific article; zbMATH DE number 3857078 (Why is no real title available?)
• scientific article; zbMATH DE number 5318491 (Why is no real title available?)
• scientific article; zbMATH DE number 42059 (Why is no real title available?)
• scientific article; zbMATH DE number 3572133 (Why is no real title available?)
• scientific article; zbMATH DE number 1042221 (Why is no real title available?)
• scientific article; zbMATH DE number 1497485 (Why is no real title available?)
• scientific article; zbMATH DE number 1390277 (Why is no real title available?)
• An upper bound for reduction sequences in the typed \(\lambda\)-calculus
• Combinatory logic. Vol. II
• Combinatory logic. With two sections by William Craig.
• Exact bounds for lengths of reductions in typed \(\lambda\)-calculus
• How to assign ordinal numbers to combinatory terms with polymorphic types
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Typability and type checking in System F are equivalent and undecidable
• ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES

Cited in

(12)

• Computer Science Logic
• A new type assignment for strongly normalizable terms
• Combinatory logic with polymorphic types
• scientific article; zbMATH DE number 1479634 (Why is no real title available?)
• scientific article; zbMATH DE number 847763 (Why is no real title available?)
• Threshold voting leads to type-revelation
• Decidability in Intuitionistic Type Theory is Functionally Decidable
• Positive recursive type assignment
• The insensitivity theorem for nonreducing reflexive types
• A type-assignment of linear erasure and duplication
• How to assign ordinal numbers to combinatory terms with polymorphic types
• A simple proof of a theorem of Statman

Describes a project that uses

Uses Software

• Automath

This page was built for publication: A decidable theory of type assignment

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q365669)