The CoCompiler: DSL Lifting via Relational Compilation
This program is tentative and subject to change.
Lifting low-level or legacy code into a domain-specific language (DSL) improves our ability to understand it, enables deeper formal reasoning, and facilitates safe modification. We present the CoCompiler, a bidirectional compiler and lifter between C and Lustre, a synchronous dataflow language used for reactive systems. The key insight behind the CoCompiler is that writing a compiler as a relation, rather than as a traditional function, yields a DSL lifter “for free”. We implement this idea by rewriting the verified Lustre-to-C compiler Vélus in the Walrus relational programming language. This solves what we call the vertical lifting problem, translating \emph{canonical} C into Lustre. To address the complementary horizontal problem—handling real-world C outside the compiler’s image—we apply semantic-preserving canonicalization passes in Haskell. The resulting tool, the CoCompiler, supports lifting real reactive C code into Lustre and onward into graphical behavioral models. Our approach is modular, language-agnostic, and fast to implement, demonstrating that relational programming offers a practical foundation for building DSL lifters by repurposing existing compilers.
This program is tentative and subject to change.
Fri 17 OctDisplayed time zone: Perth change
13:45 - 15:30 | |||
13:45 13mTalk | Designing Walrus: Relational Programming with Rich Types, On-Demand Laziness, and Structured Traces miniKanren Santiago Cuellar Princeton, Naomi Spargo Galois, Inc., Jonathan Daugherty Galois, Inc., David Darais Galois | ||
13:58 13mTalk | The CoCompiler: DSL Lifting via Relational Compilation miniKanren Naomi Spargo Galois, Inc., Santiago Cuellar Princeton, Jonathan Daugherty Galois, Inc., Chris Phifer Galois, David Darais Galois | ||
14:11 26mTalk | Typed Embedding of miniKanren for Functional Conversion miniKanren Igor Engel JetBrains Research; Constructor University Bremen, Ekaterina Verbitskaia JetBrains Research; Constructor University Bremen | ||
14:37 26mTalk | Fair intersection of seekable iterators miniKanren Michael Arntzenius None | ||
15:03 26mTalk | Encoding Numeric Computations and Infusing Heuristic Knowledge Using Integrity Constraints in stableKanren miniKanren |