-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathindex.html
171 lines (155 loc) · 8.69 KB
/
index.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
<!DOCTYPE html>
<Html lang="ja">
<head>
<meta content="text/thml; charset=utf-8" http-equiv="content-type" />
<meta content="text/css" name="content-style-type" />
<meta name="description" content="名古屋を中心に活動する定理証明器・関数型言語のコミュニティ">
<meta name="keywords" content="関数型言語,定理証明器,名古屋,証明,Coq,OCaml">
<link href="./bootstrap.css" media="screen" rel="stylesheet" type="text/css" />
<link href="./style.css" media="screen" rel="stylesheet" type="text/css" />
<title>ProofCafe - 名古屋を中心に活動する定理証明器・関数型言語のコミュニティ</title>
<!-- Google tag (gtag.js) -->
<script async src="https://www.googletagmanager.com/gtag/js?id=G-BCPFHLBVTF"></script>
<script>
window.dataLayer = window.dataLayer || [];
function gtag(){dataLayer.push(arguments);}
gtag('js', new Date());
gtag('config', 'G-BCPFHLBVTF');
</script>
</head>
<body>
<div class="container">
<div class="hero-unit">
<div class="description">
<h1>ProofCafe</h1>
<p>ProofCafeは名古屋を中心に活動する定理証明器・関数型言語のコミュニティです。</p>
<p>
<a href="https://twitter.com/share" class="twitter-share-button">Tweet</a>
<script>!function(d,s,id){var js,fjs=d.getElementsByTagName(s)[0];if(!d.getElementById(id)){js=d.createElement(s);js.id=id;js.src="//platform.twitter.com/widgets.js";fjs.parentNode.insertBefore(js,fjs);}}(document,"script","twitter-wjs");</script>
<a href="http://b.hatena.ne.jp/entry/" class="hatena-bookmark-button" data-hatena-bookmark-layout="standard" title="このエントリーをはてなブックマークに追加"><img src="http://b.st-hatena.com/images/entry-button/button-only.gif" alt="このエントリーをはてなブックマークに追加" width="20" height="20" style="border: none;" /></a><script type="text/javascript" src="http://b.st-hatena.com/js/bookmark_button.js" charset="utf-8" async="async"></script>
</p>
</div>
</div>
<div class="news alert alert-info">
<h2>おしらせ</h2>
<p>
現在おしらせはありません
</p>
</div>
<div class="row">
<div class="span4">
<h2>開催勉強会</h2>
<p>
ProofCafeではいくつかの勉強会を定期開催しています。
詳細は個別のページをご覧ください。
</p>
<h3><a href="http://proofcafe.org/wiki/">ProofCafe</a></h3>
<p>
Coqを用いたプログラムの証明について勉強する勉強会です。
コーヒーを飲みながら楽しく証明しましょう。
</p>
<h3> <a href="http://proofcafe.org/tapl/">TAPL-nagoya</a></h3>
<p>
<a href="http://www.amazon.co.jp/dp/0262162091">Types
and Programming Laungages</a>(通称TAPL)の読書会です。
ScalaやF#などの静的型付け言語の基礎になっている型理論について学びます。
</p>
<h3><a href="http://proofcafe.org/instiki/kctnagoya">休日カフェタイム, KCTNagoya</a></h3>
<p>圏論に関する勉強会です。</p>
<h3><a href="http://proofcafe.org/doehas/">どえりゃあ Haskell</a></h3>
<p>Haskellに関する勉強会です。</p>
</div>
<div class="span4">
<h2>サービス</h2>
<h3><a href="http://proofcafe.org/sf/">Software Foundations</a>(和訳)</h3>
<p>Benjamin C. Pierce氏による同名のテキストの和訳です。関数プ
ログラミグやラムダ計算についてCoqによる実例を交えながら丁寧
に説明されています。</p>
<h3><a href="http://proofcafe.org/cochin/">Cochin</a></h3>
<p>Coqの定理検索サービスです。</p>
<h3><a href="http://proofcafe.org/calcoq/">CalCoq</a></h3>
<p>Coqによる任意精度の計算機です。</p>
<h3><a href="http://proofcafe.org/k27c8/math/">数理大好き</a></h3>
<p>数学についてのいくつかのトピックに関する解説です。</p>
<h3><a href="http://search.ocaml.jp">OCaml API Search</a></h3>
<p>型によるOCaml APIの検索です。</p>
</div>
<div class="span4">
<h2>成果物</h2>
<h3>Coq Extraction機能の拡張</h3>
<p>
<a href="http://coq.inria.fr">Coq</a>のExtraction機能を拡張し、他言語への変換をサポートします。
</p>
<ul>
<li><a href="http://proofcafe.org/wiki/Coq2Scala">Coq to Scala</a></li>
<li><a href="http://github.com/mzp/coq-ruby">Coq to Ruby</a></li>
<li><a href="http://patch-tag.com/r/leque/coq-clojure-ext/home">Coq to Clojure</a></li>
</ul>
<h3><a href="http://proofcafe.org/wiki/ocamltter">OCamltter</a></h3>
<p>
ターミナルで動作するTwitterクライアントです。一部がCoqにより証明されています。
</p>
<h3><a href="http://www.msgpack.org">Msgpack for OCaml</a></h3>
<p>
Msgpackは軽量・高速を特徴とするオブジェクトシリアライザです。
Coqにより変換の正しさが証明されています。
</p>
<h3><a href="https://play.google.com/store/apps/details?id=jp.co.itpl.ocamlandroid">OCaml Toplevel on Android</a></h3>
<p>
OCamlの対話環境をAndroidに移植したものです。
</p>
<h3><a href="http://github.com/mzp/smlsharp-annot/">SML# + annot</a></h3>
<p>式の型を表示するコンパイラ拡張です。</p>
</div>
</div>
<div class="row">
<div class="span4">
<h2>過去のイベント</h2>
<ul>
<li><a href="http://proof-summit.connpass.com/event/141191/">ProofSummit 2019</a>(2019/09/29)</li>
<li><a href="http://proof-summit.connpass.com/event/91274/">ProofSummit 2018</a>(2018/09/02)</li>
<li><a href="http://proof-summit.connpass.com/event/58803/">ProofSummit 2017</a>(2017/07/23)</li>
<li><a href="https://proof-summit.connpass.com/event/34848/">ProofSummit 2016</a>(2016/09/25)</li>
<li><a href="http://proof-summit.connpass.com/event/16189/">ProofSummit 2015</a>(2015/09/12)</li>
<li><a href="http://proofcafe.org/wiki/Schedule/ProofSummit2014">ProofSummit 2014</a>(2014/09/06)</li>
<li><a href="http://proofcafe.org/wiki/StartSsreflect">StartSsreflect</a>(2014/04/26)</li>
<li><a href="http://partake.in/events/41ca44c0-c415-4f03-99da-5a6d2204941d">ProofSummit 2013</a>(2013/08/24)</li>
<li><a href="http://partake.in/events/3df37687-ccf7-440c-865c-3ddb1409f5df">Proof Summit 2012</a>(2012/09/02)</li>
<li><a href="http://partake.in/events/3dd7a673-1f26-4703-8929-3be8a7fc8938">ML名古屋</a>(2012/05/26)</li>
<li><a href="http://partake.in/events/f04706e0-0eac-4751-901f-41707bdfb1ef">スタートSML#</a>(2012/03/25)</li>
<li><a href="http://partake.in/events/ac41261d-6026-4d09-8814-5ad3e58446e8">ProofSummit</a>(2011/09/25)</li>
<li><a href="http://atnd.org/events/9238">Coq Party</a>(2010/11/27)</li>
<li><a href="http://atnd.org/events/6022">Coq庵</a>(2010/08/29)</li>
<li><a href="http://atnd.org/events/7945">名古屋Hackathon(ラムダ村)</a>(2010/10/09)</li>
</ul>
</div>
<div class="span4">
<h2>リンク</h2>
<ul>
<li><a href="http://github.com/ProofCafe">github</a></li>
<li><a href="http://www.itpl.co.jp/ocaml-nagoya/">ocaml-nagoya</a></li>
<li><a href="https://groups.google.com/group/fm-forum">Formal Method Forum</a>(東京)</li>
</ul>
</div>
</div>
<!-- Google Adsense -->
<script async src="https://pagead2.googlesyndication.com/pagead/js/adsbygoogle.js?client=ca-pub-3545276391244796"
crossorigin="anonymous"></script>
<!-- Proofcafeトップページ -->
<ins class="adsbygoogle"
style="display:block"
data-ad-client="ca-pub-3545276391244796"
data-ad-slot="8206154912"
data-ad-format="horizontal"
data-full-width-responsive="true"></ins>
<script>
(adsbygoogle = window.adsbygoogle || []).push({});
</script>
<footer>
<p>
Copyright ©right; 2010-2012 ProofCafe
</p>
</footer>
</div>
</body>
</html>