Dependent types in ultrafinitistic logic

Prelegent(ci)

Michał Gajda

Afiliacja

MIMUW

Język referatu

angielski

Termin

9 stycznia 2026 12:15

Pokój

p. 5450

Tytuł w języku polskim

Typy zależne w logice ultrafinitystycznej

Seminarium

Semantyka, Logika I Weryfikacja Oraz Wiele Ich Ciekawych Aplikacji

---

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.

---

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.

---