Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2604.17261 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866913053249896448 |
|---|---|
| author | Chen, Victor Coughlin, Ayden Bond, Michael D. |
| author_facet | Chen, Victor Coughlin, Ayden Bond, Michael D. |
| contents | Automatically translating system software from C to Rust is an appealing but challenging problem, as it requires whole-program reasoning to satisfy Rust's ownership and borrowing discipline. A key enabling step in whole-program translation is interface translation, which produces Rust declarations for the C program's top-level declarations (i.e., structs and function signatures), enabling modular and incremental code translation.
This paper introduces correct, precise C-to-Rust interface translation, called &inator. &inator employs a novel constraint-based formulation of semantic equivalence and type correctness including borrow-checking rules to produce a Rust interface that is correct (i.e., the interface admits a semantics-preserving implementation in safe Rust) and precise (i.e., it uses the simplest, least costly types). Our results show &inator produces correct, precise Rust interfaces for real C programs, but support for certain C features and scaling to large programs are challenges left for future work. This work advances the state of the art by being the first correct, precise approach to C-to-Rust interface translation. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2604_17261 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | &inator: Correct, Precise C-to-Rust Interface Translation Chen, Victor Coughlin, Ayden Bond, Michael D. Programming Languages Automatically translating system software from C to Rust is an appealing but challenging problem, as it requires whole-program reasoning to satisfy Rust's ownership and borrowing discipline. A key enabling step in whole-program translation is interface translation, which produces Rust declarations for the C program's top-level declarations (i.e., structs and function signatures), enabling modular and incremental code translation. This paper introduces correct, precise C-to-Rust interface translation, called &inator. &inator employs a novel constraint-based formulation of semantic equivalence and type correctness including borrow-checking rules to produce a Rust interface that is correct (i.e., the interface admits a semantics-preserving implementation in safe Rust) and precise (i.e., it uses the simplest, least costly types). Our results show &inator produces correct, precise Rust interfaces for real C programs, but support for certain C features and scaling to large programs are challenges left for future work. This work advances the state of the art by being the first correct, precise approach to C-to-Rust interface translation. |
| title | &inator: Correct, Precise C-to-Rust Interface Translation |
| topic | Programming Languages |
| url | https://arxiv.org/abs/2604.17261 |