Epistemic Logic for Polyglots (Short Paper)
summary
Proposes using epistemic S4 modal logic as a propositions-as-types foundation for polyglot programs, mapping agents to languages and deriving a glue calculus via Curry–Howard inspired rules patterned on Fenning and Davies. Implements glue and foreign typing, an embedded-quote introduction, and a nonlogical tell construct to enable splicing; a running shader/string example typechecks but reveals a double translation inefficiency and unresolved semantics for boxed expressions. Work remains on a logical account of tell, adjoint-logic alternatives, and automated translation.
AI-written summary · about
chapters (11)
- 0:00Introduction
- 1:56Polyglot programs
- 2:57Motivation for epistemic logic
- 4:02Epistemic modal logic foundation
- 7:13Epistemic logic for glue code
- 10:03Rewriting example with epistemic types
- 11:07Introducing tell expression
- 12:54Type checking polyglot example
- 13:58Limitations and open problems
- 14:19Conclusions and future work
- 15:04Q&A
related talks
01h 05mAll the Languages Together
01h 34mFormal Logic Undressed
47mLogic Programming à la Carte
40mFormal semantics for multi-language programs
45mLogic Meta Programming for Functional Languages
30mPlausible sealing for gradual parametricity
19mExtensible Metatheory Mechanization via Family Polymorphism
12mA Unified View of Modalities in Type Systems