Homotopy Type Theory is an emerging field of mathematics that studies a fruitful relationship between homotopy theory and (dependent) type theory. This relation plays a crucial role in Voevodsky’s program of Univalent Foundations, a new approach to foundations of mathematics based on ideas from homotopy theory, such as the Univalence Principle. The UniMath library is a large repository of computer-checked mathematics, developed from the univalent viewpoint. It is based on the computer proof assistant Coq. In this school and workshop, we aim to introduce newcomers to the ideas of Univalent Foundations and mathematics therein, and to the formalization of mathematics in a computer proof assistant based on Univalent Foundations. Participants will receive an introduction to Univalent Foundations and to mathematics in those foundations, by leading experts in the field. In the accompanying problem sessions, they will formalize pieces of univalent mathematics in the UniMath library.

Can critical systems be built according to functionally precise specifications of of their constituent components (processor, operating system, crypto library, …) and development tools (compilers, synthesis tools)? This may seem a pipe dream, but the past decade has seen remarkable advances in the technology required to realize it. The DeepSpec Summer School will provide students with knowledge and experience necessary for understanding the state of the art and for contributing to ongoing research efforts, based on the interactive proof assistant Coq. DSSS'20 will consist of two parts, with the first week being devoted to introductory topics and the second week covering current research efforts.

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. Registration is free.

Software development process has been studied for long within the field of software engineering. However, in the last two decades two events can be identified which impacted dramatically on the unfolding of the discipline: the advent of Agile Methods and Cloud Computing. Before a software system was something to be analyzed, designed, programmed, tested, released and maintained. After, these phases so neatly defined started fading their borders. Academia and industry are currently facing the challenges opened by the Devops approach: tools, rapid development–deployment processes, effects on team performance, analytics, trustworthiness, microservices… The Summer School on Software Engineering and Continuous Development aims at discussing some of these issues, present the current solutions and trends and put together professionals, academics and students in an informal and productive atmosphere.

MOVEP is a five-day summer school on modelling and verification of infinite state systems. It aims to bring together researchers and students working in the fields of control and verification of concurrent and reactive systems. MOVEP 2020 will consist of ten invited tutorials. In addition, there will be special sessions that allow PhD students to present their on-going research (each talk will last around 20 minutes). Extended abstracts (2-3 pages) of these presentations will be published in informal proceedings.

Computational complexity theory was born more than 50 years ago when researchers started asking themselves what could be computed efficiently. Classifying problems/functions with respect to the amount of resources (e.g. time and/or space) needed to solve/compute them turned out to be an extremely difficult question. This has led researchers to develop a remarkable variety of approaches, employing different mathematical methods and theories. The future development of complexity theory will require a subtle understanding of the similarities, differences and limitations of the many current approaches. In fact, even though these study the same phenomenon, they are developed today within disjoint communities, with little or no communication between them (algorithms, logic, programming theory, algebra…). This dispersion is unfortunate since it hinders the development of hybrid methods and more generally the advancement of computational complexity as a whole. The goal (and peculiarity) of the Caleidoscope school is to reunite in a single event as many different takes on computational complexity as can reasonably be fit in one week. It is intended for graduate students as well as established researchers who wish to learn more about neighbouring areas.

On this Wednesday, June 10, 10:00 am - 3:00 pm PDT, we join in the movement to #ShutdownSTEM for a global #Strike4BlackLives. We call on anyone in the global programming languages community to come listen, work, and plan to actively reject racism from the systems we create and the systems within which we exist. We know that one day of action is not enough: our goal is to both achieve small immediate change, and to facilitate the planning of broader systemic change across the world of programming languages research.

We will be holding a virtual day of conversation and focused group action. We encourage you to attend for all or most of the day, but we will be happy to welcome you if you can only be there some of the time.

The Online Worldwide Seminar on Logic and Semantics is an online-only series of research talks, highlighting the most exciting recent work in the international computer science logic community. In this time of restricted international travel, a key aim of this series is to provide a forum for informal discussion and social interaction that is so important for the progress of science. To facilitate this, the seminar incorporates in virtual form a number of features more normally associated with physical meetings, including virtual “coffee breaks” before and after the seminar, allowing participants to chat in small groups. (Don’t forget to bring your own coffee.)

Starting this Wednesday, we are excited to announce the first of our OWLS Young Researcher talks, given by a researcher within 7 years of completing their PhD. A new initiative, these OWLS-YR talks will take place fortnightly, interleaved with regular OWLS talks. Our goal is to give a platform to the excellent work being done by junior members of the community. All members of the community are encouraged to attend these talks.

The students of the Berkeley programming systems group have organized an online summer seminar series. We will be hosting students from different institutions working on various exciting topics in programming languages, software engineering, formal methods, etc. All are invited to attend!

The Chalmers Online Functional Programming Seminar Series is organized by the Chalmers Functional Programming Group, as a way to exploit the fact that so many of us in the FP community are already meeting and working online these days. Our aim is to bring the people in the FP community closer together, to educate and inspire, and to foster collaboration.

The seminars will take place every Monday (at 7am PDT / 10am EDT / 16:00 CET) and are organized through Zoom.