Interaction-Type-Theory

Tech stack & purpose

Interaction Type Theory (InTT) is a minimal formal system for logical reasoning and proof checking, created by extending Symmetric Interaction Combinators with a new "Decay" rule and a coherence condition. The system aims to express propositions and verify proofs in a manner similar to the Calculus of Constructions, with potential applications to program synthesis and symbolic AI. InTT represents types and proofs as interaction nets, where special annotation nodes can decay when they satisfy the coherence condition, and the system allows encoding of arbitrary types and type-theoretic features through introduction and elimination rules that respect coherence.

Languages

Contributors

• Victor Maia42 commits
• 
  Victor Taelin22 commits · 6,113 followers
• maiavictor19 commits
• Derenash2 commits
• MaiaVictor1 commits
• 
  Yan Mendes1 commits · 82 followers