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 |
Workshop, 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 |
Sponsors
co-Sponsors
This work is supported by JSPS KAKENHI Grant Number 25289118.