Formalizing Gödel’s System T in Lean

Title: Formalizing Gödel’s System T in Lean

Speaker: Horațiu Cheval (University of Bucharest)

Abstract:

In 1958, Gödel introduced his functional interpretation as a method of reducing the consistency of first-order arithmetic to that of a quantifier-free system of primitive recursive functionals of higher type. His work has since enabled other advances in proof theory, notably the program of proof mining. We give a brief overview of Gödel’s System T and then explore a formalization thereof as a deep embedding in the Lean proof assistant.

References:

[1] mathlib Community, The Lean Mathematical Library, 2019.
Posted on

Hack The Box University 2020 – Qualifier Round

The students of the Faculty of Mathematics and Computer Science Dragoș Albastroiu (3rd-year, CTI) – captain, Robert Dobre (3rd-year, Computer Science), Mihail Feraru (2nd-year, Computer Science) and Andrei Ciobanu (2nd-year master, Security and Applied Logic) represented the University of Bucharest at the Hack The Box University 2020 Qualifier Round, which took place in November, 19th-22nd, online. In the competition participated teams from universities all around the world, and the team of the University of Bucharest ranked among the best, becoming eligible to remain in the competition.

Posted on

Universitatea din Bucuresti – Hack the Box

Universitatea din Bucuresti este acum prezenta pe Hack the Box!

Daca aveti cont pe Hack the Box si vreti sa primiti o invitatie pentru a face parte din echipa de studenti a universitatii, trimiteti user-ul, numele complet, grupa si un e-mail de contact (catre Ruxandra Olimid).

POSTPONED: Protocols in Dynamic Epistemic Logic

POSTPONED UNTIL FURTHER NOTICE.
Speaker: Alexandru Dragomir (University of Bucharest)

Title: Protocols in Dynamic Epistemic Logic
Abstract: Dynamic epistemic logics are useful in reasoning about knowledge and certain acts of learning (epistemic actions). However, not all epistemic actions are allowed to be executed in an initial epistemic model, and this is where the concept of a protocol comes in: a protocol stipulates what epistemic actions are allowed to be performed in a model. The aim of my presentation is to introduce the audience to the account of protocols in [1, 2].

References:
[1] H. van Ditmarsch, S. Ghosh, R. Verbrugge, Y. Wang, Hidden protocols: Modifying our expectations in an evolving world, Artificial Intelligence 208 (2014), 18-40.
[2] Y. Wang, Epistemic Modelling and Protocol Dynamics, PhD thesis, University of Amsterdam, 2010.

A quantitative analysis of the “Lion-Man” game

Speaker: Ulrich Kohlenbach (Technische Universität Darmstadt)

Title: A quantitative analysis of the “Lion-Man” game
Abstract: We analyze, based on an interplay between ideas and techniques from logic and geometric analysis, a pursuit-evasion game. More precisely, we focus on a discrete lion and man game with an ε-capture criterion. We prove that in uniformly convex bounded domains the lion always wins and, using ideas stemming from proof mining, we extract a uniform rate of convergence for the successive distances between the lion and the man. As a byproduct of our analysis, we study the relation among different convexity properties in the setting of geodesic spaces.
Joint work with Genaro López-Acedo and Adriana Nicolae.

References:
[1] U. Kohlenbach, G. López-Acedo, A. Nicolae, A quantitative analysis of the “Lion-Man” game. arXiv:1806.04496 [math.MG], 2019. Submitted.
Posted on

Câștigători Burse și Premii Bitdefender

– Burse de merit anul II: Costea Marina si Nicolae Cristian (2500 RON fiecare)
– Burse de merit anul I: Marian Gusatu si Bogdan Macovei (2.500 RON fiecare)
– Premii de cercetare pentru sem I (500 RON fiecare): Marian Gusatu, Bogdan Macovei, Horatiu Cheval, Parvu Daniel
– Bursa de cercetare pentru sem II: Horatiu Cheval (1000 RON pe luna martie-iulie)

POSTPONED: Securing Businesses and Critical Infrastructure

POSTPONED UNTIL FURTHER NOTICE.

 

Speaker: Ioan Constantin (Orange Romania)

Abstract: A brief walkthrough some of the challenges in offering advanced cyber security solutions for Business and Critical Infrastructures, from a Managed Security Services Provider’s standpoint. We’ll talk threat detection and mitigation, the specifics of OT Security in Critical Infrastructure, compliance and best practices. We’ll also glance at some of the research and development in these areas.

Proudly powered by WordPress