CAST IT (video)

Felienne Hermans is full professor of Computer Science Education at the Vrije Universiteit Amsterdam.

Nutan Limaye is an associate professor at IT University of Copenhagen and an internationally leading researcher in computational complexity.

Nutan’s research focus is on the most prestigious and fundamental questions in computer science, namely: which problems can be solved with limited computational resources? Her recent breakthrough result, with Srinivasan and Tavenas, received the best paper award at the Foundations of Computer Science conference in 2021 and shows that algebraic circuits of constant size require superpolynomial depth.

We ask Nutan what these words even mean, and take a deep dive into the foundations of computer science. What are computational problems, computational models, algorithms, and how does one reason scientifically about such broad concepts? In particular, how does an impossibility result even make sense: how can one prove that a problem can never be solved, no matter how many clever ideas we (or anybody else) may have in the future?

For more information: [email protected]

Mikkel Thorup is professor of Computer Science at Copenhagen University and an internationally leading researcher in the theory of algorithms. During the Covid-19 pandemic, he has served on the scientific board advising the Danish authorities on the development of a national contact tracing app using mobile phones for exposure notification.

We sit down with Mikkel, exposure notification apps dutifully switched on, and talk about how such an application works. The Danish system, “SmitteStop”, uses Digital Privacy-Preserving Proximity Tracing. What does that even mean – how is the protocol defined, what is the mechanism by which privacy is preserved (and to which extent), and which role does the Google–Apple API play in the application?

Apart from the technical issues, we probe several issues on the fault line of technology and society. What are the alternatives to privacy-preserving exposure notification? E.g., could we do much more, and – to the extent that our phones already track everything and we share it freely – why aren’t we just using that information during a pandemic? What are the trade-offs between safety and liberty, is privacy a form of manslaughter, whom should we trust with our data, and how do different cultures around the globe manifest in deciding these tradeoffs?

Robin Hanson is an associate professor of economics at George Mason University and a research associate at the Future of Humanity Institute of Oxford University and one the world’s most influential futurists. 

Tim Roughgarden is professor in the Computer Science and Management Science and Engineering Departments at Stanford University. He is also a very active science communicator, hosting a popular algorithms course on the Coursera online learning platform. 

Claire Mathieu is a leading researcher in algorithms design and director of research at Centre national de la recherche scientifique (CNRS) in Paris, France.) Claire has been involved in the 2018 redesign of the college admission procedure in France, where close to a million students apply for more than ten thousand different college programmes. At the root of the procedure is the famous and widely used Stable Marriage method of Gale and Shapley (1962), a result that was recognised with the 2012 Nobel Prize in Economics.

Claire explains to us the basic algorithmic ideas, but also the many challenging details that must be addressed when an otherwise clean and well-understood procedure is implemented to tackle a real-world scenario. Many domain-specific peculiarities arise, such as social, cultural, political, administrative, and legal issues, which are themselves often ill-defined and frequently conflicting.

The episode was recorded on 20 August 2018, during the European Symposium of Algorithms 2018, hosted by Aalto University in Helsinki, Finland.

Yves Bertot is a senior researcher that the French Institute for Research in Computer Science and Automation (INRIA) in Sophia Antipolis and a leading researcher on correctness of software and the verification of mathematical proofs. Recently, his team was able to formally verify the correctness of the computation on the one millionth decimal digit of pi (which is 1, by the way), including a formally verifiable proof of the mathematics behind the formula and the correctness of the implementation of arithmetic operations used in the computation. We use this result as an inspiration to talk about interactive theorem proving and improving software quality.

Yves’ book with Pierre Casterán about interactive theorem proving using the Coq system is “Interactive Theorem Proving and Program Development – Coq'Art: The Calculus of Inductive Constructions”, Springer Verlag, EATCS Texts in Theoretical Computer Science, 2004, ISBN 3-540-20854-2.

Sarah Pink is a Professor of Design and Media Ethnography at RMIT University, Australia, and the author or co-editor of several books about digital ethnography.

Sarah’s book is Pink et al., Digital Ethnography: Principles and Practice, SAGE Publications, 2016.

Roman Beck is professor of Business Informatics at IT University of Copenhagen and the head of the European Blockchain Center. We talk to Roman about blockchain, a cryptographically secure, distributed database technology sometimes called a “trust machine.” Blockchain applications include the cryptocurrency Bitcoin, as well as various ideas for ensuring trust across institutional boundaries, such as contracts. It may also serve as the conceptual infrastructure of the next generation Internet. Which are the main ideas underlying this technology, how does it makes us think differently about digital information, and what are the possibilities, challenges, promises, and threats of this technology?