&inator is the first system to produce correct and precise Rust interfaces from C declarations via a constraint-based model of semantic equivalence and borrow checking.
hub
Type- Constrained Code Generation with Language Models
11 Pith papers cite this work, alongside 6 external citations. Polarity classification is still indexing.
11
Pith papers citing it
6
external citations · OpenAlex
hub tools
years
2026 11representative citing papers
SEVerA uses Formally Guarded Generative Models and a three-stage Search-Verification-Learning process to synthesize self-evolving agents that satisfy hard formal constraints while improving task performance.
Incomplete constrainers in constrained decoding push LLMs into low-probability program regions, making unconstrained decoding outperform constrained decoding on functional correctness across seven models and three benchmarks.
An LLM agent with Rocq backend automatically builds a verified RISC-V RV32I interpreter (1859 lines Rocq, 2848 lines extracted C++) that passes 265 tests and 12-hour fuzzing, while a Dafny backend fails.
Constrained Diffusion for Code (CDC) integrates constraint satisfaction into the reverse denoising process of discrete diffusion models via constraint-aware operators that use optimization and program analysis to steer generation toward feasible programs.
Hydra enables asynchronous static error checking and targeted checkpoint-rollback repair during LLM code generation, cutting latency by up to 71% and token use by up to 70% versus post-hoc repair on C/C++ tasks.
Constrained decoding derived from OpenAPI specifications eliminates hallucinated web API calls in LLM-generated code and substantially improves correctness across 24 models, while retrieval-augmented generation yields inconsistent, model-dependent gains.
Decoding Time Verification (DTV) interleaves verifier calls at structural boundaries during autoregressive code generation for C-to-Rust and JavaScript-to-TypeScript translation, raising pass rates while using fewer tokens than post-hoc baselines.
Few-shot prompting improves syntactic validity of LLM-generated code across ATL, ETL, QVTo, and Reactions, but semantic correctness gains remain uneven and language-dependent.
DIA is a training-free method that dynamically adjusts anchor positions in diffusion LLMs to improve format compliance and accuracy on reasoning benchmarks like GSM8K and MATH.
citing papers explorer
-
&inator: Correct, Precise C-to-Rust Interface Translation
&inator is the first system to produce correct and precise Rust interfaces from C declarations via a constraint-based model of semantic equivalence and borrow checking.
-
SEVerA: Verified Synthesis of Self-Evolving Agents
SEVerA uses Formally Guarded Generative Models and a three-stage Search-Verification-Learning process to synthesize self-evolving agents that satisfy hard formal constraints while improving task performance.
-
The Alignment Problem in Constrained Code Generation
Incomplete constrainers in constrained decoding push LLMs into low-probability program regions, making unconstrained decoding outperform constrained decoding on functional correctness across seven models and three benchmarks.
-
Trustworthy Software Project Generation : a Case Study with an Interactive Theorem Prover
An LLM agent with Rocq backend automatically builds a verified RISC-V RV32I interpreter (1859 lines Rocq, 2848 lines extracted C++) that passes 265 tests and 12-hour fuzzing, while a Dafny backend fails.
-
Constrained Code Generation with Discrete Diffusion
Constrained Diffusion for Code (CDC) integrates constraint satisfaction into the reverse denoising process of discrete diffusion models via constraint-aware operators that use optimization and program analysis to steer generation toward feasible programs.
-
Hydra: Efficient, Correct Code Generation via Checkpoint-and-Rollback Support
Hydra enables asynchronous static error checking and targeted checkpoint-rollback repair during LLM code generation, cutting latency by up to 71% and token use by up to 70% versus post-hoc repair on C/C++ tasks.
-
Mitigating Errors in LLM-Generated Web API Invocations via Retrieval-Augmented Generation and Constrained Decoding
Constrained decoding derived from OpenAPI specifications eliminates hallucinated web API calls in LLM-generated code and substantially improves correctness across 24 models, while retrieval-augmented generation yields inconsistent, model-dependent gains.
-
Verifier-Guided Code Translation via Meta-Step Decoding
Decoding Time Verification (DTV) interleaves verifier calls at structural boundaries during autoregressive code generation for C-to-Rust and JavaScript-to-TypeScript translation, raising pass rates while using fewer tokens than post-hoc baselines.
-
LLM4MTLs: Automated Generation and Empirical Evaluation of Model Transformation Languages
Few-shot prompting improves syntactic validity of LLM-generated code across ATL, ETL, QVTo, and Reactions, but semantic correctness gains remain uneven and language-dependent.
-
Dynamic Infilling Anchors for Format-Constrained Generation in Diffusion Large Language Models
DIA is a training-free method that dynamically adjusts anchor positions in diffusion LLMs to improve format compliance and accuracy on reasoning benchmarks like GSM8K and MATH.
- TypeProbe: Recovering Type Representations from Hidden States of Pre-trained Code Models