2014年12月4日

#TPP2014 高信頼な理論と実装のための定理証明および定理証明器

研究集会「高信頼な理論と実装のための定理証明および定理証明器」高信頼なソフトウェア開発のために必要な形式手法, ソフトウェア検証, 数学の形式化, および, 証明の計算機による検証に関する研究集会を九州大学西新プラザで開催します. 続きを読む

プログラミング TPP mizar VDM formalmethod Coq

前へ 1 ・・ 5 6

Takashi Miyamoto @tmiya_

Mizar は確かに読みやすいような気がする。定理が連番管理されているのはちょっとあれだが。#tpp2014

2014-12-04 18:22:54

Sosuke MORIGUCHI @chiguri

a,bをgeneralizeして（revertして）そのあと処理するのにin a b *という書き方をする、でいいのかな。 #TPP2014

2014-12-04 18:34:54

Yoshihiro Imai @yoshihiro503

higher inductive type について説明してもらった #tpp2014 #HoTT #coq pic.twitter.com/dl1s6JRzOr

2014-12-04 21:20:56

拡大

Alcor @Alcor80UMa

@tmiya_ Mizarでの証明作業の半分はgrepに費やされます　#tpp2014

2014-12-04 23:30:14

前へ 1 ・・ 5 6