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

  • 2023-06-16, 12:15, 5820

    Maciej Zielenkiewicz (MIM)

    Small model property in games and automata

    Small model property is an important property that implies decidability. We show that the small model size is directly related to some important resources in games and automata for checking provability. ...

  • 2023-06-02, 12:15, 5820

    Aleksy Schubert (MIM)

    O nierozstrzygalności wyprowadzania typów przy ograniczonej randze lub arności

    W modelowaniu języków funkcyjnych z polimorfizmem ważną rolę odgrywa System F Girarda i Reynoldsa. Wiadomo, że dla termów w stylu Curry'ego, jeśli system nie jest w żaden sposób ograniczony, to wyprowadzanie typów jest nierozstrzygalne już dla typów ran...

  • 2023-05-26, 12:15, 5820

    Michał Gajda (MigaMake Pte Ltd, Singapore)

    Logika ultrafinitystyczna: Filozofia i konsekwencje

    Ultrafinityzm jest filozofią negującą możliwość wnioskowania o bardzo dużych liczbach. Ponieważ przedstawienie spójnej i wystarczająco mocnej logiki ultrafinitystycznej jest uważane za problem otwarty, to przedstawię reguły wnioskowania dla takiej, podważę założenia twierdzenia ...

  • 2023-04-28, 12:15, 5820

    Konrad Zdanowski (UKSW)

    Looping proofs

    Oto autorskie streszczenie referatu:   Opowiem o pracy A. Atseriasa i M. Laurii, w której autorzy analizują dowody w klasycznym rachunku zdań, w których grafy dowodu mogą być cykliczne, tzn. możemy, na przykład, użyć  dowodzonej formuły jako jednej z przesłanek w ...

  • 2023-04-21, 12:15, 5820

    Paweł Urzyczyn (MIMUW)

    Substructural logics

    Wiadomo, że logiki BCI i BCK są NP-zupełne. Ale jak się dobrze postawi pytanie o wnioskowanie w BCK (BCI), to odpowiedź jest całkiem inna i może być nawet akermańska. It is known that BCI and BCK logics are NP-complete. But if the question of deducibility in BCK (BCI) is properly...

  • 2023-04-14, 12:15, 5820

    Andrzej Tarlecki (MIM)

    On the fragility of interpolation

    We study a version of Craig interpolation formulated in the framework of the theory of institutions. This formulation proved crucial in the development of a number of key results concerning foundations of software specification and formal development. We investigate the fragility of interpolation pr...

  • 2023-03-31, 12:15, 5820

    Aleksy Schubert (MIMUW)

    Overview of network protocol implementations in functional programming languages

    Network protocols are usually described as dynamic processes. This does not make a perfect match with functional programming paradigm. Still, there are many initiatives to implement software artifacts in functional programming languages. This talk makes an overview of such efforts in scientific cont...

  • 2023-03-17, 12:15, 5820

    Jacek Chrząszcz (MIMUW)

    News in Coq

    The talk will tell us about new things that emerged in Coq and around Coq proof assistant with its new release. ...

  • 2023-01-20, 12:15, 5820

    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 the second-order lambda calculus with existential quantifi...

  • 2022-12-16, 12:15, 5820

    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 the 1982 handwritten note was demonstrated at the occasion of the 9...

Pages