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
350
Coqの紹介 #w8lt
w8ltでCoqの紹介をしました
Shohei Yasutake
July 29, 2015
Tweet
Share
More Decks by Shohei Yasutake
See All by Shohei Yasutake
Erlang 事例紹介: メディアストリーム中継システム
amutake
0
480
Haskell の型クラスと Typeclassopedia の紹介 #w8lt
amutake
0
540
部屋のメトリクス可視化
amutake
0
760
Actario: A Framework for Reasoning About Actor Systems
amutake
0
790
🍣 #w8lt
amutake
2
530
代数的データ型について #w8lt
amutake
6
2.5k
Coq で証明付き Web アプリを作る #adf2015
amutake
2
920
FLL
amutake
1
1.4k
Other Decks in Programming
See All in Programming
クラシルを支える技術と組織
rakutek
0
190
フロントエンド開発に役立つクライアントプログラム共通のノウハウ / Universal client-side programming best practices for frontend development
nrslib
7
3.8k
GitHub Actions × AWS OIDC連携の仕組みと経緯を理解する
ota1022
0
220
dynamic!
moro
9
4.3k
GraphQL×Railsアプリのデータベース負荷分散 - 月間3,000万人利用サービスを無停止で
koxya
1
940
Reactをクライアントで使わない
yusukebe
7
6.3k
Back to the Future: Let me tell you about the ACP protocol
terhechte
0
120
CSC509 Lecture 03
javiergs
PRO
0
320
AccessorySetupKitで実現するシームレスなペアリング体験 / Seamless pairing with AccessorySetupKit
nekowen
0
200
Web フロントエンドエンジニアに開かれる AI Agent プロダクト開発 - Vercel AI SDK を観察して AI Agent と仲良くなろう! #FEC余熱NIGHT
izumin5210
2
280
実践AIチャットボットUI実装入門
syumai
7
2.3k
Web Components で実現する Hotwire とフロントエンドフレームワークの橋渡し / Bridging with Web Components
da1chi
2
1.2k
Featured
See All Featured
The Art of Programming - Codeland 2020
erikaheidi
56
14k
Bash Introduction
62gerente
615
210k
Building Better People: How to give real-time feedback that sticks.
wjessup
368
20k
Designing for humans not robots
tammielis
254
25k
GraphQLの誤解/rethinking-graphql
sonatard
72
11k
Automating Front-end Workflow
addyosmani
1371
200k
CoffeeScript is Beautiful & I Never Want to Write Plain JavaScript Again
sstephenson
162
15k
jQuery: Nuts, Bolts and Bling
dougneiner
64
7.9k
Raft: Consensus for Rubyists
vanstee
139
7.1k
StorybookのUI Testing Handbookを読んだ
zakiyama
31
6.2k
What’s in a name? Adding method to the madness
productmarketing
PRO
23
3.7k
A Modern Web Designer's Workflow
chriscoyier
697
190k
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ʹ͍ͭͯͳΜͱͳ͘Θ͔ͬͯΒ͑ͨΒخ͍͠Ͱ͢