Upgrade to Pro
— share decks privately, control downloads, hide ads and more …
Speaker Deck
Features
Speaker Deck
PRO
Sign in
Sign up for free
Search
Search
Coqの紹介 #w8lt
Search
Shohei Yasutake
July 29, 2015
Programming
0
330
Coqの紹介 #w8lt
w8ltでCoqの紹介をしました
Shohei Yasutake
July 29, 2015
Tweet
Share
More Decks by Shohei Yasutake
See All by Shohei Yasutake
Erlang 事例紹介: メディアストリーム中継システム
amutake
0
390
Haskell の型クラスと Typeclassopedia の紹介 #w8lt
amutake
0
450
部屋のメトリクス可視化
amutake
0
710
Actario: A Framework for Reasoning About Actor Systems
amutake
0
650
🍣 #w8lt
amutake
2
490
代数的データ型について #w8lt
amutake
6
2.3k
Coq で証明付き Web アプリを作る #adf2015
amutake
2
880
FLL
amutake
1
1.4k
Other Decks in Programming
See All in Programming
大公開!iOS開発の悩みトップ5 〜iOSDC Japan 2024〜
ryunakayama
0
190
Go1.23で入った errorsパッケージの小さなアプデ
kuro_kurorrr
2
390
Desafios e Lições Aprendidas na Migração de Monólitos para Microsserviços em Java
jessilyneh
2
150
RAGの回答精度評価用のQAデータセットを生成AIに作らせた話
kurahara
0
250
事業フェーズの変化に対応する 開発生産性向上のゼロイチ
masaygggg
0
200
開発を加速する共有Swift Package実践
elmetal
PRO
0
420
GraphQLの魅力を引き出すAndroidクライアント実装
morux2
3
730
エンジニア1年目で複雑なコードの改善に取り組んだ話
mtnmr
3
2k
React + TextAliveでカッコいいLyric Applicatioinを作ろう!!
tosuri13
0
400
Shinjuku.rb#95:心の技術書紹介
free_world21
1
110
The Sequel to a Dream of Ruby Parser's Grammar
ydah
1
220
今インフラ技術をイチから学び直すなら
yuhta28
1
140
Featured
See All Featured
Building an army of robots
kneath
302
42k
Documentation Writing (for coders)
carmenintech
65
4.3k
How to Create Impact in a Changing Tech Landscape [PerfNow 2023]
tammyeverts
43
2k
Designing Dashboards & Data Visualisations in Web Apps
destraynor
227
52k
Creating an realtime collaboration tool: Agile Flush - .NET Oxford
marcduiker
23
1.7k
The Language of Interfaces
destraynor
153
23k
Designing with Data
zakiwarfel
98
5k
Into the Great Unknown - MozCon
thekraken
29
1.4k
Put a Button on it: Removing Barriers to Going Fast.
kastner
58
3.4k
From Idea to $5000 a Month in 5 Months
shpigford
379
46k
I Don’t Have Time: Getting Over the Fear to Launch Your Podcast
jcasabona
26
1.9k
Visualizing Your Data: Incorporating Mongo into Loggly Infrastructure
mongodb
38
9.2k
Transcript
Coqͷհ W8LT @amutake_s
Coq • ఆཧূ໌ࢧԉܥͷͻͱͭ • ֶతͳ໋ͷূ໌ɾϓϩάϥϜͷ࣋ͭੑ࣭ ͷূ໌ͳͲʹ͑Δ
ఆཧূ໌ࢧԉܥ • ਓ͕ؒূ໌Λॻ͘ͷΛखॿ͚ͯ͘͠ΕΔ • ݱࡏͷূ໌ͷঢ়ଶɺԿΛࣔ͞ͳ͚Ε͍͚ͳ͍ͷ͔ɺ ͳͲͳͲΛදࣔͯ͘͠ΕΔ • ͪΐͬͱ͚ͩࣗಈূ໌ • ਖ਼͍͠ূ໌͔Ͳ͏͔ΛνΣοΫͯ͘͠ΕΔ
• ࢴͷ্ͷূ໌ͩͱຊʹਖ਼͍͠ͷ͔Θ͔Βͳ͍͜ͱ ͋Δ
ఆཧূ໌ࢧԉܥͷॏཁੑ • ʮͦͷূ໌ຊʹਖ਼͍͠ͷʁʯʮͦͷϓϩάϥϜຊʹ όάͳ͍ͷʁʯ • ࠷ۙͰɺग़ͯ͘ΔఆཧΛࢴ্Ͱͳ͘ఆཧূ໌ࢧԉܥ Λͬͯܗࣜతʹূ໌͍ͯ͠Δจ͕૿͖͍͑ͯͯΔ • ఆཧূ໌ࢧԉܥͷ͕ࣝڭཆʹͳΔͱ͖͕དྷΔ͔ •
จ͡Όͳ͍͖ͯ͘ͳΓূ໌Λ͚͛ͭΒΕΔ͜ͱ ͕͋ΔΒ͍͠… https://twitter.com/xuwei_k/status/409797442284969984
ఆཧূ໌ࢧԉܥ (Coq) ͷ࣮ྫ • CompCert • CoqͰॻ͔ΕͨCίϯύΠϥɻ࠷దԽͷաఔͰϓϩάϥϜͷҙຯΛม͑ͳ͍͜ͱͷূ໌ͳ Ͳ • ࢛৭ఆཧ
• ༗໊ͳఆཧɻCoqʹΑΔূ໌Ҏલʹূ໌͕͋ͬͨɺෳࡶ͗ͯ͢ຊʹਖ਼͍͔͠Ͳ͏ ͔Θ͔Βͳ͔ͬͨ • Verdi • ࠷ۙಡΜͰ͍͢͝ͱࢥͬͨࢄγεςϜ༻ͷCoqͷϑϨʔϜϫʔΫ (PLDI2015) • Coq্Ͱॻ͍ͨোੑ͕ͳ͍ࢄγεςϜͷίʔυΛɺ͋Δোʹରͯ͠ੑ͕͋Δ ͷʹมͯ͘͠ΕΔ (มޙͷϓϩάϥϜ͕োੑΛ࣋ͭ͜ͱূ໌ࡁΈ)ɻ࣮ߦՄೳ
Coqͷ͍ํ (งғؾ͚ͩ) • ϥΠϒূ໌͠·͢
Ͳ͏ͯ͠ূ໌͕Ͱ͖Δͷʁ • ΧϦʔϋϫʔυಉܕରԠʹجͮ͘ • ໋Λද͢ܕͷΛ࡞Δ͜ͱ͕Ͱ͖ΕͦΕ͕ͦ ͷ໋ͷূ໌ʹͳΔ ཧ ϓϩάϥϜ ໋1 ܕ1
໋1ͷূ໌ ܕ1ͷ ໋1㱺2 1ˠ2 ؔͷܕ ໋1a2 1 2ͷܕ ໋1a2 1 2ͷੵܕ
ূ໌߲ • Print ͨ͠ΒͣΒͣΒ Ͱͯ͘Δ͕ͭূ໌ • λΫςΟΫͷΈ߹ ΘͤʹΑΓূ໌߲͕ ࡞ΒΕΔ •
proof term ͱ͔ evidence ͱ͔ݺ Ε·͢
·ͱΊ • ఆཧূ໌ࢧԉܥʹ͍ͭͯઆ໌͠·ͨ͠ • Coqͷ͍ํʹ͍ͭͯσϞΛߦ͍·ͨ͠ • Ͳ͏ͯ͠ূ໌ͳΜͯ͜ͱ͕Ͱ͖Δ͔ʹ͍ͭͯઆ໌͠·͠ ͨ • Coqʹ͍ͭͯͳΜͱͳ͘Θ͔ͬͯΒ͑ͨΒخ͍͠Ͱ͢