"Education and Research Hub for Mathematics-for-Industry" (Program Leader：Masato WAKAYAMA)

Program：

13:00- Reynald Affeldt (AIST)

**Instrumenting Error-correcting Codes with SSReflect**

summary:

Our motivation is to provide in the Coq proof-assistant formal

definitions and lemmas about error-correcting codes. The resulting

toolkit could enable, for example, formal verification of

implementations of cryptographic schemes based on error-correcting

codes. For that purpose, we use the SSReflect library, that provides

an integrated formalization of matrices and polynomials. As a

technical introduction to formal verification in the Coq

proof-assistant, we report on the formalization of basic

properties of error-correcting codes and probabilities.

14:00- Akihiro MUNEMASA (Tohoku University)

**Super Catalan numbers and Krawtchouk polynomials**

summary:

In 1992, Ira Gessel defined super Catalan number \(S(m,n)\) as

\[

S(m,n) = \frac{(2m)!(2n)!}{m!n!(m+n)!},

\]

where \(m,n\) are positive integers, and showed

that \(S(m,n)\) is an integer.

In this talk, we point out an interpretation of

\(S(m,n)\) as a special value of a

Krawtchouk polynomial \(K_j^d(x)\).

Krawtchouk polynomials appear as the coefficients of the so-called

MacWilliams identities, and

also as the eigenvalues of the distance-\(j\) graph of the \(d\)-dimensional

cube. Our interpretation shows that

\(\{(-1)^mS(m,n)\mid m,n\geq0,\;m+n=j\}\) coincides with

the set of non-zero eigenvalues of the distance-\(j\) graph of the

\(2j\)-dimensional cube.

This is joint work with Evangelos Georgiadis and Hajime Tanaka.

15:00- Yohji AKAMA (Tohoku University)

**Set systems: Order types, continuous nondeterministic deformations, and quasi-orders**

summary:

By reformulating a learning process of a set system L as a game between

Teacher and Learner, we define the order type of L to be the order type of

the game tree, if the tree is well-founded. The features of the order type

of L (dim L in symbol) are (1) we can represent any well-quasi-order (wqo

for short) by the set system L of the upper-closed sets of the wqo such that

the maximal order type of the wqo is equal to dim L; (2) dim L is an upper

bound of the mind-change complexity of L. dim L is defined iff L has a

finite elasticity (fe for short), where, according to computational learning

theory, if an indexed family of recursive languages has fe then it is

learnable by an algorithm from positive data. Regarding set systems as

subspaces of Cantor spaces, we prove that fe of set systems is preserved by

any continuous function which is monotone with respect to the set-inclusion.

By it, we prove that finite elasticity is preserved by various

(nondeterministic) language operators (Kleene-closure, shuffle-closure,

union, product, intersection, …). The monotone continuous functions

represent nondeterministic computations. If a monotone continuous function

has a computation tree with each node followed by at most n immediate

successors and the order type of a set system L is α, then the direct image

of L is a set system of order type at most n-adic diagonal Ramsey number of

α. Furthermore, we provide an order-type-preserving contravariant embedding

from the category of quasi-orders and finitely branching simulations between

them, into the complete category of subspaces of Cantor spaces and monotone

continuous functions having Girard’s linearity between them.(To appear in

Theoretical Computer Science doi:10.1016/j.tcs.2011.08.010 )

16:00- Noriko WAKABAYASHI (Kyushu Sangyo University)

**Double shuffle and Hoffman's relations for multiple L-star values**

17:00- Naoyuki SHINOHARA (Network Security Research Institute, NICT)

**Primality proving and Grantham's problem**

summary:

There are two kinds of algorithms to determine the primality of a given

integer. The one is a primality test which is efficient but probabilistic,

namely, it rarely makes a wrong answer. Another is a primality proving

that always gives a correct answer, but it is not so efficient.

In this talk, we consider to construct an efficient primality proving

by improving Quadratic Frobenius primality test. In order to achieve our

aim, we discuss Grantham's Problem.