Dependent types in ultrafinitistic logic

Speaker(s)

Michał Gajda

Affiliation

MIMUW

Language of the talk

English

Date

Jan. 9, 2026, 12:15 p.m.

Room

room 5450

Title in Polish

Typy zależne w logice ultrafinitystycznej

Seminar

Seminar Semantics, Logic, Verification and its Applications

---

The talk will be a report on the current state of work on translating my Common Ultrafinitistic Logic (CUFL) into dependent types (DUFL) and on proving the conservativity of this extension in Agda. In addition, I am attempting to translate the subsystem for bounding term complexity (complexity bounds) into a calculus that allows encoding all total functions. For clarity, I will present the rules on slides. I will report on the current state of the work and the rules.

---

Referat będzie raportem z obecnego stanu prac nad przełożeniem mojej Spółnej Logiki Ultrafinitystycznej (CUFL) na typy zależne (DUFL) i udowodnienia konserwatywności tego rozszerzenia w Agdzie. Dodatkowo próbuję przełożyć podsystem ograniczania złożoności termów (complexity bounds) na rachunek pozwalający zakodować każde funkcje totalne. Dla przejrzystości pokażę reguły na slajdach. Zaraportuję stan prac i reguły.

---