Modeling abstract types in modules with open existential types

DOI10.1145/1480881.1480926MaRDI QIDQ5261533zbMATH OpenOpenAlexFDO

Authors Benoît Montagu, Didier Rémy

Publication date 3 July 2015

Published in Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/1480881.1480926

zbMATH Keywords

modulesmodularitylambda-calculustype systemslinear type systemsexistential typesabstract typesgenerativity

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70) Functional programming and lambda calculus (68N18)

Recommendations

• Abstract deduction and inferential models for type theory
• A modular construction of type theories
• Intensional models for the theory of types
• Modular properties of algebraic type systems
• A type system for higher-order modules
• scientific article; zbMATH DE number 2185711
• Publication:4944854
• scientific article; zbMATH DE number 4164125
• scientific article; zbMATH DE number 1342287
• scientific article; zbMATH DE number 1497733

Cited in

(6)

• The essence of dependent object types
• Recursive type generativity
• Path resolution for nested recursive modules
• Recursive type generativity
• A type system for higher-order modules
• The existential fragment of second-order propositional intuitionistic logic is undecidable

This page was built for publication: Modeling abstract types in modules with open existential types

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