scientific article; zbMATH DE number 4051569

MaRDI QIDQ3787979zbMATH OpenFDO

Authors Mitchell Wand

Publication date 1987

zbMATH Keywords

correctnesstyped \(\lambda \)-calculusalgorithm for solving the classical type-inference problemcorrect types

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Combinatory logic and lambda calculus (03B40)

Recommendations

• scientific article; zbMATH DE number 445157
• The correctness of Newman's typability algorithm and some of its extensions
• Efficient inference of partial types
• On type inference in the intersection type discipline
• Type inference in polymorphic type discipline

Cited in

(26)

• Type reconstruction with recursive types and atomic subtyping
• Type inference with recursive types: Syntax and semantics
• Formal verification of algorithm \(\mathcal{W}\): the monomorphic case
• Correcting type errors in the Curry system
• Introduction to Type Theory
• The correctness of Newman's typability algorithm and some of its extensions
• A mechanized textbook proof of a type unification algorithm
• Type inference in polymorphic type discipline
• scientific article; zbMATH DE number 3900134 (Why is no real title available?)
• An analysis of the Core-ML language: Expressive power and type reconstruction
• On the type correctness of polymorphic \(\lambda\)-terms. I
• Type inference with subtypes
• Unsolvability of type correctness problem for functional programs
• Two algorithms in search of a type-system
• Simplifying subtyping constraints: a theory
• Threshold voting leads to type-revelation
• Type Inference for Rank 2 Gradual Intersection Types
• Simply typed convertibility is \textsc{Tower}-complete even for safe lambda-terms
• scientific article; zbMATH DE number 2044493 (Why is no real title available?)
• Backward type inference for XML queries
• Type inference for rank-2 intersection types using set unification
• Operations on records (extended abstract)
• Disjoint polymorphism
• Derivation and inference of higher-order strictness types
• Safety analysis versus type inference for partial types
• M. H. Newman's Typability Algorithm for Lambda-calculus

This page was built for publication:

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