2024/01/01 by Takashi Suwa, Atsushi Igarashi · 1 voice
Computer Science · #Formal Methods in Verification #Logic, programming, and type systems #Parallel Computing and Optimization Techniques
paper · pdf · doi:10.1007/978-981-97-2300-3_13
openalex publication_date 2024/01/01 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/29
Abstract We propose MetaFM , a novel ML-style module system that enables users to decompose multi-stage programs (i.e., programs written in a typed multi-stage programming language) into loosely coupled components in a manner natural with respect to type abstraction. The distinctive aspect of MetaFM is that it allows values at different stages to be bound in a single structure (i.e., struct ⋯ end <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"><mml:mrow><mml:mi>struct</mml:mi><mml:mspace/><mml:mo>⋯</mml:mo><mml:mspace/><mml:mi>end</mml:mi></mml:mrow></mml:math> ). This feature is crucial, for example, for defining a function and a macro that use one abstract type in common, without revealing the implementation detail of that type. MetaFM also accommodates functors , higher-kinded types , the with type <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"><mml:mrow><mml:mi>with</mml:mi><mml:mspace/><mml:mi>type</mml:mi></mml:mrow></mml:math> - construct , etc. with staging features. For defining semantics and proving type safety, we employ an elaboration technique, i.e., type-directed translation to a target language, inspired by the formalization of F-ing Modules. Specifically, we give a set of elaboration rules for converting MetaFM programs into System F ω ⟨ ⟩ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"><mml:msup><mml:mi>ω</mml:mi><mml:mrow><mml:mo>⟨</mml:mo><mml:mo>⟩</mml:mo></mml:mrow></mml:msup></mml:math> , a multi-stage extension of System F ω <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"><mml:mi>ω</mml:mi></mml:math> , and prove that the elaboration preserves typing. Additionally, our language supports cross-stage persistence ( CSP ), a feature for code reuse spanning more than one stage, without breaking type safety.