Modeling abstract types in modules with open existential types

DOI10.1145/1480881.1480926zbMATH Open1315.68103OpenAlexW1970031091MaRDI QIDQ5261533FDOQ5261533

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

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
• scientific article; zbMATH DE number 1342287
• scientific article; zbMATH DE number 1497733

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)

Cited In (6)

• Recursive type generativity
• The essence of dependent object types
• 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)