3rd Logic Mentoring Workshop
Sunday 8 July 2018, Oxford

Speakers

• Gilles Barthe (IMDEA Software Institut)
• Maribel Fernandez (King's College London)
• Marco Gaboardi (University at Buffalo)
• Neelakantan R. Krishnaswami (University of Cambridge)
• Luke Ong (University of Oxford)
• Brigitte Pientka (McGill University)
• Gabriel Scherer (INRIA)

The talks will be a mixture of mentoring and research talks.

Panellists

As part of LMW, there will be a question and answer session comprising of the following panellists:

• Nick Benton (Facebook)
• Marco Gaboardi (University at Buffalo)
• Cynthia Kop (Radboud University Nijmegen)
• Alexandra Silva (University College London)

Program

Time	Session	Chair
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

Venue

The workshop will be held in the Maths Board room on the top floor of the Mathematical Institute in Oxford. For further information, please click here.

Scholarships

We are no longer accepting applications for scholarships.

Useful resources

The following are some links on resources for research skills that were mentioned during the workshop. We hope that you will find them useful! Also, you can find slides from the various talks in the next section below.

• Teaching Teaching and Understanding Understanding.
• How to write, referee, give talks etc..
• Research skills (click button).

Please let us know if there is anything else you would like us to upload here!

Abstracts and slides

Gilles Barthe. Relational Verification of Probabilistic Programs. (slides)

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.

Organizing committee

Ugo Dal Lago (University of Bologna)
Jan Hoffmann (Carnegie Mellon University)
Sandra Kiefer (RWTH Aachen University)
Brigitte Pientka (McGill University)

LMW sponsors

LICS Sponsorship

The symposium is sponsored by ACM SIGLOG and the IEEE Technical Committee on Mathematical Foundations of Computing.