On Multi-Language Abstraction: Towards a Static Analysis of Multi-Language Programs
summary
Paper gives a general, provable method to build an abstract semantics for a language obtained by combining two languages: it lifts concrete algebras to collecting semantics via the powerset lifting, uses order-sorted algebraic signatures for syntax and semantics, and moves fixpoint constructions with the Kleene Fixpoint Transfer theorem. Soundness and forward/backward completeness are proved; the approach is instantiated on two imperative languages to produce a combined multi-language sign analysis that computes cross-language properties.
AI-written summary · about
chapters (11)
- 0:00Introduction
- 1:10Why multi-language needs analysis
- 3:26Multi-language semantics
- 6:29Order-sorted signatures basics
- 9:30Multi-language signatures
- 10:34Collecting semantics
- 13:35Fixpoint semantics
- 15:08Abstract semantics
- 16:40Multi-language abstract semantics
- 18:07Completeness and instantiation
- 18:52Conclusion
related talks
40mFormal semantics for multi-language programs
16mA metalanguage for multi-phase modularity
14mTowards Cumulative Abstract Semantics via Handlers (Short Paper)
20mA Modular Approach to Metatheoretic Reasoning for Extensible Languages
52mThink Abstractly, Work Concretely
01h 05mVerifying Infinitely Many Programs at Once
20mUnifying compositional verification and certified compilation with a three-dimensional(…)
18mOn the Expressive Power of Languages for Static Variability