Skip to content

add GhostCell proof

Ralf Jung requested to merge ci/ralf/ghostcell into master

I propose we add the GhostCell proof to the lambda-rust master. This is basically a cleanup and forward-port of the existing proof for that paper. The original proofs are by Joshua Yanovski.

The branch isn't done yet, I'll add more commits here as I make progress, but if you have comments already, feel free to chime in. :) I'll do my best to make the individual commits meaningful, so reviewing commit-by-commit is probably best.

  • Lifetime logic basics
  • Type system changes
  • BrandedVec proof
  • GhostCell proof
Edited by Ralf Jung

Merge request reports