Logic-ml July 2019

logic-ml@fos.kuis.kyoto-u.ac.jp

9 participants
10 discussions

第54回MLG数理論理学研究集会
by Naosuke MATSUDA 29 Oct '19

29 Oct '19

第54回MLG数理論理学研究集会のご案内みなさま神奈川大学の松田です． MLG数理論理学研究集会は，1971年開始された，この分野の多くの研究者が参加している40年以上続く研究集会です．成果を発表し合ったり，アイデアを交換したりと，ザックバランな雰囲気で行われています．数学の他分野や，広く数理科学，情報科学，哲学の方々や，外国からの研究者を迎えるなど，オープンに運営されています．第54回MLG数理論理学研究集会は以下の要領で開催させていただきます．多くの皆様のご参加をお待ちしております． ==開催要領== 期間： 2019年12月14日 (土) ～ 16日 (月) 場所：マホロバ・マインズ三浦〒238-0101 神奈川県三浦市南下浦町上宮田 3231 0120-046-891 幹事：松田直祐（神奈川大学） matsuda.naosuke(a)gmail.com 詳細は以下のページをご確認ください． https://sites.google.com/view/mlg2019/home ==参加希望== 参加希望者でホテルでの宿泊を希望される方は， 11月14日までに下記の情報を松田までお送りください．件名を「MLG2019」などとしていただけると助かります． -- 氏名：所属：宿泊：7日・8日（不要なものを削除してください）夕食：7日・8日（不要なものを削除してください）朝食：8日・9日（不要なものを削除してください）講演希望：あり・なし（不要なものを削除してください）講演題目：その他： -- == Naosuke Matsuda, Department of Information Sciences. Kanagawa University Tsuchiya 2946 Hiratsuka-shi, Kanagawa 259-1293, Japan

1 2

セミナー案内
by KASHIMA Ryo 06 Sep '19

06 Sep '19

数理論理学セミナーのお知らせ東工大大岡山キャンパスで定期的に開催しているセミナー（普段はlogic-mlには流していません）の特別版を　　９月８日（金）と１５日（金）に開催します。以下に「話者（所属）題目」の一覧を載せました。どなたでも参加できますが、普段のセミナー案内を受け取っていない方の場合はご一報ください。 ----- 鹿島亮東京工業大学情報理工学院数理・計算科学系 kashima(a)is.titech.ac.jp ＝＝＝＝＝＝＝＝【８日（金）】西牟田祐樹（慶應大）一般化乗法的論理結合子のシーケント化定理とdecomposabilityについて藤原誠（早大）Bar induction and restricted classical logic 武原直紀（東工大）直観主義二階命題論理と論理式完備ハイティング代数について松田直祐（神奈川大）Curry's last problemへの弱い解答中村誠希（東工大）関係Kleene代数におけるatomic negationについて（仮題）新屋良磨（東大）論文紹介 Cyclic Arithmetic Is Equivalent to Peano Arithmetic 【１５日（金）】池上貴大（東工大）様相命題論理におけるツリーシークエント計算（仮題）河野友亮（東工大）Quantum logic の implication algebra と restricted negation について（仮題）鹿島亮（東工大）２階の関数記号を持つ１階述語論理について山﨑紗紀子（首都大）ゲーデル・マッキンゼイ・タルスキの定理の証明論的証明ー後件複数な直観主義論理のG3-style sequent calculus を用いてー大森仁（京大）Jaskowskiのdiscussive logicの周辺金沢誠（国立情報学研）Context-Free Languages with Finite Context and Kernel Properties 高橋正子 Grzegorczyk階層について＝＝＝＝以上＝＝＝＝

1 8

代数・論理・幾何と情報科学（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 29 Jul '19

29 Jul '19

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

1 0

JAIST Logic Seminar Series
by Tatsuji Kawai 26 Jul '19

26 Jul '19

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

1 0

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

25 Jul '19

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

1 0

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

18 Jul '19

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

1 0

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

14 Jul '19

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

1 0

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

12 Jul '19

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

1 0

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

08 Jul '19

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

1 0

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Logic-ml July 2019