Logic-ml

9 participants
1781 discussions

Hans van Ditmarsch教授講演
by Satoshi Tojo 30 Aug '19

30 Aug '19

みなさま， LORIA-CNRSのHans van Ditmarsch教授により，以下の講演を行います．どうぞふるってご参加ください．日時：9/13(金)15:00--17:00 場所：北陸先端科学技術大学院大学　情報 II 棟コラボ6 東条 ********* One Hundred Prisoners and a Light Bulb Consider this riddle: "A group of 100 prisoners, all together in the prison dining area, are told that they will be all put in isolation cells and then will be interrogated one by one in a room containing a light with an on/off switch. The prisoners may communicate with one another by toggling the light-switch (and that is the only way in which they can communicate). The light is initially switched off. There is no fixed order of interrogation, or interval between interrogations, and the same prisoner will be interrogated again at any stage. When interrogated, a prisoner can either do nothing, or toggle the light-switch, or announce that all prisoners have been interrogated. If that announcement is true, the prisoners will (all) be set free, but if it is false, they will all be executed. While still in the dining room, and before the prisoners go to their isolation cells (forever), can the prisoners agree on a protocol that will set them free?" In this presentation I will present a solution, however I will mainly address such puzzles of knowledge in general. There are many others, such as the ‘Muddy Children Puzzle’ (also known as the ‘Wisemen Puzzle’), ‘Surprise Examination’, ‘Monty Hall’, etc. They often involve a (seemingly) paradoxical aspect making agents knowledgeable by announcements of their ignorance. Their provenance and dissemination is intriguing. Haruyuki Kawabe kindly told me that in Japan, a version of the Muddy Children Puzzle with coloured hats is known as 'Dirac's Puzzle', after the physicist Paul Dirac who introduced some Japanese physicists to the riddle about 1938, and it seems one of them wrote a novel using the idea of the puzzle in 1940. There is a relation between such knowledge puzzles and the area in logic known as ‘dynamic epistemic logic’. More information on such puzzles is found in the book also entitled 'One Hundred Prisoners and a Light Bulb' (Copernicus, 2015) and on the webpage http://personal.us.es/hvd/lightbulb.html. The puzzlebook has been translated into Japanese by Haruyuki Kawabe. Hans van Ditmarsch is a senior researcher at CNRS (the French National Research Organization), and based at LORIA in Nancy, where he is heading the research team CELLO (Computational Epistemic Logic in Lorraine). He is also affiliated to IMSc (Institute for Mathematical Sciences), in Chennai. His research is on the dynamics of knowledge and belief, information-based security protocols, modal logics, and combinatorics. He has been an editor of the Journal of Philosophical Logic. He is an author of the book Dynamic Epistemic Logic, an editor of the Handbook of Epistemic Logic. *************

1 0

AWPL2020 - CALL FOR PAPERS
by 小野寛晰 26 Aug '19

26 Aug '19

===================================================== AWPL 2020: 5th Asian Workshop on Philosophical Logic 7-9 April 2020 Hangzhou, China https://www.xixilogic.org/events/awpl2020/ <https://www.xixilogic.org/events/awpl2020/> ===================================================== CALL FOR PAPERS The 5th Asian Workshop on Philosophical Logic, 7-9 April 2020, Hangzhou, China Asian Workshop on Philosophical Logic (AWPL) is an event-series initiated by a group of Asian logicians, and in 2012 the first installment took place at the JAIST in Japan. It is devoted to promote awareness, understanding, and collaborations among researchers in philosophical logic and related fields. The workshop emphasizes the interplay of philosophical ideas and formal theories. Topics of interest include non-classical logics, philosophical logics, algebraic logics, and their applications in computer science, cognitive science, and social sciences. The second, third and fourth workshops took place successfully in Guangzhou (2014), Taipei (2016) and Beijing (2018), respectively. The previous post conference proceedings were published in the Studia Logica book series “Logic in Asia” (http://www.springer.com/series/13080?detailsPage=titles <http://www.springer.com/series/13080?detailsPage=titles>) with Springer. The Fifth Asian Workshop on Philosophical Logic (AWPL 2020) will be held in Hangzhou, China, on 7-9 April 2020, organized by the Institute of Logic and Cognition at Zhejiang University. The AWPL 2020 workshop is an event in the Zhejiang Logic for AI Summit (ZjuLogAI 2020, https://www.xixilogic.org/zjulogai/ <https://www.xixilogic.org/zjulogai/>) which takes place on 6-10 April 2020. All AWPL participants are invited to attend other events as well. ------------------------ INVITED SPEAKERS To be confirmed. ------------------------ SUBMISSION All submissions should present original works not previously published. Submissions should be typeset in English, using the LNCS template (https://www.springer.com/gp/computer-science/lncs/conference-proceedings-gu… <https://www.springer.com/gp/computer-science/lncs/conference-proceedings-gu…>), be prepared as a PDF file with at most 12 pages (including reference list, appendixes, acknowledgements, etc.), and be sent to the workshop electronically via EasyChair (https://easychair.org/conferences/?conf=awpl2020 <https://easychair.org/conferences/?conf=awpl2020>) by the corresponding author on time. It is assumed that, once a submission is accepted, at least one of its authors will attend the workshop and present the accepted work. After the workshop, selected submissions will be invited to revise and submit to a post conference proceedings, to be published in the “Logic in Asia” series. ------------------------ IMPORTANT DATES Submission deadline: 30 November 2019 Notification: 1 January 2020 Workshop: 7-9 April 2020 ------------------------ PROGRAM COMMITTEE (to be confirmed) Thomas Ågotnes, University of Bergen Nick Bezhanishvili, University of Amsterdam Sujata Ghosh, Indian Statistical Institute Meiyun Guo, South-West University, China Fengkui Ju, Beijing Normal University Kok-Yong Lee, National Chung Cheng University Beishui Liao, Zhejiang University (chair) Hanti Lin, University of California Davis Fenrong Liu, Tsinghua University Hu Liu, Sun Yat-Sen University Xinwen Liu, Chinese Academy of Social Sciences Minghui Ma, Sun Yat-Sen University Hiroakira Ono, JAIST, Japan Eric Pacuit, University of Maryland R Ramanujam, Institute of Mathematical Sciences, India Olivier Roy, University of Bayreuth Katsuhiko Sano, Hokkaido University Yì N. Wáng, Zhejiang University (co-chair) Chin-Mu Yang, Taiwan National University Jiji Zhang, Lingnan University

1 0

代数・論理・幾何と情報科学（ALGI）8月31日～9月1日（福岡）講演募集
by Akitoshi Kawamura 17 Aug '19

17 Aug '19

皆様（重複してお受取りの際はご容赦ください。）九大の河村と申します。標記の研究集会についてお知らせ致します。 ************************************************** 第三十回 ALGI（代数・論理・幾何と情報科学研究集会）令和元年8月31日（土）～9月1日（日）九州大学伊都キャンパス（福岡県福岡市西区）開催のお知らせと講演の募集 https://sites.google.com/site/algimeeting/ ************************************************** ALGI (Algebra, Logic, Geometry and Informatics) は、代数学や論理学、幾何学の情報科学への応用について、および情報科学の代数学や論理学、幾何学への応用についての研究集会で、年一回の頻度で開催されています。今年は、九州大学マス・フォア・インダストリ研究所（IMI）の共同利用研究集会として開催します。第30回記念の特別企画として、 ALGI各分野の応用的側面の話題について招待講演を予定しております。奮ってご参加ください。 ●招待講演勝股審也（国立情報学研究所）竹内泉（産業技術総合研究所）長谷川勇（スクウェア・エニックス）前原貴憲（理化学研究所） ●日程令和元年（2019年）8月31日（土）～9月1日（日） ●会場九州大学　伊都キャンパス IMIコンファレンスルーム（ウエスト一号館D棟4階W1-D-414） http://www.imi.kyushu-u.ac.jp/pages/joint_research_auditorium.html 講演を希望される方は、・題目・講演者名・所属・希望時間（基本は質疑応答含め30分です）・講演に必要な道具・梗概（後日でも構いません）・講演資料を後日ご提供いただけるかどうか※［はい／いいえ］などの情報を、幹事の西澤 nishizawa(a)kanagawa-u.ac.jp までお寄せください。「講演したいと思っている」程度の不完全情報でも結構です。 ※研究所共同利用の報告書に記載するため、もし差支えなければ、　講演内容について一件3～15ページ程度の資料（スライドのコピー等でも　結構です）を御提供いただけると幸いです。　「はい」を選択いただいた方には開催終了後に改めてお伺いさせて頂きます。時間の空きがある限り、開催直前まで講演申込を受け付けるつもりですが、申込順に発表時間を割り当てていきますので、講演をお考えの方は、なるべくお早めにお知らせいただけますようにお願い致します。参加自体は申込不要で自由にご参加いただけますが、初日の夕方に予定している懇親会については、事前に詳細を告知し参加申込を受け付ける予定です。できるだけ多くの皆さんのご講演・ご参加をお待ちしております。幹事・世話人河村彰星（九州大学）津曲紀宏（崇城大学）西澤弘毅（神奈川大学）溝口佳寛（九州大学）

1 2

PPL サマースクール 2019 のご案内
by Kohei SUENAGA 17 Aug '19

17 Aug '19

皆様，．（重複してお受け取りの場合はご容赦ください．）京都大学の末永と申します．日本ソフトウェア科学会大会併設の PPL サマースクール 2019 のご案内です．事前登録締め切りは8月19日となっております．今年は古瀬淳さんにブロックチェーンやスマートコントラクトについて Tezos を用いたハンズオンを含むセミナーをお願いしております．以下の Web サイトからご登録の上ご参加ください．よろしくお願いいたします． PPL 2019 サマースクール幹事末永幸平 -- PPLサマースクール2019：ブロックチェーンと形式検証 Webページ：http://ppl.jssst.or.jp/index.php?ss2019 参加登録：https://jssst2019.wordpress.com/participation/ 日本ソフトウェア科学会プログラミング論研究会 (PPL) 主催日本ソフトウェア科学会第36回大会併設企画講師：古瀬淳（ダイラムダ株式会社） 2019年8月26日(月) 10時～17時 (9時30分受付開始) 芝浦工業大学芝浦キャンパス（〒108-8548東京都港区芝浦3-9-14） * 概要ブロックチェーン技術というと，仮想通貨，仮想通貨というと，投機，規制，などの話題がどうしても先行しがちだが，技術面では，暗号，分散環境，プログラミング言語，形式的検証などの計算機科学最先端の技術が沢山使われている．このサマースクールでは，ブロックチェーン技術におけるこれらの理論面の関わりを，主にプログラミング言語に比重を置いて紹介し，実際に現在使用されているスマートコントラクト環境であるTezosのテストネットを使った実習を行う． * 講師紹介古瀬淳 (Jun FURUSE; ふるせじゅん) ダイラムダ株式会社代表取締役，Tezos Japan 理事．2002年パリ第七ディドロ大学博士課程修了，Ph.D．関数型言語の型システムの研究を行う．以降， LexiFi?，Jane Street Capital，Standard Chartered Bank 等で主に堅牢な金融システムを関数型言語による開発に従事．2018年から第三世代ブロックチェーン技術である Tezos のコア開発チームに唯一の日本人として参加している． * プログラム（予定） 9:30 - 10:00 受付 10:00 - 11:30 第1部: 通貨とブロックチェーンへのイントロダクション 11:30 - 13:00 昼休み 13:00 - 14:00 第2部: ブロックチェーンの基礎と Proof-of-stake 14:00 - 16:00 第3部: スマートコントラクトハンズオン 16:00 - 16:15 休憩 16:15 - 17:30 第4部: ブロックチェーンと形式検証第1部: 通貨とブロックチェーンへのイントロダクション通貨と通貨の歴史について概観し，オープンな分散データベースであるブロックチェーンが，なぜ仮想通貨の基盤として用いられているのかを解説する．また，ブロックチェーンや仮想通貨基盤における安全性の重要性について議論する．第2部: ブロックチェーンの基礎と Proof-of-stake ブロックチェーンの技術的詳細について解説する．また，代表的な合意形成アルゴリズムである proof-of-work (PoW) と proof-of-stake (PoS) について解説する．第3部: スマートコントラクトハンズオンスマートコントラクトは，ブロックチェーン上で動作する通貨授受をともなう契約自動執行プログラムであり，近年 Ethereum や Tezos において実装されている．今回は参加者の持参する PC の上で Tezos のスマートコントラクトを実際に記述し動作させてみる．第4部: ブロックチェーンと形式検証ブロックチェーンや，その上で実装される仮想通貨，スマートコントラクトにおいては，その安全性が非常に重要である．これらが安全でなかったためにこれまでに起きた事象をいくつか取り上げ，安全性を保証するための手法である形式検証がどのようにブロックチェーンやスマートコントラクトに使われているかを解説する． * 参加費学生会員1000円, 学生非会員2000円, 一般会員2000円, 一般非会員3000円参加ご希望の方は，日本ソフトウェア科学会第36回大会および併設イベントの参加申し込みページ https://jssst2019.wordpress.com/participation/ からお申し込みください．事前登録をお願いしております． * 受講者へのご連絡ハンズオンのパートは，ノート PC をご持参いただけるとよりお楽しみになれます．事前準備については，参加登録された方にメールでお知らせいたします． -- Kohei Suenaga (末永幸平), Ph.D Associate professor (准教授) Graduate School of Informatics, Kyoto University (京都大学情報学研究科) ksuenaga(a)gmail.com http://www.fos.kuis.kyoto-u.ac.jp/~ksuenaga/

1 0

リマインダ: SLACS 2019 講演募集のお知らせ
by Kensuke Kojima 12 Aug '19

12 Aug '19

皆様（複数のメイリングリストに送信しています。重複して受信の際はどうぞご容赦ください。）講演・懇親会申し込み締切まで二週間となりましたので、リマインダをお送りします。申し込み締切は8月25日です。ご検討よろしくお願いいたします。 SLACS 2019（記号論理と情報科学） https://sites.google.com/view/slacs-2019/home 日時 2019年9月9日（月）から2019年9月10日（火）場所京都市左京区吉田本町京都大学総合研究8号館3階講義室3 参加費無料。ただし、懇親会費は別途徴収します（懇親会は初日夕方に開催予定）。幹事京都大学小島健介連絡先 kozima(a)kuis.kyoto-u.ac.jp SLACSとは以下はSLACSのページの冒頭からの抜粋です。 http://www.math.s.chiba-u.ac.jp/SLACS/ 「SLACS（スラックス）は，記号論理学と情報科学の境界領域に関する研究発表・研究討論の場を提供することを目的にして開催されている研究集会です． 1985年1月に第１回が開催されて以来，毎年１回のペースで開催されています． SLACS は，堅苦しい研究会ではなく，その年の幹事を中心とした参加者自らの手作りによるフレンドリーな雰囲気を持った集会です．気軽に発表できる場ですから，研究が進行中の話題を持ってきて議論したり，学生さんが発表する場としても適当です．もちろん，発展を続けるこの分野の最先端の研究テーマに関する発表も数多く聞くことができます．参加者の資格は問いませんので，原則として，どなたでも講演発表・聴講いただけます．発表はごく少数の例外を除いて日本語です．」より詳しい情報はSLACSのページや最近の開催情報をご確認ください。 SLACS2018 (北海道大学) https://sites.google.com/view/slacs-2018/home SLACS 2017 (千葉工業大学) http://super.para.media.kyoto-u.ac.jp/~abet/slacs2017/index.html SLACS 2016 (名古屋大学) http://www.st.nanzan-u.ac.jp/info/sasaki/2016slacs/SLACS2016.html SLACS 2015 (南山大学) https://sites.google.com/site/ptslacs2015/ SLACS 2014 (東京工業大学) http://www.jaist.ac.jp/~y-keita/2014SLACS-NSA/ 講演・懇親会申込方法：講演・懇親会参加を希望される方は、以下のフォームよりお申し込み下さい。（聴講のみの場合は申し込み不要です。）フォーム送信後に表示される URL を控えておくと後で回答内容を編集できます。講演申し込み: https://docs.google.com/forms/d/e/1FAIpQLSdYjYnWTM8peBMkh7NraVW3SdFPmmSz8QD… 懇親会参加申し込み: https://docs.google.com/forms/d/e/1FAIpQLSckwAzNX3nRuDfKOmju0YphATiYnjcsbT4… 講演申込期限は **2019年8月25日** としますが、講演する意思があるという方は早目にご連絡いただけると幸いです。

1 0

９月３日(火)午後東大駒場「応用論理学」
by Toshio Suzuki 04 Aug '19

04 Aug '19

（複数お受け取りの方はご容赦下さい）首都大学東京の鈴木登志雄です。2019年9月3日午後に東大駒場で「応用論理学」という講演会を開催します。これは日本応用数理学会 2019年度年会の中の正会員主催オーガナイズドセッション（臨時の分科会）です。このセッション以外にも、年会には多くの講演が予定されています。皆様のご来場をお待ちしております。日本応用数理学会年会のプログラム・参加費・会場案内については年会ウェブページ https://annual2019.jsiam.org/ をご覧下さい。 ------- 「応用論理学」 2019年9月3日(火)16:30から17:50 東京大学駒場キャンパス21KOMCEE棟A(K211)室ご来場前に年会受付にお越し下さい：数理科学研究科（会場とは別の建物）117室チュートリアル AND-OR木の探索コスト / 鈴木登志雄 (首都大学東京) 重み付きAND-OR木の固有分布について【招待講演40分】 / 田中一之 (東北大学) ソロベイ還元と連続性 / 鈴木登志雄 (首都大学東京) (隈部正博、宮部賢志、水澤勇気との共同研究）連絡先鈴木登志雄 toshio-suzuki[atmark]tmu.ac.jp -------- セッション「応用論理学」チラシ http://toshio-suzuki-logic.jp/meeting/jsiam2019logic.pdf 日本応用数理学会年会のウェブ通常参加申込みは８月２６日まで、当日受付・当日払いもあります。 -- 鈴木登志雄首都大学東京理学研究科　数理科学専攻 toshio-suzuki(a)tmu.ac.jp

1 0

[参加募集] The Coq Workhsop 2019
by Jacques Garrigue 01 Aug '19

01 Aug '19

Logic-mlの皆様、名古屋大学のGarrigueです。 Coq Workshop 2019の開催案内をお送りします。ご参加をお待ちしております。早期参加申し込み締切：2019-08-04 ********************************************************************** The Coq Workshop 2019: Call for Participation Colocated with the 10th International Conference on Interactive Theorem Proving (ITP 2019), Portland, OR, USA ********************************************************************** We are pleased to invite you to participate in the Coq workshop 2019, which will be held on September 8 2019, in Portland, OR, USA. The Coq workshop is part of ITP 2019 (https://itp19.cecs.pdx.edu/). Topic: - The Coq workshop 2019 is the 10th Coq Workshop. The Coq Workshop series (https://coq.inria.fr/coq-workshop/) brings together Coq (https://coq.inria.fr/) users, developers, and contributors. While conferences usually provide a venue for traditional research papers, the Coq Workshop focuses on strengthening the Coq community and providing a forum for discussing practical issues, including the future of the Coq software and its associated ecosystem of libraries and tools. Thus, the workshop will be organized around informal presentations and discussions, supplemented with invited talks. Program: - Invited talk: + Nicolas Tabareau: Not a single proof assistant for all, but proof assistants for everyone - Discussion session with the Coq development team - Accepted talks: + Kazuhiko Sakaguchi. Validating Mathematical Structures + Akira Tanaka. A Gallina Subset for C Extraction of Non-structural Recursion + Christian Doczkal and Damien Pous. Graph Theory in Coq: Minors, Treewidth, and Isomorphisms + Bruno Bernardo, Raphaël Cauderlier, Basile Pesin, Zhenlei Hu and Julien Tesson. Mi-Cho-Coq, a framework for certifying Tezos Smart Contracts + Reynald Affeldt, Jacques Garrigue, Xuanrui Qi and Kazunari Tanaka. Experience Report: Type-Driven Development of Certified Tree Algorithms in Coq + Enrico Tassi and Erik Martin-Dorel. SSReflect in Coq 8.10 + Matthieu Sozeau, Yannick Forster, Simon Boulier, Nicolas Tabareau and Théo Winterhalter. Coq Coq Codet! + Florian Steinberg and Holger Thies. Computable analysis, exact real arithmetic and analytic functions in Coq + Florian Steinberg. _Some formal proofs about summable sequences in Coq - See https://staff.aist.go.jp/reynald.affeldt/coq2019/ for the schedule. Registration: - Early registration is before [2019-08-04 Sun] - See the ITP 2019 website for registration information: https://itp19.cecs.pdx.edu/registration/ Program Committee: - Reynald Affeldt (AIST) - Christian Doczkal (CNRS - LIP, ENS Lyon) - Jacques Garrigue (Nagoya University) - Chantal Keller (LRI, Univ. Paris-Sud) - Dominique Larchey-Wendling (CNRS, Loria) - Gregory Malecha (BedRock Systems Inc.) - Pierre-Marie Pédrot (INRIA) - Ilya Sergey (Yale-NUS College and NUS School of Computing) - John Wiegley (DFINITY) Organization contact (co-chairs): reynald.affeldt AT aist.go.jp, garrigue AT math.nagoya-u.ac.jp -- このメールは Google グループのグループ「sonoteno」に登録しているユーザーに送られています。このグループから退会し、グループからのメールの配信を停止するには sonoteno+unsubscribe(a)googlegroups.com <mailto:[email protected]> にメールを送信してください。このディスカッションをウェブ上で閲覧するには https://groups.google.com/d/msgid/sonoteno/19b8a2be-d4a4-4f0b-a68a-d64955ae… <https://groups.google.com/d/msgid/sonoteno/19b8a2be-d4a4-4f0b-a68a-d64955ae…> にアクセスしてください。

1 0

PPL サマースクール 2019 のご案内
by Kohei SUENAGA 29 Jul '19

29 Jul '19

皆様，．（重複してお受け取りの場合はご容赦ください．）京都大学の末永と申します．日本ソフトウェア科学会大会と同時開催される PPL サマースクール 2019 のご案内です今年は，ダイラムダ株式会社の古瀬淳さんに，ブロックチェーンやスマートコントラクトについてハンズオンを含むセミナーをお願いしました．これらの技術に形式検証等の技術がどのように役に立つか，という話もしていただく予定です．近年よく耳にするこれらの技術ですが，実際に動かしながら学べる機会は貴重ですので，どうぞ奮ってご参加ください．事前の参加登録が必要です．以下の Web サイトからご登録の上ご参加ください．よろしくお願いいたします． PPL 2019 サマースクール幹事末永幸平 -- PPLサマースクール2019：ブロックチェーンと形式検証 Webページ：http://ppl.jssst.or.jp/index.php?ss2019 参加登録：https://jssst2019.wordpress.com/participation/ 日本ソフトウェア科学会プログラミング論研究会 (PPL) 主催日本ソフトウェア科学会第36回大会併設企画講師：古瀬淳（ダイラムダ株式会社） 2019年8月26日(月) 10時～17時 (9時30分受付開始) 芝浦工業大学芝浦キャンパス（〒108-8548東京都港区芝浦3-9-14） * 概要ブロックチェーン技術というと，仮想通貨，仮想通貨というと，投機，規制，などの話題がどうしても先行しがちだが，技術面では，暗号，分散環境，プログラミング言語，形式的検証などの計算機科学最先端の技術が沢山使われている．このサマースクールでは，ブロックチェーン技術におけるこれらの理論面の関わりを，主にプログラミング言語に比重を置いて紹介し，実際に現在使用されているスマートコントラクト環境であるTezosのテストネットを使った実習を行う． * 講師紹介古瀬淳 (Jun FURUSE; ふるせじゅん) ダイラムダ株式会社代表取締役，Tezos Japan 理事．2002年パリ第七ディドロ大学博士課程修了，Ph.D．関数型言語の型システムの研究を行う．以降， LexiFi?，Jane Street Capital，Standard Chartered Bank 等で主に堅牢な金融システムを関数型言語による開発に従事．2018年から第三世代ブロックチェーン技術である Tezos のコア開発チームに唯一の日本人として参加している． * プログラム（予定） 9:30 - 10:00 受付 10:00 - 11:30 第1部: 通貨とブロックチェーンへのイントロダクション 11:30 - 13:00 昼休み 13:00 - 14:00 第2部: ブロックチェーンの基礎と Proof-of-stake 14:00 - 16:00 第3部: スマートコントラクトハンズオン 16:00 - 16:15 休憩 16:15 - 17:30 第4部: ブロックチェーンと形式検証第1部: 通貨とブロックチェーンへのイントロダクション通貨と通貨の歴史について概観し，オープンな分散データベースであるブロックチェーンが，なぜ仮想通貨の基盤として用いられているのかを解説する．また，ブロックチェーンや仮想通貨基盤における安全性の重要性について議論する．第2部: ブロックチェーンの基礎と Proof-of-stake ブロックチェーンの技術的詳細について解説する．また，代表的な合意形成アルゴリズムである proof-of-work (PoW) と proof-of-stake (PoS) について解説する．第3部: スマートコントラクトハンズオンスマートコントラクトは，ブロックチェーン上で動作する通貨授受をともなう契約自動執行プログラムであり，近年 Ethereum や Tezos において実装されている．今回は参加者の持参する PC の上で Tezos のスマートコントラクトを実際に記述し動作させてみる．第4部: ブロックチェーンと形式検証ブロックチェーンや，その上で実装される仮想通貨，スマートコントラクトにおいては，その安全性が非常に重要である．これらが安全でなかったためにこれまでに起きた事象をいくつか取り上げ，安全性を保証するための手法である形式検証がどのようにブロックチェーンやスマートコントラクトに使われているかを解説する． * 参加費学生会員1000円, 学生非会員2000円, 一般会員2000円, 一般非会員3000円参加ご希望の方は，日本ソフトウェア科学会第36回大会および併設イベントの参加申し込みページ https://jssst2019.wordpress.com/participation/ からお申し込みください．事前登録をお願いしております． * 受講者へのご連絡ハンズオンのパートは，ノート PC をご持参いただけるとよりお楽しみになれます．事前準備については，参加登録された方にメールでお知らせいたします． -- Kohei Suenaga (末永幸平), Ph.D Associate professor (准教授) Graduate School of Informatics, Kyoto University (京都大学情報学研究科) ksuenaga(a)gmail.com http://www.fos.kuis.kyoto-u.ac.jp/~ksuenaga/

1 0

JAIST Logic Seminar Series
by Tatsuji Kawai 26 Jul '19

26 Jul '19

皆様 Padova大学のFrancesco Ciraulo先生の講演のお知らせです。どうぞふるってご参加ください。河井達治北陸先端科学技術大学院大学情報科学系 e-mail: tkawai(a)jaist.ac.jp ----------------------------------------------- * JAIST Logic Seminar Series * * The seminar below is held as a part of JSPS Core-to-Core Program, A. Advanced Research Networks and EU Horizon 2020 Marie Skłodowska-Curie actions RISE project CID (http://www.jaist.ac.jp/logic/ja/core2core, http://cid.uni-trier.de/). Date: Wednesday 31st July, 2019, 15:20-17:00 Place: JAIST, Collaboration room 6 (I-57g) (https://www.jaist.ac.jp/english/top/access/index.html) Speaker: Francesco Ciraulo (University of Padova) Title: Overlap algebras: a constructive alternative to complete Boolean algebras Abstract: Although (complete) Boolean algebras does exist in a constructive framework, they fail to capture very basic examples, such as powersets. Constructively, the subsets of a given set form a complete Heyting algebra (locale), but one of a very special kind: it is an “overlap algebra”. The definition of an overlap algebra, as proposed by Giovanni Sambin some years ago, collapses to that of a complete Boolean algebra (Boolean locale) if the Principle of Excluded Middle (PEM) holds. Overlap algebras can be useful to obtain constructive versions of classical results about complete Boolean algebras. For instance, the regular open sets in a topological space form an overlap algebra. More generally, the smallest strongly dense sublocale of an overt locale is an overlap algebra. (The latter is a version of Isbell’s density theorem.) The sublocales of an overlap algebra have not been completely understood yet (contrary to the case of Boolean locales). At the moment we only know that the open sublocales of a given overlap algebra L are overlap algebras, and that there is a bijection between those sublocales of L which are overlap algebras, on one side, and the overt weakly closed sublocales of L (i.e. the points of its lower-powerlocale), on the other side. The internal locales in the topos of sheaves over a given locale L correspond to morphisms with codomain L in the (external) category of locales. In particular, internal overt locales correspond to open maps. Since overlap algebras are a special class of overt locales, it should be possible to identify internal overlap algebras in a localic topos as a special class of open maps. The ultimate goal would be to exploit the fact that a locale which is not an overlap algebra can “become” an overlap algebra internally in many Grothendieck toposes.

1 0

Talk by Nobuko Yoshida (July 30th, Tuesday, 14.00-)
by Kazushige TERUI 25 Jul '19

25 Jul '19

みなさま来週火曜日に京都大学にて吉田展子さん（Imperial College London）によるご講演があります。詳細は下記の通りです（いつもとは曜日・時間が異なりますのでご注意ください）。よろしければぜひご参加ください。京都大学数理解析研究所照井一成 ========== Time: 14:00-15:00, July 30th, Tuesday, 2019 Place: Rm 478, Research Building 2, Main Campus, Kyoto University 京都大学本部構内総合研究2号館 4階478号室 http://www.kyoto-u.ac.jp/en/access/yoshida/main.html (Building 34) Title: Behavioural Type-based Static Verification Framework for Go Speaker: Nobuko Yoshida (Imperial College London) http://mrg.doc.ic.ac.uk/ Abstract: I first give an overview of recent researches of my group. Go is a production-level statically typed programming language whose design features explicit message-passing primitives and lightweight threads, enabling (and encouraging) programmers to develop concurrent systems where components interact through communication more so than by lock-based shared memory concurrency. Go can detect global deadlocks at runtime, but does not provide any compile-time protection against all too common communication mismatches and partial deadlocks. In this work we present a static verification framework for liveness and safety in Go programs, able to detect communication errors and deadlocks by model checking. Our toolchain infers from a Go program a faithful representation of its communication patterns as behavioural types, where the types are model checked for liveness and safety.

1 0

Jump to page:

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Logic-ml