On the Expressive Power of Languages for Static Variability
summary
A formal semantic domain for static variability models configurations as functions-to-variants, and the paper proves soundness, completeness, and relative expressiveness for several languages, including choice calculus and algebraic decision trees (both complete) and several incomplete formalisms; translations are implemented as an Agda library so every proof is an executable compiler, artifacts are available and evaluated, and practical costs appear: clone‑and‑own is complete but causes combinatorial blowup (e.g. Linux has 5,000 options).
AI-written summary · about
chapters (8)
- 0:00Static variability intro
- 2:05Choice calculus formalization
- 4:56Variational expressions semantics
- 6:21Expressiveness criteria and proofs
- 8:47Soundness, completeness, clone-and-own
- 11:16Choice calculus as lambda calculus
- 13:23ACT implementation and repo
- 14:03Q&A on constraints
related talks
31mGenerating Constraint Programs for Variability Model Reasoning: A DSL and Solver-...
12mOn the power of syntactic methods: It is all syntax after all…
40mFormal semantics for multi-language programs
30mThe Verse Calculus: A Core Calculus for Deterministic Functional Logic Programmi...
18mLanguages with Decidable Learning: A Meta-theorem
20mA Modular Approach to Metatheoretic Reasoning for Extensible Languages
01h 31m"Thoughts on language evolution"
40mFormal semantics for multi-language programs
