The correctness of Newman's typability algorithm and some of its extensions

DOI10.1016/j.tcs.2011.03.016zbMath1221.03016OpenAlexW2132382388MaRDI QIDQ549191

Herman Geuvers, Robbert Krebbers

Publication date: 7 July 2011

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

Full work available at URL: https://doi.org/10.1016/j.tcs.2011.03.016

zbMATH Keywords

unificationsimply typed lambda calculusprincipal typetyping algorithms

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Uses Software

• ML
• Automath

Cites Work

• The lambda calculus, its syntax and semantics
• Linear unification
• A theory of type polymorphism in programming
• On theories with a combinatorial definition of 'equivalence'
• An Efficient Unification Algorithm
• Introduction to Type Theory
• M. H. Newman's Typability Algorithm for Lambda-calculus
• A Machine-Oriented Logic Based on the Resolution Principle
• The Principal Type-Scheme of an Object in Combinatory Logic
• New Foundations for Mathematical Logic
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: The correctness of Newman's typability algorithm and some of its extensions