Logic-ml September 2016

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

15 participants
22 discussions

特任研究員の募集
by koba＠kb.is.s.u-tokyo.ac.jp 16 Sep '16

16 Sep '16

東京大学の小林と申します．当研究室では現在，高階モデル検査（高階再帰スキームのモデル検査）とそのプログラム検証などへの応用をテーマとした研究を精力的に進めており，プロジェクトに携わる特任研究員若干名を探しております．身近にご興味のある方がいらっしゃいましたら，10月31日までに小林 (koba(a)is.s.u-tokyo.ac.jp) までメールでお知らせいただければ幸いです。その際、できれば略歴および論文リスト（フォーマット自由）もメールに添えるかまたは郵送でお送りください。（後日、さらに詳細な資料をお願いする可能性があります）．募集の条件は概ね以下のとおりです。 ================ 着任時期：2017年4月（数ヵ月の前後は応相談）任期：年度単位の更新で、業績により最長2020年3月まで延長可能給与：月額36～45万円　　（大学の規定および本人の実績による．細かい条件は応相談.）研究テーマ：高階モデル検査（高階再帰スキームのモデル検査）および、そのプログラム検証やデータ圧縮、知識発見などへの応用。高階モデル検査については，プロジェクトのページ　　　http://www-kb.is.s.u-tokyo.ac.jp/~koba/hmc/ および下の参考文献をご覧ください。　　本プロジェクトは科学研究費補助金基盤研究(S)：　　　課題名：高階モデル検査の深化と発展　　　研究代表者：小林直樹（東京大学）　　　研究分担者：五十嵐淳（京都大学）、篠原歩（東北大学）　　の支援をいただいており、その補助金で研究員を雇用する予定です。条件： - 着任時に博士号を取得していること - 理論計算機科学全般に明るいこと． - 以下の中の１つ以上のトピックに詳しくプログラミング能力が高いか、　　　２つ以上のトピックに詳しいことモデル検査（特にソフトウェアモデル検査）型システムプログラム意味論プログラム解析・検証・変換オートマトンと形式言語理論自動定理証明　　　　　計算量理論 (可逆)データ圧縮技術自然言語処理ゲノムデータ解析問い合わせ先：　　小林直樹　　東京大学大学院情報理工学系研究科コンピュータ科学専攻　　〒113-0033 東京都文京区本郷7-3-1 　　Phone, Fax: 03-5841-4124 　　email: koba(a)is.s.u-tokyo.ac.jp 参考文献： Naoki Kobayashi, "Model Checking Higher-Order Programs", Journal of the ACM, 60(3), 2013. Naoki Kobayashi, Ryosuke Sato, and Hiroshi Unno, "Predicate Abstraction and CEGAR for Higher-Order Model Checking", Proceedings of PLDI 2011, pp.222-233, 2011. Naoki Kobayashi, Kazutaka Matsuda, Ayumi Shinohara, Kazuya Yaguchi, "Functional Programs as Compressed Data", Higher-Order and Symbolic Computation, 2(1), pp.39-84, 2012. Naoki Kobayashi, "Higher-Order Model Checking: From Theory to Practice", Invited paper in Proceedings of LICS 2011. (A very brief survery of the field)

1 0

Talk by Quentin Heath, 29 Sept.
by koba＠kb.is.s.u-tokyo.ac.jp 16 Sep '16

16 Sep '16

皆様、東京大学の小林です。以下のとおり講演会を開催いたしますので、ご興味のある方はお集まりください。小林直樹東京大学大学院情報理工学系研究科コンピュータ科学専攻〒113-0033 東京都文京区本郷7-3-1 Phone: 03-5841-4124 Fax: 03-5841-4124 email: koba(a)is.s.u-tokyo.ac.jp ================== Time: 3:00pm, Thursday, the 29th September Place: Room 214, 7th Building of Faculty of Science （理学部7号館） Title: Proof certificates as proof theory for model checking Speaker: Quentin Heath (LIX, Ecole polytechnique) Abstract: Model checking has proved valuable on its own for locating errors in finite state computer models and specifications. However, model checkers can also be used to prove properties that will be consumed by other computational logic systems, such as theorem provers. In order for the model checker to be trusted by an external tool, we ask that it outputs its ``proof evidence'' as a formally defined document---a proof certificate---and that this document is checked by a trusted proof checker. We propose such a proof checker based on a first-order variant of linear logic, and justify why this logic is appealing as a foundation for model checking. We also provide a proof system for this logic, and tie in the notion of proof certificates in a way that makes proof checking sound for a minimal amount of work. As a result, a range of model checking computations can be imported in formal proofs and certified by a proof checker that is simple, non idiosyncratic, and easy to certify.

1 0

Nagoya Set Theory seminar
by 吉信康夫 15 Sep '16

15 Sep '16

名古屋集合論セミナーのご案内：(重複して受け取られた方はご容赦ください) 日時：2016年9月16日(金) 午後3時30分より場所：名古屋大学大学院情報科学研究科2階206号室講演者：薄葉季路(早稲田大学) 題目：Ground Axiomの変種について概要：Ground Axiomは「universeがforcing extensionになっていない」ことを主張する公理であるが、forcingをc.c.c., properなどに限定した Ground Axiomの編集について考察し、例えば「c.c.c. forcing extensionではないがproper forcing extensionになる」などのconsistencyを示す。多数のご参加をお待ちしております。名古屋大学大学院情報科学研究科吉信康夫

1 0

第19回プログラミングおよびプログラミング言語ワークショップ（PPL2017）論文募集/発表募集
by Isao Sasano 14 Sep '16

14 Sep '16

皆様第19回プログラミングおよびプログラミング言語ワークショップ（PPL2017）のご案内です。申込方法や詳細につきましては、webページにて確定次第お知らせします。是非ご投稿、ご参加をご検討ください。 ====================================================================== 第19回プログラミングおよびプログラミング言語ワークショップ (PPL2017) https://ppl2017.ipl-e.ai.kyutech.ac.jp/ 論文募集/発表募集主催: 日本ソフトウェア科学会プログラミング論研究会日程: 2017年3月8日(水)～3月10日(金) 会場: 山梨県笛吹市石和温泉「華やぎの章慶山」 PPL2017は，プログラミングとプログラミング言語に関連する幅広い分野の研究者・技術者・学生が一堂に会し，最新の研究成果の発表や，新たな研究課題の提案・討論・アイディア交換を行うことを目的とした，合宿形式の研究集会です．プログラミング方法論，プログラミング言語の理論・設計・実装などに関する研究発表を，カテゴリ別に幅広く募集します．カテゴリ1 (国内外未発表論文) ---------------------------- 完成した理論やシステムの研究発表のみならず，萌芽的なアイディアや問題点の提示等も歓迎します．発展途上の研究内容も積極的に採録する方針です．また，カテゴリ1で発表された研究については，会場での討議や査読コメントをもとにその完成度を高め，将来の学術雑誌・国際会議等での業績に結び付けることを奨励しています．そのため，予稿集の配布は参加者のみへの限定的なものとします．投稿手続きは2段階です．発表申込締切: 2016年12月21日(水) 17:00 (JST) 論文提出締切: 2017年1月11日(水) 17:00 (JST) 採否通知：2017年2月3日(金) カテゴリ2 (国外既発表論文) -------------------------- 査読付の国際会議または学術雑誌等で既発表であるが国内では未発表である研究を紹介する場です．採録決定済みの研究も含みます．PPLへの関連をもとに採否を判定いたしますが，申し込み多数の場合はプログラム委員会で選考致します．発表申込締切: 2017年1月25日(水) 17:00 (JST) 採否通知：2017年2月6日(月) カテゴリ3 (ポスター・デモ発表) ------------------------------ 2時間程度のセッション内でのポスター発表またはデモ発表です．既発表・未発表の別を問いません．PPLへの関連をもとに採否を判定いたしますが，申し込み多数の場合はプログラム委員会で選考致します．発表申込締切: 2017年2月8日(水) 17:00 (JST) 採否通知：2017年2月15日(水) カテゴリ4 (サーベイ・チュートリアル発表) ---------------------------------------- 研究動向の紹介(発表者の研究も含む) や分野間の相互理解と参加者の知識の底上げとなる発表を募集します．既発表・未発表の別を問いません．PPLへの関連，著者の研究発表実績，トピックや切り口の興味深さをもとに，プログラム委員会で選考致します．発表申込締切: 2017年1月25日(水) 17:00 (JST) 採否通知：2017年2月6日(月) 申込方法や詳細につきましては，上記ウェブページにて確定次第お知らせ致します． ====================================================================== 問い合わせ先 ppl2017-oc(a)ipl-e.ai.kyutech.ac.xn--jp()-753c9gpa1b92cqcsg7jrh5d1ix122cxi0h ppl2017-pc-chairs(a)ipl-e.ai.kyutech.ac.xn--jp(/)-m53d8hra6b05cmntd6e6b1719ok76b ====================================================================== プログラム委員会青谷知幸 (東京工業大学) 浅田和之 (東京大学) Reynald Affeldt (産業技術総合研究所) 稲葉一浩 (Google) 上野雄大 (東北大学) 菊池健太郎 (東北大学) 小宮常康 (電気通信大学) 篠埜功 (芝浦工業大学) 佐藤亮介 (東京大学) 首藤一幸 (東京工業大学) 末永幸平 (京都大学) 宋剛秀 (神戸大学) 千葉滋 (東京大学) 土屋達弘 (大阪大学) 中野圭介 (電気通信大学) 鍋島英知 (山梨大学) 番原睦則 (神戸大学) 前田敦司 (筑波大学) 松田一孝 (東北大学) 森畑明昌 (東京大学) 八杉昌宏 (九州工業大学) 組織委員会江本健斗 (九州工業大学) [組織委員長] 平石拓 (京都大学) 佐藤重幸 (高知工科大学) 海野広志 (筑波大学) 対馬かなえ (国立情報学研究所) 塚田武志 (東京大学) 篠埜功 (芝浦工業大学) [プログラム共同委員長] 番原睦則 (神戸大学) [プログラム共同委員長] ====================================================================== 篠埜　功 -- Isao Sasano <sasano(a)sic.shibaura-it.ac.jp>

1 0

第51回MLG数理論理学研究集会参加・講演募集（10/27-30箱根）
by Kazushige TERUI 13 Sep '16

13 Sep '16

第51回MLG数理論理学研究集会参加・講演募集 MLG数理論理学研究集会は，1971年開始された，この分野の多くの研究者が参加している40年以上続く研究集会です。成果を発表し合ったり，アイデアを交換したりと，ザックバランな雰囲気で行われています。数学の他分野や，広く数理科学，情報科学，哲学の方々や，外国からの研究者を迎えるなど，オープンに運営されています。（昨年度の様子：http://www.kurims.kyoto-u.ac.jp/~terui/mlg2015.html ）今回は試験的な試みとして「未解決問題セッション」を設けたいと思います（詳細はHP）。どうぞ奮ってご参加ください。日時：2016年10月27日（木）午後 − 30日（日）午前場所：四季の湯強羅静雲荘（ http://gora-seiunsou.jp/ ）参加費用：全参加の場合30,000円（3食つき、懇親会費は別途）参加・講演申し込み： 9月25日（日）までウェブページ：http://www.kurims.kyoto-u.ac.jp/~terui/mlg2016.html 詳細は上記Web Pageをご覧ください。みなさまの参加をお待ちしております。京都大学数理解析研究所照井　一成 ------------------------------------------ Kazushige TERUI Research Institute for Mathematical Sciences, Kyoto University. Kitashirakawa Oiwakecho, Sakyo-ku, Kyoto 606-8502, JAPAN. Phone: +81-75-753-7235 Fax: +81-75-753-7276 terui(a)kurims.kyoto-u.ac.jp http://www.kurims.kyoto-u.ac.jp/~terui/ ------------------------------------------ Kazushige TERUI Research Institute for Mathematical Sciences, Kyoto University. Kitashirakawa Oiwakecho, Sakyo-ku, Kyoto 606-8502, JAPAN. Phone: +81-75-753-7235 Fax: +81-75-753-7276 terui(a)kurims.kyoto-u.ac.jp http://www.kurims.kyoto-u.ac.jp/~terui/

1 0

第35回量子情報技術研究会(QIT35)のご案内
by NISHIMURA Harumichi 09 Sep '16

09 Sep '16

logic-mlの皆様 QIT35世話人に代わりまして第35回量子情報技術研究会(QIT35)の会告を以下の通り投稿させていただきます．どうぞよろしくお願いいたします．名古屋大学大学院情報科学研究科西村治道 --------------------------------------------------- 第35回量子情報技術研究会(QIT35)のお知らせ情報科学と量子力学を融合させた新しい分野、量子情報科学に関する研究会を下記のとおり開催いたします。ふるってご発表、ご参加ねがいます。 https://staff.aist.go.jp/s-kawabata/qit/qit35 ・日時：平成28年11月24日（木），25日（金）・会場：高エネルギー加速器研究機構（KEK）（〒305-0801 茨城県つくば市大穂1-1）・発表募集分野：量子情報，量子計算，量子暗号など広く量子情報技術に関わる理論的研究，実験的研究，計算機科学的研究，数学的研究，及びその他関連分野・申込締切： - 口頭講演：平成28年10月7日（金） - ポスター発表：平成28年10月21日（金） - 参加登録（事前）：平成28年10月28日（金）・招待講演： - 清水明（東大総合文化）「アンサンブルの等価性の量子破綻にともなう異常な量子状態」 - 長谷川祐司（ウィーン工科大・北大）「残留する確定性：混合状態でも有効な誤差と擾乱の不確定性関係」 - 横倉祐貴（理研）「ネーター不変量としての熱力学エントロピー」・チュートリアル講演 - 高柳匡（京大基研）「Emergent Spacetime from Qubits via Holography」・KEK加速器実験施設の見学ツアーも予定しています。・詳細については下記ウェブページをご覧ください： https://staff.aist.go.jp/s-kawabata/qit/qit35 ・参加費（事前振込）：一般2,500円，学生1,000円（当日払いは+1,000円）懇親会費（事前振込）：一般3,500円，学生2,000円（当日払いは+500円）・定員：200名程度・問合せ先：筒井泉（KEK）、磯暁（KEK）、鶴丸豊広（三菱電機） E-mail: qit35(a)ml.post.kek.jp ・主催：電子情報通信学会量子情報技術時限研究専門委員会共催：応用物理学会量子エレクトロニクス研究会 ---------------------------------------------------

1 0

JAIST Logic Seminar Series
by Hajime Ishihara 09 Sep '16

09 Sep '16

皆様ルートヴィヒ・マクシミリアン大学ミュンヘンのChuangjie Xu博士の講演のお知らせです。どうぞふるってご参加ください。問合せ先：石原　哉北陸先端科学技術大学院大学情報科学系 e-mail: ishihara(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 FP7 Marie Curie Actions IRSES project CORCON. (http://www.jaist.ac.jp/logic/ja/core2core, https://corcon.net/) Date: Wednesday 28 September, 2016, 15:20-17:00 Place: JAIST, Collaboration room 7 (I-56) (Access: http://www.jaist.ac.jp/english/location/access.html) Speaker: Chuangjie Xu (Ludwig-Maximilians-Universität München) Title: Continuity in Type Theory Abstract: If all functions (N -> N) -> N are continuous then 0 = 1. We establish this in intuitionistic type theory, with existence in the formulation of continuity expressed as a Sigma-type via the Curry-Howard interpretation. But with an intuitionistic notion of anonymous existence, defined as the propositional truncation of Sigma, it is consistent that all such functions are continuous. On the other hand, any of these two intuitionistic conceptions of existence give the same, consistent, notion of uniform continuity for functions (N -> 2) -> N. Moreover, we constructively develop a model of uniform continuity and implemented it within type theory using Agda.

1 0

Workshop 参加者募集のお知らせ
by Hideki Tsuiki 07 Sep '16

07 Sep '16

Workshop 参加者募集のお知らせ (再送) Second call for participation 日本学術振興会研究拠点形成事業「数理論理学とその応用に関するワークショップ」 JSPS Core-to-Core Program "Workshop on Mathematical Logic and its Application” http://www.i.h.kyoto-u.ac.jp/~matthew/core2core2016/index.html 2016 年 9月16,17日（金, 土曜日）京都大学、吉田南キャンパス、総合人間学部棟 1401 教室 September 16--17, 2016, Faculty of Integrated Human Studies Building, room 1401 Kyoto University 北陸先端科学技術大学院大学が内外の協力機関および協力者と実施しております日本学術振興会研究拠点形成事業「数理論理学とその応用の国際拠点形成」 (http://www.jaist.ac.jp/logic/core2core) の一環として、表記のワークショップを京都で開催いたします。本拠点形成事業参加研究者のためのワークショップですが、それ以外の方もご参加いただけます。プログラムなどの情報は、上記ホームページを御覧ください。両日とも、朝 9:00 から夕方 5:30 頃まで講演がある予定です。当日参加も可能ですが、本事業参加研究者以外で参加を予定されている方は、下記フォームにて、できるだけ事前にご連絡を頂けますようにお願い申し上げます。ご質問等がございましたら、core2core2016(a)jaist.ac.jp までお寄せください。多くの方のご参加をお待ちしております。オルガナイザー：石原哉立木秀樹照井一成 Matthew de Brecht 根元多佳子 --------------------------------------- 「数理論理学とその応用に関するワークショップ」に参加します。所属：名前：

1 0

CTFM2016(9/20-21, 早稲田大学)、CTFM Companion Lecture(9/23, 東京工業大学)のご案内
by Makoto Fujiwara 06 Sep '16

06 Sep '16

皆様 (English follows.) 早稲田大学の藤原誠です。 1. CTFM2016 先日ご案内させていた研究集会 Computability Theory and Foundations of Mathematics 2016 (2016年9月20日(火)～9月21日(水)、早稲田大学国際会議場) の暫定プログラムが以下のページからご覧いただけます。 (プログラムに変更があった場合は随時更新いたします。) http://www.sendailogic.com/CTFM2016/timetable.html 多くの方々にご参加いたたけることを期待しております。本研究集会への参加は自由となっておりますので、どうぞふるってご参加下さい。なお、20日夜の懇親会への参加を希望される方は9月12日までに以下より参加登録をお願いいたします。 http://www.sendailogic.com/CTFM2016/registration.html 詳しくは下記ホームページをご覧ください。 http://www.sendailogic.com/CTFM2016/ 本研究集会に関するお問い合わせは以下へお願いいたします。 ctfm2016[at]fastmail.com 2. CTFM Companion Lecture 9月23日に東京工業大学にてStephan G. Simpson先生(Vanderbilt University)の講演が行われますのでこちらも合わせてご案内させていただきます。詳しくは下記ホームページをご覧ください。 http://www.sendailogic.com/Titechworkshop/ どうぞよろしくお願いいたします。 ============================================================== Computability Theory and Foundations of Mathematics 2016 Waseda University, Tokyo, Japan, September 20 - 21, 2016 http://www.sendailogic.com/CTFM2016/ ============================================================== Computability Theory and Foundations of Mathematics (CTFM) aims to develop computability theory and logical foundations of Mathematics. The scope involves the topics Computability Theory, Reverse Mathematics, Nonstandard Analysis, Proof Theory, Set Theory, Philosophy of Mathematics, Constructive Mathematics, Theory of Randomness and Computational Complexity Theory. This is the sixth conference of the CTFM conference series: http://www.jaist.ac.jp/CTFM/CTFM_SERIES/ This conference is supported by the Waseda Insitute for Advanced Study and JSPS KAKENHI Grant Numbers JP26540001 and JP15H03634. ------------------------------------------------------------------------------------------------------------------------- Invited speakers: • David Belanger (National University of Singapore) • Chi Tat Chong (National University of Singapore) • Daisuke Ikegami (Tokyo Denki University) • Wei Li (National University of Singapore) • Kenshi Miyabe (Meiji University) • Paul Shafer (Ghent University) • Frank Stephan (National University of Singapore) • Philip Welch (University of Bristol) • Guohua Wu (Nanyang Technological University) • Takeshi Yamazaki (Tohoku University) • Yang Yue (National University of Singapore) ------------------------------------------------------------------------------------------------------------------------- Registration deadline: September 12, 2016. (It will still be possible to register for the conference after the deadline, but in that case the participant cannot attend the banquet. The banquet will be held on September 20 (18:30-20:30), at the same place as the conference venue.) ------------------------------------------------------------------------------------------------------------------------- Organising Committee: Makoto Fujiwara (Waseda University, co-chair) Florian Pelupessy (Tohoku University) Kazuyuki Tanaka (Tohoku University, co-chair) Toshimichi Usuba (Waseda University) Keita Yokoyama (JAIST) ------------------------------------------------------------------------------------------------------------------------ Participants are also invited to attend the Workshop on Mathematical Logic at the Tokyo Institute of Technology on September 23, which includes a CTFM companion lecture by Stephen G. Simpson: http://www.sendailogic.com/Titechworkshop/ ============================================ 藤原誠 (Makoto Fujiwara) 早稲田大学高等研究所 (Waseda Institute for Advanced Study, Waseda University) E-mail: makoto_fujiwara(a)aoni.waseda.jp ============================================

1 0

RIMS研究集会「無限組合せ論と強制法理論」のお知らせ
by Teruyuki YORIOKA 06 Sep '16

06 Sep '16

静岡大学の依岡です。今年度の公理的集合論のRIMS研究集会「無限組合せ論と強制法理論」が 11月28日（月）から12月1日（木）まで開催されます。みなさまのご参加をお待ちしております。講演申し込みの締め切りは10月7日です。 RIMS Set Theory Workshop 2016 http://www.ipc.shizuoka.ac.jp/~styorio/rims16/

1 0

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Logic-ml September 2016