Misquoted No More: Securely Extracting F* Programs with IO

Cezar-Constantin Andrici, Abigail Pribisova, Danel Ahman +3

Shallow embeddings that use monads to represent effects are popular in proof-oriented languages because they are convenient for formal verification. Once shallowly embedded program…