Datasetpublic

ReactorJet/Coq-Iris

Coq-Iris Structured dataset from Iris, a higher-order concurrent separation logic framework for Coq. Schema Column Type Description fact string Declaration body type string Lemma, Definition, Class, Global, Local, etc. library string Module (iris, iris_heap_lang, iris_unstable, etc.) imports list Require/Import statements filename string Source file path symbolic_name string Declaration identifier Statistics By… See the full description on the dataset page: https://huggingface.co/datasets/ReactorJet/Coq-Iris.

sourceHugging Facebsd-3-clauseupdated 6mo agoView on Hugging Face

0likes8downloads

Dataset Card

Coq-Iris

Structured dataset from Iris, a higher-order concurrent separation logic framework for Coq.

Dataset Description

—Source: gitlab.mpi-sws.org/iris/iris
—Entries: 10,229
—Files processed: 213
—License: BSD-3-Clause

Schema

Column	Type	Description
fact	string	Declaration body
type	string	Lemma, Definition, Class, Global, Local, etc.
library	string	Module (iris, irisheaplang, iris_unstable, etc.)
imports	list	Require/Import statements
filename	string	Source file path
symbolic_name	string	Declaration identifier

Statistics

By Type

Type	Count
Lemma	4,569
Global	3,262
Local	932
Definition	707
Class	205
Ltac	124
Notation	96
Program	81
Inductive	78
Record	59

By Library

Library	Count
iris	8,278
tests	981
irisheaplang	657
iris_unstable	197
iris_deprecated	116

About Iris

Iris is a framework for higher-order concurrent separation logic, used for reasoning about concurrent and distributed programs. It is widely used in verified systems software research.

Use Cases

—Retrieval/RAG for Iris/separation logic
—Learning concurrent verification patterns
—Training embeddings for formal proofs
—Verified systems research