You are not logged in |
Weekly research seminar
Organizers
- dr hab. Aleksy Schubert, prof. ucz.
- prof. dr hab. Andrzej Tarlecki
- prof. dr hab. Paweł Urzyczyn
Information
Fridays, 12:15 p.m. , room: 5450Research fields
List of talks
-
Jan. 22, 2027, 12:15 p.m.
Aleksy Schubert (MIM)
Semantyka denotacyjna dla stopniowego typowania (Denotational semantics for gradual typing)
-
-
Jan. 8, 2027, 12:15 p.m.
Maja Kądziołka (MIM)
Konstruktywna zawartość klasycznych dowodów (Constructive content of classical proofs)
-
Dec. 18, 2026, 12:15 p.m.
Aleksy Schubert (MIM)
Hierarchia Minca dla kwantyfikatora egzystencjalnego (Minc hierarchy for the existential quantifier)
-
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. 13, 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))
-
Nov. 6, 2026, 12:15 p.m.
Vincent Moreau (Tallinn University of Technology)
Profinite λ-terms and higher-order regular languages (λ-terms proskończone i regularne języki wyższego rzędu)
For several years now, there has been a growing connection between automata theory and λ-calculus, in terms of syntax, semantics and logic. We introduce profinite λ-terms, a higher-order generalization of the notion of profinite word …
-
Oct. 30, 2026, 12:15 p.m.
Konrad Zdanowski (UKSW)
O zupełnych algebrach Heytinga (On complete Heyting algebras)
This presentation is based upon a recent paper 'Two applications of the point-free coderivative'by Zoltan A. KocsisThe abstract of this paper isWe present two new applications of Simmons' point-free Cantor-Bendixsoncoderivative operator in intuitionistic logic. First, we …
-
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)
