Organizatorzy

dr hab. Aleksy Schubert, prof. ucz.
prof. dr hab. Andrzej Tarlecki
prof. dr hab. Paweł Urzyczyn

Informacje

piątki, 12:15 , sala: 5450

Dziedziny badań

Lista referatów

11 grudnia 2026 12:15
Andrzej Radźmiński (MIM)
Rozszerzenia systemu typów Rusta (Extensions of Rust type system)
20 listopada 2026 12:15
Maja Kądziołka (MIM)
Syntetyczna teoria obliczeń (Synthetic computation theory)
6 listopada 2026 12:15
Aleksy Schubert (MIM)
O dowodzeniu AD 2026 (i roli LLM-ów) (On proving in 2026 (and the role of LLMs therein))
13 marca 2026 12:15
Aleksy Schubert (MIMUW)
What is higher in the higher-order matching now? (Co nowego udało się dopasować w dopasowaniu wyższego rzędu?)
23 stycznia 2026 12:15
Andrzej Tarlecki (MIMUW)
On the stability and fragility of interpolation (O stabilności i delikatności interpretacji)
Głównym tematem tego wystąpienia jest wersja twierdzenia Craiga o interpolacji sformułowana dla dowolnego systemu logicznego ujętego w postaci instytucji, będącej kluczowym pojęciem w rozwoju szeregu istotnych idei i wyników dotyczących podstaw specyfikacji oprogramowania oraz jego …
9 stycznia 2026 12:15
Michał Gajda (MIMUW)
Dependent types in ultrafinitistic logic (Typy zależne w logice ultrafinitystycznej)
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 …
19 grudnia 2025 12:15
Michał Gajda (MIMUW)
MaxSAT and its applications (MaxSAT i jego zastosowania)
Największa Spełnialność (MaxSAT) korzysta z rozwiązywaczy spełnialności (SAT) do optymalizacji dyskretnej. Zasadą jest maksymalizacja liczby jednocześnie spełnionych reguł „opcjonalnych” (bo reguły obowiązkowe muszą być spełnione zawsze.) Umożliwia to rozwiązywanie problemów NP-trudnych, takich jak pokrycie zbiorów …
12 grudnia 2025 12:15
Marcin Benke (MIMUW)
What is solid in the new Solidity? (Co nowego w Solidity?)
28 listopada 2025 12:15
Konrad Zdanowski (UKSW)
Strong completeness for CTL, continuation (Silne twierdzenie o pełności dla CTL, ciąg dalszy)
21 listopada 2025 12:15
Kordula Świętorzecka (UKSW)
Strong completeness for CTL (Silne twierdzenie o pełności dla CTL)
7 listopada 2025 12:15
Maurycy Wojda (MIMUW)
A Search Engine for Theorems (Wyszukiwarka twierdzeń)
24 października 2025 12:15
Paweł Balawender (MIMUW)
Reasoning about bounded arithmetic within Lean 4 (Rozumowanie o ograniczonej arytmetyce w Lean 4)
Teorie nowoczesnych asystentów dowodowych (np. Rocq, Lean, Mizar) mają bardzo dużą siłę wyrazu. Zazwyczaj jest to cecha pożądana, bo chcemy by te narzędzia były w stanie weryfikować dowody trudnych twierdzeń. Czasem jednak chcemy rozumować w …
17 października 2025 12:15
Jacek Chrząszcz (MIMUW)
What rocks in the new Rocq? (Co w nowym Rocq-u?)
Podczas seminarium opowiemy o najnowszych zmianach w The Rocq Prover, dawniej the Coq Proof Assistant. Przedstawimy w szczególności nowe elementy provera, takie jak reguły przepisywania (wreszcie ;), a także opowiemy o zmianach w elementach istniejących. …
13 czerwca 2025 12:15
Aleksy Schubert (MIMUW)
(talk cancelled) ((referat usunięty))
13 czerwca 2025 12:15
Michał Gajda
Eldarica and Horn clause solvers (Eldarica i solvery dla klauzul Hornowskich)