Information
The workshop Theorem Proving and Provers for Reliable Theory and Implementations will be held on December 3rd(Wed)-5th(Fri) at Nishijin Plaza, Kyushu University. TPP (Theorem Proving and Provers Meeting) is held every year since 2005, and provides a forum to exchange ideas for both users and implementors of theorem provers and proof assistants. This is the tenth anniversary workshop.
Workshop Report:
Theorem proving and provers for reliable theory and implemaentations」(PDF 7.4MB)
(Y.Mizoguchi, J.Garrigue, M.Hagiwara, R.Affeldt, ed.)
,
MI Lecture Notes, Vol.61, Kyushu University, 138pages, 2015/03/06.
Date
- December 3, 2014 (13:00pm) -- December 5, 2014 (16:00pm)
Venue
TPPmark2014(Problem)
- We would like you to solve a problem (PDF) with your favorite theorem prover.
Please send your proof to the email address below.
Submitted proofs are published in the
github Repository.
We are going to compare proofs at the workshop.
Invited Speakers
- Correct-by-Construction Program Synthesis in Coq
(Adam Chlipala (MIT, USA)) (Dec. 3. 13:00 - 14:00)Fiat is a Coq library supporting deriving efficient programs from specifications. We think of it as enabling a new style of modularity in programming, where it is possible to separate functionality from performance, with language-enforced encapsulation keeping the latter from interfering with the former. More concretely, the programmer starts with a program written to be as easy to understand as possible. From here, optimization scripts are applied to do stepwise refinement, gradually replacing nondeterministic constructions with deterministic ones, and replacing slow algorithms with fast ones. As the implementation language of optimization scripts, we reuse Ltac, Coq's language for coding proofs and decision procedures. We inherit Ltac's support for generating proof trails that vouch for the soundness of all operations. With highly expressive functional programming languages for both the functionality and performance parts of programs, we develop new abstraction and modularity patterns on each side of the divide. Our main case study so far deals with specifications that resemble SQL query and update operations. A set of operations over a particular schema are packaged together as an abstract data type, hiding the concrete representation of a relational database. We refine these nondeterministic descriptions of operations into efficient functional programs, which can be extracted to OCaml and run with good performance. In ongoing work, we are extending the refinement process to produce efficient assembly code using imperative data structures (via the Bedrock library), retaining proof trails to relate those programs to the original specifications. We are also exploring several new specification domains with associated refinement strategies, including for parsing, graph algorithms, and stencils in scientific computing.
Joint work with Benjamin Delaware, Clément Pit--Claudel, and Jason Gross
- Mathematical components and algebraic numbers
(Cyril Cohen (INRIA Sophia-Antipolis, France)) (Dec. 5, 13:30-14:30)The Mathematical Components project spanned 6 years and involved 15 people, with the purpose of formalizing a proof of Feit-Thompson theorem (also known as the odd order theorem), which is a milestone in the classification of finite groups. The proof relies on various areas in mathematics, including group theory, linear algebra, representation theory, Galois theory,... The project succeeded in formalizing the proof thanks to the development of a large set of libraries and methodologies covering the mathematics. One of the main achievements of the project, besides the formalization of the main theorem, is this set of libraries, which were designed to be reused. They were indeed reused in other developments such as, for example, in formalizations on homological algebra, elliptic curves, Shannon's information theory, error correcting codes,... My personal contribution to the Mathematical Components libraries was to build algebraic numbers and the tools to construct and use them. In this talk, I will give an overview of the project, its library and I will detail my own contributions.
Program
- Schedule of Dec. 3
13:00 - Registration
Time Specker Title 13:30 - 14:00 Shogo Sekine
(Chiba Univ.)Formalizing Karp and Miller Acceralation for Petri Nets using SSReflect 14:00 - 14:30 Sosuke Moriguchi
(Kwansei Gakuin Univ.)Towards verification of program generations 14:30 - 15:00 Ryosuke Obi
(Chiba Univ.)Formalization of Variable-Length Source Coding Theorem: Converse Part 15:00 - 15:30 Kazuhiko Sakaguchi
(University of Tsukuba)Formalizing Strong Normalization Proofs 15-minute Break 15:45 - 16:15 Masahiko Sato
(Kyoto Univ.)A name-free lambda calculus 16:15 - 16:45 Kazuhisa Nakasho
(Shinshu Univ.)Formalization of Direct Sum Decomposition of Groups in Mizar 16:45 - 17:15 Hiroyuki Okazaki
(Shinshu Univ.)Formalization of polynomially bounded functions in Mizar
- Schedule of Dec. 4
Time Specker Title 09:30 - 10:30 Yoshihiro Imai
(IT Planning, Inc.)Formalization and verification of stream data processing for datacasting in Coq 10-minute Break 10:40 - 11:40 Taro Kurita
(FeliCa Networks, Inc.)The Application of VDM (Vienna Development Method) to the Industrial Development of Firmware for a Smart Card IC Chip 80-minute Lunch 13:00 - 14:00 Adam Chlipala
(MIT)Correct-by-Construction Program Synthesis in Coq 15-minute Break 14:15 - 14:45 Reynald Affeldt(AIST)
Jacques Garrigue(Nagoya Univ.)Formalization of Error-correcting Codes using SSReflect 14:45 - 15:15 Fadoua Ghourabi
(Kwansei Gakuin Univ.)Formalization of matrix representation of direction relations with application to the superposition of rectangles 15:15 - 15:45 Yoshinori Tanabe
(NII)Coq code extraction to Scala and its correctness 15-minute Break 16:00 - 16:30 Kentaro Okumura
(Kyoto Univ.)Formalization of Featherweight Java on Coq by using weak HOAS 16:30 - 17:00 Masahiro Yasugi
(Kyushu Institute of Technology)Towards Design of Universal Typed Intermediate Languages in Consideration of Memory Models 17:00 - 17:30 Masahiro Sato
(Nagoya Univ.)An intuitionistic Set-theoretical Model of the Extend Calculus of Construction 15-minute Break 17:45 - 18:30 TPPmark2014 (Repository)
Banquet(19:00 - ) @ Hinatabokko (Cusual Pub.)
* If you want to participate, please e-mail me.
- Schedule of Dec. 5
Time Specker Title 09:30 - 10:30 Shunsuke Yatabe
(JR West)Preparing formal specifications: uses of semiformal methods in the concept phase of a system design 10-minute Break 10:40 - 11:10 Kenichi Kuga(Chiba Univ.)
Manabu Hagiwara(Chiba Univ.)On formalization of basic geometric topology 11:10 - 11:40 Takafumi Saikawa
(Nagoya Univ.)Formalizing a coding theory 11:40 - 12:10 Tetsuo Ida
(University of Tsukuba)Formalization of geometric algebra with application to computational origami 80-minute Lunch 13:30 - 14:30 Cyril Cohen
(INRIA)Mathematical Components and Algebraic Numbers 15-minute Break 14:45 - 15:45 Kazushi Ahara
(Meiji Univ.)Interactive geometry software and automated theorem proving - Cinderella and KidsCindy
16:00 Closing
Submission/Questions
- tpp2014 at imi.kyushu-u.ac.jp (Yoshihiro Mizoguchi, Kyushu University)
Comittee
- Yoshihiro Mizoguchi (Kyushu University, Japan)
- Jacques Garrigue (Nagoya University, Japan)
- Manabu Hagiwara (Chiba University, Japan)
- Reynald Affeldt (AIST, Japan)
Organizer
Laboratory of Advanced Software in Mathematics, Institute of Mathematics for Industry, Kyushu University.
Co-organizer
Coop with Math Program, The Institute of Statistical Mathematics
Supporter
IEICE
Kyushu Section* This workshop is supported by in part by JSPS KAKENHI(Grant-in-Aid for Exploratory Research) Grant Number 25610034 and 25289118.
