4th Logic Mentoring Workshop

Saturday 22 June 2019, Vancouver
### Overview

### Speakers

Bob Atkey (University of Strathclyde)
Kuen-Bang Hou (Favonia) (University of Minnesota)
Ohad Kammar (University of Edinburgh)
Étienne Miquey (INRIA, Gallinette)
Brigitte Pientka (McGill University)
Sylvain Schmitz (LSV, ENS Paris Saclay & CNRS)
Ana Sokolova (Universität Salzburg)
### Panellists

### Program

### Venue

The workshop will be held in the McLean Management Studies Lab (Room 2945) on the second floor of Harbour Centre, Simon Fraser University. Click here for a map.
### Travel Awards

### Useful resources

The following are some links on resources for research skills.
We hope that you will find them useful!
### Abstracts and slides

**Bob Atkey.** *Reviewing*. (slides)
**Kuen-Bang Hou (Favonia).** *Introduction to Cubical Type Theory*. (slides)
**Ohad Kammar.** *Where do ideas come from?*. (slides)
**Étienne Miquey.** *Sequent calculus and their computational content* (slides)
**Brigitte Pientka.** *How to give a talk* (slides)
**Sylvain Schmitz.** *Well-quasi-orders in Logic* (slides)
**Ana Sokolova.** *On Coalgebra, Loving What You Do, and Doing Beautiful Science*. (slides)
### Organizing committee

William J. Bowman (University of British Columbia)

Mike Dodds (Galois, Inc)

Sandra Kiefer (RWTH Aachen University)

Filip Mazowiecki (University of Bordeaux)

### LMW sponsors

Saturday 22 June 2019, Vancouver

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 '19 builds on the resounding success of the first editions held in 2016, 2017 and 2018. It will be co-located with the Symposium on Logic in Computer Science 2019, the premier international forum on theoretical and practical topics in computer science related to logic. LMW will take place on June 22 in Vancouver before the main conference.

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

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

- Kuen-Bang Hou (Favonia) (University of Minnesota)
- Ohad Kammar (University of Oxford)
- Ana Sokolova (Universität Salzburg)
- Brigitte Pientka (McGill University)

Time | Session | Chair |
---|---|---|

08:00 — 09:00 | — Coffee & Pastries — | |

09:00 — 09:30 | Ana Sokolova: On Coalgebra, Loving What You Do, and Doing Beautiful Science | Sandra Kiefer |

09:30 — 10:00 | Get-to-Know-Each Other and Find a Conference Buddy | |

10:00 — 10:30 | — Break — | |

10:30 — 11:00 | Favonia: Introduction to Cubical Type Theory | Filip Mazowiecki |

11:30 — 12:00 | Ohad Kammar: Where do ideas come from? | |

12:00 — 12:30 | Étienne Miquey: Sequent calculus and their computational content | |

12:30 — 14:00 | — Lunch Break — | |

14:00 — 14:30 | Sylvain Schmitz: Well-quasi-orders in Logic | William J. Bowman |

14:30 — 15:00 | Brigitte Pientka: How to give a talk | |

15:00 — 15:30 | Bob Atkey: Reviewing | |

15:30 — 16:00 | — Break — | |

16:00 — 17:00 | Panel with Favonia, Ohad Kammar, Brigitte Pientka, Ana Sokolova | Sandra Kiefer |

We do not accept applications for travel awards anymore.

**The deadline for applications was May 17th, 2019.**

- Teaching Teaching and Understanding Understanding.
- How to write, referee, give talks etc.
- Research skills.

I'll talk about how I go about writing, reading, and responding to reviews. Reviews are an essential part of academic publishing, but why do we do them (for free!), and why do we care what they say? I discuss how reviews are used by programme committees and chairs to decide what papers are selected for conferences (and journals), how I think you should go about doing reviews, and why you should write reviews. I'll also talk about reading reviews written about your own work, and how to go about the author response period effectively.

Homotopy type theory is a new area to explore type theory with inspiration from by homotopy theory, the study of topological spaces up to continuous deformation. Despite its success, the newly introduced features disturbed canonicity; that is, all closed proof terms should have been equal to some constructor form, but in general they are not. The quest to restore this property motivated the study of cubes and eventually led to the creation of cubical type theory. This talk will introduce cubical type theory and some of the current open problems.

We are in the ideas business: collecting, fleshing out, developing, and communicating them. I will discuss the life-cycle of (my) ideas, and give some pragmatic advice on managing and cultivating them.

Sequent calculus was originally introduced by Gentzen in order to reformulate the system of natural deduction in a more symmetric presentation. He was looking at the time for a proof of normalization for the natural deduction system in order to prove the coherence of first-order arithmetic. The principal novelty of this system is that it gives an equal importance to left and right parts (hypotheses and conclusions) of sequents. Through the lenses of the Curry-Howard correspondence, sequent calculi can be given a computational content which has the benefits of emphasizing implicit symmetries of computation such as the duality between programs and contexts or the duality between call-by-name and call-by-value evaluation strategies. Also, by presenting reductions systems that are close from the one of abstract machines, sequent calculi are particularly convenient when it comes to defining operational semantics, continuation-passing style translations or even realizability interpretations. During this talk, I will give an introduction to Curien and Herbelin's λµµ̃-calculus illustrating these different aspects.

No one sets out to give a bad talk, but unfortunately they still happen. I will present some subjective guiding principles on how to give a good talk and make the most out of the opportunity of being able to present one's work. In particular, I will draw on "How to talk Mathematics" by P.R. Halmos, an article that appeared in Notices of the AMS (1974) 21:3155-158 and share some of my own strategies.

This is meant as a short tutorial that illustrates through a few examples how well-quasi-orders can be exploited in proof theory, finite model theory, and verification.

In this talk I would like to emphasise the beauty of science, how I found my way around so far, and in particular what I loved and still love about coalgebra. The talk will have a technical part, but this will be incorporated in a personal story including (hopefully) some useful mentoring advice, and my opinion how we all choose topics, choose advisors and career paths, and what we could maybe improve / think of along the way.

Mike Dodds (Galois, Inc)

Sandra Kiefer (RWTH Aachen University)

Filip Mazowiecki (University of Bordeaux)

LMW sponsors have generously offered financial aid for students to travel to Vancouver and attend LICS and LMW.

The symposium is sponsored by ACM SIGLOG, the IEEE Technical Committee on Mathematical Foundations of Computing, the Association for Symbolic Logic, the European Association for Theoretical Computer Science, the Pacific Institute for the Mathematical Sciences, Simon Fraser University, and Google.

Website by Sam Staton based on a bootstrap design by Hartmut Eilers and Eric Koskinen.