Type inference with recursive types: Syntax and semantics

DOI10.1016/0890-5401(91)90020-3zbMath0722.68076OpenAlexW2079958455MaRDI QIDQ756435

Mario Coppo, Felice Cardone

Publication date: 1991

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0890-5401(91)90020-3

zbMATH Keywords

completeness theoreminterpretationrecursive typesfunctional programming languagesinfinite (regular) type expressionstype inference system

Mathematics Subject Classification ID

Theory of programming languages (68N15) Semantics in the theory of computing (68Q55) General topics in the theory of software (68N01) Combinatory logic and lambda calculus (03B40)

Related Items

A Light Modality for Recursion, Calculi, types and applications: essays in honour of M. Coppo, M. Dezani-Ciancaglini and S. Ronchi della Rocca, Confluence of the lambda calculus with left-linear algebraic rewriting, Logic of subtyping, Flow-sensitive type systems and the ambient calculus, Type inference for variant object types, CPO-models for second order lambda calculus with recursive types and subtyping, Combining type disciplines, A coinductive completeness proof for the equivalence of recursive types

Uses Software

• ML
• LCF

Cites Work

• The solutions of two star-height problems for regular trees
• Combinatory logic. With two sections by William Craig.
• Completeness of type assignment in continuous lambda models
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Set-theoretical models of lambda-calculus: theories, expansions, isomorphisms
• Fundamental properties of infinite trees
• Polymorphic type inference and containment
• Algebras and combinators
• A theory of type polymorphism in programming
• Edinburgh LCF. A mechanized logic of computation
• The completeness theorem for typing lambda-terms
• A filter lambda model and the completeness of type assignment
• On Proving Limiting Completeness
• An ideal model for recursive polymorphic types
• The Relation between Computational and Denotational Properties for Scott’s ${\text{D}}_\infty $-Models of the Lambda-Calculus
• The Principal Type-Scheme of an Object in Combinatory Logic
• Modified basic functionality in combinatory logic
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item