Coq-CompCert – Dataset by phanerozoic | AlphaNeural AI

You can deploy this model and start earning money today!

phanerozoic/
Coq-CompCert

like

0

text-generation

feature-extraction

theorem-proving

compiler-verification

Views

No views yet

Coq-CompCert

A structured dataset of formalizations from CompCert, the verified C compiler.

Source

Repository: https://github.com/AbsInt/CompCert Commit: 0ef26dad76446c803da02d7368eb4f9d074c1401 Files: 222 License: other

	Schema

Column Type Description

statement string Declaration signature/claim with the leading keyword removed (verbatim slice); the full declaration minus its proof

proof string Verbatim proof/body, empty if the… See the full description on the dataset page: https://huggingface.co/datasets/phanerozoic/Coq-CompCert.