چارچوب Eigenius برای نگهداری دانشِ نوع‌دار و ثبت منشأ شواهد معرفی شد

در نظریه‌های نوع برای ریاضیات یا راستی‌آزمایی برنامه، معمولاً کافی است گزاره‌ای درست باشد؛ اما یک مخزن دانش پایدار باید ثبت کند چه کسی ادعا را تأیید کرده، این تأیید بر چه استدلال یا ابزار بیرونی تکیه داشته و تحت چه فرض‌هایی انجام شده است. پیش‌چاپی در arXiv نظریهٔ Eigenius را برای پاسخ به این نیاز صورت‌بندی می‌کند.

هستهٔ Eigenius بر نظریهٔ نوع وابسته استوار است و جهان‌های تجمعی، جهان گزاره‌های impredicative، خانواده‌های استقرایی و نوع همانی intensional را در بر می‌گیرد. در این چارچوب، بی‌ربطی اثبات یک اصل با شاهد صریح است، نه قاعده‌ای برای حذف تفاوت اثبات‌ها هنگام تبدیل؛ بنابراین اثبات‌های یک گزاره برابر دانسته می‌شوند، اما همچنان به‌صورت عبارت‌های متمایز باقی می‌مانند.

پژوهش همچنین منطق توجیه را برای ردیابی شواهد و پشتوانهٔ ادعاها، سازمان‌دهی محیط‌ها به‌شکل یک institution، و نظریه‌ای برای گراف دانش نوع‌دار با رکوردها، کلاس‌ها و refinementها توسعه می‌دهد. نویسندگان سازگاری چارچوب را با یک مدل نظریه‌مجموعه‌ای اثبات کرده‌اند و درستی تبدیل، نرمال‌سازی با ارزیابی و type checking دوسویه را نیز بررسی کرده‌اند. همراه این کار، پیاده‌سازی صوری در Lean 4 ارائه شده است.