Type inference with recursive types: Syntax and semantics

DOI10.1016/0890-5401(91)90020-3zbMATH Open0722.68076OpenAlexW2079958455MaRDI QIDQ756435FDOQ756435

Authors: Felice Cardone, Mario Coppo 

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

Recommendations

• scientific article; zbMATH DE number 1377611
• Publication:2771055
• Publication:4490755
• A Rewriting Semantics for Type Inference
• scientific article; zbMATH DE number 1231454
• Type inference for bimorphic recursion
• Interpretations of recursively defined types
• scientific article; zbMATH DE number 16188
• scientific article; zbMATH DE number 2003149
• A syntax for higher inductive-inductive types

zbMATH Keywords

interpretationcompleteness theoremrecursive typesfunctional programming languagesinfinite (regular) type expressionstype inference system

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (16)

• Type inference for variant object types
• Interpretations of recursively defined types
• A coinductive completeness proof for the equivalence of recursive types
• A Light Modality for Recursion
• Title not available (Why is that?)
• Confluence of the lambda calculus with left-linear algebraic rewriting
• Logic of subtyping
• CPO-models for second order lambda calculus with recursive types and subtyping
• Types for Proofs and Programs
• Combining type disciplines
• Flow-sensitive type systems and the ambient calculus
• Polymorphic higher-order context-free session types
• Calculi, types and applications: essays in honour of M. Coppo, M. Dezani-Ciancaglini and S. Ronchi della Rocca
• Denotational semantics of recursive types in synthetic guarded domain theory
• Title not available (Why is that?)
• Title not available (Why is that?)

Uses Software

• ML
• LCF

This page was built for publication: Type inference with recursive types: Syntax and semantics

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