Pith. sign in

REVIEW 3 major objections 5 minor 43 references

Misquoted No More: Securely Extracting F* Programs with IO

T0 review · 3 major / 5 minor · reviewed 2026-08-02 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read This paper claims that shallowly embedded effectful programs in a proof-oriented language can be extracted to a deeply embedded lambda calculus while preserving Robust Relational Hyperproperty Preservation, the strongest known secure-compil

desk verdict Real formal result, but the abstract oversells RrHP: the theorem covers syntactically typed λ_io contexts, not arbitrary linked OCaml; still worth refereeing. read the letter →

arxiv 2602.19973 v4 pith:QI34GDOS submitted 2026-02-23 cs.PL cs.CR

Cezar-Constantin Andrici , Abigail Pribisova , Danel Ahman , Catalin Hritcu , Exequiel Rivas , Théo Winterhalter This is my paper · ORCID
classification cs.PLcs.CR MSC 68N3068N20
keywords securecompilationprogramextractionrelationalquotationtranslationvalidationlogicalrelationsRobustHyperpropertyPreservationshallowembeddingsIOeffects
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper sets out to show that extracting shallowly embedded effectful programs to a deep lambda calculus need not sacrifice security: extraction can be split so that the only unverified piece is a small metaprogram producing a typing derivation, while all syntax generation and its semantic correctness proof are verified once and for all. The authors build SEIO*, a framework for a proof-oriented language that extracts programs with file-based IO, and give a machine-checked proof of Robust Relational Hyperproperty Preservation (RrHP) for it. RrHP is a very strong secure-compilation criterion: if the result holds, an extracted program behaves the same against any syntactically typed adversarial context as the original program does, preserving trace properties and hyperproperties such as noninterference. A sympathetic reader would care because this is the first extraction pipeline for such a language to aim at security guarantees against linked unverified code, not just correctness.

What carries the argument

The load-bearing object is the typing relation over the shallow embedding, using open values as functions from evaluation environments; this lets typing derivations be tied by dependent types to a specific F* program. A metaprogram follows the program's structure to produce a derivation, which the proof language validates by type-checking—this is translation validation limited to quotation. A verified syntax-generation function then maps derivations to lambda_io expressions. Two asymmetric cross-language logical relations, defined on a trace-producing operational semantics with histories, local traces, and fresh file descriptors, connect source and target behaviors and support the RrHP proof

What would settle it

Take two target contexts that differ only in how they use the actual file system—say, a write followed by a read of the same descriptor, whose result depends on stored file contents—and check whether the trace semantics assigns them the same events. If the observable result of a linked extracted program differs between a concrete file system and the trace semantics, then the RrHP theorem, as proved over traces, would not apply to that program; finding such a program would show the guarantee is trace-level, not state-level.

Watch

Extended reading notes

Core claim

The central claim is that relational quotation—a translation-validation step in which a metaprogram constructs a typing derivation that the host type-checker itself validates against the original shallowly embedded program—makes the rest of extraction a pure, once-and-for-all verified function. From a valid typing derivation, SEIO* generates lambda_io syntax whose traces are guaranteed, by two cross-language logical relations, to match the source program's traces for every possible history. The paper proves in the host proof assistant that this setup satisfies RrHP: for every target context there exists a source context such that the linked extracted program and the linked source program pro

Load-bearing premise

The theorem's guarantee lives in an abstract trace semantics and for syntactically typed target contexts; it does not model actual file-system state, and the final step to an executable goes through an explicitly unverified compiler, so 'arbitrary adversarial linked code' in practice is not covered by the proof.

Editorial extensions

If this is right

  • Verified effectful programs extracted with SEIO* keep their safety and trace properties even when linked with code that is itself unverified, as long as the context is expressible in the typed target calculus.
  • Observational equivalence is preserved: two source programs that cannot be told apart by source contexts remain indistinguishable after extraction, and vice versa.
  • RrHP is transitive, so SEIO* can be composed with earlier secure-compilation layers for the same proof language to push guarantees closer to machine code.
  • The approach narrows the trusted computing base: the only unverified part of extraction is the derivation-generating metaprogram; syntax generation and semantic preservation are machine-checked.
  • Hyperproperties such as noninterference are preserved against adversarial contexts, a guarantee stronger than full abstraction alone.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • Because the trace semantics does not model actual file-system state, the theorem covers programs whose IO behavior is fully described by the sequence of operation events; a program relying on invisible state, such as the content of a file across two reads of the same descriptor, may not be protected by the result as stated.
  • The same two-phase structure—unverified relational quotation plus verified syntax generation—could be transplanted to other dependently typed proof assistants, though the typing-derivation construction would need to be re-proved for each language's metaprogramming support.
  • If the final unverified link to an executable is replaced by a verified compiler step satisfying RrHP, the overall pipeline would deliver end-to-end security; until then, 'arbitrary linked adversarial code' should be read as code in the typed target calculus, not arbitrary machine code.
  • The trace-based semantics suggests a natural testable extension: add a concrete file-state model and check whether RrHP still holds; if it fails, the current guarantee is strictly about event traces, not file contents.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 5 minor

Summary. The paper introduces SEIO★, a framework written in F★ for extracting shallowly embedded F★ programs with IO (IO★) to a deep embedding λ_io. The key idea is to split extraction into two phases: an unverified metaprogram called 'relational quotation' that produces a typing derivation for a given shallow program, followed by a verified pure syntax-generation function that turns the derivation into λ_io code. The paper claims a machine-checked proof, in F★, that SEIO★ satisfies Robust Relational Hyperproperty Preservation (RrHP), the strongest secure compilation criterion of Abate et al. [1], which implies full abstraction and preservation of trace properties and hyperproperties against adversarial contexts. The formal development uses two cross-language logical relations between IO★ and λ_io, with compatibility lemmas and back-translation of target contexts.

Significance. If the claims are accurate, the paper makes a significant contribution to certified extraction and secure compilation: it provides the first machine-checked secure extraction guarantee for a proof-oriented language with effects, and it introduces relational quotation as a way to minimize the trusted translation-validation step. The artifact contains a substantial F★ formalization (over 900 top-level definitions) and machine-checked proofs of RrHP. The separation of the unverified metaprogram (whose output is type-checked) from the verified syntax generator is a clean and reusable idea. The paper is also honest about several limitations, including the unverified final compilation step and the abstract trace semantics. However, as detailed below, the advertised scope of the guarantee is broader than what the formal theorem actually states, and this mismatch needs to be addressed before publication.

major comments (3)
  1. [Abstract, §5.1, Theorem 5.1] The abstract and introduction claim RrHP holds 'against arbitrary linked adversarial code'. In contrast, Theorem 5.1 quantifies over target contexts C_T of type ctxT, defined in §5.1 as (ct:value & typingλ empty ct i.ct), i.e., syntactically typed λ_io contexts. Since §5.1 also states that λ_io is 'basically untyped', and §6.2 explicitly leaves the λ_io → λ□ → Malfunction → OCaml step unverified, the machine-checked theorem does not cover untyped λ_io contexts, let alone arbitrary OCaml code. This is a scope mismatch between the headline claim and the formal result, not an internal inconsistency in the proof. I recommend restating the abstract and Theorem 5.1 with the precise hypothesis: the guarantee is for all syntactically typed λ_io contexts that are linked through the verified syntax-generation step, and the executable pipeline is outside the theorem.
  2. [§3.2, §5.1] Theorem 5.1 quantifies over source programs P:progS i, where progS includes a typing derivation. The metaprogram generate_derivation that is supposed to produce this derivation is not verified; the paper itself admits (§3.2) that it cannot formally guarantee that the generated derivation will type-check. Consequently the statement 'SEIO★ extracts F★ programs' is stronger than the formal result: the RrHP guarantee applies only when relational quotation succeeds and F★ type-checks the resulting derivation. The paper should make this conditional explicit in the abstract, in the list of contributions, and around Theorem 5.1, e.g., by phrasing the theorem as 'for every program for which SEIO★ successfully produces a derivation'.
  3. [§4.2, §5.2] The operational semantics of λ_io does not model file-system state; it only generates abstract events, as acknowledged in §4.2. As a result, RrHP is a theorem about the trace-producing abstraction (e.g., events like EvRead and EvOpen) rather than about real file contents or filesystem behavior. This is a modeling limitation, not a flaw in the proof, but it should be stated more prominently in the introduction and conclusion so that readers do not over-interpret 'IO' as covering full file-system semantics. The running example's wrapper_correct property is itself defined over traces, which is consistent, but this point deserves explicit discussion.
minor comments (5)
  1. [§3.2] The sentence 'The metaprogram is simple, since the typing derivation follows the structure of the original program' should be qualified: the paper later explains that the metaprogram is unverified and may fail. Please rephrase to avoid implying a formal completeness result.
  2. [§5.1, linkT] In the definition of linkT, the code reads 'EApp pt (dfst e)' but 'e' is not in scope; presumably it should be 'dfst ct'. Please fix this typo.
  3. [§4.6, c3 proof sketch] In step (4) of the c3 proof sketch, the text says 'beh★ ((λx'→fs_r_f x') fs_r_x)' which appears to be a typo for 'beh★ (fs_r_f fs_r_x)'. The surrounding narrative should be checked for consistency.
  4. [§6.2, Figure 4] Figure 4 labels the pipeline from λ_io to executable but the text does not clearly state which components are verified and which are not. Adding explicit color/annotation for the trusted vs. verified parts would help readers.
  5. [§7] The related-work discussion is thorough, but it would be useful to explicitly compare the adversary model with that of SCIO★ and SecRef★, since those frameworks also prove RrHP but over different target languages. The current text mentions them only briefly at the end.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the machine-checked RrHP proof is derived from independently proved compatibility lemmas, logical-relation fundamental properties, and back-translation; self-citations are contextual or non-load-bearing, and the stated scope restrictions are limitations rather than circular inputs.

full rationale

Following the derivation chain: relational quotation produces a candidate typing derivation whose type is `typing empty _ (\_ -> wrapper)`, and this candidate is validated by F*'s type-checker, so the link between derivation and original program is checked rather than assumed. Syntax generation is a pure recursive function on the typing derivation, and its semantic correctness is stated using the two cross-language logical relations, which are defined from the trace-producing beahviour predicates in §4.2–§4.3, not from RrHP. The compatibility lemmas in §4.6 establish the fundamental property by induction, and Theorems 5.2 and 5.3 compose those lemmas with back-translation to obtain the two directions of RrHP. No step fits a parameter to the claimed conclusion, and no theorem is assumed under a renamed heading. The artifact is machine-checked in F*, and the paper explicitly treats the F* type-checker as trusted, which is a TCB choice rather than a circular premise. Self-citations are not load-bearing: Abate et al. [1] supplies the external RrHP criterion being proved, SCIO* [10] and SecRef* [11] are described as prior secure-compilation frameworks and future-composition targets, and none of these is a premise of Theorem 5.1. The paper also discloses real scope limitations: §4.2 says the operational semantics 'does not actually model any of the files being accessed as some form of state'; §5.1 defines `ctxT` as `ct:value & typing\lambda empty ct i.ct`, so only syntactically typed λ_io contexts are covered; and §6.2 describes an explicitly unverified λ_io→λ□→Malfunction→OCaml step. These restrict the advertised 'arbitrary linked adversarial code' guarantee and are correctness/scope concerns, but they do not make the derivation circular.

Assumptions & free parameters 0 free parameters · 5 assumptions · 0 invented entities

The central theorem depends on the soundness of F*'s type-checker, on an abstract trace model of IO, on restricting attacker contexts to syntactically typed λ_io, and on the unproved completeness of the relational quotation metaprogram. No numeric free parameters are fitted and no new physical entities are postulated.

assumptions (5)
  • domain assumption F*'s type checker is sound and can validate that a generated typing derivation is indeed a derivation for the original program.
    Section 2.2 and 3.2: the metaprogram is intentionally unverified; all trust is placed on F* type-checking of the derivation, including normalization and unification in step 3(c).
  • domain assumption IO can be modeled abstractly: each operation non-deterministically succeeds or fails with a fresh descriptor/error, and no file-system state is represented.
    Section 4.2 explicitly says the operational semantics does not model files as state; Section 4.3 maps all possible IO events to traces. RrHP is relative to this event model.
  • domain assumption Attacker target contexts are exactly syntactically typed λ_io expressions; the subsequent λ_io→λ□→OCaml compilation is unverified.
    Section 5.1 defines ctxT with typing λ; Section 6.2 describes an unverified step to make executables. Thus 'arbitrary linked code' in the abstract is narrower than stated.
  • ad hoc to paper The relational quotation metaprogram is complete: every IO★ program yields a derivation that F* can type-check.
    Section 3.2 claims implicit inference and equality checking 'should always succeed' but provides no proof; the authors admit they cannot formally guarantee generated derivations type-check. If false, extraction fails, though it would not unsoundly succeed.
  • domain assumption The extracted IO★ subset is terminating and free of recursion, dependent types, and refinement types.
    Section 3.1 states 'All IO★ programs are terminating' and lists unsupported features as future work; divergence and recursive behavior are outside the theorem.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Misquoted No More: Securely Extracting F* Programs with IO." pith.science (2026). https://pith.science/paper/QI34GDOS

@misc{pith2026260219973,
  author       = {Pith},
  title        = {Pith review of: Misquoted No More: Securely Extracting F* Programs with IO},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/QI34GDOS}},
  note         = {Machine review of arXiv:2602.19973}
}
read the original 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 formal correctness guarantees using translation validation to certify individual extraction results. We build on this idea, but limit the use of translation validation to a first extraction step that we call relational quotation and that uses a metaprogram to construct a typing derivation for the given shallowly embedded program. This metaprogram is simple, since the typing derivation follows the structure of the original program. Once we validate that the typing derivation is valid for the original program, we pass it to a verified syntax-generation function that produces code guaranteed to be semantically related to the original program. We apply this general idea to build SEIO*, a framework for extracting shallowly embedded F* programs with IO and refinement types to a deeply embedded simply typed lambda-calculus while providing formal secure compilation guarantees. Using two cross-language logical relations, we devise a machine-checked proof in F* that SEIO* guarantees Robust Relational Hyperproperty Preservation (RrHP), a very strong secure compilation criterion that implies full abstraction as well as preservation of trace properties and hyperproperties against arbitrary linked adversarial code. This goes beyond the state of the art in verified and certifying extraction, which so far has focused on correctness rather than security.

Figures

Figures reproduced from arXiv: 2602.19973 by the authors.

Figure 1
Figure 1. An overview of extraction using SEIO★. Solid lines are verified pure F★ functions. The dashed arrow represents the relational quotation metaprogram, the result of which is checked by F★ to be a typing derivation for the original verified program. Contributions: ▶ We introduce relational quotation, a translation validation technique for quoting shallowly embedded programs in a dependently typed language. The idea is … view at source ↗
Figure 2
Figure 2. Running example: a validation wrapper for unverified agents. [PITH_FULL_IMAGE:figures/full_fig_p004_2.png] view at source ↗
Figure 3
Figure 3. The typing relation for IO★. is typed as a value, and each branch is typed in the environment extended with the matched component. QIf is similar for Booleans. In the FGCBV terminology of Levy et al. [26], these are complex values: elimination forms whose result is a value rather than a computation. Second, QLambdaIO is the rule for effectful 𝜆-abstractions: it types a value of type a →io b by requiring the body to … view at source ↗
Figures from the paper (1 more)
Figure 4
Figure 4. Figure 4: Compilation pipeline from 𝜆𝑖𝑜 to executable. then using the tooling provided by the Peregrine project [14] to compile to OCaml (Malfunction [17, 19]) to obtain code that can be later linked with a runtime in OCaml. The 𝜆□ language was introduced in the context of progr…

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

43 extracted references · 1 linked inside Pith

  1. [1]

    Abate, R

    C. Abate, R. Blanco, D. Garg, C. Hritcu, M. Patrignani, and J. Thibault. Journey beyond full abstraction: Exploring robust property preservation for secure compilation.CSF. 2019

    2019

  2. [2]

    Abrahamsson, S

    O. Abrahamsson, S. Ho, H. Kanabar, R. Kumar, M. O. Myreen, M. Norrish, and Y. K. Tan. Proof-producing synthesis of CakeML from monadic HOL functions.Journal of Automated Reasoning (JAR), 2020

    2020

  3. [3]

    Ahman and T

    D. Ahman and T. Uustalu. Update monads: Cointerpreting directed containers.TYPES, 2013

    2013

  4. [4]

    Ahman, C

    D. Ahman, C. Hriţcu, K. Maillard, G. Martínez, G. Plotkin, J. Protzenko, A. Rastogi, and N. Swamy. Dijkstra monads for free.POPL. 2017

    2017

  5. [5]

    Ahman, C

    D. Ahman, C. Fournet, C. Hriţcu, K. Maillard, A. Rastogi, and N. Swamy. Recalling a witness: Foundations and applications of monotonic state.PACMPL, 2(POPL):65:1–65:30, 2018

    2018

  6. [6]

    Ahman, K

    D. Ahman, K. Bhargavan, B. Bond, J. Bosamiya, C. Brzuska, A. Delignat-Lavaud, C. Fournet, A. Fromherz, S. Gibson, C. Hawblitzel, C. Hriţcu, M. Kohlweiss, G. Martínez, H. Ni, B. Parno, J. Protzenko, T. Ramananandro, A. Rastogi, E. Rivas, N. Swamy, and S. Zanella-Béguelin. Project Everest: Perspectives from developing industrial-grade high-assurance softwar...

    2025

  7. [7]

    A. Ahmed. Verified compilers for a multi-language world.SNAPL. 2015

    2015

  8. [8]

    A. J. Ahmed.Semantics of Types for Mutable State. PhD thesis, Princeton University, 2004

    2004

Show all 43 references
  1. [9]

    Anand, A

    A. Anand, A. Appel, G. Morrisett, Z. Paraskevopoulou, R. Pollack, O. S. Belanger, M. Sozeau, and M. Weaver. CertiCoq: A verified compiler for Coq. In3rd Workshop on Coq for Programming Languages (CoqPL), 2017

    2017

  2. [10]

    Andrici, Ş

    C.-C. Andrici, Ş. Ciobâcă, C. Hritcu, G. Martínez, E. Rivas, É. Tanter, and T. Winterhalter. Securing verified IO programs against unverified code in F★.Proc. ACM Program. Lang., 8(POPL):2226–2259, 2024

    2024

  3. [11]

    Andrici, D

    C.-C. Andrici, D. Ahman, C. Hriţcu, R. Icleanu, G. Martínez, E. Rivas, and T. Winterhalter. SecRef★: Securely sharing mutable references between verified and unverified code in F★.Proc. ACM Program. Lang., 9(ICFP), 2025

    2025

  4. [12]

    Annenkov, M

    D. Annenkov, M. Milo, J. B. Nielsen, and B. Spitters. Extracting functional programs from Coq, in Coq.Journal of Functional Programming, 32:e11, 2022

    2022

  5. [13]

    Carneiro

    M. Carneiro. Lean4Lean: Towards a formalized metatheory for the Lean theorem prover.CoRR, abs/2403.14064, 2024

    2024 arXiv

  6. [14]

    Chapman, S

    J. Chapman, S. Dima, L. Escot, Y. Forster, O. Melkonian, E. Nielsen, M. Sozeau, and B. Spitters. Peregrine project: a unified middle-end for code generation from proof assistants. https://peregrine-project.github.io

  7. [15]

    J. M. Cohen and P. Johnson-Freyd. A formalization of core Why3 in Coq.Proc. ACM Program. Lang., 8(POPL), 2024

    2024

  8. [16]

    Devriese, M

    D. Devriese, M. Patrignani, and F. Piessens. Fully-abstract compilation by approximate back-translation.POPL, 2016

    2016

  9. [17]

    S. Dolan. Malfunctional programming. InML Family Workshop 2016, 2016

    2016

  10. [18]

    Forster and F

    Y. Forster and F. Kunze. A certifying extraction with time bounds from Coq to call-by-value lambda calculus. In J. Harrison, J. O’Leary, and A. Tolmach, editors,10th International Conference on Interactive Theorem Proving, ITP 2019, Portland, OR, USA, September 9-12, 2019. 2019

    2019

  11. [19]

    Forster, M

    Y. Forster, M. Sozeau, and N. Tabareau. Verified extraction from Coq to OCaml.Proc. ACM Program. Lang., 8(PLDI): 52–75, 2024

    2024

  12. [20]

    Gladshtein, G

    V. Gladshtein, G. Pîrlea, Q. Zhao, V. Kurin, and I. Sergey. Foundational multi-modal program verifiers.Proc. ACM Program. Lang., 10(POPL):2233–2264, 2026

    2026

  13. [21]

    Gonthier, B

    G. Gonthier, B. Ziliani, A. Nanevski, and D. Dreyer. How to make ad hoc proof automation less ad hoc.Journal of Functional Programming, 23(4):357–401, 2013

    2013

  14. [22]

    Grimm, K

    N. Grimm, K. Maillard, C. Fournet, C. Hriţcu, M. Maffei, J. Protzenko, T. Ramananandro, A. Rastogi, N. Swamy, and S. Zanella-Béguelin. A monadic framework for relational verification: Applied to information security, program equivalence, and optimizations.CPP, 2018

    2018

  15. [23]

    Hupel and T

    L. Hupel and T. Nipkow. A verified compiler from Isabelle/HOL to CakeML. In A. Ahmed, editor,Programming Languages and Systems - 27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Th...

    2018

  16. [24]

    Kumar, M

    R. Kumar, M. O. Myreen, M. Norrish, and S. Owens. CakeML: a verified implementation of ML. InThe 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL. 2014

    2014

  17. [25]

    Letouzey.Programmation fonctionnelle certifiée : L’extraction de programmes dans l’assistant Coq

    P. Letouzey.Programmation fonctionnelle certifiée : L’extraction de programmes dans l’assistant Coq. (Certified functional programming: Program extraction within Coq proof assistant). PhD thesis, University of Paris-Sud, Orsay, France, 2004

    2004

  18. [26]

    P. B. Levy, J. Power, and H. Thielecke. Modelling environments in call-by-value programming languages.Inf. Comput., 185(2):182–210, 2003

    2003

  19. [27]

    Liesnikov and J

    B. Liesnikov and J. Cockx. Building a correct-by-construction type checker for a dependently typed core language. In O. Kiselyov, editor,Programming Languages and Systems - 22nd Asian Symposium, APLAS 2024, Kyoto, Japan, October 22-24, 2024, Proceedings. 2024

    2024

  20. [28]

    Maillard, D

    K. Maillard, D. Ahman, R. Atkey, G. Martínez, C. Hriţcu, E. Rivas, and E. Tanter. Dijkstra monads for all.PACMPL, 3 (ICFP), 2019. Misquoted No More: Securely Extracting F★ Programs with IO 25

    2019

  21. [29]

    Martínez, D

    G. Martínez, D. Ahman, V. Dumitrescu, N. Giannarakis, C. Hawblitzel, C. Hriţcu, M. Narasimhamurthy, Z. Paraskevopoulou, C. Pit-Claudel, J. Protzenko, T. Ramananandro, A. Rastogi, and N. Swamy. Meta-F*: Proof automation with SMT, tactics, and metaprograms.ESOP. 2019

    2019

  22. [30]

    Meier, M

    W. Meier, M. Jensen, J. Pichon-Pharabod, and B. Spitters. CertiCoq-Wasm: A verified WebAssembly backend for CertiCoq. InProceedings of the 14th ACM SIGPLAN International Conference on Certified Programs and Proofs. 2025

    2025

  23. [31]

    Mullen, S

    E. Mullen, S. Pernsteiner, J. R. Wilcox, Z. Tatlock, and D. Grossman. Œuf: minimizing the Coq extraction TCB. In Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs. 2018

    2018

  24. [32]

    M. O. Myreen and S. Owens. Proof-producing translation of higher-order logic into pure and stateful ML.Journal of Functional Programming (JFP), 24(2-3):284–315, 2014

    2014

  25. [33]

    G. Neis, C. Hur, J. Kaiser, C. McLaughlin, D. Dreyer, and V. Vafeiadis. Pilsner: a compositionally verified compiler for a higher-order imperative language.ICFP, 2015

    2015

  26. [34]

    M. S. New, W. J. Bowman, and A. Ahmed. Fully abstract compilation via universal embedding.ICFP. 2016

    2016

  27. [35]

    Nezamabadi, M

    D. Nezamabadi, M. O. Myreen, and Y. K. Tan. Verified VCG and verified compiler for Dafny. InProceedings of the 15th ACM SIGPLAN International Conference on Certified Programs and Proofs. 2026

    2026

  28. [36]

    Patrignani, A

    M. Patrignani, A. Ahmed, and D. Clarke. Formal approaches to secure compilation: A survey of fully abstract compilation and related work.ACM Computing Surveys, 2019

    2019

  29. [37]

    Pit-Claudel, J

    C. Pit-Claudel, J. Philipoom, D. Jamner, A. Erbsen, and A. Chlipala. Relational compilation for performance-critical applications: extensible proof-producing translation of functional models into low-level code. In R. Jhala and I. Dillig, editors,PLDI ’22: 43rd ACM SIGPLAN Int...

    2022

  30. [38]

    Protzenko, J.-K

    J. Protzenko, J.-K. Zinzindohoué, A. Rastogi, T. Ramananandro, P. Wang, S. Zanella-Béguelin, A. Delignat-Lavaud, C. Hriţcu, K. Bhargavan, C. Fournet, and N. Swamy. Verified low-level programming embedded in F*.PACMPL, 1 (ICFP):17:1–17:29, 2017

    2017

  31. [39]

    Protzenko, B

    J. Protzenko, B. Parno, A. Fromherz, C. Hawblitzel, M. Polubelova, K. Bhargavan, B. Beurdouche, J. Choi, A. Delignat- Lavaud, C. Fournet, N. Kulatova, T. Ramananandro, A. Rastogi, N. Swamy, C. M. Wintersteiger, and S. Z. Béguelin. EverCrypt: A fast, verified, cross-platform cr...

    2020

  32. [40]

    Rastogi, G

    A. Rastogi, G. Martínez, A. Fromherz, T. Ramananandro, and N. Swamy. Programming and proving with indexed effects, 2021

    2021

  33. [41]

    Sozeau, Y

    M. Sozeau, Y. Forster, M. Lennon-Bertrand, J. Nielsen, N. Tabareau, and T. Winterhalter. Correct and complete type checking and certified erasure for Coq, in Coq.J. ACM, 72(1), 2025

    2025

  34. [42]

    N. Swamy. Agentic proof-oriented programming. RiSE MSR Blog, 2026

    2026

  35. [43]

    Swamy, C

    N. Swamy, C. Hriţcu, C. Keller, A. Rastogi, A. Delignat-Lavaud, S. Forest, K. Bhargavan, C. Fournet, P.-Y. Strub, M. Kohlweiss, J.-K. Zinzindohoué, and S. Zanella-Béguelin. Dependent types and multi-monadic effects in F*.POPL. 2016

    2016

Pith tools

Reviewed August 2, 2026 · model on record in the stance chip above.