Workshop on Formalization of Applied Mathematical Systems

A joint project of Chiba University and the University of Hawai`i

September 25 to October 2, 2015 at the University of Hawai`i, Manoa

Organized by Manabu Hagiwara (CU, Japan) and Monique Chyba (UH, USA)

Tentative Schedule (in progress)

-12:30 14:00-
Friday, Sept. 25 Organization Meeting, for workshop staffs,

Time: 11:00a-12:30a,
Room: Physical Science Building, Room 315
Monday, Sept. 28 Special Session on
Formalization of Coding Theory,

Time: 10:30a-12:30a,
Room: Campus Center Room 307,
Chair: Manabu Hagiwara (Chiba University),

Abstract: Report on ongoing project "Formalization of (Modern) Coding Theory".
Tuesday, Sept. 29 Special Session on
Formalization of Statistics,

Time: 10:30a-12:30a,
Room: Campus Center Room 307,
Chair: Jingfang Wang (Chiba University),

Abstract: Introduction to how to use Coq for formalization of probability theory.

Part I: Universal Algebraic Approach to Probabilistic Conditional Independence
10:30a - 11:00a Cain algebra for probabilistic conditional independence, Jinfang Wang (Chiba University)
11:00a - 11:15a Comments, J.B.Nation (University of Hawaii)

Part II: Formalization of Probabilistic Conditional Independence
11:30a - 11:50a Formalization of Lattice by Coq/SSReflect
S.Shimoyama and R.Yamaguchi (Chiba Univesity)
11:50a - 12:30a Formalization of cain using Coq/SSReflect
12:30a - Comments
J.B.Nation (UH), M.Hagiwara and K.Kuga (CU)
Wednesday, Sept. 30 Special Session on
Monads and Universal Algebra for Applied Mathematical Systems,
-Towards a formalization of universal algebras and its computation.-

Room: Campus Center Room 307,
Chair: Yoshihiro Mizoguchi (IMI, Kyushu University),

Abstract: The main aim of this session is considering structured proof database. There are many propositions and proofs which are similar. Those propositions can be proved generally for an abstracted statement. Further we may need to make connections between an individual proposition and an abstracted one. We consider those connections and hierarchies of theories from the viewpoints of formalization of Mathematics. As examples of hierarchies of theories, we first consider universal algebras and monads, matrix algebra and Clifford algebra, and class field theory and number theory.

10:30a - 11:15a Introduction (Yoshihiro Mizoguchi)
Algebraic Semantics of Programming Language - Category Theory, Universal Algebra, Kleisli Category, Monad(Triple), Algebraic Semantics -
11:30a - 11:45a Matrix Algebra (Naoya Yamaguchi, Kyushu University) Towards a formalization of Clifford algebra.
11:45a - 12:00a Class Field Theory (Kentaro Kamoda, Kyushu University) Towards a formalization of Number theory
12:15a - 12:30a Discussion
2:00p - 2:45p Tutorial: Infinitary theories (Y. Mizoguchi) Powerset monad as a complete semilattice, Filter monad as a continuous latteice, Ultrafilter monad as a compact Hausdorff space. or Tutorial: Assertion semantics using relational calculus (Y. Mizoguchi) Categorical assertion semantics in toposes.
3:00p - 4:45p Hands-on: How to use Coq Library for the theory of relational calculus

Workshop Dinner,

Time: 6:00p -,
Chair: TBA
Thursday, Oct. 1st Workshop,

Time: 9:05a-12:05a,
Room: Campus Center Room 307.

Chair: TBA,
9:05- 9:10 Manabu Hagiwara, Opening Remarks
9:10- 9:35 Jinfang Wang, Towards computer-verified probabilistic conditional independence
9:35- 10:00 Yusuke Kawamoto, Formal and Statistical Approach to Quantitative Information Flow of Programs
10:00- 10:20 Kenta Inoue, Formalizing Neural Network Struture
10:20- 10:40 Takafumi Saikawa, Coq's type theory and its soundness

10:40- 11:00 Break

Chair: TBA
11:00- 11:15 Kyosuke Nakano, Formalization of the Channel Capacity of Binary Erasure Channel in Coq/SSReflect
11:15- 11:40 Reynald Affeldt, Formalization of Error-correcting Codes: from Hamming to Modern Coding Theory
11:40- 12:05 Jacques Garrigue, Certification of a sum-product algorithm for LDPC on a BSC

Time: 13:20 - 16:50,
Room: Campus Center Room 307

Chair: TBA
13:20- 13:40 Gordon Okimoto, The JAMMIT Algorithm
13:40- 14:00 J.B. Nation, The LUST Algorithm
14:00- 14:25 Yoshihiro Mizoguchi, A Coq Library for the Theory of Realational Calculus
14:25- 14:50 Hyungrok Jo, Hash functions from expander graphs

14:50- 15:10 Break

Chair: TBA

15:10- 15:25 Tze-Wei Liu, Mathematics in Chiba: An Intercultural experience
15:25- 15:50 Yuichiro Fujiwara, Quantum error correction under a phenomenological syndrome error model I: The basics
15:50- 16:15 Yuu Tsunoda, Quantum error correction under a phenomenological syndrome error model II: Improved bounds through probabilistic methods
16:15- 16:35 Kenta Kasai, On spatially coupled low density parity check codes
16:35- 16:40 J.B. Nation, Closing Remarks
Friday, Oct. 2nd - Closing Meeting,

Colloquium Presentation to UH Mathematics Department.
Time: 3:30p - 5:00p,
Room: Keller Hall 401,
Speaker: Ken'ichi Kuga,
Title: Wild Topology and Formalizatoin



This work is supported by JSPS KAKENHI Grant Number 25289118.