Organizers

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

Information

Fridays, 12:15 p.m. , room: 5450

Research fields

List of talks

Dec. 11, 2026, 12:15 p.m.
Andrzej Radźmiński (MIM)
Rozszerzenia systemu typów Rusta (Extensions of Rust type system)
Nov. 20, 2026, 12:15 p.m.
Maja Kądziołka (MIM)
Syntetyczna teoria obliczeń (Synthetic computation theory)
Nov. 6, 2026, 12:15 p.m.
Aleksy Schubert (MIM)
O dowodzeniu AD 2026 (i roli LLM-ów) (On proving in 2026 (and the role of LLMs therein))
March 13, 2026, 12:15 p.m.
Aleksy Schubert (MIMUW)
What is higher in the higher-order matching now? (Co nowego udało się dopasować w dopasowaniu wyższego rzędu?)
Jan. 23, 2026, 12:15 p.m.
Andrzej Tarlecki (MIMUW)
On the stability and fragility of interpolation (O stabilności i delikatności interpretacji)
The main topic of this talk is a version of the Craig interpolation theorem formulated for an arbitrary logical system formalised as an institution, which proved crucial in the development of a number of key …
Jan. 9, 2026, 12:15 p.m.
Michał Gajda (MIMUW)
Dependent types in ultrafinitistic logic (Typy zależne w logice ultrafinitystycznej)
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, …
Dec. 19, 2025, 12:15 p.m.
Michał Gajda (MIMUW)
MaxSAT and its applications (MaxSAT i jego zastosowania)
Maximum Satisfiability (MaxSAT) uses satisfiability solvers (SAT) for discrete optimization. The principle is to maximize the number of simultaneously satisfied "optional" rules (because mandatory rules must always be satisfied). This enables solving NP-hard problems such …
Dec. 12, 2025, 12:15 p.m.
Marcin Benke (MIMUW)
What is solid in the new Solidity? (Co nowego w Solidity?)
Nov. 28, 2025, 12:15 p.m.
Konrad Zdanowski (UKSW)
Strong completeness for CTL, continuation (Silne twierdzenie o pełności dla CTL, ciąg dalszy)
Nov. 21, 2025, 12:15 p.m.
Kordula Świętorzecka (UKSW)
Strong completeness for CTL (Silne twierdzenie o pełności dla CTL)
We will discuss the history of the development of Prior’s temporal logics, which are now used in computer science. Our main focus will be the branching-time logic CTL. We will examine issues related to completeness …
Nov. 7, 2025, 12:15 p.m.
Maurycy Wojda (MIMUW)
A Search Engine for Theorems (Wyszukiwarka twierdzeń)
Oct. 24, 2025, 12:15 p.m.
Paweł Balawender (MIMUW)
Reasoning about bounded arithmetic within Lean 4 (Rozumowanie o ograniczonej arytmetyce w Lean 4)
The theories of modern proof assistants (e.g. Rocq, Lean, Mizar) are highly expressive. This is usually a desirable feature, since we want these tools to be capable of verifying proofs of complex theorems. However, sometimes …
Oct. 17, 2025, 12:15 p.m.
Jacek Chrząszcz (MIMUW)
What rocks in the new Rocq? (Co w nowym Rocq-u?)
In the talk, we will present the latest changes in The Rocq Prover, formerly known as the Coq Proof Assistant. In particular, we will present new features of the prover, such as rewriting rules (at …
June 13, 2025, 12:15 p.m.
Aleksy Schubert (MIMUW)
(talk cancelled) ((referat usunięty))
June 13, 2025, 12:15 p.m.
Michał Gajda
Eldarica and Horn clause solvers (Eldarica i solvery dla klauzul Hornowskich)