• 07/28 Schedule/ProofCafe_22
• 時間: 14:30 - 17:30
• 場所: 名古屋大学 理学部1号館(多元数理科学棟)3階307教室
• 参加登録: PARTAKE: 第22回 ProofCafe
• ソフトウェアの基礎の命題と論拠のはじめから
• ドキュメントはCoqソースコードから自動生成されています。ソースコード全体はこちら: http://proofcafe.org/sf/sfja.tar.gz
• 参加者: 10人

特別講演

今日はGarrigue先生の研究留学生の研究に関する講演をお願いしました。

• タイトル: “Proving the Soundness of OCaml’s relaxed value restriction in Coq”
• 講演者: Thomas Leventis

練習問題: ★, optional (okd_before2_valid)

Theorem okd_before2_valid : okd_before2.
Proof.
unfold okd_before2.
intros.
apply okd_before with d2.
apply okd_before with d3.
apply H. apply H1. apply H0.
Qed.  
Print okd_before2_valid.

練習問題: ★, optional (okd_before2_valid_defn)

Print okd_before2_valid.

okd_before2_valid = 
fun (d1 d2 d3 : day) (H : ok_day d3) (H0 : day_before d2 d1)
  (H1 : day_before d3 d2) => okd_before d1 d2 (okd_before d2 d3 H H1) H0
     : okd_before2