9th TPP (2013) in Shinshu University – Program

November 21(Thu.)(木)

13:00 – 13:10 opening

13:10 – 13:55 session 1

後藤瑞貴 高橋和子(関西学院大学)

Inductive formalization of PLCA

13:55 – 14:40 session 1

14:50 – 15:35 session 2

アフェルト レナルド、坂口和彦(産業技術総合研究所、筑波大学)

C言語プログラムの形式検証のためのCoqライブラリの紹介

15:35 – 16:20 session 2

坂口和彦(筑波大学)

線形合同法数列の周期

16:30 – 17:30 session 3

Artur Kornilowicz(University of Bialystok)

New features of the Mizar system

18:00 – 20:00 party

November 22(Fri.)(金)

9:30 – 10:15 session 4

中正和久(信州大学)

Mizarによる有限可換群の基本定理の形式化

10:15 – 11:00 session 4

師玉康成、渡瀬泰成(信州大学、日本Mizar学会)

Mizarプロジェクトの現状について
初等整数論の形式化のすすめ

11:10 – 11:55 session 5

Fadoua Ghorabi and Kazuko Takahashi(関西学院大学)

Qualitative Spatial Reasoning about Superposition of Rectangles using Isabelle/HOL

13:00 – 13:45 session 6

平井洋一(産業技術総合研究所)

関係データベースの第三正規化の形式的検証

13:50 – 14:50 session 7

斉藤裕太(信州大学)

TPPmark2013

回答発表募集中,どしどしご応募ください.
現地にこれなくても回答だけ送っていただければ発表を行います.

14:50 – 15:00 closing