Write a Blog >>
POPL 2021
Sun 17 - Fri 22 January 2021 Online
Sun 17 Jan 2021 19:15 - 19:30 at CPP - Formalized Mathematics Chair(s): Amin Timany

Kolmogorov complexity is an essential tool in the study of algorithmic information theory, and is used in the fields of Artificial Intelligence, cryptography, and coding theory. The formalisation of the theorems of Kolmogorov complexity is also key to proving results in the theory of Intelligent Agents, specifically the results in Universal Artificial Intelligence. In this paper, we present a mechanisation of some of these fundamental results. In particular, building on HOL4’s existing model of computability, we provide a formal definition of the complexity of a binary string, and then prove (i) that Kolmogorov complexity is uncomputable; (ii) the Kolmogorov Complexity invariance theorem; (iii) the Kraft and Kolmogorov-Kraft inequalities; and (iv) key Kolmogorov Complexity inequalities.

Sun 17 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

18:45 - 19:30
Formalized MathematicsCPP at CPP
Chair(s): Amin TimanyAarhus University

Streamed session: https://youtu.be/U_ZT9hfDAUQ?t=2768

18:45
15m
Talk
Formalizing the Ring of Witt VectorsDistinguished Paper Award
CPP
Johan CommelinUniversität Freiburg, Robert Y. LewisVrije Universiteit Amsterdam
Pre-print Media Attached
19:00
15m
Talk
Formal Verification of Semi-algebraic Sets and Real Analytic Functions
CPP
J Tanner SlagelNASA Langley Research Center, Lauren WhiteKansas State University, Aaron DutleNASA Langley Research Center
Pre-print Media Attached
19:15
15m
Talk
On the Formalisation of Kolmogorov Complexity
CPP
Elliot CattANU, Michael NorrishData61, CSIRO & ANU
Pre-print Media Attached