Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Coq formalization of IDL-Soundness #143

Merged
merged 7 commits into from
Dec 4, 2020
Merged

Coq formalization of IDL-Soundness #143

merged 7 commits into from
Dec 4, 2020

Conversation

nomeata
Copy link
Collaborator

@nomeata nomeata commented Nov 30, 2020

based on our experience, we really can really use some formal treatment of our
Candid work.

This branch contains some initial work. Current status and rough plan:

  • A simple Coq setup (using the more modern dune-based setup)
  • A nix-setup to build this
  • Simple CI integration
  • A Coq-ification of the definitions in IDL-Soundness.md
  • Mechanizing the “canonical subtyping is sound” proof in that document
  • Wait for the discussion in Still not sound: Gradual typing vs. opportunistic decoding #141 to settle
  • Verify the rules of a “toy candid” (with much fewer types, but still
    enough to express the interesting bits)

using the shiny new support in dune to build Coq projects:
https://dune.readthedocs.io/en/stable/dune-files.html#coq-theory
without the proof for canonical subtyping yet.
@nomeata nomeata force-pushed the joachim/coq branch 3 times, most recently from 7feddc1 to b0fd483 Compare November 30, 2020 18:16
@rossberg
Copy link
Contributor

He he, thumbs up!

@nomeata nomeata changed the title [WIP] Coq formalization of Candid Coq formalization of IDL-Soundness Dec 3, 2020
@nomeata nomeata marked this pull request as ready for review December 3, 2020 11:20
@nomeata
Copy link
Collaborator Author

nomeata commented Dec 3, 2020

This might be good enough to get into the repo. Not tacking Candid proper yet, that should wait for #141 to settle.

@nomeata nomeata merged commit b25d736 into master Dec 4, 2020
@nomeata nomeata deleted the joachim/coq branch December 4, 2020 09:19
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants