How to get the most out of a conference like FLOC?
ABSTRACT. An important aspect of research is to attend conferences: it allows you to learn and stay up to date on recent progress, meet like-minded colleagues, build a research and collaboration network, promote your own research, catch up with old friends and make new ones. Yet, attending a conference like FLOC can also be intimidating and overwhelming. In this talk, I will discuss some concrete strategies and share some advice.
ABSTRACT. A good way to interact with research material (research articles and research talks) is to ask questions -- to yourself first, and then to others. Formulating questions can help you understand the work, is essential in reviewing an article, and will miraculously prevent you from falling asleep (or into your mailbox) during a talk. What is a good question? What is not a good question? What's a good time and a good way to deliver the question? This will be covered in this talk which will also include, of course, a large part of answers to your questions.
ABSTRACT. In the medieval European university, logic was counted as one of the three foundational subjects of the liberal arts, which were reckoned to be the essential knowledge for living life as a free human being. The Naiyyayikas of ancient India held logic in even higher regard, regarding it as one of the fundamental instruments for achieving enlightenment.
In the modern day, logic does not hold such an exalted position in our collective imagination. It is regarded as a dry and technical subject, whose details are of interest only to scientific specialists. Still, logic has achieved an extraordinary level of sophistication, and is an essential tool that informs much research in computer science.
Given the overwhelming impact of the computer upon society, it is worth considering again the questions of how - and whether - logic can help us live ethical lives. In this talk, I will explores the kinds of ethical questions one can expect to find in modern logic and computer science research, and reflect upon the different answers that modern logicians have made over the decades (both to our credit and discredit).
ABSTRACT. As society becomes more and more connected, so does research. Research in logic and computer science is changing, becoming more collaborative and open. This often contrasts with the needs that young researchers have of building their own research. In this talk, starting from my personal experience, I will provide some advices on how to survive in collaborative research.
ABSTRACT. 2-safety properties go beyond the traditional formulation of program verification by considering pairs of traces (instead of traces). In the probabilistic setting, verification of 2-safety properties is conveniently achieved using probabilistic relational program logics such as pRHL. The talk will highlight a fruitful connection between pRHL and probabilistic couplings, a well-known tool from analyzing Markov chains, and discuss applications to cryptography and differential privacy.
Constrained Horn clauses as a basis of automatic program verification: the higher-order case
ABSTRACT. We introduce constrained Horn clauses in higher-order logic, and study satisfiability and related decision problems motivated by the automatic verification of higher-order programs. Although satisfiable systems of higher-order clauses in the standard semantics do not generally have least models, by viewing these systems as a kind of monotone logic programs, we show that there are non-standard semantics that do satisfy the least model property. Moreover the respective satisfiability problems in the standard and non-standard semantics are inter-reducible. With a view to exploiting the remarkable efficiency of SMT solvers, we survey recent developments in the algorithmic solution of higher-order Horn systems by reduction to first order, and discuss related problems.