Type inference with recursive types: Syntax and semantics

DOI10.1016/0890-5401(91)90020-3MaRDI QIDQ756435zbMATH OpenOpenAlexFDO

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

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)

Recommendations

• scientific article; zbMATH DE number 1377611
• scientific article; zbMATH DE number 1705161
• 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

Cites work

• scientific article; zbMATH DE number 3898200 (Why is no real title available?)
• scientific article; zbMATH DE number 3938562 (Why is no real title available?)
• scientific article; zbMATH DE number 4051569 (Why is no real title available?)
• scientific article; zbMATH DE number 3780545 (Why is no real title available?)
• scientific article; zbMATH DE number 3993540 (Why is no real title available?)
• scientific article; zbMATH DE number 3448081 (Why is no real title available?)
• scientific article; zbMATH DE number 3379785 (Why is no real title available?)
• A filter lambda model and the completeness of type assignment
• A theory of type polymorphism in programming
• Algebras and combinators
• An ideal model for recursive polymorphic types
• Combinatory logic. With two sections by William Craig.
• Completeness of type assignment in continuous lambda models
• Edinburgh LCF. A mechanized logic of computation
• Fundamental properties of infinite trees
• Modified basic functionality in combinatory logic
• On Proving Limiting Completeness
• Polymorphic type inference and containment
• Set-theoretical models of lambda-calculus: theories, expansions, isomorphisms
• 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
• The completeness theorem for typing lambda-terms
• The lambda calculus. Its syntax and semantics. Rev. ed.
• The solutions of two star-height problems for regular trees

Cited in

(16)

• scientific article; zbMATH DE number 1231454 (Why is no real title available?)
• Type inference for variant object types
• Interpretations of recursively defined types
• A coinductive completeness proof for the equivalence of recursive types
• Confluence of the lambda calculus with left-linear algebraic rewriting
• scientific article; zbMATH DE number 445161 (Why is no real title available?)
• Logic of subtyping
• CPO-models for second order lambda calculus with recursive types and subtyping
• Combining type disciplines
• Flow-sensitive type systems and the ambient calculus
• Types for Proofs and Programs
• 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
• Type inference for bimorphic recursion
• Denotational semantics of recursive types in synthetic guarded domain theory
• scientific article; zbMATH DE number 1705161 (Why is no real title available?)

Describes a project that uses

Uses Software

• LCF
• ML

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)