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

DOI10.1016/J.TCS.2011.03.016zbMATH Open1221.03016OpenAlexW2132382388MaRDI QIDQ549191FDOQ549191

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

Recommendations

• M. H. Newman's Typability Algorithm for Lambda-calculus
• On type inference in the intersection type discipline
• scientific article
• Higher-order unification via combinators
• On the type correctness of polymorphic \(\lambda\)-terms. II

zbMATH Keywords

unificationsimply typed lambda calculusprincipal typetyping algorithms

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Cites Work

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

Cited In (2)

• An analysis of ML typability
• Title not available (Why is that?)

Uses Software

• ML
• Automath

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

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