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

20 stycznia 2023 12:15
Aleksy Schubert (MIM)
Provability of existential quantification in intuitionistic logics
The type inhabitation problem, in other terminology formula provability problem, in the second-order lambda calculus with existential quantifier and arrow will be proved during the talk to be undecidable, which contrasts with the result that …
16 grudnia 2022 12:15
Paweł Urzyczyn (MIMUW)
Excavation works in my office
I will present a result of excavation works in my office, namely a forgotten theorem of Plotkin: adding fixpoint combinator to simply typed lambda-calculus does not enlarge the class of definable functions. The contents of …
25 listopada 2022 12:15
Andrzej Tarlecki (MIMUW)
Interpolation is (not always) easy to spoi)
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 …
28 października 2022 12:15
Daria Walukiewicz-Chrząszcz (MIMUW)
Definitional Proof Irrelevance in Coq
3 czerwca 2022 12:15
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 zdaniowej przy założeniu, …
27 maja 2022 12:15
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 …
20 maja 2022 12:15
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 …
13 maja 2022 12:15
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”, już to …
25 marca 2022 12:15
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 …
25 marca 2022 12:15
Jacek Chrząszcz (MIMUW)
News in Coq
Na referacie przedstawione zostaną ostatnie dodatki do narzędzia do dowodzenia twierdzeń Coq.
11 marca 2022 12:15
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
11 marca 2022 12:15
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 …
28 stycznia 2022 12:15
Konrad Zdanowski (Cardinal Stefan Wyszynski University)
Intuitionistic SAT solver
I will present an article by F. Besson, Itauto: An Extensible Intuitionistic SAT Solver, which was presented at the conference Interactive Theorem Proving, ITP 2021 (url: https://drops.dagstuhl.de/opus/frontdoor.php?source_opus=13904 ). The author presents an implementation of an …
21 stycznia 2022 12:15
Aleksy Schubert (MIMUW)
Prenex fragment of first-order intuitionistic logic and word unification
I will recall an old result by Gurevich and Voronkov connecting the monadic case in the prenex intuitionistic predicate logic with equality with word unification.
3 grudnia 2021 12:15
Marcin Benke (MIMUW)
(E)TiML: A Functional Language for Practical Complexity Analysis)
TiML is a variant of ML whose types contain resource bounds, designed by Peng Wang as his PhD thesis on MIT. When a TiML program passes the typechecking, upper bounds on its resource usage can …