You are not logged in | log in

Wydział Matematyki, Informatyki i Mechaniki Uniwersytetu Warszawskiego

  • Skala szarości
  • Wysoki kontrast
  • Negatyw
  • Podkreślenie linków
  • Reset

Seminar Semantics, Logic, Verification and its Applications

Weekly research seminar


List of talks

  • 2022-11-25, 12:15, 5820

    Andrzej Tarlecki (MIMUW)

    Interpolation is (not always) easy to spoil

    Many results in foundations of software specification and development depend on interpolation properties of the underlying logical systems. Craig interpolation has been known to hold for first-order logic at least since the late 50ties, with well studied links to other crucial properties, li...

  • 2022-10-28, 12:15, 5820

    Daria Walukiewicz-Chrząszcz (MIMUW)

    Definitional Proof Irrelevance in Coq

  • 2022-06-03, 12:15, online, wysyłam link po zgłoszeniu emailem

    Aleksy Schubert (MIMUW)

    Algorithm for proving in intuitionistic propositional logic with limited number of atoms

    Na mocy twierdzenia Diego, które mówi o skończoności algebraicznego modelu wolnego dla minimalnej logiki zdaniowej, oraz jego uszczegółowień szacujących rozmiar tego modelu wiadomo, że istnieje wielomianowy algorytm rozstrzygający prawdziwość formuł minimalnej logiki z...

  • 2022-05-27, 12:15, on-line, link sent by email

    Konrad Zdanowski (UKSW)

    Undecidability of First-Order Modal and Intuitionistic Logics with Two Variables and One Monadic Predicate Letter

    Zostanie przedstawiona praca panów Rybakov i Shaktov, pt. Undecidability of First-Order Modal and Intuitionistic Logics with Two Variables and One Monadic Predicate Letter pokazująca nierozstrzygalność logik modalnych i intuicjonistycznych z dwoma zmiennymi i jednym unarnym symbolem re...

  • 2022-05-20, 12:15, on-line, link podaję emailem/I send link on request by email

    Aleksy Schubert (MIMUW)

    On word unification in Coq

    W trakcie referatu przedstawiony zostanie szkic dowodu poprawności podstawowych własności algorytmu znajdowania unifikatorów na słowach oraz zakres jego formalizacji w Coq-u. A sketch of algorithm correctness for an algorithm to solve word unification problem will be presented. This will...

  • 2022-05-13, 12:15, 5820

    Marcin Benke (MIMUW)

    Theorem Proving for All

    Jedną z istotnych zalet czystych języków funkcyjnych, takich jak Haskell jest możliwość równościowego wnioskowania o programach. Jednakże do tej pory takie wnioskowanie miało charakter zewnętrzny względem programu: już to (najczęściej) ręcznie „na papierze”...

  • 2022-03-25, 12:15, 5820

    Jacek Chrząszcz (MIMUW)

    News in Coq

    Na referacie przedstawione zostaną ostatnie dodatki do narzędzia do dowodzenia twierdzeń Coq. ...

  • 2022-03-25, 12:15, on-line

    Paweł Urzyczyn (MIMUW)

    Duality between Unprovability and Provability in Forward

    The speaker will talk about the paper Camillo Fiorentini, Mauro Ferrari: Duality between Unprovability and Provability in Forward Refutation-search for Intuitionistic Propositional Logic. ACM Trans. Comput. Log. 21(3): 22:1-22:47 (2020), where a system is defined to derive refutation...

  • 2022-03-11, 12:15, 5820

    Aleksy Schubert (MIMUW)

    Ethereum vulnerabilities

    Ethereum vulnerabilities   Ethereum is an open decentralised platform based upon peer-to-peer network principles. It enables the possibility to deploy decentralised applications that run on the platform and manage  the resources of financial kind available on the platform. I wil...

  • 2022-03-11, 12:15, 5820

    Aleksy Schubert

    Ethereum vulnerabilities

    Szanowni Państwo, jeszcze jeden dodatek, referat p.t. Ethereum vulnerabilities - jak wszystkie referaty tego seminarium do odwołania - będzie on-line pod linkiem meet.google.com/xiq-ruco-ayy Pozdrawiam, Aleksy Schubert ...

Pages