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 で証明付き Web アプリを作る #adf2015
Search
Shohei Yasutake
March 29, 2015
2
920
Coq で証明付き Web アプリを作る #adf2015
Shohei Yasutake
March 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
Coqの紹介 #w8lt
amutake
0
350
🍣 #w8lt
amutake
2
530
代数的データ型について #w8lt
amutake
6
2.5k
FLL
amutake
1
1.4k
Featured
See All Featured
Large-scale JavaScript Application Architecture
addyosmani
513
110k
Faster Mobile Websites
deanohume
310
31k
The Power of CSS Pseudo Elements
geoffreycrofte
78
6k
The Web Performance Landscape in 2024 [PerfNow 2024]
tammyeverts
9
840
Six Lessons from altMBA
skipperchong
28
4k
JavaScript: Past, Present, and Future - NDC Porto 2020
reverentgeek
52
5.6k
A better future with KSS
kneath
239
17k
Understanding Cognitive Biases in Performance Measurement
bluesmoon
29
2.6k
Agile that works and the tools we love
rasmusluckow
330
21k
Helping Users Find Their Own Way: Creating Modern Search Experiences
danielanewman
30
2.9k
A Tale of Four Properties
chriscoyier
160
23k
Exploring the Power of Turbo Streams & Action Cable | RailsConf2023
kevinliebholz
34
6.1k
Transcript
Coq Ͱূ໌͖ Web ΞϓϦΛ࡞Δ @amutake @amutake_s
Coq? • ఆཧূ໌ࢧԉܥͷͻͱͭ • ؔΛॻ͍ͯɺͦͷؔͷੑ࣭Λূ໌Ͱ͖Δ • ྫ: forall l :
list A, reverse (reverse l) = l. • Coq ୯ମͰϓϩάϥϜͷ࣮ߦͰ͖ͳ͍͕ɺ OCaml, Haskell, Scheme ʹมՄೳ
OCaml, Haskell, Scheme ʹมՄೳ
→ Coq Ͱ Web ΞϓϦ͕ ࡞ΕΔʂ(ͬͨʔʂ)
࡞Γํᶃ • ෭࡞༻Λىؔ͜͢ Coq ͰఆٛͰ͖ͳ͍ͷͰɺ७ਮͳ ෦͚ͩΛ Coq Ͱ࡞ͬͯɺ͏·͍͜ͱ OCaml ͱ࿈ܞ͢Δ
࡞Γํᶄ • Coq ͷ΄͏ Request -> Response ͷؔ Λ࡞Δ͚ͩ
࡞Γํᶅ (Coq Λ͍ͬͯΔਓ͚) • Ͳ͏ͯ͠෭࡞༻Λى͕͍͍ؔͨ͜͢ ߹ Parameter (ܕ͚ͩͰ࣮ମ͕ະఆٛͳ) ͳͲΛ͍ɺOCaml ͷؔΛࢦఆ͢Δ
Parameter read_file : string -> option string. Extract Constant read_file => “MyModule.read_file”.
࣮༻ྫ (clarus/coq-chick-blog) • https://github.com/clarus/coq-chick-blog • Coq ϒϩάΤϯδϯ • http://coq-blog.clarus.me/ ←
͜ͷϒϩά Coq (͔Βม͞Εͨ OCaml) Ͱಈ͍ͯΔ
Ͳ͜Λূ໌͢Δͷ • ূ໌͍ͨ͠ਓͳΜ͔దʹ͢Ε͍͍Μ͡Ό ͳ͍Ͱ͠ΐ͏͔ • clarus/coq-chick-blog ͰɺʮϩάΠϯ͠ ͍ͯͳ͍߹هࣄΛฤूͰ͖ͳ͍ʯΈͨ ͍ͳ͜ͱΛূ໌͍ͯ͠Δ
ࠓޙͷ՝ɾ·ͱΊ • ϥΠϒϥϦԽ͍ͨ͠ • OCaml ͷ෦͍͍ͩͨڞ௨ • Request -> Response
͚ͩॻ͚ಈ͘Α͏ʹ͍ͨ͠ • Coq ָ͍͠ͷͰͬͯΈ͍ͯͩ͘͞ʂ • ͓͢͢Ίॳ৺ऀ͚: http://proofcafe.org/sf/
༨ஊ: @clarus ͞ΜͭΑ͍ • Coq Λ Real World Ͱ͑ΔΑ͏ʹ͠Α͏ͱ͍ͯ͠Δਓ (Inria
ͷ PhD student) • ࠷ۙ io γϦʔζ (io, io-system, io-system-ocaml, …) Λ࡞͍ͬͯΔ • Coq ্Ͱ IO Effect Λදݱ͢ΔϥΠϒϥϦ܈ (coq-chick-blog ͷதͰ ͍ͬͯΔ IO ෦ΛϥΠϒϥϦͱͯ͠Γग़ͨ͠ͷͬΆ͍) • OCaml ίʔυΛॻ͔ͣʹ Coq Λมͯͦ͠ͷ··࣮ߦͰ͖ͨΓ • 3લ Coq ͷόάΛ͍ͭͯҙͷ໋Λূ໌Ͱ͖ΔϥΠϒϥϦΛެ։͠ ͯͨ