The algebra of expansion

DOI10.3233/FI-2012-771MaRDI QIDQ4903714zbMATH OpenOpenAlexFDO

Authors Sébastien Carlier, J. B. Wells

Publication date 24 January 2013

Published in Fundamenta Informaticae (Search for Journal in Brave)

Full work available at URL https://doi.org/10.3233/fi-2012-771

zbMATH Keywords

expansion algebraformalized proofintersection typeslambda-calculusproof assistantsterm-rewriting systemstype inference

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Grammars and rewriting systems (68Q42)

Recommendations

• Expansion: the crucial mechanism for type inference with intersection types: a survey and explanation
• Linearization of the lambda-calculus and its relation with intersection type systems
• Intersection type assignment systems with higher-order algebraic rewriting
• A Complete Realisability Semantics for Intersection Types and Arbitrary Expansion Variables
• Expansion for universal quantifiers

Cited in

(7)

• Expansion: the crucial mechanism for type inference with intersection types: a survey and explanation
• Expander2: program verification between interaction and automation
• Expansion for universal quantifiers
• On realisability semantics for intersection types with expansion variables
• Programming Languages and Systems
• A Complete Realisability Semantics for Intersection Types and Arbitrary Expansion Variables
• Formal Methods in Software and Systems Modeling

Describes a project that uses

Uses Software

• Coq

This page was built for publication: The algebra of expansion

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