The Logic Mentoring Workshop (LMW) will introduce young researchers to the technical and practical aspects of a career in logic research. It is targeted at students, from senior undergraduates to graduates, and will include talks and panel sessions from leaders in the subject.
LMW '18 builds on the resounding success of the first two editions held in 2016 and 2017. It will be co-located with the Symposium on Logic in Computer Science 2018, the premier international forum on theoretical and practical topics in computer science related to logic, within the frame of the Federated Logic Conference 2018. LMW will take place on July 8 in Oxford before the main conference and other workshops.
As part of LMW, there will be a question and answer session comprising of the following panellists:
|09:00 — 09:30||Brigitte Pientka: How to get the most out of a conference like FLOC?||Sandra Kiefer|
|09:30 — 10:00||Gabriel Scherer: Asking Questions to Yourself and Others|
|10:00 — 10:30||Get-to-Know-Each Other and Find a Conference Buddy|
|10:30 — 11:00||— Break —|
|11:30 — 12:00||Luke Ong: Higher-order Constrained Horn Clauses and Automatic Program Verification||Ugo Dal Lago|
|12:00 — 12:30||Marco Gaboardi: Research as a Collaborative Effort|
|12:30 — 14:00||— Lunch Break —|
|14:00 — 14:30||Gilles Barthe: Relational Verification of Probabilistic Programs||Jan Hoffmann|
|14:30 — 15:00||Neelakantan R. Krishnaswami: Can Logic Make Us Better People?|
|15:00 — 15:30||Maribel Fernandez: Rewriting Systems and Applications|
|15:30 — 16:00||— Break —|
|16:00 — 17:00||Panel with Nick Benton, Marco Gaboardi, Cynthia Kop, Alexandra Silva||Brigitte Pientka|
We are no longer accepting applications for scholarships.
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.Maribel Fernandez. Rewriting Systems and Applications. (slides)
In this talk I will briefly present my research area, focusing on recent results on nominal rewriting and including some mentoring aspects.Marco Gaboardi. Research as a Collaborative Effort. (slides)
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.Neelakantan R. Krishnaswami. Can Logic Make Us Better People? (slides)
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).Luke Ong. Higher-order Constrained Horn Clauses and Automatic Program Verification. (slides)
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.Brigitte Pientka. How to get the most out of a conference like FLoC? (slides)
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.Gabriel Scherer. Asking Questions to Yourself and Others. (slides)
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.