Skip to content
Merged
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
29 changes: 29 additions & 0 deletions CITATION.cff
Original file line number Diff line number Diff line change
@@ -0,0 +1,29 @@
cff-version: 1.2.0
message: "If you use this software, please cite it as below."
type: software
title: "Absolute Zero"
abstract: "Multi-prover formal verification of Certified Null Operations (CNO: programs provably computing nothing) and Observational Null Disclosure (OND: programs provably revealing nothing). Two co-equal, logically independent pillars mechanised in several provers, including Coq, Lean 4 and Agda, with axiom counts and out-of-scope residue lists honestly surfaced."
authors:
- family-names: "Jewell"
given-names: "Jonathan D.A."
orcid: "https://orcid.org/0000-0002-3078-6652"
Comment thread
hyperpolymath marked this conversation as resolved.
repository-code: "https://github.com/hyperpolymath/absolute-zero"
keywords:
- "coq"
- "agda"
- "lean4"
- "formal-verification"
- "epistemic-computing"
- "epistemic-infrastructure"
- "equivalence-aware-computing"
- "hyperpolymath"
- "open-source"
- "rocq-prover"
- "theorem-proving"
- "typed-provenance"
- "veridical-computing"
- "certified-null-operations"
- "multi-prover-verification"
- "observational-null-disclosure"
- "proof-engineering"
- "reversible-computing"
Loading