interaction-calculus-of-constructions

Tech stack & purpose

The Interaction Calculus of Constructions is a minimal proof checker exploring whether a simpler type system than the traditional Calculus of Constructions can verify mathematical proofs. Built on interaction combinators extended with a single annotation node primitive, the system aims to support dependent types and inductive reasoning through encoded constructs rather than primitives. The repository includes a toy implementation written in a functional style, along with example proofs demonstrating how dependent functions, dependent pairs, and inductive types can be expressed using the annotation and bridge operators. The work represents an evolution of prior research by the same author on interaction-based type theory.

Languages

Contributors

• 
  Victor Taelin18 commits · 6,113 followers
• NoamDev1 commits