This project is maintained by ksk
TPP (Theorem Proving and Provers) ミーティングは，2005年から年に1回開催され，定理証明系を作っている人から使う側の人まで幅広い人たちが集まり，様々な側面からの話をしてアイディアの交換をしてきたものです．
ミーティング期間中の討論を大切にしたいと考えていますので，出来上がった仕事の講演だけでなく，進行中の仕事，未完成の仕事についての講演も歓迎します． 参加者には可能な限りご講演いただくことを期待しています．
TPP is a series of annual meetings for developers as well as users of theorem provers. Discussions from various aspects and exchanges of ideas have taken place in the past meetings since 2005.
We regard the discussions during the meeting to be most important. As such, not only the talks about completed work, but those about ongoing work and half-baked work are also welcome. We hope all participants would consider giving a talk.
2018年11月21日（水）午後から 11月22日（木）まで / From the afternoon on Wednesday, November 21 to Thursday, November 22, 2018
東北大学 電気通信研究所 本館 6階大会議室 (M601) / Conference Room (M601), 6th floor, Main Building, Research Institute of Electric Communication, Tohoku University (片平キャンパスについて / Map and Direction)
会場は片平キャンパス内にあります． 東北大学には仙台市内に複数のキャンパスがございますのでご注意ください．/ The venue is located in the Katahira Campus. Please keep in mind that Tohoku University has several campuses in Sendai.
〒980-8577 宮城県仙台市青葉区片平2-1-1 / 2-1-1 Katahira, Aoba-ku, Sendai, Miyagi 980-8577 (Google Maps)
中野圭介 (東北大学 電気通信研究所) / Keisuke NAKANO (Research Institute of Electrical Communication, Tohoku University) 問い合わせはこちらへ
11/9(金)までに こちらからお願いします．
題目をクリックすると概要がご覧になれます． / Click on the title of each talk to inspect its abstract.
■ 13:50 - 14:00 〜 オープニング 〜
14:00 - 15:00
Unification of the λ-caclulus and combinatory logic [スライド]
佐藤雅彦（京都大学情報学研究科）
The λ-calculus and combinatory logic have been studied as two closely related but distinct systems of logic and computation. In this talk, however, we will argue that they are in fact one and the same calculus.
We substantiate our argument by introducing what we will call the external syntax and the internal syntax for the two calculi. The external syntax will be given as a natural common extension of syntax for the λ-calculus and combinatory logic. The terms defined by the internal syntax will be characterized as the closed αη normal terms of the external syntax.
Thus, the external syntax provides us with human readable syntax containing all the traditional λ-terms and combinatory-terms, and the internal syntax is suitable for the infrastructure of a proof assistant.
We have checked the main results of this work using the Minlog proof assistant.15:00 - 15:30
Intrinsically Typed Reflection of a Gallina Subset Supporting Dependent Types for Non-structural Recursion of Coq [スライド]
Akira Tanaka（AIST）
Our goal is the production of formally-verified pieces of low-level code. We are developing a Coq plugin to generate C code. Currently we try to reduce trusted computing base of the code generation itself. For a part of the development, we designed an AST to represent Gallina terms. The AST can represent non-structural recursion using dependent type. The AST is GADT-style and can be denoted to the original Gallina term. This means that it is easy to verify the AST is correctly represent the original term by checking the orignal term and denotation of the AST are convertible. The AST is usable to implement translation from the AST to C in Gallina which can be verified directly in Coq.
■ 15:30 - 16:00 〜 休憩 〜
16:00 - 16:30
定理証明支援系Coqにおける余帰納的証明のガード条件の漸進的検査
小澤祐也（電気通信大学 大学院情報理工学研究科），中野圭介（東北大学 電気通信研究所）
定理証明支援系Coqでは，無限に続くリストのような余帰納的構造をもつデータについての証明を，タクティクと呼ばれるコマンドを用いて進めることができる．ただ，Coqでは無限のデータや証明をそのまま扱うことはできないため，再帰的な表現による有限の形で表している．このような無限のデータや証明は再帰関数として表現されるため，意味のないループの形でないという，ガード条件の検査(guardedness check)が証明の最後に行われている．このため，証明全体を走査するために時間がかかってしまうという問題や，途中でガード条件が成立しなくなっていてもユーザは証明の最後の検査まで気づくことができないという問題がある．Coqには証明途中でガード条件の検査を行うGuardedコマンドが存在するが，これもそれまでの証明全体を走査し検査を行うために，タクティクごとに実行すると時間効率が悪い．
そこで本発表では，Coqにおける余帰納的証明のガード条件の検査を証明中に少しずつ行い，ガード条件が成立しなくなった際，即座にユーザに知らせることができるような手法を提案する．本手法ではタクティクの実行毎に新しく作られた部分の証明のみを取得し，その部分的な証明に対してガード条件の検査を行う．検査を行った後は，その時点での環境などの情報を保持しておき，次回のタクティク実行時のガード条件の検査に用いる．16:30 - 17:00
ペトリネットにおける有界性判定の形式化 [スライド]
稲垣衛（千葉大学大学院 融合理工学府），山本光晴（千葉大学大学院 理学研究院）
ペトリネットはシステムのモデル化に使用される有向２部グラフであり、並行的、非同期的、非決定的動作の記述に使われる。我々のグループでは以前の研究において、Coq/SSReflectを用いて、対象とするペトリネットにおいてKarp-Miller木を構成する関数を定義し、それを用いてペトリネットが被覆性を有するか否かを判定する決定手続きを定義して、その手続きの正当性の形式的証明を与えた。本発表では、ペトリネットの性質のうち、有界性を同じくKarp-Miller木を用いて判定する手続きを定義し、その正当性の形式的証明を与える。
17:00 - 17:30
Challenges in blockchain certification [スライド]
Diego Olivier Fernandez Pons（Tezos Southeast Asia）
Blockchains are fault-tolerant open distributed databases with stored procedures. The fact they are permissionless and need an internal currency to achieve data replication makes them targets of choice for hackers. Formal verification techniques like theorem proving are required to achieve financial-grade security in blockchains. This presentation shows the challenges in certifying blockchain components.
■ 18:30 - 21:00 〜 懇親会 〜
9:30 - 10:00
Correctness of the LOUDS encoding of tree structures [github]
Jacques Garrigue（名古屋大学多元数理科学研究科）
Succinct data structures give space efficient representations of large amounts of data without sacrificing performance. In order to do that they rely on cleverly designed data representations and algorithms. We present here the formalization in Coq/SSReflect of the Level-Order Unary Degree Sequences (aka LOUDS), which encode the structure of a tree in breadth first order as a sequence of bits, where access operations can be defined in terms of Rank and Select, which work in constant time for static bit sequences.
10:00 - 10:30
Proving properties of the tree representation of dynamic bit sequences [スライド]
田中一成（名古屋大学多元数理科学研究科）
Succinct data structures give space efficient representations of large amounts of data without sacrificing performance. In order to do that they rely on cleverly designed data representations and algorithms. We present here the formalization in Coq/SSReflect of dynamic bit sequences represented as binary red-black trees, where Rank and Select present a low logarithmic overhead compared to their static versions, and with efficient Insert and Delete. It can be combined with the LOUDS representation of trees to provide a dynamic representation of dictionaries for instance.
■ 10:30 - 11:00 〜 休憩 〜
11:00 - 11:30
TPPMark 2018 について [スライド]
中野圭介（東北大学 電気通信研究所）
今年の TPPMark について出題内容および出題意図，提出された解答を紹介します．
11:30 - 12:15
Solving TPP2018 Mark Problem with CafeOBJ
二木厚吉（JAIST/NII/AIST）
A solution of TPP2018 Mark Problem with CafeOBJ is presented. Focuses of the talk are
(1) Proof score approach for theorem proving (or specification verification).
(2) Theorem proving only with reduction/rewriting over order-sorted first-order terms.
Some other cases of specification verifications with CafeOBJ are also planned to be explained.
■ 12:15 - 14:00 〜 休憩 〜
14:00 - 14:15
Mizarによる離散確率分布の識別不能性の形式化 [スライド]
岡崎裕之（信州大学）
発表者らは暗号の安全性証明の形式検証についての研究を進めている。暗号理論の為の確率についての諸定理、諸概念のMizarによる形式化について過去のTPPでも、離散確率分布や事象、無視可能関数等について報告した。本報告では確率分布の統計的な同一性の判定方法としてノンパラメトリック検定の「一種であるKS検定を利用することとし、そのMizarによる形式化の進捗報告と、前述の各形式化ライブラリとあわせて離散確率分布の識別不能性を形式化する方針について報告する。
14:15 - 14:45
The Correctness of Origami Geometric Constructions: A Challenge to Theorem Provers
Fadoua Ghourabi（Ochanomizu University, Tokyo）
Geometric construction is incomplete without a formal proof. So is origami geometric construction. When we propose an origami construction that has such or such property, it is natural to support our claim with a formal proof. Throughout the development of the computational origami system, called Eos, we have employed symbolic computation algorithms to prove properties about origami folds.
In this talk, We will cover some of the proof challenges that can be readily formulated from proving origami geometric constructions. We will also present our preliminary work on formalizing origami geometry in a proof assistant.
■ 14:45 - 15:00 〜 クロージング 〜
今回の問題は自然数の有限列に関する問題です． 解答は問い合わせ先までお送りください． お送りいただいたご解答は， TPP2018の2日目にお名前とともにこのページで公開いたします． なお，以下の記述において， 自然数とは非負整数のことであり， n%d は n を d で割った余りを表す 0 以上 d 未満の整数であるものとします．
The TPPmark problem of this year is about finite sequences of natural numbers. Please submit your solution to this address. The submitted solutions will be published on this Web page with the name of the authors on the second day of TPP 2018. In the following description, natural numbers mean non-negative integers and n%d stands for the remainder of dividing n by d where n%d is an integer between 0 and d−1 (both are inclusive).
自然数を要素とする有限列 [a0,a1,…,ak−1] (長さ k ≥ 1) が 妥当 ( valid ) であるとは，次の性質を満たすこととします．
すべての自然数 m, n について，m + am%k = n + an%k ならば m = n である．
たとえば，[1,1,1] や [2,0] や [1,5,3] や [2,0,1,9] は妥当ですが， [1,2,1] や [3,0] や [1,3,5] や [2,0,1,8] は妥当ではありません． このとき，以下の問いにお答えください．
is_valid を定義して，その判定が正しいことを証明してください．A finite sequence [a0,a1,…,ak−1] (of length k ≥ 1) of natural numbers is said valid when it satisfies the following condition:
for all natural numbers m and n, if m + am%k = n + an%k, then m = n
For instance, [1,1,1], [2,0], [1,5,3], and [2,0,1,9] are valid but [1,2,1], [3,0], [1,3,5], and [2,0,1,8] are not. Then please solve the following problems.
is_valid function that decides whether a given sequence is valid and give a formal proof to the correctness of the defined function.Mitsuharu Yamamoto (Coq/SSReflect)
Kenta Inoue (Coq/SSReflect)
Jacques Garrigue (Coq/SSReflect)
Kokichi Futatsugi (CafeOBJ, zipped archive)
TPP2017 / TPP2016 / TPP2015 / TPP2014 / TPP2013 / TPP2012 / TPP2011 / TPP2010 / TPP2009 / TPP2008 / TPP2007 / TPP2006 / TPP2005