A calculus with recursive types, record concatenation and subtyping

DOI10.1007/978-3-031-21037-2_9MaRDI QIDQ6176573zbMATH OpenOpenAlexFDO

Authors Yaoda Zhou, Bruno C. d. S. Oliveira, Andong Fan

Publication date 25 July 2023

Published in Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-031-21037-2_9

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Formalization of mathematics in connection with theorem provers (68V20)

Recommendations

• Taming the merge operator
• Applicative intersection types
• A record calculus with principal types
• Disjoint polymorphism

Cites work

• A 3-part type inference engine
• A filter lambda model and the completeness of type assignment
• Automata, Languages and Programming
• Bounded quantification is undecidable
• Comparing object encodings.
• Disjoint intersection types
• Disjoint polymorphism
• Distributive disjoint polymorphism for compositional programming
• Elaborating intersection and union types
• Family polymorphism
• scientific article; zbMATH DE number 3864476 (Why is no real title available?)
• scientific article; zbMATH DE number 954811 (Why is no real title available?)
• scientific article; zbMATH DE number 944097 (Why is no real title available?)
• scientific article; zbMATH DE number 814798 (Why is no real title available?)
• scientific article; zbMATH DE number 814801 (Why is no real title available?)
• Intersection types and computational effects
• Operations on records
• Semantic subtyping, dealing set-theoretically with function, union, intersection, and negation types
• Subtyping with union types, intersection types and recursive types
• The essence of dependent object types
• Type inference for record concatenation and subtyping

Cited in

(5)

• scientific article; zbMATH DE number 3980461 (Why is no real title available?)
• scientific article; zbMATH DE number 1302055 (Why is no real title available?)
• A record calculus with principal types
• Applicative intersection types
• Recursive subtyping for all

This page was built for publication: A calculus with recursive types, record concatenation and subtyping

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