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

March 25, 2022, 12:15 p.m.
Jacek Chrząszcz (MIMUW)
News in Coq
Na referacie przedstawione zostaną ostatnie dodatki do narzędzia do dowodzenia twierdzeń Coq.
March 11, 2022, 12:15 p.m.
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 …
March 11, 2022, 12:15 p.m.
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
Jan. 28, 2022, 12:15 p.m.
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 …
Jan. 21, 2022, 12:15 p.m.
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.
Dec. 3, 2021, 12:15 p.m.
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 …
Nov. 26, 2021, 12:15 p.m.
Aleksy Schubert (MIMUW)
Verification of Ethereum programs
The general overview of blockchain and smart contract technologies is given. Based upon that a state-of-the art verification technique VerX is discussed. You can join the meeting under the Zoom link: https://us02web.zoom.us/j/83143002443?pwd=dnlSQ05pVjB3L3cwSUkzOEVOTnJVUT09
Nov. 19, 2021, 12:15 p.m.
Maciej Zielenkiewicz (MIMUW)
Small model property reflects in games and automata
Let's choose a logic theory having the small model property. I will show that the size of the small model used in the definition of the property can be directly used to show a limit …
Nov. 5, 2021, 12:15 p.m.
Jacek Chrząszcz (MIMUW)
Cameleer: a Deductive Verification Tool for OCaml
Despite all the advances in deductive verification and proof automation over the past few decades, little attention has been given to the family of functional languages. We present Cameleer, a tool for the deductive verification …
Oct. 29, 2021, 12:15 p.m.
Aleksy Schubert (MIMUW)
NP-completeness of BCI - another view
Another proof of NP-hardness of provability in BCI is presented. As a more natural source of the reduction, the one-in-three 3SAT problem is assumed.
Oct. 22, 2021, 12:15 p.m.
Paweł Urzyczyn (MIMUW)
NP-completeness of BCI
We will see a proof of NP-completness of propositional implicational logic BCI, in which each assumption is used exactly once.
Oct. 8, 2021, 12:15 p.m.
Aleksy Schubert (MIMUW)
Nierozstrzygalność semiunifikacji na chuseczce do nosa
Problem semiunifikacji pojawia się naturalnie w zagadnieniach związanych z typowalnością programów funkcyjnych, w których systemy typów opartych na systemie F. Intuicyjnie chodzi tutaj o typowanie, w którym funkcji w programie staramy się przypisać jak najbardziej …
Sept. 9, 2013, 10:15 a.m.
Kokichi Futatsugi (JAIST-RCSV)
Generate and check method for invariant verification in CafeOBJ
Effective coordination of inference (a la theorem proving) and search (a la model checking) is one of the most important and interesting research topics in formal methods. We have developed several kinds of techniques for …
Dec. 3, 2012, 10:15 a.m.
Bartosz Zieliński (Uniwersytet Łódzki)
Maude jako preprocesor SQL
p, li { white-space: pre-wrap; } Opowiem o pomyśle wykorzystania systemów przepisywania termów jako lepszych makroprocesorów, w szczególności opiszę tworzony obecnie system (na wczesnym etapie rozwoju) reprezentowania zapytań SQL jako termów Maude i jego zastosowanie …
Nov. 5, 2012, 10:15 a.m.
Michał R. Przybyłek (Uniwersytet Warszawski)
Associated Categories
Pokażę, że z obiektami dowolnej skończenie zupełnej 2-kateorii z notacją dyskretności, można związać kategorie, tak aby 1-morfizmy odpowiadały funktorom pomiędzy dowiązanymi kategoriami, 2-morfizmy naturalnym transformacjom, a dyskretne obiekty dyskretnym (w klasycznym sensie) kategoriom. Pozwoli to …