Equational reasoning for linking with first-class primitive modules

DOI10.1007/3-540-46425-5_27MaRDI QIDQ4518890zbMATH OpenFDO

Authors J. B. Wells, René Vestergaard

Publication date 20 May 2001

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-46425-5_27

zbMATH Keywords

\(\lambda\)-calculus\(m\)-calculus

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• A calculus of module systems
• A calculus for link-time compilation
• A calculus of open modules: call-by-need strategy and confluence
• Theoretical Computer Science
• Modules, abstraction, and parametric polymorphism

Cited in

(8)

• A formalised first-order confluence proof for the \(\lambda\)-calculus using one-sorted variable names.
• The mechanisation of Barendregt-style equational proofs (the residual perspective)
• Computational soundness of a call by name calculus of recursively-scoped records
• Featherweight Jigsaw. Replacing inheritance by composition in Java-like languages
• A calculus of module systems
• A calculus for link-time compilation
• A typed context calculus
• A flexible model for dynamic linking in Java and C\#

This page was built for publication: Equational reasoning for linking with first-class primitive modules

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