Metadata Release of the Archive of Formal Proofs for Isabelle2021 (04-16)
收藏NIAID Data Ecosystem2026-03-12 收录
下载链接：
https://zenodo.org/record/4697475
下载链接
链接失效反馈官方服务：
资源简介：
Archive of Formal Proofs Metadata
This is a release of the entries metadata from the Archive of Formal Proofs which corresponds to https://foss.heptapod.net/isa-afp/afp-2021 @ 679cb16760ca490e5bd161495ad9cb5b629d16a6 (2021-04-16).
Format
The data is in the form of a list of JSON objects, one per entry. The objects are ordered by session name but there is no strict ordering of the attributes in each object.
session
Required: Yes
Type: String
Description: The name of the Isabelle session. This is the name used when importing the theory.
title
Required: Yes
Type: String
Description: The title of the entry in the Archive of Formal Proofs
authors
Required: Yes
Type: [String]
Description: A list of the authors in the order they were submitted in
contributors
Required: No
Type: [String]
Description: Optional list of contributors, often with a description under the extra attribute
date
Required: Yes
Type: String
Description: Date of submission in the YYYY-MM-DD ISO 8601 format
topics
Required: Yes
Type: [String]
Description: List of topics
abstract
Required: Yes
Type: String
Description: The abstract of the entry which may contain HTML, MathJax and newlines ("\n")
extra
Required: No
Type: {String: String}
Description: Extra information about the entry which is "Change history" most of the time. Other keys found here are "Origin" and "Note".
license
Required: Yes
Type: String
Description: Either "BSD" or "LGPL". "BSD" is the default license in the AFP.
olderReleases
Required: No
Type: [{String: String}]
Description: Date of each release and the corresponding Isabelle release it featured in, in descending order.
dependencies
Required: No
Type: [String]
Description: Session names that the entry is dependent on.
theories
Required: No
Type: [String]
Description: List of theory files in order that they are executed in.
Changes from the upstream data
The license is always specified.
Dependencies, older releases and theories are new attributes.
The upstream data uses strings for all attributes.
The author names are consolidated so that authors can be collated properly.
Author email addresses are removed.
The example submission is omitted.
创建时间：
2021-04-17
