The correctness of Newman's typability algorithm and some of its extensions
type: Item
instance of: scholarly article
title: The correctness of Newman's typability algorithm and some of its extensions
zbMATH Open document ID: 1221.03016
author: Herman Geuvers
author: Robbert Krebbers
published in: Theoretical Computer Science
publication date: 2011-07-07T00:00:00Z
Mathematics Subject Classification ID: 03B40
zbMATH DE Number: 5918237
zbMATH Keywords: simply typed lambda calculus
zbMATH Keywords: unification
zbMATH Keywords: typing algorithms
zbMATH Keywords: principal type
describes a project that uses: ML
describes a project that uses: Automath
MaRDI profile type: Publication
full work available at URL: j.tcs.2011.03.016
OpenAlex ID: W2132382388
cites work: Unification theory
cites work: The lambda calculus, its syntax and semantics
cites work: Introduction to Type Theory
cites work: The Principal Type-Scheme of an Object in Combinatory Logic
cites work: M. H. Newman's Typability Algorithm for Lambda-calculus
cites work: An Efficient Unification Algorithm
cites work: A theory of type polymorphism in programming
cites work: On theories with a combinatorial definition of 'equivalence'
cites work: Q5834314
cites work: Linear unification
cites work: New Foundations for Mathematical Logic
cites work: A Machine-Oriented Logic Based on the Resolution Principle
cites work: Q4799892
cites work: Q3787979
DOI: 10.1016/J.TCS.2011.03.016
description: scientific article; zbMATH DE number 5918237