The Scientific Program of the 4th HLF was back in full swing on Thursday with a strong line-up of laureate lectures. Raj Reddy and Richard Stearns, who are both ACM A.M. Turing Award recipients, took the first round of lectures. The second duo was handled by Fields Medalist Vladimir Voevodsky and yet another ACM A.M. Turing Award winner Leslie Lamport. Lecture videos and the complete abstracts are both available online. PhD students were also able to present their work in the Poster Session, which attracted quite the crowd.
“Too Much Information and Too Little Time”
This talk is about having to cope with too much information within human time limitations given that we are not changing at exponential rates like semiconductors. Humans make errors, tend to forget, are impatient and look for least effort solutions. Such limitations, sometimes, lead to catastrophic results. At the same time, humans learn with experience, tolerate error and ambiguity, use vast amounts of knowledge, and communicate using speech and language. Such features are still lacking in most of our systems. Most systems don’t get better with experience. Future opportunities lie in creating tools for coping with 21st century world of “too much information and too little time”. In this talk we will present two families of intelligent agents, viz., “cognition amplifiers” and “guardian angels” to help with problem of scarcity of attention. A Cognition Amplifier is a personal autonomic intelligent agent that anticipates what you want to do and helps you to do it with less effort. A Guardian Angel is a personal autonomic intelligent agent that discovers and warns you about unanticipated, possibly catastrophic, events that could impact your safety, security, and wellbeing. Both Cogs and Gats are enduring, autonomic, nonintrusive intelligent agents which are always-on, always working, and always-learning. Future breakthroughs will emerge from those understand human limitations and can cater to such human needs.
Richard Edwin Stearns
“Strategies for Extensive Form Games”
We want to describe sets of mixed strategies using linear equations such that
1. The number of variables is small compared to the game size.
2. Every mixed strategy has an equivalent strategy in the set.
3. Implementing the strategies is easy.
It is known how to do this for players with perfect recall using equations for behavior strategies or equations for path probabilities. We generalize the perfect recall techniques to cover players without perfect recall. Although the number of variables needed is not always small, it will be small if the recall is close enough to perfect.
UniMath is a library of formalized mathematics that is based on the Univalent Foundations and written in what we call the UniMath language which is a small subset of the language of the Coq proof assistant. I wrote the core of the library under the name Foundations in 2010-11 to try out whether the Univalent Foundations can be used with Coq to formalize some real mathematics. After discovering that it can we, Benedikt Ahrens, Dan Grayson and myself, formed a GitHub organization called UniMath. Today UniMath has 12 authors, about 7 of them, including all three of the founders, are active in expanding and improving the library.
“The PlusCal Algorithm Language”
An algorithm is not a program, so why describe it with a programming language? PlusCal is a tiny toy-like language that is infinitely more expressive than any programming language because an expression can be any mathematical formula.
Participants of the 4th HLF enjoyed an entertaining evening at the Technik Museum Speyer (Speyer Museum of Technology). After a guided-tour of the medieval city, highlighted by the Speyer Cathedral, they were greeted at the museum by the SAP BIG BAND. Speyer’s Lord Mayor Hansjörg Eger welcomed everyone to the museum and the city of Speyer. The keynote address was given by Volker Springel, head of the Theoretical Astrophysics (TAP) at Heidelberg Institute for Theoretical Studies (HITS), and Nobel Laureate in Physics, Brian Schmidt, who also gave this year’s ‘Lindau Lecture’. Since the evening was sponsored by SAP, their Chief Financial Officer, Luka Mucic did the honors of opening the buffet. The participants were also encouraged to enjoy the ‘Night in the Museum’ and were free to wander through the exhibits.
Photos from the 4th Heidelberg Laureate Forum are available on the flickr account.