"Meta-Theory a la Carte" (MTC) uses a model of language extension where modules build on a shared set of declarations of syntax categories and relations, declaring new syntax constructors and rules defining the relations. The set of shared declarations also includes properties, with each module adding its own part of the property proof for the parts of the language it introduces, these parts being composed to form a full proof for a composed language.
The set of shared declarations MTC uses is sort of a degenerate host language, so we model it as such. The shared declarations form a module introducing the syntax categories and relations, but not rules for them, other than the rules for a fixed relation we use to specify the language's property we will prove. This property, type preservation, is declared by the module making declarations. Each other module then adds new syntax constructors and rules, as well as a new proof of type preservation for its part of the language, similar to MTC.
In MTC, in contrast to Extensibella's approach, only shared properties can be proven completely, with any module-specific properties needed to support them requiring glue code to complete the proofs for a composition. Additionally, MTC defines language semantics and writes proofs using Mendler algebras, building the modularity restrictions into the underlying logic. We believe our approach, which uses an encoding into our logic that is substantially the same as non-extensible approaches take, leads to a more readable specification of language semantics and properties, and more confidence they correspond to what was intended.
z or s(N) for
some N