Semantyka, Logika I Weryfikacja Oraz Wiele Ich Ciekawych Aplikacji

Organizatorzy

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

Informacje

Dziedziny badań

• Logika w informatyce
• Semantyka i metody formalne
• Teoria automatów

Lista referatów

• 22 stycznia 2027 12:15
  Aleksy Schubert (MIM)
  Semantyka denotacyjna dla stopniowego typowania (Denotational semantics for gradual typing)
  

  ---

• 15 stycznia 2027 12:15
  Wojciech Paupa (MIM)
  Wprowadzenie do Leana (Introduction to Lean)
  

  ---

• 8 stycznia 2027 12:15
  Maja Kądziołka (MIM)
  Konstruktywna zawartość klasycznych dowodów (Constructive content of classical proofs)
  

  ---

• 18 grudnia 2026 12:15
  Aleksy Schubert (MIM)
  Hierarchia Minca dla kwantyfikatora egzystencjalnego (Minc hierarchy for the existential quantifier)
  

  ---

• 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))
  

  ---

• 30 października 2026 12:15
  Konrad Zdanowski (UKSW)
  O zupełnych algebrach Heytinga (On complete Heyting algebras)
  

  ---

• 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)
  

  ---