\documentclass[acmsmall,screen,nonacm]{acmart}
\usepackage{listings}
\usepackage{booktabs}
\usepackage{xspace}
\settopmatter{printacmref=false}
\renewcommand\footnotetextcopyrightpermission[1]{}
\hypersetup{pdfproducer={pdfTeX}}

\input{numbers_v2}

\lstdefinelanguage{lean}{
  morekeywords={theorem,def,by,fun,let,in,have,intro,simp,structure,inductive,match,with,where,open,namespace,end,import},
  sensitive=true, morecomment=[l]{--}, morestring=[b]"}
\lstset{language=lean, basicstyle=\ttfamily\footnotesize, columns=fullflexible, keepspaces=true,
  literate={→}{{$\to$}}1 {∀}{{$\forall$}}1 {∃}{{$\exists$}}1 {∧}{{$\wedge$}}1 {∨}{{$\vee$}}1 {≤}{{$\le$}}1
           {≠}{{$\ne$}}1 {¬}{{$\neg$}}1 {⟨}{{$\langle$}}1 {⟩}{{$\rangle$}}1 {≈}{{$\approx$}}1 {⁻¹}{{$^{-1}$}}1
           {∈}{{$\in$}}1 {·}{{$\cdot$}}1 {…}{{$\dots$}}1}

\newcommand{\code}[1]{\texttt{#1}}
\setlength{\emergencystretch}{3em}

\begin{document}

\title{Proof-Carrying Modernization: LLM Translations of COBOL Batch Programs, Each Proved Against the Original in Lean}

\author{Tejasvi Singh Tomar}
\email{}

\begin{abstract}
\input{sec-abstract}
\end{abstract}

\maketitle

\input{sec-intro}
\input{sec-example}
\input{sec-stack}
\input{sec-migration}
\input{sec-trust}
\input{sec-further}
\input{sec-related}
\input{sec-limits}
\input{sec-conclusion}

\section*{Data Availability}
The artifact~\cite{fvtechreport} (\url{https://doi.org/10.5281/zenodo.23996137}) contains the technical report, with
the full text of the study, every re-check and the kernel replay behind each result; the source snapshots of our
semantics, tools and proofs at the versions named in Appendix~\ref{app:pins} and the technical report; the pre-registrations and the deviation log; and the summaries and hash lists of the checks. The LaTeX source of this paper
is at \url{https://github.com/tejasvi/proof-carrying-modernization}.

\section*{Acknowledgements}
Generative AI tools were used to write code, run analyses and draft text; the author directed the work and takes full
responsibility for its content.

\bibliographystyle{ACM-Reference-Format}
\bibliography{refs}

\appendix
\input{sec-appendix}

\end{document}