- Logic-ml - fos.kuis.kyoto-u.ac.jp

第22回プログラミングおよびプログラミング言語ワークショップ (PPL 2020) 論文/発表募集
by Kazuyuki ASADA 30 Aug '19

30 Aug '19

皆様，（重複受信ご容赦ください） 2020年3月2日（月）～3月4日（水）に佐賀県嬉野市で開催予定の PPL 2020の論文/発表募集をお送りします．理論・実装を問わずプログラミング・プログラミング言語に関する研究発表を幅広く募集します．どうぞ投稿をご検討ください．よろしくお願いいたします．森畑明昌（東京大学）平石拓（京都大学）（PPL 2020 プログラム共同委員長）（代理で浅田和之（東北大学）が送信しました） ================================================== 第22回プログラミングおよびプログラミング言語ワークショップ (PPL 2020) 発表募集 2020年3月2日（月）-- 3月4日（水）佐賀県嬉野市「嬉野温泉和多屋別荘」 https://jssst-ppl.org/workshop/2020/ ** 重要な日程 ** カテゴリ1: 発表申込締切 2019年12月24日（火）17:00 (JST) 論文提出締切 2020年 1月 7日（火）17:00 (JST) 採否通知 2020年 1月31日（金）カテゴリ2: 発表申込締切 2020年 1月21日（火）17:00 (JST) 採否通知 2020年 2月 3日（月）カテゴリ3: 発表申込締切 2020年 2月 3日（月）17:00 (JST) 採否通知 2020年 2月 7日（金）カテゴリ4: 発表申込締切 2020年 1月21日（火）17:00 (JST) 採否通知 2020年 2月 3日（月） ** PPL2020とは ** PPL2020は，プログラミングとプログラミング言語に関連する幅広い分野の研究者・技術者・学生が一堂に会し，最新の研究成果や新たな研究課題の提案・討論・アイディア交換を行うことを目的とした，合宿形式の研究集会です．代表的なトピックは以下のようなものですが，これに限らず，プログラミング・プログラミング言語に関する研究発表を幅広く受け入れます．基礎理論: 意味論，ラムダ計算，型理論，項書き換え，形式論理と証明，形式言語とオートマトン，圏論，チューリング機械，アルゴリズムなど言語デザイン: 各種プログラミングパラダイム（オブジェクト指向・関数型・論理型・アスペクト指向，その他あらゆるパラダイムを含む），モジュール化，メタプログラミング，並行・並列・分散計算，型システム，言語や言語システム等の相互運用，領域限定言語など言語処理系技術: コンパイラ，インタプリタ，実行時システム，仮想機械，プログラム最適化，プログラム解析，プログラム変換，メモリ管理などプログラミング補助: プログラム検証器，デバッガ，プロファイラ，統合開発環境，プログラム合成，リファクタリングなどケーススタディ: ソフトウェア開発報告，プログラミング技法，ツールの紹介など応用: システムソフトウェア，Webシステム，データベースシステム，数値計算，ユーザーインタフェース，セキュリティ，プログラミング教育，人工知能・機械学習など ** 発表募集カテゴリ ** 以下の4カテゴリの研究発表を募集します．詳しい募集要項は後日webページで公開します．カテゴリ1: 国内外で未発表の研究の発表カテゴリ2: 国際会議・学術雑誌等で既発表であるが，国内では未発表の研究の紹介カテゴリ3: ポスター・デモ発表カテゴリ4: サーベイ・チュートリアル発表カテゴリ1では，国内外で未発表の研究についての論文発表を募集します．PPL での議論をもとに研究を発展させ，国際会議や学術論文誌への投稿につなげることを奨励しています．会場で実りある議論ができるような，発展途上の研究を特に歓迎します．カテゴリ1の発表は，複数名の査読者によってその新規性・重要性・根拠の確かさ・説明の明瞭さを評価し，プログラム委員による議論によって採否を判断します．特に以下の点に注意してください． - 理論的な研究については，形式化の明瞭さと正しさが重要です．論文中に明示してあれば証明等が未完成でも構いませんが，証明等について議論できる程度の形式化は求められます． - 実装研究については，実装したソフトウェアやツールの有用性，実装のデザインチョイス，実装技術などが明瞭に説明されているかが重要です．論文中に明示してあれば実装や実験が未完成でも構いませんが，上記の点を議論できる程度の完成度は求められます．カテゴリ2では，国際会議や国際学術論文誌等で発表された，または採録決定済みの，国内では未発表の研究成果の紹介を募集します．PPLとの関連性・プログラム全体のバランス・発表された媒体をもとに，プログラム委員による議論によって採否を判断します．カテゴリ3では，PPLに関連する内容（未発表・既発表いずれでも構いません）についてのポスター発表を募集します．萌芽的なアイデアの紹介やツールのデモンストレーションなども歓迎します．PPLとの関連性・プログラム全体のバランスをもとに，プログラム委員による議論によって採否を判断します．カテゴリ4では，既存研究のサーベイやツールのチュートリアルなど，PPLの聴衆にとって有益な学術知識の紹介を募集します．内容は未発表・既発表いずれでも構いません．PPLとの関連性・内容の重要性・発表者の経歴・プログラム全体のバランスをもとに，プログラム委員による議論によって採否を判断します．カテゴリ1の採択論文の中から，特に独創的なアイディアや顕著な成果を含むものに対して論文賞を授与する予定です．さらに，カテゴリ1・2・4の全発表のなかから最も聴衆の支持を集めたものに発表賞，カテゴリ3の全発表のなかから最も聴衆の支持を集めたものにポスター賞を授与する予定です（いずれも一般の部・学生の部の2種類，ただし「発表賞」は既受賞者を除く）． ** プログラム委員会 ** 安部達也千葉工業大学荒堀喜貴東京工業大学石崎一明日本IBM 今井敬吾岐阜大学岩崎英哉電気通信大学岩間太日本IBM 馬谷誠二神奈川大学江本健斗九州工業大学大岩寛産業技術総合研究所紙名哲生大分大学亀山幸義筑波大学川端英之広島市立大学川本裕輔産業技術総合研究所菊池健太郎東北大学木村大輔東邦大学小島健介京都大学新屋良磨秋田大学関山太朗国立情報学研究所叢悠悠東京工業大学寺内多智弘早稲田大学日高宗一郎法政大学平石拓京都大学 (プログラム共同委員長) 廣川直北陸先端科学技術大学院大学水島宏太オプト森口草介関西学院大学森畑明昌東京大学 (プログラム共同委員長) ** 問い合わせ先 ** ppl2020-oc(a)googlegroups.xn--com()-m53d8hra6b34cycyguk0hje6i3045cmp3h ppl2020-pc-chair(a)jssst-ppl.xn--org(/)-043e5ita1c46ctozdpfoc1401qpyjc ==================================================

1 0

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 小野寛晰 27 Aug '19

27 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:sonoteno+unsubscribe@googlegroups.com> にメールを送信してください。このディスカッションをウェブ上で閲覧するには 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

[1st CFP] SOCREAL 2019
by Katsuhiko Sano 18 Jul '19

18 Jul '19

The First Call for Papers SOCREAL 2019 5th International Workshop on Philosophy and Logic of Social Reality 15 - 17 November 2019 Hokkaido University, Sapporo, JAPAN Under the auspices of Philosophy and Ethics Laboratory at Faculty of Humanities and Human Sciences, Hokkaido University, CAEP Center for Applied Ethics and Philosophy at Faculty of Humanities and Human Sciences, Hokkaido University, and LOG-UCI An interdisciplinary study of the logical dynamics of the interaction between utterances and social contexts, A research Project funded by JSPS (JSPS KAKENHI Grant Number JP 17H02258) [About SOCREAL] Since the last years of the 20th century, a number of attempts have been made in order to model various aspects of social interaction among agents including individual agents, organizations, and individuals representing organizations. The aim of SOCREAL Workshop is to bring together researchers working on diverse aspects of such interaction in logic, philosophy, ethics, computer science, cognitive science and related fields in order to share issues, ideas, techniques, and results. The earlier editions of SOCREAL Workshop has been held in March 2007, March 2010, October 2013, and October 2016. Building upon the success of these editions, its fifth edition will be held from 15 November till 17 November 2019. SOCREAL 2019 will consist of keynote lectures by invited speakers and presentations of submitted papers. Keynote lectures will be given by Barteld Kooi (University of Groningen), Jeremy Seligman (University of Auckland), and Tomoyuki Yamada (Hokkaido University). The working language of SOCREAL Workshop is English. [Submission] Researchers from various fields, including logic, philosophy, ethics, computer science, cognitive science are hereby invited to submit an extended abstract (up to two thousand words) by 23 August 2019 to yamada(a)let.hokudai.ac.jp . Each abstract will be peer-reviewed by the program committee of the workshop. The abstract should be written in English and sent as an attachment in .pdf format. Each abstract should include a title, names and contact details of the author or all the co-authors. It is requisite for the author or at least one of the co-authors of each accepted paper to attend the workshop and present the paper. [Important Dates] Deadline for Submission of Abstracts: 23 August 2019 Notification of Acceptance: 13 September 2019 Deadline for Registration: 14 October 2019 Workshop: 15-17 November 2019 [Publication] A printed booklet containing the abstracts of all the accepted papers will be available at the workshop. On-line proceedings containing the papers and the presentation slides presented at the workshop will be made available after the workshop. Authors of the presented papers will also be encouraged to submit (the revised versions of) the full papers for publication in an issue of The Journal of Applied Ethics and Philosophy after the workshop. The papers should be written according to the submission guidelines of the journal, and will be peer-reviewed. Further particularities and instructions will be announced after the workshop. [Website] For more information, please visit the following website: http://www.asahi-net.or.jp/~yt6t-ymd/sr19/index.html . [Contact] Tomoyuki Yamada yamada(a)let.hokudai.ac.jp

1 0

Talk by Gabriele Vanoni (July 18th, 11.00-)
by Kazushige TERUI 14 Jul '19

14 Jul '19

みなさま今週木曜に京都大学にてGabriele Vanoniさんによるご講演があります。詳細は下記の通りです。よろしければご参加ください。京都大学数理解析研究所照井一成 ========== Time: 11:00-12:00, July 18th, 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) Speaker: Gabriele Vanoni (Univ. Bologna) Title: The Geometry of Abstract Machines Joint work with Ugo Dal Lago and Beniamino Accattoli Geometry of Interaction (GOI) is a semantic framework describing the dynamics of cut-elimination in the Multiplicative Exponential fragment of Linear Logic (MELL). It has been formulated in many ways, from operator algebras to traced symmetrical monoidal categories. Remarkably, some of these formulations, in particular Context Semantics by Gonthier et al. led to the introduction of compilation techniques (Mackie '95) and abstract machines for higher-order functional languages (Danos and Regnier '99). However, these machines were always based on a proof-net representation of programs, via the so-called Girard translation. We introduce an abstract machine in the spirit of GOI based directly on the λ-calculus, without any explicit use of proof-nets. We prove soundness and adequacy, and we derive in our framework an optimization already presented by Danos and Regnier. We intend to analyze in the future the complexity of these machines, with particular emphasis on the trade-off between space and time efficiency.

1 0

論理学と形而上学についての講演会；7月18日14時30分より、名古屋大学情報学棟第4講義室
by 久木田水生 12 Jul '19

12 Jul '19

皆さま、 BCCにて失礼します。名古屋大学情報学研究科の久木田です。この度、岸田功平さんをお招きして下記の通り講演会を開催します。岸田功平さんはDalhousie大学のDepartment of Mathematics and Statisticsに所属されており、様相論理や圏論がご専門です。今回は様相述語論理と形而上学に関連するお話をしていただきます。岸田さんのウェブサイト https://www.mathstat.dal.ca/~kishida/ 皆様、どうぞ振るってご参加ください。また、興味のありそうな方に声をかけていただけると幸いです。久木田水生記日時：2019年7月18日（木）、14時30分から場所：名古屋大学情報学棟1F第4講義室。アクセス→ https://www.i.nagoya-u.ac.jp/access/ 講演者：岸田功平タイトル：Quantified Logic for Modal Reasoning and Theorizing 要旨： Logicians and metaphysicians have developed various models and semantics of quantified modal logic. These semantics come with ontological and metaphysical implications regarding the references of singular terms --- such as the necessity of Hesperus being Phosphorus. My primary question in this talk is how these metaphysical facts can be a posteriori facts, as opposed to a matter of logic, of the sort that a cognizer can come to know. The goal of this talk is to give a semantics that sheds new light on this aposteriority. I will take an approach in terms of intensional logic that treats all singular terms, predicates, and quantifiers as uniformly intensional. Combined with epistemic logic, my approach will provide a semantics and logic in which metaphysical principles regarding cross-world reference are substantial facts that a cognizer can both learn and use in their modal reasoning and theorizing. 以上

1 0

第41回量子情報技術研究会（QIT41）会告案内
by Yasuhito Kawano 08 Jul '19

08 Jul '19

logic-mlの皆様、 NTTの河野です。第41回量子情報技術研究会（QIT41）の会告案内をお送りします。皆様のご参加をお待ちしております。よろしくお願いします。河野泰人 ----------------------------------------------------------------- 第41回量子情報技術研究会（QIT41）研究会の内容：　　情報科学と量子力学を融合させた新しい分野，量子情報科学に関する研究会です．　情報を担う物理系の量子力学的側面を積極的に活かした新しい情報処理原理の研究と　そこから開かれる新しい学問体系の構築および新しい情報技術パラダイムの創生を　目指して，情報科学，物理学，光エレクトロニクスを含む理学，工学，数理科学に　携わる研究者間に自由な討論の場を提供し，この研究分野の発展を図ることを目的と　しています．　　第41回研究会を下記のように開催いたします．現在この分野で活躍する研究者は勿論，　自分の研究資産が何らかの形で使えそうだと予感している研究者・技術者など，　広く関連する分野の研究者・技術者からの発表を募集致します．聴講のみの参加も　歓迎致しますので，奮ってお申し込みください．　　なお，第38回研究会から学生発表賞を創設いたしました．応募方法等については，　下記のQITウェブサイトをご確認下さい．日時: 2019年11月18日(月)〜19日(火) 会場: 学習院大学百周年記念会館 (〒171-8588 東京都豊島区目白1-5-1) 発表募集分野 (申し込み状況によっては査読の可能性あり)：　量子情報，量子計算，量子暗号など広く量子情報技術に関わる理論的研究，実験的研究，　計算機科学的研究，数学的研究，および，その他関連分野．定員: 180名程度参加費：　一般4,000円，学生3,000円懇親会費：一般4,000円，学生2,000円 ※当日現地支払いの場合，参加費・懇親会費は上記に+1,000円が増額されます．　（参加事前登録または銀行振込が期限に間に合わない場合も，これに該当します．） ※学生限定・当日受付・予稿集なし・懇親会なしの参加費1,000円という選択肢もあります．　こちらは事前手続き不要です．研究会参加申込要領：　参加申込は下記 Web にて受付けます：　https://www.ieice.org/es/qit/qit41/ 　講演 (口頭，ポスター) の申込，予稿集原稿PDFの提出は，電子情報通信学会の　Webシステムを使用する予定．各種締切：【口頭講演申込締切】　　2019年10月4日（金）【ポスター講演申込締切】2019年10月18日（金）【予稿原稿提出締切】　　2019年10月18日（金）【参加申込締切】　　　　2019年11月1日（金）【問合せ先】　田崎晴明 (学習院大学) 　衞藤雄二郎（産総研）　柴田康介（学習院大学）　並木亮（学習院大学）　Email: qit41(a)qo.phys.gakushuin.ac.jp 主催: 量子情報技術特別研究専門委員会 (委員長: 平野琢也(学習院大学)) 共催: 応用物理学会量子エレクトロニクス研究会

1 0

モデル理論夏の学校・研究集会のお知らせ
by kota takeuchi 29 Jun '19

29 Jun '19

皆様２０１９年度のモデル理論夏の学校研究集会のお知らせです。本研究集会は，例年夏に開催されるモデル理論に関する研究集会です。モデル理論に興味のある方はだれでも参加していただけます。申し込み締め切り：８月２日（金）セミナーハウスに宿泊する場合は部屋数に限りがありますのでお早めにお申し込みください。また限られた予算内ですが旅費の援助も検討しています。希望される方はご相談ください。研究集会HP：https://sites.google.com/view/model-theory-summer-school-201/home 期間：２０１９年９月２日（月）午後～９月４日（水）午前場所：東海大学山中湖セミナーハウス山梨県南都留郡山中湖村山中３２３－１〒４０１－０５０１ＴＥＬ０５５５－６２－４１００世話役：竹内耕太、坪井明人筑波大学 kota(a)math.tsukuba.ac.jp, tsuboi(a)math.tsukuba.ac.jp 竹内耕太

1 0

（詳報）第18回関西集合論セミナ：2019年7月5日大阪府立大学
by Masaru KADA 21 Jun '19

21 Jun '19

みなさま：大阪府立大学嘉田勝です。過日ご案内しました小集会「第18回関西集合論セミナ」の詳報です。お問い合わせは嘉田まで。（講演のお申し込みは締め切りました）なお、関西集合論セミナの後、16:30 より、同じ講義室にて、 Paul Larson 氏による談話会講演を計画しています。（講演題目未定） ======== 第18回関西集合論セミナ 2019年7月5日（金） 13:00–-15:50 大阪府立大学中百舌鳥キャンパス A14棟333講義室プログラム（進行により多少前後します） 13:00--13:50 Paul Larson (Miami University, Ohio USA) Balanced Forcing Extensions 14:00--14:30 静間荘司（大阪府立大学） title to be announced 14:40--15:10 依岡輝幸（静岡大学） title to be announced 15:20--15:50 渕野昌（神戸大学） title to be announced ---- Paul Larson 氏講演概要 Title: Balanced Forcing Extensions Abstract: We will introduce the notions of virtual conditions and balanced conditions in definable partial orders, and apply these ideas to forcing extensions of the Solovay model. We will present a variety of independence results, and some ZF implications, for weak forms of the Axiom of Choice, and discuss related issues concerning the preservation of cardinals and chromatic numbers. Some of these results can be stated more generally using a natural classification of definable partial orders in terms of amalgamation properties. ======== -------- Masaru KADA （嘉田勝） kada(a)mi.s.osakafu-u.ac.jp --------

1 0

第18回関西集合論セミナ：2019年7月5日（金）大阪府立中百舌鳥キャンパス
by Masaru KADA 18 Jun '19

18 Jun '19

みなさま：大阪府立大学嘉田勝です。下記のとおり集合論研究者向けの小集会を開催します。ご参加、ご講演のお申し込みはお気軽に嘉田まで。 ======== 第18回関西集合論セミナ 2019年7月5日（金） 13:00–16:00（予定）大阪府立大学中百舌鳥キャンパス（講義室未定）講演者（6月18日現在）（順不同） Paul Larson (Miami University, Ohio USA) 静間荘司（大阪府立大学）依岡輝幸（静岡大学）お問い合わせ：嘉田勝 kada(a)mi.s.osakafu-u.ac.jp ======== -------- Masaru KADA （嘉田勝） kada(a)mi.s.osakafu-u.ac.jp --------

1 0

日本数学会2019年度秋季総合分科会の講演申し込みが開始されました
by Teruyuki YORIOKA 18 Jun '19

18 Jun '19

みなさま静岡大学の依岡です．日本数学会2019年度秋季総合分科会の講演申し込みが開始されました．多くのみなさまに講演をしていただきたいと思います．講演をご希望の方はなるべく早くに申し込みをしてください．講演締め切りは6月21日（金）までです． http://mathsoc.jp/meeting/kanazawa19sept/ なお，金沢駅周辺の宿泊事情により，参加ご予定の方はなるべく早めに宿泊予約をしていただくことが会場校より推奨されています．講演申し込みに併せて，早めの宿泊施設の予約もお願いします．

1 1

連続講演「計算量への数理論理学的アプローチ」
by Yoriyuki Yamagata 08 Jun '19

08 Jun '19

みなさま、下記のような連続講演を行います。表題：計算量への数理論理学的アプローチ日時：2019年7月5日20:00-21:00(初回）それ以降の開催日は参加者と相談して決定場所：大阪分散技術コミュニティ（大阪府大阪市福島区海老江２丁目８−２９ 2F）参加登録：https://connpass.com/event/134707/ 概要：計算量に関わる問題、とくにP≠NP問題を数理論理学的にアプローチする試みについて紹介します。最初に計算量理論を簡単に紹介したのち、Bussによる「限定算術」の階層がそれとどのように関わるかを説明します。さらに、限定算術の階層を等式系の無矛盾性証明を用いて分離する試みについて、講演者の次の二つの論文を紹介することにより報告します。 - CONSISTENCY PROOF OF A FRAGMENT OF PV WITH SUBSTITUTION IN BOUNDED ARITHMETIC, Journal of Symbolic Logic 2018 - Separation of bounded arithmetic using a consistency statement, Preprint 予備知識は特に要求しません。参加は事前登録制です。なお、民間の会議室を借りて行うため、入場料1000円が必要です。また、Skypeによる遠隔参加も可能ですので、興味をお持ちの方はSkype idをメールで送付いただければと思います。本メールは興味のありそうな方に自由に転送していただいて結構です。よろしくご参集ください。 -- Yoriyuki Yamagata (Senior Researcher) National Institute of Advanced Industrial Science and Technology

1 0

[CFP] The Coq Workhsop 2019 (締切延長)
by Jacques Garrigue 05 Jun '19

05 Jun '19

logic-mlの皆様、名古屋大学のガリグです。 Coq Workshop 2019の投稿締切を2019-06-10(月)まで延長しましたのでお知らせします。ぜひ投稿をご検討ください。投稿〆切：2019-06-10 (2ページの概要) よろしくお願いいたします。 -- ********************************************************************* The Coq Workshop 2019: Call for Talk Proposals Colocated with the 10th International Conference on Interactive Theorem Proving (ITP 2019), Portland, OR, USA ********************************************************************** We are pleased to invite you to submit talk proposals for 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/). 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. We invite all members of the Coq community to propose informal talks, discussion sessions, or any potential uses of the day allocated to the workshop. Important dates: - June 10 2019: Deadline for abstract submission (Extended) - July 2 2019: Notification to authors - September 8 2019: Workshop Submission Instructions: Authors should submit short proposals through EasyChair (https://easychair.org/conferences/?conf=coq2019) in the form of a PDF extended abstract of less than 2 pages, in full-page single-column style. Relevant subject matter includes but is not limited to: - Theory and implementation of the Calculus of Inductive Constructions - Language or tactic features - Plugins and libraries for Coq - Techniques for formalization programming languages and mathematics - Applications and experience in education and industry - Tools and platforms built on Coq (including interfaces) - Formalization tricks and pearls 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 For more information: https://staff.aist.go.jp/reynald.affeldt/coq2019/

1 0

2019年度数学基礎論サマースクールのご案内
by Teruyuki YORIOKA 03 Jun '19

03 Jun '19

みなさま静岡大学の依岡です． 2019年度数学基礎論サマースクールのウェブサイトを公開しました． https://www.sci.shizuoka.ac.jp/~math/yorioka/ss2019/ サマースクールに参加ご希望の方は以下の情報を8月2日(金)までに email で，件名を「SS2019」として依岡（ yorioka(a)shizuoka.ac.jp ）までお送りください．氏名：所属：身分： email アドレス：懇親会：参加・不参加みなさまぜひ9月の第1週目は静岡にお越しください．みなさまのご参加をお待ちしております．

1 0

Nagoya logic seminar
by 吉信康夫 28 May '19

28 May '19

皆様：名古屋大学の吉信です。以下の要領で名古屋ロジックセミナーを開催します。日時：5月31日(金) 15:30〜場所：名古屋大学大学院情報学研究科棟1階122室(講義室2) 講演者：渕野昌(神戸大学) タイトル：The trichotomy of the possible size of the continuum under the existence of a Laver-generic large cardinal 詳しくは名古屋ロジックセミナーのページをごらんください。 http://www.math.mi.i.nagoya-u.ac.jp/~kihara/logic-seminar.html 多数の方のご参加をお待ちしております。

1 0

SLACS 2019 講演募集のお知らせ
by Kensuke Kojima 26 May '19

26 May '19

皆様（複数のメイリングリストに送信しています。重複して受信の際はどうぞご容赦ください。） SLACS 2019（記号論理と情報科学）幹事の京都大学の小島健介です。今年度の講演募集を以下のとおり行います。ご検討よろしくお願いいたします。 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… 講演申込期限は **2018年8月25日** としますが、講演する意思があるという方は早目にご連絡いただけると幸いです。

1 0

[CFP] The Coq Workhsop 2019
by Jacques Garrigue 22 May '19

22 May '19

Logic-mlの皆様、名古屋大学のGarrigueです。投稿締切が近づきましたので、再度Coq Workshop 2019のCFPを送らせていただきます。フランス国立情報学自動制御研究所のNicolas Tabareau博士とCoqの開発チームによる招待講演を予定しております！ぜひ投稿をご検討ください。投稿〆切：2019-06-04 (2ページの概要) よろしくお願いいたします。 -- ********************************************************************* The Coq Workshop 2019: Call for Talk Proposals Colocated with the 10th International Conference on Interactive Theorem Proving (ITP 2019), Portland, OR, USA ********************************************************************** We are pleased to invite you to submit talk proposals for 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/). 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. We invite all members of the Coq community to propose informal talks, discussion sessions, or any potential uses of the day allocated to the workshop. Important dates: - June 4 2019: Deadline for abstract submission - July 2 2019: Notification to authors - September 8 2019: Workshop Submission Instructions: Authors should submit short proposals through EasyChair (https://easychair.org/conferences/?conf=coq2019) in the form of a PDF extended abstract of less than 2 pages, in full-page single-column style. Relevant subject matter includes but is not limited to: - Theory and implementation of the Calculus of Inductive Constructions - Language or tactic features - Plugins and libraries for Coq - Techniques for formalization programming languages and mathematics - Applications and experience in education and industry - Tools and platforms built on Coq (including interfaces) - Formalization tricks and pearls 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 For more information: https://staff.aist.go.jp/reynald.affeldt/coq2019/ _______________________________________________ jssst-ppl mailing list jssst-ppl(a)fos.kuis.kyoto-u.ac.jp http://www.fos.kuis.kyoto-u.ac.jp/cgi-bin/mailman/listinfo/jssst-ppl

1 0

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Logic-ml