ICFP/SPLASH 2025
Sun 12 - Sat 18 October 2025 Singapore

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 Oct

Displayed time zone: Perth change

13:45 - 15:30
Relational conversion, compilation, and encodingminiKanren at Peony NW
13:45
13m
Talk
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
13m
Talk
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
26m
Talk
Typed Embedding of miniKanren for Functional Conversion
miniKanren
Igor Engel JetBrains Research; Constructor University Bremen, Ekaterina Verbitskaia JetBrains Research; Constructor University Bremen
14:37
26m
Talk
Fair intersection of seekable iterators
miniKanren
15:03
26m
Talk
Encoding Numeric Computations and Infusing Heuristic Knowledge Using Integrity Constraints in stableKanren
miniKanren
Xiangyu Guo Arizona State University, Ajay Bansal Arizona State University