Proof-Carrying Modernization: LLM Translations of COBOL Batch Programs, Each Proved Against the Original in Lean
Source files
root filemain.tex · root file2 KiB · SHA-256 fbd61913ee1acf19… · view textauxiliary filenumbers_v2.tex3 KiB · SHA-256 d1656cd2b7890e52… · view textauxiliary filerefs.bib34 KiB · SHA-256 54f7b6653b664324… · view textauxiliary filesec-abstract.tex1 KiB · SHA-256 88edd9b8292b6ec8… · view textauxiliary filesec-appendix.tex5 KiB · SHA-256 5e6d64d4b14d42a1… · view textauxiliary filesec-conclusion.tex1 KiB · SHA-256 83235bcc1a282e9f… · view textauxiliary filesec-example.tex7 KiB · SHA-256 37d162182f400d71… · view textauxiliary filesec-further.tex2 KiB · SHA-256 3509af5e9a0b4557… · view textauxiliary filesec-intro.tex5 KiB · SHA-256 2c9aab46841d0be7… · view textauxiliary filesec-limits.tex7 KiB · SHA-256 777ca6be61c3587b… · view textauxiliary filesec-migration.tex18 KiB · SHA-256 c562e10b8cd27916… · view textauxiliary filesec-related.tex6 KiB · SHA-256 1de48b0ad338e6ff… · view textauxiliary filesec-stack.tex12 KiB · SHA-256 41b1b52f17ed8995… · view textauxiliary filesec-trust.tex16 KiB · SHA-256 8191f2ddde8902ec… · view textauxiliary filesec-ub-para.tex2 KiB · SHA-256 0ccc9488bf87b98e… · view text