Paper

Misquoted No More: Securely Extracting F* Programs with IO

arXiv:2602.19973v3 Announce Type: replace-cross Abstract: Shallow embeddings that use monads to represent effects are popular in proof-oriented languages because they are convenient for formal verification. Once shallowly embedded programs are verified, they are often extracted to mainstream languages like OCaml or C and linked into larger codebases. The extraction process is not fully verified because it often involves quotation -- turning the shallowly embedded program into a deeply embedded one -- and verifying quotation remains a major open challenge. Instead, some prior work obtains form…

Authors:

Related discussions