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

16 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 久木田水生 11 Jul '19

11 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 吉信康夫 27 May '19

27 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

ENTROPY 2019: Call for Participation - Co-located with EuroS&P'19
by David Nowak 21 May '19

21 May '19

*************************************************************** Call for participation — ENTROPY 2019 ENabling TRust through Os Proofs … and beYond 16 June 2019 Second International workshop on the use of theorem provers for modelling and verification at the hardware-software interface https://entropy2019.sciencesconf.org Co-located with EuroS&P'19, KTH, Stockholm, June 2019 *************************************************************** PROGRAM HIGHLIGHTS Formal Proof of a Secure OS Full Trusted Computing Base by Dominique Bolignano, Prove & Run Time protection: principled prevention of timing channels by Gernot Heiser, University of New South Wales Proving the security of interrupt handling against interrupt-based side-channel attacks: a case study by Frank Piessens, KU Leuven Nailing Down the Architectural Abstraction by Peter Sewell, University of Cambridge

1 0

Final Call for Papers: One week deadline extension of LORI-VII (18-21 October 2019@Chongqing)
by Katsuhiko Sano 15 May '19

15 May '19

Logic-ml の皆様、北海道大学の佐野勝彦です。今年10月に中国の重慶で開催される LORI-VII の final cfp をお送りいたします。皆様、奮ってご投稿ください。佐野勝彦 -------------------------------------------------------------------------------------------------------------- Final Call for Papers: One week deadline extension The Seventh International Conference on Logic, Rationality and Interaction (LORI-VII), South-West University, Chongqing, China, 18-21 October 2019. Conference Website: http://golori.org/lori2019/. The International Conference on Logic, Rationality and Interaction (LORI) conference series aims to bring together researchers working on a wide variety of logic-related fields that concern the understanding of rationality and interaction. The series aims at fostering a view of logic as an interdisciplinary endeavor, and supports the creation of an East -Asian community of interdisciplinary researchers. Keynote Speakers: Thomas Ågotnes (Bergen/Southwest) ∙ Leila Amgoud (Toulouse) ∙ Kevin Kelly (Carnegie Mellon) ∙ Rineke Verbrugge (Groningen) ∙ Michael Wooldrige (Oxford) ∙ Yanjing Wang (Beijing) We invite submission of contributed papers on any of the broad themes of the LORI series; specific topics of interest include, but are not limited to, formal approaches to: Agency, argumentation and agreement, belief representation, cooperation, belief revision and belief merging, strategic reasoning, games, decision making and planning, knowledge and action, epistemology, dynamics of informational attitudes, knowledge representation, interaction, norms and normative systems, natural language, rationality, philosophy and philosophical logic, preference and utility, social choice, probability and uncertainty, social interaction, intentions, plans, and goals. Submitted papers should be at most 12 pages long, with one additional page for references, in PDF format following the Springer LNCS style. Please submit your title and abstract by May 20, 2019, and your full paper by May 27, 2019. Submission is via the EasyChair for LORI-VII: https://easychair.org/my/conference?conf=lori7. Accepted papers will be collected as a volume in the FoLLi series on Logic, Language and Information, and extended versions of some will later be considered for publication in a special issue of the Journal of Logic, Language and Information (JoLLI). Local Chair: Meiyun Guo, South-West University, Chongqing, China. Program Committee: Andreas Herzig, Davide Grossi, Dominik Klein, Dongmo Zhang, Emiliano Lorini (co-chair), Eric Pacuit, Fengkui Ju, Fernando R. Velázquez-Quesada, Gabriella Pigozzi, Gregory Wheeler, Guo Meiyun, Hiroakira Ono, Hans van Ditmarsch, Hu Liu, Jakub Szymanik, Jeff Horty, Jeremy Seligman, Jérôme Lang, Junhua Yu, Katsuhiko Sano, Kaile Su, Kohei Kishida, Luciana Benotti, Natasha Alechina, Nina Gierasimczuk, Olivier Roy, Patrick Blackburn (co-chair), Paolo Turrini, R. Ramanujam, Robert van Rooij, Sara Negri, Sonja Smets, Soroush Rafiee Rad, Thomas Bolander, Thomas Icard, Thomas Ågotnes, Valentin Goranko, Wesley Holliday, Yì N. Wáng. Inquiries concerning the submission of papers should be addressed to Patrick Blackburn (patrick.rowan.blackburn(a)gmail.com) and Emiliano Lorini (Emiliano.Lorini(a)irit.fr).

1 0

教員公募（早稲田大学基幹理工学部、女性限定）
by USUBA Toshimichi 14 May '19

14 May '19

皆様、早稲田大学基幹理工学部の薄葉です。早稲田大学基幹理工学部応用数理学科で女性限定の公募を開始いたしました。職位：専任講師、准教授または教授 1 名【女性限定】所属：早稲田大学理工学術院専門分野：応用数理担当講義：応用数理に関する専門科目、理工学術院における一般教育数学科目着任時期：2020年4月以降なるべく早い時期勤務形態：常勤（任期なし）応募締め切り:2019年7月19日（金）（必着）詳細につきましてはリンク先のpdfをご覧ください。 https://waseda.box.com/shared/static/4oft3dtumtlz958gcl27hg5x21qlr6ih.pdf 「専門分野：応用数理」は幅広い意味でとらえていただいて構いません。関係各位にご周知いただくと共に、適任者をご存知の場合は応募をお勧めくださいますようお願い申し上げます -- Toshimichi USUBA School of Fundamental Science and Engineering, Waseda University

1 0

国際会議AQIS2019のご案内
by NISHIMURA Harumichi 13 May '19

13 May '19

logic-mlの皆様量子情報科学に関する国際会議AQIS2019のCFPを代理投稿させていただきます．締め切りまで２週間弱ですが関連する成果をお持ちの方の積極的なご投稿を宜しくお願い致します．名古屋大学大学院情報学研究科西村治道 ------------------------------------------------------------------------------------ CALL FOR PAPERS 19th Asian Conference on Quantum Information Science (AQIS'19)http://aqis-conf.org/2019/ 19-23 August 2019, Seoul, Korea Apologies if you receive this multiple times. Please forward to interested colleagues. We would like to draw your attention, and that of the quantum information community, to the 19th edition of the Asian Conference on Quantum Information Science (AQIS'19). AQIS is the leading conference in the subject in Asia and one of the longest-running worldwide, its highly successful predecessors having been EQIS'01-05 and AQIS'06-18. The topics covered include (but are not limited to) quantum computing, quantum information processing, quantum communication and cryptography, and foundations of quantum mechanics. Details about the conference are to be found on the website http://aqis-conf.org/2019/ Please check repeatedly as the information there will be updated regularly. Like its previous editions, AQIS'19 will consist of tutorials, invited talk, as well as oral and poster presentations, selected by a high-profile international program committee. Invited speakers are: * Giulio Chiribella (Hong Kong University) * Peng Xue (Beijing Computational Science Research Center) * XiaoLiang Qi (Stanford University) * Michelle Simmons (University of New South Wales / CQC2T) * Kihwan Kim (Tsinghua University) * Joe Fitzsimons (Singapore University of Technology and Design) * ChaoYang Lu (University of Science and Technology of China) * Liang Jiang (Yale University) Tutorials are: * Nathan Wiebe (Microsoft Research) ― Quantum Machine Learning * Debbie Leung (University of Waterloo) ― Embezzlement and Applications The submission deadline is 25 May 2019 (Sat), 23:59 Anywhere on Earth (AoE). All submissions should follow the guidelines specified on the web site:http://aqis-conf.org/2019/submission/ We are looking forward to seeing you in Seoul! Committee Chairs Steering Committee: Jaewan KIM (KIAS, Chair) Program Committee: Howard Wiseman (Griffith U, Chair) Runyao Duan (U Tech Sydney / Baidu, Co-Chair) Eleanor Rieffel (NASA, Co-Chair) Organizing Committee: Jaewan KIM (KIAS, Chair)

1 0

フォーマルアプローチ特集論文募集のご案内
by mano.ken＠lab.ntt.co.jp 09 May '19

09 May '19

logic-ml の皆様，電子情報通信学会論文誌英文 ED 分冊“フォーマルアプローチ特集”の，論文募集のご案内をさせていただきます．真野（NTT） =========================================================================== フォーマルアプローチ特集論文募集電子情報通信学会論文誌英文 ED 分冊フォーマルアプローチ特集編集委員会フォーマルアプローチ（形式手法・形式技法・形式理論）は，情報システムや組込みシステムの設計開発における信頼性向上の鍵となる重要な基盤です．これまで，設計対象のモデル化，要求分析と仕様記述，コード自動生成，テストと検証，保守と再利用などに関する技術と理論的知見を生み出してきました．近年の情報技術の進展に伴う対象領域の拡大に伴い，フォーマルアプローチは従来にも増して多様な分野で用いられるようになり，ますます発展しています．本小特集（2020 年 8 月号掲載）は，情報システムや組込みシステムの設計・運用におけるフォーマルアプローチについて，基礎理論から応用まで，幅広い研究を対象にしています．個別の対象領域に特化したケーススタディから，分野横断的な手法や理論まで，様々な方面から，フォーマルアプローチ研究に携わる若手研究者を奨励するとともに，この分野の研究が更に発展することを目指しております．奮って御投稿下さいますよう御案内申し上げます． 1. 対象分野主な対象は以下のとおりですが，これに限らず，「情報システムや組込みシステム及びそれをとりまく環境を定式化した上で，そのシステムの振舞いの解析や性質の導出を厳密に行い，設計・運用に関わる種々の問題の解決を図る」ことを目指した論文を広く募集します． - 基礎理論：システムの構造や振舞いの形式記述・検証に関する基礎理論 - 形式技法：ソフトウェア，ハードウェア，ネットワークなどのシステムに対する体系だった記述・検証技法 - 形式ツール：モデル検査器や定理証明器など，形式手法に基づくツール - 応用：情報システムや組込システム，回路系，情報セキュリティ，車載システム，人工知能・機械学習システム，マルチエージェントなどへの形式手法の適用事例 - 教育：教育事例 2. 論文の執筆と取扱い論文 (一般論文)，レター，及びサーベイ論文を募集します．投稿規程等は電子情報通信学会の英文誌の規程と同じです．以下の規程を御参照下さい． "The Information for Authors" (IEICE Transactions on Information and Systems) http://www.ieice.org/eng/shiori/mokuji_iss.html 3. 主なスケジュール論文投稿締切 2019 年 9 月 24 日 (火) 23:59 JST (厳守) 第一回判定通知予定 2019 年 11 月 22 日 (金) 初回修正締切 2020 年 1 月 17 日 (金) 最終判定通知予定 2020 年 3 月 6 日 (金) 発行予定 2020 年 8 月号 4. 投稿方法投稿に際しては，著者のうち少なくとも1名は本会会員でなければなりません．ただし招待論文に関してはこの限りではありません．必要な投稿資格を満たしていない著者からの投稿論文については，投稿を受け付けないこととなりますので御注意下さい．入会の案内はこちらを御覧下さい． http://www.ieice.org/jpn/join/index.html 本特集では，電子投稿のみを受付けます．論文を下記の web page から投稿して下さい．初期投稿時に，編集可能な論文本体 (TeX/Word)，図，著者の写真， biography も投稿する必要があります． https://review.ieice.org/regist/regist_baseinfo_e.aspx 投稿の際には以下の項目を選択してください． "Journal/Section" -> "[Special FO] Formal Approaches" 同時に WEB 上で著作権譲渡手続きができます．投稿手続きについて御不明な点がございましたら，問合先まで御連絡下さい． 5. 掲載料招待論文を含むすべての著者は，論文が採録となった場合，2020 年 4 月頃に掲載料をお支払い頂くことになります．2020 年 5 月 15 日までに支払いが完了しない場合には，採録取り消しとなります． 6. オープンアクセスオプション電子情報通信学会論文誌は，2019 年 1 月号掲載論文から，著者が通常の掲載料に加え追加料金を支払うことで，論文をオープンアクセスにできる選択肢を試行的に提供致します．オープンアクセスオプションに関する詳細は，"Information for Authors" (http://www.ieice.org/eng/shiori/mokuji_iss.html)を御参照下さい（オープンアクセスオプションは試行段階であり，予告なく変更されることがあります）． 7. 特集編集委員会委員長：真野健(NTT) 幹事：石川冬樹(情報研)，中川博之(阪大) 委員：青木利晃(北陸先端大)，青木善貴（日本ユニシス），來間啓伸(日立)，小林孝一(北大)，立石孝彰(日本IBM)，土屋達弘(阪大)，山口真悟(山口大) 8. 問合せ先本特集のホームページ: (和文) http://www.brl.ntt.co.jp/people/mano/fa2019/jp/ (英文) http://www.brl.ntt.co.jp/people/mano/fa2019/ 真野健 NTT コミュニケーション科学基礎研究所〒243-0198 神奈川県厚木市森の里若宮 3-1 ken.mano.eh(a)hco.ntt.co.jp =========================================================================== CALL FOR PAPERS Special Section on Formal Approaches The IEICE Transactions on Information and Systems announces a forthcoming special section on Formal Approaches to be published in August 2020. Formal methods and techniques play a key role in designing and developing highly reliable information systems and embedded systems. The last decades have seen various new techniques and profound theoretical results using formal methods in surprisingly many fields such as modeling, requirements analysis, specification, automatic generation of codes, testing, verification, and maintenance. They are rapidly extending their application domains as a result of the recent growth of information and communication technologies. The Special Section on Formal Approaches aims at stimulating research on formal approaches to information systems and embedded systems, ranging from fundamental theory to practical applications. Our emphasis is put on the cross-fertilization of related research fields and encouragement of young researchers. Topics: The major topics are listed below, but we solicit submissions in all areas of formal approaches, i.e., first to formalize information systems, embedded systems, and their environment, next to analyze their behavior and to derive their properties rigorously, and then to solve various problems in designing and managing the systems. - Theoretical foundations: all aspects of theory related to formal description and verification for structure and behavior of systems. - Formal techniques: techniques for mainly describing and analyzing systems, such as software, hardware and networks. - Formal tools: tools based on formal methods such as model checkers, theorem provers, and static and dynamic analyzers. - Applications: practical experiences of applying formal methods to information systems, embedded systems, circuits, security, AI systems, machine learning systems, multi-agent systems, automotive systems, etc. - Education: education on formal methods. Submission Instructions: The deadline for submission is Sep 24, 2019, 23:59 JST(GMT+9). Manuscripts should be carefully prepared according to the guideline in the "Information for Authors" (available at http://www.ieice.org/eng/shiori/mokuji_iss.html). The preferred length of the manuscript is 8 pages. Only electronic submission through the web page is accepted. Submit a complete paper and transfer copyright of the paper using the IEICE Web site https://review.ieice.org/regist/regist_baseinfo_e.aspx Authors should choose the [Special FO] Formal Approaches" as a "Journal/Section" on the online screen. Editorial Committee: Guest Editor-in-Chief: Ken Mano (NTT Communication Science Laboratories) Guest Editors: Fuyuki Ishikawa (National Institute of Informatics) Hiroyuki Nakagawa (Osaka University) Guest Associate Editors: Toshiaki Aoki (JAIST) Yoshitaka Aoki (Nihon Unisys) Koichi Kobayashi (Hokkaido University) Hironobu Kuruma (Hitachi, Ltd.) Takaaki Tateishi (IBM Japan) Tatsuhiro Tsuchiya (Osaka University) Shingo Yamaguchi (Yamaguchi University) Further information may be obtained from the web page at: http://www.brl.ntt.co.jp/people/mano/fa2019/ All inquiries should be sent to the guest editor in chief: Ken Mano NTT Communication Science Laboratories 3-1 Morinosato Wakamiya Atsugi Kanagawa 243-0198 Japan E-mail: ken.mano.eh(a)hco.ntt.co.jp Important Dates: Submission Deadline: Sep 24, 2019 23:59 JST (GMT+9) [strict] First Notification: Nov 22, 2019 Revised Version Deadline: Jan 17, 2020 Final Notification: Mar 6, 2020 Important Notice. (1) At least one of the authors must be an IEICE member when the manuscript is submitted for review. For the application of IEICE membership, visit http://www.ieice.org/eng/member/OM-appli.html (2) When a paper has been accepted for publication, the authors are required to pay the page charges covering part of the cost of publication. Please carefully read the submission guideline at http://www.ieice.org/eng/shiori/mokuji_iss.html (3) Upon accepted for publication, all authors, including authors of invited papers, should pay the page charges covering partial cost of publication around April, 2020. If payment is not completed by May 15, 2020, your manuscript will be handled as rejection. (4) [Open Access Option] Papers published in January 2019 issue and following issues will be offered a trial basis option which can make the papers open access if authors pay an additional charge on top of the usual page charge. For details on open access options, please carefully refer to “The Information for Authors” (http://www.ieice.org/eng/shiori/mokuji_iss.html). Note that open access option is still in the pre-trial stage, and it may be changed without notice. ===========================================================================

1 0

【Final CFP】Haskell Symposium 2019@ベルリン【投稿締切 5/10】
by Kazutaka Matsuda 07 May '19

07 May '19

（もし複数受けとりましたらご容赦ください）皆様，東北大学の松田です． ICFP併設の国際会議であるHaskell Symposium 2019のfinal CFPをお送りいたします．〆切（5/10）まで残りわずかとなりましたが，可能でしたらどうぞ投稿をご検討いだけますと幸いです．投稿の際は今年は軽量double blind reviewingが採用されていることにご注意ください． ================================================================================ ACM SIGPLAN CALL FOR SUBMISSIONS Haskell Symposium 2019 Berlin, Germany 22--23 August, 2019 http://www.haskell.org/haskell-symposium/2019/ ================================================================================ The ACM SIGPLAN Haskell Symposium 2019 will be co-located with the 2019 International Conference on Functional Programming (ICFP). **NEW THIS YEAR**: We will be using a lightweight double-blind reviewing process. See further information below. The Haskell Symposium presents original research on Haskell, discusses practical experience and future development of the language, and promotes other forms of declarative programming. Topics of interest include: * Language design, with a focus on possible extensions and modifications of Haskell as well as critical discussions of the status quo; * Theory, such as formal semantics of the present language or future extensions, type systems, effects, metatheory, and foundations for program analysis and transformation; * Implementations, including program analysis and transformation, static and dynamic compilation for sequential, parallel, and distributed architectures, memory management, as well as foreign function and component interfaces; * Libraries, that demonstrate new ideas or techniques for functional programming in Haskell; * Tools, such as profilers, tracers, debuggers, preprocessors, and testing tools; * Applications, to scientific and symbolic computing, databases, multimedia, telecommunication, the web, and so forth; * Functional Pearls, being elegant and instructive programming examples; * Experience Reports, to document general practice and experience in education, industry, or other contexts; * System Demonstrations, based on running software rather than novel research results. Regular papers should explain their research contributions in both general and technical terms, identifying what has been accomplished, explaining why it is significant, and relating it to previous work, and to other languages where appropriate. Experience reports and functional pearls need not necessarily report original academic research results. For example, they may instead report reusable programming idioms, elegant ways to approach a problem, or practical experience that will be useful to other users, implementers, or researchers. The key criterion for such a paper is that it makes a contribution from which other Haskellers can benefit. It is not enough simply to describe a standard solution to a standard programming problem, or report on experience where you used Haskell in the standard way and achieved the result you were expecting. System demonstrations should summarize the system capabilities that would be demonstrated. The proposals will be judged on whether the ensuing session is likely to be important and interesting to the Haskell community at large, whether on grounds academic or industrial, theoretical or practical, technical, social or artistic. Please contact the program chair with any questions about the relevance of a proposal. Submission Details ================== Early and Regular Track ----------------------- The Haskell Symposium uses a two-track submission process so that some papers can gain early feedback. Strong papers submitted to the early track are accepted outright, and the others will be given their reviews and invited to resubmit to the regular track. Papers accepted via the early and regular tracks are considered of equal value and will not be distinguished in the proceedings. Although all papers may be submitted to the early track, authors of functional pearls and experience reports are particularly encouraged to use this mechanism. The success of these papers depends heavily on the way they are presented, and submitting early will give the program committee a chance to provide feedback and help draw out the key ideas. Formatting ---------- Submitted papers should be in portable document format (PDF), formatted using the ACM SIGPLAN style guidelines. Authors should use the `acmart` format, with the `sigplan` sub-format for ACM proceedings. For details, see: http://www.sigplan.org/Resources/Author/#acmart-format It is recommended to use the `review` option when submitting a paper; this option enables line numbers for easy reference in reviews. Functional pearls, experience reports, and demo proposals should be labelled clearly as such. Lightweight Double-blind Reviewing ---------------------------------- Haskell Symposium 2019 will use a lightweight double-blind reviewing process. To facilitate this, submitted papers must adhere to two rules: 1. Author names and institutions must be omitted, and 2. References to authors’ own related work should be in the third person (e.g., not “We build on our previous work …” but rather “We build on the work of …”). The purpose of this process is to help the reviewers come to an initial judgment about the paper without bias, not to make it impossible for them to discover the authors if they were to try. Nothing should be done in the name of anonymity that weakens the submission or makes the job of reviewing the paper more difficult (e.g., important background references should not be omitted or anonymized). In addition, authors should feel free to disseminate their ideas or draft versions of their paper as they normally would. For instance, authors may post drafts of their papers on the web or give talks on their research ideas. A reviewer will learn the identity of the author(s) of a paper after a review is submitted. Page Limits ----------- The length of submissions should not exceed the following limits: Regular paper: 12 pages Functional pearl: 12 pages Experience report: 6 pages Demo proposal: 2 pages There is no requirement that all pages are used. For example, a functional pearl may be much shorter than 12 pages. In all cases, the list of references is not counted against these page limits. Deadlines --------- Early track: Submission deadline: 15 March 2019 (Fri) Notification: 19 April 2019 (Fri) Regular track and demos: Submission deadline: 10 May 2019 (Fri) Notification: 21 June 2019 (Fri) Camera-ready deadline for accepted papers: 30 June 2019 (Sun) Deadlines are valid anywhere on Earth. Submission ---------- Submissions must adhere to SIGPLAN's republication policy (http://sigplan.org/Resources/Policies/Republication/), and authors should be aware of ACM's policies on plagiarism (https://www.acm.org/publications/policies/plagiarism). The paper submission deadline and length limitations are firm. There will be no extensions, and papers violating the length limitations will be summarily rejected. Papers should be submitted through HotCRP at: https://haskell19.hotcrp.com/ Improved versions of a paper may be submitted at any point before the submission deadline using the same web interface. Supplementary material: Authors have the option to attach supplementary material to a submission, on the understanding that reviewers may choose not to look at it. This supplementary material should not be submitted as part of the main document; instead, it should be uploaded as a separate PDF document or tarball. Supplementary material should be uploaded at submission time, not by providing a URL in the paper that points to an external repository. Authors are free to upload both anonymized and non-anonymized supplementary material. Anonymized supplementary material will be visible to reviewers immediately; non-anonymized supplementary material will be revealed to reviewers only after they have submitted their review of the paper and learned the identity of the author(s). Resubmitted Papers: Authors who submit a revised version of a paper that has previously been rejected by another conference have the option to attach an annotated copy of the reviews of their previous submission(s), explaining how they have addressed these previous reviews in the present submission. If a reviewer identifies him/herself as a reviewer of this previous submission and wishes to see how his/her comments have been addressed, the principal editor will communicate to this reviewer the annotated copy of his/her previous review. Otherwise, no reviewer will read the annotated copies of the previous reviews. Travel Support ============== Student attendees with accepted papers can apply for a SIGPLAN PAC grant to help cover travel expenses. PAC also offers other support, such as for child-care expenses during the meeting or for travel costs for companions of SIGPLAN members with physical disabilities, as well as for travel from locations outside of North America and Europe. For details on the PAC program, see its web page (http://pac.sigplan.org). Proceedings =========== Accepted papers will be included in the ACM Digital Library. Authors must grant ACM publication rights upon acceptance (http://authors.acm.org/main.html). Authors are encouraged to publish auxiliary material with their paper (source code, test data, etc.); they retain copyright of auxiliary material. Accepted proposals for system demonstrations will be posted on the symposium website but not formally published in the proceedings. All accepted papers and proposals will be posted on the conference website one week before the meeting. Publication date: The official publication date of accepted papers is the date the proceedings are made available in the ACM Digital Library. This date may be up to two weeks prior to the first day of the conference. The official publication date affects the deadline for any patent filings related to published work. Program Committee ================= Ki-Yung Ahn Hannam University Christiaan Baaij QBayLogic B.V. José Manuel Calderón Trilla Galois, Inc Benjamin Delaware Purdue University Richard Eisenberg (chair) Bryn Mawr College Jennifer Hackett University of Nottingham Kazutaka Matsuda Tohoku University Trevor McDonell Utrecht University Ivan Perez NIA / NASA Formal Methods Nadia Polikarpova University of California, San Diego Norman Ramsey Tufts University Christine Rizkallah University of New South Wales Eric Seidel Bloomberg LP Alejandro Serrano Mena Utrecht University John Wiegley Dfinity Foundation Thomas Winant Well-Typed LLP Ningning Xie University of Hong Kong If you have questions, please contact the chair at: rae(a)richarde.dev ================================================================================

1 0

【参加募集】Bx 2019（6/4，フィラデルフィア）【Early Registeration〆5/4】
by Kazutaka Matsuda 25 Apr '19

25 Apr '19

皆様，東北大学の松田です．来たる6/4にアメリカのフィラデルフィアで開催される双方向変換に関する国際ワークショップBx 2019の参加募集をお送りいたします． Bx 2019 Call for Participation ============================== Highlights ---------- * Invited speaker: Zack Ives on Views, Update Propagation, and Provenance * Registration information (early deadline: May 4) * List of accepted papers and talks General Information ------------------- * 8th International Workshop on Bidirectional Transformations * http://bx-community.wikidot.com/bx2019:home * June 4, 2019, Saint Joseph’s University, Philadelphia, PA, USA * as part of the Philadelphia Logic Week (PLW) 2019: https://sites.sju.edu/plw/ Bidirectional transformations (bx) are a mechanism for maintaining the consistency of at least two related sources of information. Such sources can be relational databases, software models and code, or any other document following standard or ad hoc formats. Bx are an emerging topic in a wide range of research areas, with prominent presence at top conferences in several different fields (namely databases, programming languages, software engineering, and graph transformation), but with results in one field often getting limited exposure in the others. Bx 2019 is a dedicated venue for bx in all relevant fields, and is part of a workshop series that was created in order to promote cross-disciplinary research and awareness in the area. As such, since its beginning in 2012, the workshop has rotated between venues in different fields. Bx 2019 will be a part of Philadelphia Logic Week (PLW) 2019, which also includes conference and workshops on logic, provenance, and databases, topics that we hope will complement Bx and help build engagement with these communities. Registration ------------ * https://sites.sju.edu/plw/plw-2019-registration/ * Early registration deadline: May 4 * Passes available for attending multiple co-located events, including LPNMR (Logic Programming and Nonmonotonic Reasoning) and workshops, Datalog 2.0 (Resurgence of Datalog in Academia and Industry), and TaPP (Theory and Practice of Provenance) * Opportunities for students to receive financial support from the LPNMR Doctoral Consortium Invited Talk ------------ * Views, Update Propagation, and Provenance Zachary Ives (University of Pennsylvania) http://www.cis.upenn.edu/~zives/ Accepted Papers and Talks ------------------------- The abstracts can be found at http://bx-community.wikidot.com/bx2019:accepted . * ASN.1 Encoding Schemes Done Right Using CMPCT Mark Tullsen (Galois, Inc.) * Lenses and Learners Brendan Fong (Massachusetts Institute of Technology) and Michael Johnson (Macquarie University) * Multicategories of Multiary Lenses Michael Johnson (Macquarie University) and Robert Rosebrugh (Mount Allison University) * Incremental Bidirectional Model Transformation with eMoflon::IBeX (Tool Paper) Nils Weidmann (Paderborn University), Anthony Anjorin (Paderborn University), Lars Fritsche (TU Darmstadt), Gergely Varró, Andy Schürr (TU Darmstadt), and Erhan Leblebici (TU Darmstadt) * A Bidirectional Krivine Machine (Short Paper) Mikael Mayer (University of Chicago) and Ravi Chugh (University of Chicago) * Consistent Runtime Adaptation of User Interfaces (Short Paper) Anthony Anjorin (Paderborn University), Enes Yigitbas (Paderborn University), and Hermann Kaindl (Vienna University of Technology) * Symmetric d-Lenses and Symmetric c-Lenses are not Coextensive (Short Paper) Michael Johnson (Macquarie University) and François Renaud (Université Catholique de Louvain) * A Toolbox of Lenses: Dimensions of the Lens Design Space (Talk) Zinovy Diskin (McMaster University) * Expanding the Power of Lens Synthesis (Talk) Anders Miltner (Princeton University), Solomon Maina (University of Pennsylvania), Kathleen Fisher (Tufts University), Benjamin Pierce (University of Pennsylvania), David Walker (Princeton University), and Steve Zdancewic (University of Pennsylvania) * Optics and Type Equivalences (Talk) Jacques Carette (McMaster University) and Amr Sabry (Indiana University Bloomington) * Reified Correspondences: A New Component of the Multiary Delta Lenses Framework (Talk) Zinovy Diskin (McMaster University)

1 0

ERATO 蓮尾メタ数理システムデザインプロジェクトシンポジウム--高信頼自動運転システムのための先進的研究-- のご案内
by Kohei SUENAGA 25 Apr '19

25 Apr '19

（複数受け取られましたらご容赦ください．）皆様，京大の末永です．本 ML をお借りして，5/21に行われるシンポジウムについてご案内させていただきます．NII の蓮尾先生が総括の ERATO MMSD プロジェクトのシンポジウムです．特に自動運転を対象として活発で幅広い研究活動を行っているプロジェクトで，その中間成果報告となります．どうぞご参加をご検討ください．よろしくお願いいたします． =========================================================== ERATO 蓮尾メタ数理システムデザインプロジェクトシンポジウム高信頼自動運転システムのための先進的研究数理的理論から，AI 協働，ソフトウェアプラットフォームへ https://group-mmm.org/eratommsd/ja/vvav-symposium-201905/ 《開催のご案内》 =========================================================== 蓮尾一郎 ERATO MMSD プロジェクト研究総括国立情報学研究所システム設計数理国際研究センターセンター長　ERATO 蓮尾メタ数理システムデザインプロジェクト（ERATO MMSD）は，国立研究開発法人科学技術振興機構（JST）の戦略的創造研究推進事業 ERATO 傘下の研究プロジェクトの一つです．ERATO MMSD では，Society 5.0 の大きな柱となる物理情報システムの品質保証手法の学術的研究を推進しています．特に，物理情報システムの来るべき典型例の一つとして注目を集める自動運転システムを戦略的応用対象に設定し，その信頼性保証を支えるモデリング手法・形式検証手法・テスト手法，さらにこれらを包括する実用的な V&V 技術の研究開発に取り組んでいます．　今回のシンポジウムでは，産業界で研究開発に携わるみなさまを対象として，高信頼自動運転システムに向けた国内外の研究動向，ERATO MMSD で開発している V&V 技術，及び今後の本プロジェクトのビジョンと取り組みをご紹介いたします．　自動運転システムの信頼性という大きな挑戦に取り組む上では，ソフトウェア・制御・AI といった多様な学術分野の協働が欠かせません．ERATO MMSD では，このような学術分野融合の確固とした基礎となる数理的（メタ）理論を重視し，実用的 V&V 技術とともに研究を推進しています．よって今回のシンポジウムでは， o 「今日」すぐに使える技術・ツール， o 「明日」可能になる技術，さらに， o これらの技術の進展が描き出す「明後日」の未来像，この3つを見渡すような，学術プロジェクトならではのビジョンを御覧頂けると確信しております．　また今回のシンポジウムでは，カナダ Waterloo 大学で自動運転車開発プロジェクトAutonomooseを率いる Krzysztof Czarnecki 教授も講演を行います．ソフトウェア工学の立場から，特に信頼性・安全性に重点をおいて自動運転車を開発する Czarnecki 教授は，ERATO MMSD のメンバーでもあります．　本シンポジウムをきっかけとして，今後皆様と情報を共有させていただきながら，当該分野の振興に貢献を行っていく所存です．多くの皆様のご参加をお待ちしております． ----------------------- 開催概要 ------------------------- イベント名 ERATO 蓮尾メタ数理システムデザインプロジェクトシンポジウム：高信頼自動運転システムのための先進的研究数理的理論から，AI 協働，ソフトウェアプラットフォームへ日時（予定） 2019年5月21日（火）13:00〜19:00 （受付開始 12:30）会場（予定） TKP築地新富町カンファレンスセンター（東京都中央区）主催国立研究開発法人科学技術振興機構（JST）ERATO 蓮尾メタ数理システムデザインプロジェクト（ERATO MMSD）国立情報学研究所（NII）システム設計数理国際研究センター参加対象自動車産業および関連産業において，研究・開発・調査等に携わる方々参加方法シンポジウムウェブページの参加登録フォームから事前登録をお願い致します https://group-mmm.org/eratommsd/ja/vvav-symposium-201905/ 参加登録受付は 5/10まで，参加料は無料．受付用にお名刺を二枚ご持参頂けますようお願い申し上げます．定員に達した場合，ご参加いただけない旨のご連絡を差し上げる場合があります．ご了承ください．使用言語 Krzysztof Czarnecki 教授の発表は英語，その他の発表は日本語お問い合わせ先「ERATO MMSD シンポジウム」運営事務局 E-mail: hasuolab-secr(a)nii.ac.jp Tel: 03-6273-4886 受付時間 10:00〜17:30 （土・日・祝日を除く） ---------------------- プログラム（仮）----------------------- 12:30 受付開始 13:00〜13:25 ご来賓挨拶 13:25〜13:55 （仮題）「ERATO MMSDプロジェクト紹介：物理情報システム品質保証のための包括的学術研究」蓮尾一郎国立情報学研究所，ERATO MMSDプロジェクト研究総括 13:55〜14:00 休憩 14:00〜15:00 （仮題）「自動運転システム開発プロジェクト Autonomoose：高信頼自動運転システムへのソフトウェア工学的取り組み」 Krzysztof Czarnecki Waterloo大学，ERATO MMSD グループ２リーダー Autonomoose プロジェクトリーダー 15:00〜15:15 休憩 15:15〜16:00 （仮題）「高信頼自動運転システム実現にむけて：ソフトウェア工学・機械学習の視点からの技術俯瞰」石川冬樹国立情報学研究所，ERATO MMSD グループ３リーダー 16:00〜16:45 （仮題）「高信頼自動運転システム実現にむけて：ソフトウェア科学・形式手法・数理的基盤の視点からの技術俯瞰」蓮尾一郎国立情報学研究所，ERATO MMSD 研究総括 16:45〜17:00 休憩 17:00〜18:00 研究員・大学院生による技術ショウケース 18:00〜19:00 懇談会 ---------------------- その他 ----------------------- 本件連絡先「ERATO MMSD シンポジウム」運営事務局 E-mail: hasuolab-secr(a)nii.ac.jp Tel: 03-6273-4886 受付時間 10:00〜17:30 （土・日・祝日を除く） -- 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

論理学について議論するSlackグループ
by Yoriyuki Yamagata 18 Apr '19

18 Apr '19

皆様、産総研の山形です。倫理学（数学・計算機科学・哲学・言語学その他、論理に関わる話題全般）を議論するSlackグループを作成しました。下のリンクからどなたでも参加できます。皆様のご参加をお待ちしております。よろしくお願いいたします。 https://join.slack.com/t/logic-ja/shared_invite/enQtNjExNTIyNjEzMDEyLTMyNTU… -- Yoriyuki Yamagata

1 0

Talk by Gordon Plotkin on 1st April 2019 at Kyoto
by Masahito Hasegawa 26 Mar '19

26 Mar '19

皆様、来週の月曜（４月１日）、京都大学数理解析研究所で、プログラム意味論などの研究で著名なGordon Plotkinさん（Edinburgh大学）の講演があります。詳細は下記のとおりです。関心をお持ちの方のご来聴を歓迎します。どうぞよろしくお願いいたします。京都大学数理解析研究所長谷川真人 ========== Time: 14:00-15:00, 1st April 2019 (Mon.) Place: Room 110, Research Institute for Mathematical Sciences, Kyoto University 京都大学数理解析研究所（本館）１階１１０号室 http://www.kurims.kyoto-u.ac.jp/en/access-01.html Speaker: Gordon Plotkin (LFCS, University of Edinburgh) Title: One-and-a-half simple differentiable programming languages Abstract: Languages for learning pose interesting foundational challenges. We look at one case: the foundations of differentiable programming languages with a first-class differentiation operator. Graphical and linguistic facilities for differentiation have proved their worth over recent years for deep learning (deep learning makes use of gradient descent optimisation methods to choose weights in neural nets). Automatic differentiation, also known as algorithmic differentiation, goes much further back, at least to the early 1960s, and provides efficient techniques for differentiation, e.g., via source code transformation. It seems fair to say, however, that differentiable programming languages have begun to appear only recently. It seems further fair to say that, while there has certainly been some foundational study of differentiable programming languages, there is ample opportunity to do more. We investigate the semantics of a simple first-order functional programming language with reals, product types, and a first-class reverse-mode differentiation operator (reverse-mode differentiation generalises gradients). The semantics employs a standard concept of real analysis: smooth multivariate functions with open domain. It turns out that such partial functions fit well with programming constructs such as conditionals and recursion; indeed they form a complete partial order, and so standard fixed-point methods can be applied. We give an operational semantics which, roughly, can be seen as a formalisation of a version of the trace (or tape) method used to implement automatic differentiation. The semantics consists of three parts: ordinary evaluation, symbolic evaluation to eliminate control constructs, and a source-code transformation to symbolically differentiate terms with no control constructs, >From a programming language point of view, however, many types are lacking, particularly sum types and recursive types, such as lists. We conclude with a brief presentation of notions of shapely datatypes and smooth functions. These can be used to give the semantics of such types and the usual functions between them while retaining first-class differentiation. This work constitutes only an initial exploration, and we look forward to a rich field connecting two worlds: programming languages and their foundations, and real analysis and allied areas of mathematics. ==========

1 0

第40回量子情報技術研究会(QIT40)のご案内
by Yasuhito Kawano 22 Mar '19

22 Mar '19

皆様 NTT の河野と申します。本メーリングリストをお借りして、第40回量子情報技術研究会(QIT40)の会告案内を送らせていただきます。よろしくお願いいたします。 ----------------------------------------------------------------- 第40回量子情報技術研究会（QIT40）研究会の内容：　　情報科学と量子力学を融合させた新しい分野，量子情報科学に関する研究会です．　情報を担う物理系の量子力学的側面を積極的に活かした新しい情報処理原理の研究と　そこから開かれる新しい学問体系の構築および新しい情報技術パラダイムの創生を　目指して，情報科学，物理学，光エレクトロニクスを含む理学，工学，数理科学に　携わる研究者間に自由な討論の場を提供し，この研究分野の発展を図ることを目的と　しています．　　第40回研究会を下記のように開催いたします．現在この分野で活躍する研究者は勿論，　自分の研究資産が何らかの形で使えそうだと予感している研究者・技術者など，　広く関連する分野の研究者・技術者からの発表を募集致します．聴講のみの参加も　歓迎致しますので，奮ってお申し込みください．　　なお，第38回研究会から学生発表賞を創設いたしました．応募方法等については，　下記のQITウェブサイトをご確認下さい．日時: 2019年5月20日(月)〜21日(火) 会場: 九州大学筑紫キャンパス筑紫ホール (〒816-8580　福岡県春日市春日公園6-1) 発表募集分野 (申し込み状況によっては査読の可能性あり)：　量子情報，量子計算，量子暗号など広く量子情報技術に関わる理論的研究，実験的研究，　計算機科学的研究，数学的研究，および，その他関連分野．定員: 200名参加費：　一般4,000円，学生3,000円懇親会費：一般4,000円，学生2,000円 ※当日現地支払いの場合，参加費・懇親会費は上記に+1,000円が増額されます．　（参加事前登録または銀行振込が期限に間に合わない場合も，これに該当します．） ※学生限定・当日受付・予稿集なし・懇親会なしの参加費1,000円という選択肢もあります．　こちらは事前手続き不要です．研究会参加申込要領：　参加申込は下記 Web にて受付けます：　https://www.ieice.org/es/qit/ 　講演 (口頭，ポスター) の申込，予稿集原稿PDFの提出は，電子情報通信学会の　Webシステムを使用する予定．各種締切：【口頭講演申込締切】　　2019年4月19日（金）【ポスター講演申込締切】2019年4月19日（金）【予稿原稿提出締切】　　2019年4月19日（金）【参加申込締切】　　　　2019年4月24日（水）【問合せ先】　原田裕一 (九州大学) 　落合啓之（九州大学）　廣川真男（広島大学）　和久井健太郎（情報通信研究機構）　Email: qit40(a)gic.kyushu-u.ac.jp 主催: 量子情報技術特別研究専門委員会 (委員長: 平野琢也(学習院大学)) 共催: 応用物理学会量子エレクトロニクス研究会

1 0

2nd CFP: 3rd International Workshop on User-Oriented Logic Paradigms
by Christos Rodosthenous 19 Mar '19

19 Mar '19

*** IULP 2019 *** 3rd International Workshop on User-Oriented Logic Paradigms June 3 or 4, 2019 https://iulp2019.uni-leipzig.de Collocated with the 15th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR 2019) Philadelphia, USA June 4 - 6, 2019 -------------------------------------------- Since the emergence of logic reasoning paradigms, such as logic programming, argumentation, and other non-monotonic reasoning formalisms, a lot of theoretical work has been done, for example with respect to different semantics and their properties. More recently, implementations and IDEs emerged which have been used for various problem-solving applications. However, user-friendliness is still an issue for both experts and non-experts working with logic paradigms; for example experts benefit from features like debugging and heuristic tuning, non-experts from educational material, explanations, and intuitive visualisations - all of which are ongoing topics of research. The 3rd International Workshop of User-Oriented Logic Paradigms (IULP) focuses on discussing different aspects involved in making logic paradigms more user-friendly/oriented, where the "user" could be either an expert of the paradigm, or a non-expert who simply uses tools developed for the paradigm in some application. IULP aims to bring together researchers working on different logic paradigms, such as answer set programming, constraint logic programming, probabilistic logic programming, abductive logic programming, inductive logic programming, argumentation, principles of teaching etc., as user- friendliness is an important topic in all of these areas. IULP aims to provide an international forum for researchers in the AI, KR, and applied sciences community to discuss and present advances in theories, formalisms, and applications to deliver the mature and well-defined methods of logic paradigms to a wider audience. We solicit the submission of papers broadly centred on issues and research related to user-friendliness in logic paradigms and related fields. We welcome papers of either theoretical or practical nature, including work in progress. IMPORTANT DATES -------------------------------------------- * Submission deadline: Sun, March 31st 2019 * Notification to authors: Mon, April 29th 2019 * Camera-ready version due: Mon, May 20th 2019 * Workshop date: June 3 or 4, 2019 TOPICS -------------------------------------------- Topics of interest include (but are not limited to): * IDEs * debugging * explanations * visualisation * best practice * modularity * usage of natural language * heuristic tuning * LP education * language extensions * transparency * algorithmic bias * credibility * accountable systems SUBMISSIONS -------------------------------------------- Papers must be formatted in Springer LNCS style (http://www.springer.com/lncs) and should not exceed 13 pages (excluding references and appendices). All submissions have to be written in English and submitted electronically as a PDF through easychair (https://easychair.org/conferences/?conf=iulp2019). A short system demonstration version which should not exceed 6 pages (excluding references and appendices) can be submitted electronically too. We encourage the submission of original research on all topics as well as relevant results that have been submitted or accepted elsewhere provided that the initial publication is mentioned in a footnote on the first page. Note that authorship is not anonymous and that at least one author of each accepted paper is required to attend the workshop to present the contribution. PROCEEDINGS -------------------------------------------- There are no formal proceedings for IULP. The accepted papers will be published as a technical report and will be made available in the Computing Research Repository (CoRR). The copyright of the papers lies with the authors and, as far as IULP is concerned, authors are free to submit their work to other conferences and workshops. COMMITTEE -------------------------------------------- Chairs: * Stefan Ellmauthaler (Leipzig University) * Christos Rodosthenous (Open University of Cyprus) Program Committee * Bart Bogaerts (Vrije Universiteit Brussel) * Gerhard Brewka (Leipzig University) * Marina De Vos (University of Bath) * Marc Denecker (Katholieke Universiteit Leuven) * Martin Gebser (Potsdam University) * Antonis C. Kakas (University of Cyprus) * Antonio Lieto (University of Turin) * Loizos Michael (Open University of Cyprus) * Yisong Wang (Guizhou University) * Stefan Woltran (Vienna University of Technology) CONTACT -------------------------------------------- iulp2019 [at] informatik [dot] uni-leipzig [dot] de HOMEPAGE -------------------------------------------- https://iulp2019.uni-leipzig.de

1 0

Nagoya logic seminar
by 吉信康夫 14 Mar '19

14 Mar '19

皆様：名古屋大学の吉信です。以下の要領で名古屋ロジックセミナーを開催します。日時：3月19日(火) 15:30〜場所：名古屋大学大学院情報学研究科棟314室講演者：Sabrina Ouazzani(エコール・ポリテクニーク) タイトル：How to compute with an infinite time Turing machine? 概要：In this talk, we present infinite time Turing machines (ITTM), from the original definition of the model to some new infinite time algorithms. We will present algorithmic techniques that allow to highlight some properties of the ITTM-computable ordinals. In particular, we will study gaps in ordinal computation times, that is to say, ordinal times at which no infinite time program halts. We will explain some properties of the gaps in the ordinal computation times. 多数の方のご参加をお待ちしております。

1 0

[CFP] The Coq Workhsop 2019
by Jacques Garrigue 13 Mar '19

13 Mar '19

皆様、名古屋大学のGarrigueです。本メーリングリストをお借りして、 2019年9月にポートランド(オレゴン州)で開催される Coq Workshop 2019の CFPを送らせていただきます。ぜひ投稿をご検討ください。投稿〆切：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/

1 0

UNIF 2019: 2nd CFP
by Takahito Aoto 12 Mar '19

12 Mar '19

単一化に関するワークショップのご案内です．タイトル&アブストラクトの〆切が4/14，本文の〆切が4/21となっています． FSCDのサテライトワークショップとして6/24に開催です．ご投稿を検討頂ければ幸いです． --- 青戸等人(新潟大学) ------------------------------------------------------------------ Second Call for Papers: UNIF 2019 Website: http://www.mat.unb.br/unif2019 The 33rd International Workshop on Unification is the 33rd event in a series of international meetings devoted to unification theory and its applications. Unification is concerned with the problem of making two terms equal, finding solutions for equations, or making formulas equivalent. It is a fundamental process used in a number of fields of computer science, including automated reasoning, term rewriting, logic programming, natural language processing, program analysis, types, etc. Traditionally, the scope of the UNIF workshops has covered the topic of unification in a broad sense. Topics of interest to this forum include, but are not limited to: Unification algorithms, calculi, and implementations Equational unification and unification modulo theories Admissibility of Inference Rules Unification in modal, temporal and description logics Narrowing Formalisation of unification Matching Problems Applications Unification in Special Theories Higher-Order Unification Combination problems Constraint Solving Disunification Complexity Issues Type Checking and reconstruction The International Workshop on Unification (UNIF) is a yearly forum for researchers in unification theory and related fields to meet old and new colleagues, to present recent (even unfinished) work, and to discuss new ideas and trends. It is also a good opportunity for young researchers and scientists working in related areas to get an overview of the state of the art in unification theory. The workshop is proposed to be hosted by the 4th International Conference on Formal Structures for Computation and Deduction (FSCD, Dortmund, 24-29 June 2019). ** Invited Speakers Jörg Siekmann (DFKI and University of Saarland) Narciso Marti-Oliet (Universidad Complutense de Madrid) ** Submission Instructions Following the tradition of UNIF, we call for submissions of abstracts (5 pages) in EasyChair style, to be submitted electronically as PDF through the EasyChair submission site: https://easychair.org/conferences/?conf=unif2019 Abstracts will be evaluated by the Programme Committee (if necessary with support from external reviewers) regarding their significance for the workshop. We will allow work presented/submitted in/to another conference. Accepted abstracts will be presented at the workshop and included in the informal proceedings of the workshop, available in printed form at the workshop and in electronic form from the UNIF homepage: http://www.pps.jussieu.fr/~treinen/unif/ Based on the number and quality of submissions we will decide whether to organise a special journal issue. ** Important Dates Submission of titles and abstracts: April 14, 2019 Submission of full paper: April 21, 2019 Author notification: May 31, 2019 Camera-ready papers: June 4, 2019 UNIF 2019: June 24, 2019 (intended) ** Program Committee - Serdar Erbatur (LMU Munich) co-chair - Daniele Nantes Sobrinho (Universidade de Brasília) - co-chair - Takahito Aoto (Niigata University) - Alexander Baumgartner (University of Chile) - Mauricio Ayala Rincón (Universidade de Brasília) - Evelyne Contejean (LRI, CNRS, Univ Paris-Sud, Orsay) - Kimberly Cornell (The College of Saint Rose) - Santiago Escobar (Universitat Politècnica de València) - Maribel Fernández (King's College London) - Temur Kutsia (RISC- Johannes Kepler University Linz) - Jordy Levy (IIIA - CSIC) - Hai Lin (Shenyang Normal University) - Christopher Lynch (Clarkson University) - Andrew M. Marshall (University of Mary Washington) - Catherine Meadows (US Naval Research Laboratory) - Paliath Narendran (University at Albany--SUNY) - Christophe Ringeissen (INRIA) - David Sabel (Ludwig Maximilian University of Munich) - René Thiemann ( University of Innsbruck) - Manfred Schmidt-Schauss (Goethe-University Frankfurt am Main) - Ralf Treinen (IRIF- Université Paris-Diderot) - Daniel Lima Ventura (Universidade Federal de Goiás) ** Organizers Daniele Nantes Sobrinho (Universidade de Brasília) (dnantes(at)mat.unb.br) Serdar Erbatur (LMU Munich) (serdar.erbatur(at)ifi.lmu.de) ------------------------------------------------------------------

1 0

ENTROPY 2019: Second Call for Papers - Co-located with EuroS&P'19
by David Nowak 11 Mar '19

11 Mar '19

NEW: two more invited speakers ************************************************************************** Second Call for papers — ENTROPY 2019 ENabling TRust through Os Proofs … and beYond Second International workshop on the use of theorem provers for modelling and verification at the hardware-software interface https://entropy2019.sciencesconf.org Co-located with EuroS&P'19, KTH, Stockholm, June 2019 ************************************************************************** INVITED SPEAKERS Dominique Bolignano, Prove & Run Gernot Heiser, University of New South Wales Frank Piessens, KU Leuven Peter Sewell, University of Cambridge IMPORTANT DATES Paper submission: March 11 2019 Author notification: April 10, 2019 Camera-ready versions: April 22, 2019 (strict) Workshop: 16 June 2019 AIM AND SCOPE Low level software such as kernels and drivers, along with the hardware this software runs on, is critical for application security. In contrast with user applications, OS kernel software runs in privileged CPU mode and is thus highly critical. Large projects such as seL4, VeriSoft, CertiKoS and Prosper have invested considerable resources in developing formally verified systems such as hypervisors and microkernels, supplying proofs that they satisfy critical properties. Such proofs are delicate in terms of the scale and complexity of real systems, the models used in performing the proof search, and the relations between the two, which recent vulnerabilities such as Spectre and Meltdown have shown to be a highly non-trivial issue. The purpose of this workshop is to share, compare and disseminate best practices, tools and methodologies to verify OS kernels, also setting the stage for future steps in the direction of fully verified systems, dealing with issues related to modelling, model validation, and large proof maintenance through system evolution. On one hand, we need to make low-level proofs more scalable, modular and cost-effective. On the other hand, once certified systems are available, preservation and maintenance of their proofs of validity become key questions. The goal of the ENTROPY workshop is to provide a forum for researchers and practitioners in this space, linking operating systems, formal methods, and hardware architecture, interested in system design as well as machine verified mathematical proofs using proof assistants such as Coq, Isabelle and HOL4. This will be the second edition of the ENTROPY workshop series. The first workshop was organised by the Pip Development Team at University of Lille in 2018. TOPICS OF INTEREST Specific topics include, but are not limited to: * Verified kernels and hypervisors * Verified security architectures and models * Tools and frameworks for hardware security analysis * Tools and frameworks for security analysis * Formal hardware models and model validation techniques * Theorem prover based tools and frameworks for verification of low level code * Combinations of static analysis and theorem proving * Theories and techniques for compositional security analysis * Case studies and industrial experience reports * Proof maintenance techniques and problems * Compositional models and verification techniques * Proof oriented design The aim of the workshop is to stimulate innovation and active exchange of ideas, so position papers, work-in-progress and industrial experience submissions are welcome. SUBMISSION AND PUBLICATION There are two categories of submissions: 1. Regular papers describing fully developed work and complete results (10 pages, references included, IEEE format) 2. Short papers, position papers, industry experience reports, work-in-progress submissions (4 pages, references included, IEEE format) All papers should be in English and describe original work that has not been published or submitted elsewhere. The submission category should be clearly indicated. All submissions will be fully reviewed by members of the Programme Committee. Papers will appear in IEEE Xplore in a companion volume to the regular EuroS&P proceedings. For formatting and submission instructions see https://entropy2019.sciencesconf.org. PROGRAM CHAIRS Mads Dam, KTH Royal Institute of Technology David Nowak, CNRS and University of Lille PROGRAM COMMITTEE Christoph Baumann, Ericsson AB Gustavo Betarte, Univ. de la República, Uruguay David Cock, ETH Zurich Mads Dam, KTH Royal Institute of Technology (chair) Anthony Fox, ARM Deepak Garg, MPI Saarbrucken Ronghui Gu, Columbia University Samuel Hym, Univ. Lille Thomas Jensen, INRIA and Univ. Rennes Toby Murray, Univ. Melbourne David Nowak, CNRS & Univ. Lille (chair) Vicente Sanchez-Leighton, Orange Labs Thomas Sewell, Chalmers -- David Nowak http://www.cristal.univ-lille.fr/~nowakd/

1 1

LCC 2019（7月8日・パトラ）発表募集
by Akitoshi Kawamura 10 Mar '19

10 Mar '19

メーリングリストの皆様九大の河村と申します。7月に国際会議ICALPの併設集会としてギリシアのパトラで行われる「論理学と計算量」研究集会LCC 2019の御案内をお送りいたします。投稿は3～4ページで、締切は5月1日です。 =========================================================== First Call for Contributions LCC 2019 20th International Workshop on Logic and Computational Complexity July 8, 2019, Patras, Greece Collocated with ICALP 2019 http://www.cs.swansea.ac.uk/lcc/ =========================================================== LCC meetings are aimed at the foundational interconnections between logic and computational complexity, as present, for example, in implicit computational complexity (descriptive and type-theoretic methods); deductive formalisms as they relate to complexity (e.g. ramification, weak comprehension, bounded arithmetic, linear logic and resource logics); complexity aspects of finite model theory and databases; complexity-mindful program derivation and verification; computational complexity at higher type; and proof complexity. The program will consist of invited lectures as well as contributed talks selected by the Program Committee. IMPORTANT DATES: * submission May 1, 2019 * notification May 20, 2019 * workshop July 8, 2019 SUBMISSION: Submissions must be in English and in the form of an abstract of about 3-4 pages. All submissions should be submitted through Easychair at: https://easychair.org/conferences/?conf=lcc19 We also welcome submissions of abstracts based on work submitted or published elsewhere, provided that all pertinent information is disclosed at submission time. There will be no formal reviewing as is usually understood in peer-reviewed conferences with published proceedings. The program committee checks relevance and may provide additional feedback. PROGRAM COMMITTEE: Lauri Hella, Co-chair, Tampere University, Finland Monika Seisenberger, Co-chair, Swansea University, UK Sam Buss, University of California, San Diego, US Anupam Das, University of Copenhagen, Denmark Anuj, Dawar, University of Cambridge, UK Akitoshi Kawamura, Kyushu University, Fukuoka, Japan Arne, Meier, University of Hannover, Germany Lidia Tendera, University of Opole, Poland CONTACT: To contact the workshop organizers, please send an e-mail to lcc19(a)easychair.org -- 河村彰星九州大学システム情報科学研究院情報学部門〒819-0395　福岡市西区元岡744 092-802-3806 kawamura(a)inf.kyushu-u.ac.jp

1 0

Nagoya logic seminar
by 吉信康夫 05 Mar '19

05 Mar '19

皆様：名古屋大学の吉信です。先日ご案内いたしました名古屋ロジックセミナーについて、概要をいただきましたのであらためてお知らせいたします。日時：3月8日(金) 15:30〜場所：名古屋大学大学院情報学研究科棟314室講演者：渕野昌(神戸大学) タイトル：Reflection axioms which imply the continuum is very large 概要：Stationary logic の variations 対する，``妥当な'' Löwenheim-Skolem Theorem が成立するべきである，という前提のもとで，連続体の濃度は $\aleph_1$ あるいは $\aleph_2$ あるいは非常に大きなもの (weakly Mahlo, weakly hyper Mahlo 等) になるかのいずれかとなることを示す．この三分律に対応する３つの generic supercompactness axioms についても論ずる．多数の方のご参加をお待ちしております。

1 0

Re: [logic-ml] CSCAT 2019 開催案内
by Kensuke Kojima 04 Mar '19

04 Mar '19

皆様京都大学の小島です。申し込み締め切りが近づいてきましたので、 CSCAT 2019 のご案内を再送いたします。懇親会・講演申し込みの締め切りは22日（金）となっております。特に懇親会に参加を希望される方は早めにお申し込み下さい。講演につきましては枠が残っている限り22日を過ぎても受け付ける予定ですが、仮プログラム作成のため早めにお知らせいただけるとありがたいです。講演申し込み https://goo.gl/forms/DscPaYGBsIbUFDua2 懇親会申し込み https://goo.gl/forms/7cCq16mOxlV1GZ6o2 小島 2019年1月13日(日) 12:40 Kensuke Kojima <kozima(a)kuis.kyoto-u.ac.jp>: > > CSCAT メーリングリストの皆様、 > > 京都大学の小島です。 > 今年の CSCAT のお知らせです。 > > 日時： 2019年3月9日（土）〜3月10日（日） > 会場：東北大学理学部数理科学記念館（川井ホール） > URL：https://sites.google.com/view/cscat2019/home > 連絡先：cscat2019(a)grp.tohoku.ac.jp > > 今年は会場の手配を東北大学の赤間先生にお願いして、 > 講演の取りまとめを小島が行う形で開催することになりました。 > > 懇親会を3月9日の夜に行う予定です。予算は一人6000円程度の見込みです。 > > 講演・懇親会への参加を希望される方は2月22日までに、 > それぞれ以下の申し込みフォームへご記入下さい。 > （聴講のみで懇親会にも参加されない場合は申し込み不要です。） > > 講演申し込み https://goo.gl/forms/DscPaYGBsIbUFDua2 > 懇親会申し込み https://goo.gl/forms/7cCq16mOxlV1GZ6o2 > > 皆様の参加をお待ちしております。 > > 小島

1 1

seminar
by 吉信康夫 03 Mar '19

03 Mar '19

皆様名古屋大学の吉信です。以下の要領で名古屋ロジックセミナーを開催します。日時：3月8日(金) 15:30〜場所：名古屋大学大学院情報学研究科棟314室講演者：渕野昌(神戸大学) タイトル：Reflection axioms which imply the continuum is very large 多数の方のご参加をお待ちしております。

1 0

Summer School in Dynamic Epistemic Logic, Sapporo (Japan), 13-23 Aug 2019
by Katsuhiko Sano 25 Feb '19

25 Feb '19

Dear all, The Department of Philosophy at Hokkaido University (Sapporo, Japan) will hold a two-week summer school in dynamic epistemic logic and its applications, jointly with one guest lecturer, Hans van Ditmarsch, from LORIA in Nancy, between August 13 and August 23 as part of Hokkaido Summer Institute (HSI) 2019. The following two intensive courses are scheduled to be offered during the summer school. Course 1 (13/Aug/2019 - 17/Aug/2019): Introduction to Logic 2019 (For details, see https://hokkaidosummerinstitute.oia.hokudai.ac.jp/courses/CourseDetail=G096) Course 2 (19/Aug/2019 - 23/Aug/2019): Dynamic Epistemic Logic and its Applications 2019 (For details, see https://hokkaidosummerinstitute.oia.hokudai.ac.jp/courses/CourseDetail=G099) The main lecturer of Course 1 is Katsuhiko Sano (Department of Philosophy, Hokkaido University). The main lecturer of Course 2 is Hans van Ditmarsch (Lorraine Research Laboratory in Computer Science and its Applications, Centre national de la recherche scientifique, France). Tomoyuki Yamada (Hokkaido University) will also join the classes to help students follow the lectures, and communicate with the lecturers. The courses are intended for graduate students. Course 1 is meant for students without prior knowledge of logic and will prepare them for Course 2. Each course is designed to be independent from the other course. Those students who have some familiarity with basics of propositional logic, first-order logic, and modal logic can skip Course 1, and those who wish to take only Course 1 can learn basics of logic. There are several application periods for students from universities other than Hokkaido University: 1st application: ** from February 1 to February 28 2019.** 2nd application: ** from April 4 to 10 2019.** 3rd application: ** from April 26 to May 8 2019.** For more details about applications, please check the HSI official website: https://hokkaidosummerinstitute.oia.hokudai.ac.jp/applications/ As the summer in Sapporo is beautiful and pleasant, it's a good idea to learn logic this summer in Sapporo. Katsuhiko Sano Department of Philosophy Graduate School of Letters Hokkaido University

1 0

「圏論シンポジウム」開催のお知らせ; Symposium on the Categorical Unity of the Sciences
by Yoshihiro Maruyama 25 Feb '19

25 Feb '19

皆様、 Oxford大学のSamson Abramsky教授来日に際し、下記の通り圏論シンポジウムを開催いたします。登録不要ですので、お気軽にお立ち寄り下さい。 ------------------------------------------------------------------------------ 圏論シンポジウム Symposium on the Categorical Unity of the Sciences 3月22-23日、益川ホール、北部キャンパス、京都大学 22-23 March at Maskawa Hall, Kyoto University, Japan https://sites.google.com/view/categorical-unified-science/ 講演者 Speakers - Samson Abramsky (University of Oxford) - 久木田水生 (名古屋大学) - 谷村省吾 (名古屋大学) - 蓮尾一郎 (国立情報学研究所) - 春名太一 (東京女子大学) - 丸山善宏 (京都大学) - 三好博之 (京都産業大学) 事前登録/参加費不要。 No registration required. 問い合わせ先 Contact 丸山善宏（京都大学） maruyama(a)i.h.kyoto-u.ac.jp 旅費援助を希望される方は、上記までお早めにご連絡下さい。 (可能な数に限りはございます.) Limited travel funding is available; contact the organizer asap. ------------------------------------------------------------------------------ なおスケジュール詳細はウェブページの方にあります。どうぞよろしくお願い致します。丸山善宏（京都大学白眉センター）

1 0

CTFMのご案内
by 小俣安彦 22 Feb '19

22 Feb '19

皆様 CTFM主催者である彭寧寧氏(武漢理工大学)に代わり，下記のご案内をさせていただきます． Computability Theory and Foundations of Mathematics (CTFM) 昨年の明治大学での開催につづき，本年は標記国際会議が下記の日程で開催されます．日程：2019年 3月 21 日 (木) Registaration 　　　22日〜 25日 Lectures and Talks 　　　26-27日 Discussions and Excursions 場所：中国　武漢理工大学参加申し込みなどさらに詳しい情報は，次のウェブサイトをご覧ください． http://www.ctfm2019.com/index.html 講演申し込みはすでに締め切っておりますが，追加講演が認められる場合もございますので，何かご要望等がございましたら ctfm2019(a)gmail.com　までご相談ください．よろしくお願いします．田中一之（東北大学）小俣安彦（東北大学）

1 0

【参加募集(最終案内)】第21回プログラミングおよびプログラミング言語ワークショップ（PPL2019）
by Kazuyuki ASADA 19 Feb '19

19 Feb '19

PPLの皆様（重複ご容赦ください），東北大学の浅田です． 3月6日(水) 〜 8日(金)に，岩手県花巻市で開催される，第21回プログラミングおよびプログラミング言語ワークショップ (PPL2019) の参加登録の最終案内をいたします．参加登録の締切は明日2月20日(水)です．送迎バスアンケートの締切も同日です．締切までの参加費等のお支払いを忘れずにお願いいたします．会議のプログラムを公開いたしました： https://jssst-ppl.org/workshop/2019/program.html 多くの方々のご参加をお待ちしております． -------------------------------------------------------------------------- 第21回プログラミングおよびプログラミング言語ワークショップ（PPL2019） https://jssst-ppl.org/workshop/2019/ 参加登録のご案内主催: 日本ソフトウェア科学会プログラミング論研究会日程: 2019年3月6日(水) 〜 8日(金) 会場: 岩手県花巻市志戸平温泉「湯の杜ホテル志戸平」 PPL2019は，プログラミングとプログラミング言語に関連する幅広い分野の研究者・技術者・学生が一堂に会し，最新の研究成果の発表や，新たな研究課題の提案・討論・アイディア交換を行うことを目的とした，合宿形式の研究集会です．参加登録ならびに宿泊予約を日本旅行のウェブサービスにて受け付けております．参加費および参加登録方法については次のウェブページをご参照ください． https://jssst-ppl.org/workshop/2019/registration.html 参加登録締切：2019年2月20日(水) 問い合わせ先： ppl2019-oc(a)googlegroups.xn--com()-m53d8hra6b34cycyguk0hje6i3045cmp3h ppl2019-pc-chair(a)jssst-ppl.xn--org(/)-043e5ita1c46ctozdpfoc1401qpyjc ================================================================ ・プログラム委員会笹田耕一 (クックパッド)[プログラム共同委員長] 末永幸平 (京都大学)[プログラム共同委員長] 青谷知幸 (東京工業大学) 赤間陽二 (東北大学) 浅井健一 (お茶の水女子大学) 稲葉一浩 (Google) 鵜川始陽 (高知工科大学) 遠藤侑介 (クックパッド) Jacques Garrigue (名古屋大学) Oleg Kiselyov (東北大学) 酒井政裕 (PFN) 佐藤重幸 (東京大学) 関山太朗 (国立情報学研究所) 高野保真 (青山学院大学) 田中哲 (産業技術総合研究所) 千代英一郎 (成蹊大学) 千葉滋 (東京大学) 塚田武志 (東京大学) 照井一成 (京都大学) 中澤巧爾 (名古屋大) 林崎弘成 (Google) 平井洋一 (brainbot technologies AG) 堀江倫大 (日本IBM) 前田敦司 (筑波大学) 森畑明昌 (東京大学) 山田晃久 (国立情報学研究所) ・組織委員会浅田和之 (東北大学)[組織委員長] 平石拓 (京都大学)[組織副委員長] 木村大輔 (東邦大学)[財務担当] 森口草介 (関西学院大学)[財務副担当] 新屋良磨 (秋田大学)[会場担当] 安部達也 (千葉工業大学)[会場副担当] 佐藤亮介 (九州大学)[渉外担当] 笹田耕一 (クックパッド)[プログラム共同委員長] 末永幸平 (京都大学)[プログラム共同委員長] ================================================================

1 0

CADE-27: Second Call for Papers
by Nao Hirokawa 19 Feb '19

19 Feb '19

皆様来年８月にブラジル・ナタールで開催されます、自動演繹に関する国際会議 CADE の論文募集の案内をお送り致します。締切が少し延び、概要締切が20日、論文締切が 27 日 (AoE) となりました。是非、投稿をご検討下さい。廣川 (JAIST) --- The 27th International Conference on Automated Deduction (CADE-27) Natal, Brazil 25-30 August 2019 http://www.cade-27.info CALL FOR PAPERS CADE is the major international forum for presenting research on all aspects of automated deduction. High-quality submissions on the general topic of automated deduction, including foundations, applications, implementations, theoretical results, practical experiences and user studies are solicited. Key dates: Abstract deadline (extended): 20 February 2019 Submission deadline (extended): 27 February 2019 * Logics of interest include propositional, first-order, equational, higher-order, classical, description, modal, temporal, many-valued, constructive, other non-classical, meta-logics, logical frameworks, type theory, set theory, as well as any combination thereof. * Paradigms of interest include theorem proving, model building, constraint solving, computer algebra, model checking, proof checking, and their integration. * Methods of interest include resolution, superposition, completion, saturation, term rewriting, decision procedures, model elimination, connection methods, tableaux, sequent calculi, natural deduction, as well as their supporting algorithms and data structures, including matching, unification, orderings, induction, indexing techniques, proof presentation and explanation, proof planning. * Applications of interest include program analysis, verification and synthesis of software and hardware, formal methods, computational logic, computer mathematics, natural language processing, computational linguistics, knowledge representation, ontology reasoning, deductive databases, declarative programming, robotics, planning, and other areas of artificial intelligence. Submissions can be made in two categories: regular papers and system descriptions. The page limit in Springer LNCS style is 15 pages excluding references for regular papers and 10 pages excluding references for system descriptions. Submissions must be unpublished and not submitted for publication elsewhere. They will be judged on relevance, originality, significance, correctness, and readability. System descriptions must contain a link to a working system and will also be judged on usefulness and design. Proofs of theoretical results that do not fit in the page limit, executables of systems, and input data of experiments should be made available, via a reference to a website or in an appendix of the paper. For papers containing experimental evaluations, all data needed to rerun the experiments must be available. Reviewers will be encouraged to consider this additional material, but submissions must be self-contained within the respective page limit; considering the additional material should not be necessary to assess the merits of a submission. The review process will include a feedback/rebuttal period where authors will have the option to respond to reviewer comments. The PC chair may solicit further reviews after the rebuttal period. The proceedings of the conference will be published in the Springer LNCS/LNAI series. Formatting instructions and the LNCS style files can be obtained at http://www.springer.de/comp/lncs/authors.html At every CADE conference the Program Committee selects one of the accepted papers to receive the CADE Best Paper Award. The award recognizes a paper that the Program Committee collegially evaluates as the best in terms of originality and significance, having substantial confidence in its correctness. Overall technical quality, completeness, scholarly accuracy, and readability are also considered. Characteristics associated with a best paper include, for instance, introduction of a strong new technique or approach, solution of a long-standing open problem, introduction and solution of an interesting and important new problem, highly innovative application of known ideas or existing techniques, and presentation of a new system of outstanding power. Under exceptional circumstances, the Program Committee may give two awards (ex aequo) or give no award. IMPORTANT DATES Abstract deadline: 20 February 2019 Submission deadline: 27 February 2019 Rebuttal phase: 2 April 2019 Notification: 15 April 2019 Final version: 27 May 2019 SUBMISSION INSTRUCTIONS Papers should be submitted via https://easychair.org/conferences/?conf=cade27 CADE-27 ASSOCIATED EVENTS Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements (ARCADE), http://cl-informatik.uibk.ac.at/users/swinkler/arcade/ The CADE ATP System Competition, http://www.tptp.org/CASC/27/ Deduction Mentoring Workshop Logical and Semantic Frameworks, with Applications (LSFA), https://sites.google.com/view/lsfa2019 Proof eXchange for Theorem Proving (PxTP), http://pxtp.gforge.inria.fr/2019/ Theorem Prover Components for Educational Software (ThEdu'19), http://www.uc.pt/en/congressos/thedu/thedu19 The 6th Vampire Workshop CADE-27 ORGANIZERS Conference Chair: Elaine Pimentel Federal University of Rio Grande do Norte, Brazil Organizers: Carlos Olarte Federal University of Rio Grande do Norte, Brazil Joao Marcos Federal University of Rio Grande do Norte, Brazil Claudia Nalon University of Brasilia, Brazil Giselle Reis CMU, Qatar Program Committee Chair: Pascal Fontaine Universite de Lorraine, CNRS, Inria, LORIA, France Workshop, Tutorial, and Competition Chair: Giles Reger University of Manchester, UK Publicity Chair: Geoff Sutcliffe University of Miami, USA Program Committee: Carlos Areces, FaMAF - Universidad Nacional de Cordoba, Argentina Franz Baader, TU Dresden, Germany Clark Barrett, Stanford University, USA Jasmin Christian Blanchette, Vrije Universiteit Amsterdam, The Netherlands Maria Paola Bonacina, Universita degli Studi di Verona, Italy Leonardo Mendonca de Moura, Microsoft Research, USA Hans de Nivelle, Nazarbayev University, Astana, Kazakhstan Clare Dixon, University of Liverpool, UK Mnacho Echenim, Universite de Grenoble, France Marcelo Finger, University of Sao Paulo, Brazil Pascal Fontaine, Universite de Lorraine, CNRS, Inria, LORIA, France Silvio Ghilardi, Universita degli Studi di Milano, Italy Juergen Giesl, RWTH Aachen University, Germany Rajeev Gore, The Australian National University, Australia Stefan Hetzl, Technische Universitaet Wien, Austria Marijn J. H. Heule, The University of Texas at Austin, USA Nao Hirokawa, JAIST, Japan Moa Johansson, Chalmers University of Technology, Sweden Cezary Kaliszyk, University of Innsbruck, Austria Deepak Kapur, University of New Mexico, USA Benjamin Kiesl, Technische Universitaet Wien, Austria Konstantin Korovin, The University of Manchester, UK Laura Kovacs, Technische Universitaet Wien, Austria Ramana Kumar, DeepMind, UK Claudia Nalon, University of Brasilia, Brazil Vivek Nigam, Federal University of Paraiba & Fortiss, Brazil & Germany Carlos Olarte, Federal University of Rio Grande do Norte, Brazil Jens Otten, University of Oslo, Norway Andre Platzer, Carnegie Mellon University, USA Andrew Reynolds, The University of Iowa, USA Philipp Ruemmer, Uppsala University, Sweden Renate A. Schmidt, The University of Manchester, UK Stephan Schulz, DHBW Stuttgart, Germany Roberto Sebastiani, University of Trento, Italy Natarajan Shankar, SRI International, USA Viorica Sofronie-Stokkermans, Universitaet Koblenz-Landau, Germany Martin Suda, Czech Technical University, Czech Republic Geoff Sutcliffe, University of Miami, USA Rene Thiemann, University of Innsbruck, Austria Uwe Waldmann, Max Planck Institute for Informatics, Germany Christoph Weidenbach, Max Planck Institute for Informatics, Germany Sarah Winkler, University of Innsbruck, Austria

1 0

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Logic-ml