Student Talks 2020 (abstracts)
Preclosure Hyperdoctrines, Completeness of (Higher Order) Spatial Logic for Closure Spaces
University of Udine, Italy
We introduce the categorical notion of preclosure hyperdoctrines as an abstract theoretical framework for investigating the logical aspects of preclosure spaces, a generalization of topological spaces covering also the notion of neighbourhood in discrete structures. Using this theory, we provide the first axiomatisation and sound and complete semantics for Spatial Logic for Closure Spaces, a modal logic for the specification and verification on spatial properties over preclosure spaces. Moreover, exploiting general results from categorical logic we introduce a new, higher order, version of SLCS, with a sound and complete semantics. Thus, the theory of preclosure hyperdoctrines is useful in the analysis and definition of new spatial logics for various applications.
Probabilistic protocol complex: Topology for randomized distributed algorithms
Universite de Paris - Paris Diderot - IRIF, France
A variety of problems in distributed algorithms can be understood and studied with topological tools. In particular, combinatorial topology allows to prove impossibility results for consensus and k-set agreement (these results come from Herlihy and Shavit's works). However, these problems become solvable when randomization is added to the system.
I present a result of my PhD thesis, stating that topological methods can be applied to probabilistic settings in order to infer probabilistic lower bounds for any algorithms.
An Efficient Coding Technique to Reduce Communication for Distributed Deep Learning
Rishikesh Reddy Gajjala
Indian Institute of Technology Delhi, India
As the scale and size of the deep neural network (DNN) models are increasing, distributed stochastic algorithms over multiple computing nodes, equipped with gradient compression techniques such as quantization, are becoming popular in efficiently training these models. However, communicating the quantized gradients among the computing nodes in a distributed set-up remains a challenging task because of their humongous dimensionality. As a result, the gain one can expect due to compression can be suppressed due to greater communication costs. In this paper, we propose a lossless encoding strategy based on the classic Huffman encoding and run-length encoding. More precisely, we use the existing codebook quantization techniques, such as quantized SGD (QSGD), ternary gradient (TernGrad), natural compression, ZIPML, and LPC-SVRG and propose efficient encoding strategies for communicating quantized gradients resulting from these techniques.
To reduce the encoding time for run-length Huffman codes, we propose a sampling technique that can find efficient lossless encoding for large dimensional vectors. Using this technique we relax the compression to (1+ε) times the optimal compression but reduce the decoding time significantly. Finally, we show the effectiveness of our proposed encoding strategies across several DNN models on different data-set. In a practical setting, we were able to achieve 5 times better compression than the 16-bit run-length encoding taking just 5% extra time in comparison to 16-bit run-length coding.
Cartesian restriction categories and their string diagrams
Tallinn University of Technology
Dept. of Software Science, Estonia
Restriction categories are categories in which maps can be partial, in the sense that they are defined on only part of their domain. For example, the category of partial recursive functions is a cartesian restriction category. In this talk, I will explain how the widely used string diagrams for monoidal categories can be used to reason about cartesian restriction categories, and discuss potential applications.
A Formal Proof of the Group Law for Edwards Curves
The verification of the group properties of an elliptic curve is a classical exercise in theorem proving. Typically, the challenges lie in the necessary trade-off between the complexity of the mathematical formalism used and the difficulty of implementing it in a proof assistant.
In this talk, an elementary computational proof of the group law for Edwards elliptic curves is explained. The associative law is expressed as a polynomial identity over the integers that is directly checked by polynomial division. Unlike other proofs, no preliminaries such as intersection numbers, Bézout’s theorem, projective geometry, divisors, or Riemann Roch are required. The proof of the group law has been formalized in the Isabelle/HOL proof assistant.
The talk will elaborate on the main insights of the mechanized proof, the proving tools used and will suggest further directions in the formalization of elliptic curves, as well as possible improvements in the Isabelle’s automatic proof methods.
The work was done in collaboration with Prof. Thomas C. Hales and will be submitted to IJCAR2020.
Are SIS hash functions collapsing?
University of Tartu
Inst. of Computer Science, Estonia
Hash functions are a core primitive in cryptography. In classical cryptography one of the most important properties of a hash function is collision resistance, which states that it is hard to find two values which hash to the same image. This notion captures a sort of computational injectivity, which seemingly disappears in the post-quantum setting. For example in commitment schemes, a standard construction using a collision resistant function is actually completely insecure.
In response, a new strengthening of collision resistance called the collapsing property was introduced. This is a fairly natural notion in the post-quantum setting and often works as a direct replacement for collision resistant hash functions. While several currently used hash functions have already been shown to be collapsing, some have yet to be proven to be so.
In our work, we prove that the hash function family keyed by a uniformly random matrix is collapsing. This hash function is often used in lattice cryptography, including some of the signature schemes proposed in the NIST pqc competition. We do this by creating a family of collapsing hash functions and show that they are indistinguishable from the set of matrices of appropriate dimension.
This is a work in progress: the overall proof structure and steps are set, but we currently don't have the concrete security bounds, and additional details of the proof are not yet solidified.
Perfect matching is hard for tree-like Res(xor)
St. Petersburg Dept. of Steklov Math. Inst.,
Russian Academy of Sciences, Russian Federation
Res(xor) is an extension of the Resolution proof system that operates with linear equations modulo 2 instead of literals. There are no known hard examples for that system and proving one is a step forward towards a lower bound for ACC0-Frege.
Tree-like Res(xor) is a much weaker system and there are many known hard examples for it such as pigeonhole principle (PHPnm), ordering principle, two-fold Tseitin formulas and a few others. On of the methods to establish lower bounds for this system is by showing a lower bound on polynomial calculus degree of the same formula.
Interestingly, perfect matching formula (PMnn+1) encoding the statement that a bipartite graph with n vertices in the first part and n+1 vertices in the other has a perfect matching has a polynomial-size tree-like Res(xor) proof.
We show that PMnn+2 (in contrast with PMnn+1) has only exponential-size proofs in tree-like Res(xor), which is noteworthy because PMnn+2 (in an appropriate encoding) has a small-degree Nullstellensatz refutation and thus the polynomial calculus degree method does not work for this formula.
This talk is based on joint work with Dmitry Itsykson.
A new proof technique in elementary number theory based on context-free grammar
Jose Manuel Rodriguez Caballero
University of Tartu
Inst. of Computer Science, Estonia
We present a recent technique developed by the speaker, which was successfully applied in order to prove theorems in elementary number theory by transforming the non-trivial arithmetical statements into easier problems about context-free grammars. We present a library in Isabelle/HOL in order to formalize this technique (work-in-progress). We show some connections with the Hodge structure of the Hilbert scheme of n points in the 2-dimensional algebraic torus.
 Jose Manuel Rodriguez Caballero, "Jordan's Expansion of the Reciprocal of Theta Functions and 2-densely Divisible Numbers", INTEGERS, 2020.
 Jose Manuel Rodriguez Caballero, "Integers Which Cannot Be Partitioned Into an Even Number of Consecutive Parts", INTEGERS, 2019.
 Jose Manuel Rodriguez Caballero, "On a function introduced by Erdös and Nicolas", Journal of Number Theory, 2019.
 Jose Manuel Rodriguez Caballero, "Symmetric Dyck Paths and Hooley’s Delta-function", Combinatorics on Words. Springer, 2017.
 Jose Manuel Rodriguez Caballero, Library in GitHub "Dyck Paths" (work-in-progress)
Bounded-Depth Frege Complexity of Tseitin Formulas for All Graphs
St. Petersburg State University
Fac. of Math. and Mechanics, Russian Federation
We show that, if a Tseitin formula for a graph G has size s, then for all large enough d, it has a depth-d Frege proof of size 2(tw(G)O(1/d)) poly(s), where tw(G) is a treewidth of a graph G. This upper bound matches the lower bound up to a constant in the top exponent. The upper bound gives us polynomial-size Frege proofs for depth log(tw(G)). Along with the lower bound it induces strict depth-hierarchy for the proof complexities of Tseitin formulas over an infinite sequence of graphs. To prove this, we use compact representations of linear functions over boolean variables by propositional formulas of depth d. We also use the notion of tree partition width, which is a structural graph parameter similar to treewidth.
The talk is based on a joint work with Nicola Galesi, Dmitry Itsykson and Artur Riazanov (which includes both upper bound and lower bound). This paper was presented at MFCS 2019.
Pointless Topology in Univalent Foundations
Chalmers University of Technology, Sweden
Topology is the discipline of mathematics concerned with the study of continuous functions: a notion that pervades practically all of mathematics. Implementing topology in type theory, however, is not a straightforward task as topology is usually developed in a setting that is classical and impredicative. There have been many works addressing this question such as those by Sambin, Coquand, and others [0, 1, 2]. The question I consider in my thesis is: how can one can continue this line of work in the age of Univalent Foundations? In my talk, I will present an approach to formal topology I have been working on, that is based on indexed containers  and makes use of higher inductive types. The development to be presented is completely constructive and predicative thanks to the use of Cubical Agda that provides computational content for the Univalence Axiom. Furthermore, I will present (time permitting) various applications of this topological machinery such as implementing domains as certain kinds of topologies. The talk will be intended for a general CS audience and I will not assume any background in topology.
 Sambin, G. 1987. Intuitionistic Formal Spaces - A First Communication. Mathematical Logic and Its Applications. D.G. Skordev, ed. Springer. 187-204.
 Coquand, T. et al. 2003. Inductively generated formal topologies. Annals of Pure and Applied Logic. 124, 1–3 (2003), 71-106. doi: https://doi.org/10.101/s0168-0072(03)00052-6
 Coquand, T. 2003. Formal Topology with Posets. (Jun. 2003).
 Petersson, K. and Synek, D. 1989. A set constructor for inductive sets in Martin-Löf’s type theory. Category Theory and Computer Science (Berlin, Heidelberg, 1989), 128-140.
November 26, 2014 19:55 Europe/Helsinki (GMT +02:00)
local organizers, ewscs20(at)cs.ioc.ee
EWSCS'20 page: //cs.ioc.ee/ewscs/2020/