Mechanized Artifacts for "A Necessary Formation-Theoretic Invariant Against Illegitimate Propositional Lifting"

Zenodo (CERN European Organization for Nuclear Research) 2026 Open access

Read full text
Authors: Najih Salhab
DOI: 10.5281/zenodo.18196604
Cited by: 0

Abstract

This repository contains mechanized artifacts (Z3 and Cubical Agda) accompanying the paper“A Necessary Formation-Theoretic Invariant Against Illegitimate Propositional Lifting”. The artifacts provide independent validation of the formation-level results.They introduce no additional assumptions and are not required for reading or verifying the main proof.

Fields of Study & Subjects

Logic programming and type systems Reasoning and Knowledge Formal Methods in Verification

Publication details

Journal / source
Zenodo (CERN European Organization for Nuclear Research)
Publication date
9 January 2026