Tony's Wiki
Search
Search
Dark mode
Light mode
Explorer
Tag: context/research
20 items with this tag.
Jun 05, 2026
Deep Target Splitting
type/concept
context/research
project/iso-types
Jun 05, 2026
Distributivity Subtyping Laws (dist-arrow, dist-mu)
type/concept
context/research
project/iso-types
Jun 05, 2026
Double-Vision Recursive Modules
type/concept
context/research
project/modrec
Jun 05, 2026
Incompleteness of the Algorithmic μ-Rule
type/concept
context/research
project/iso-types
Jun 05, 2026
Locator-Anchored Signatures
type/concept
context/research
project/modrec
Jun 05, 2026
Partial Recursive Signatures
type/concept
context/research
project/modrec
Jun 05, 2026
Size-Stratified Mutual Transitivity
type/concept
context/research
project/iso-types
Jun 05, 2026
Source-to-Source Encoding Correctness (double vision)
type/concept
context/research
project/modrec
Jun 05, 2026
Split-Cover and Polarity Certificates (CLIMB / RIGID)
type/concept
context/research
project/iso-types
Jun 05, 2026
Weakly Positive Subtyping (wp)
type/concept
context/research
project/iso-types
Jun 05, 2026
wp Transitivity via Cover Routing (v3 → v4 → Option C)
type/concept
context/research
project/iso-types
Jun 05, 2026
Driving Claude Code on Hard Proofs
type/lesson
context/research
project/iso-types
Jun 05, 2026
Proof Engineering Lessons (Rocq wp_isorec)
type/lesson
context/research
project/iso-types
Jun 05, 2026
A-posteriori soundness condition for deep splitting
type/question
context/research
project/iso-types
Jun 05, 2026
Applicative vs generative encoding — is the () barrier the only difference?
type/question
context/research
project/modrec
Jun 05, 2026
Better decidability — higher-kinded witnesses never compared by equivalence?
type/question
context/research
project/modrec
Jun 05, 2026
Does the cover CLIMB/RIGID wall imply algorithmic incompleteness?
type/question
context/research
project/iso-types
Jun 05, 2026
Global ≡ premise under a CLIMB cov_BC entry
type/question
context/research
project/iso-types
Jun 05, 2026
How deep must target splitting go?
type/question
context/research
project/iso-types
Jun 05, 2026
iff/equivalence vs preservation+reflection for encoding correctness?
type/question
context/research
project/modrec