Typing Rules Become Programs in Tree Calculus, All Theorems Mechanized in Rocq
teropa · x · 2026-11-05
Barry Jay released a new paper showing that in tree calculus, typing rules become programs: type inference is just evaluation (infer @ t ⟹ Sm T), and type application replaces function types, type variables, and quantifiers—no stratified type hierarchy needed. The system supports general recursion, polymorphic lists, type-directed conditionals, length-indexed arrays, queries and updates, with a type-inference program that types itself. All theorems are mechanized in Rocq, with proofs open-sourced on GitHub under MIT license.
More from Research
- Stanford benchmark: frontier models reach best team deal in only 14% of conflicts — rohanpaul_ai · 2026-11-05
- RL theory monograph by Chen, Chi, Fan et al: Statistical Foundations of RL, a non-asymptotic view — burny_tech · 2026-11-05
- Weight-space programming reproduced: GPT-6.1 beats PPO baseline 21x, no open-weight model passes it — burny_tech · 2026-11-05
- Chinese AI Scientist completes 11,382-step experiment in 203 hours autonomously — yogthos · 2026-11-05
- 8% of Nature peer reviews since June 2025 are fully AI-generated, analysis finds — TuhinChakr · 2026-11-05
- HandsOn benchmark: best dexterous manipulation policy manages only 29.1% success on Core-50 — jiqizhixin · 2026-11-05