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

JAIST Logic Seminar Series
by Hajime Ishihara 10 Jan '15

10 Jan '15

皆様スワンジー大学のAnton Setzer先生の講演のお知らせです。どうぞふるってご参加ください。問合せ先：石原　哉北陸先端科学技術大学院大学情報科学研究科 e-mail: ishihara(a)jaist.ac.jp ----------------------------------------------- * JAIST Logic Seminar Series * * This seminar is held as a part of the EU FP7 Marie Curie Actions IRSES projects COMPUTAL (http://computal.uni-trier.de/) and CORCON (http://corcon.net/). Date: Thursday 22 January, 2015, 15:10-16:40 Place: JAIST, Collaboration room 6 (I-57g) (Access: http://www.jaist.ac.jp/english/location/access.html) Speaker: Anton Setzer (Swansea University) Title: Extraction of programs from proofs using postulated axioms (joint work with Chi Ming Chuang) Abstract: In this talk we discuss how to extract programs from proofs with postulated axioms in dependent type theory. Since type theory has constructive logic, it is easy to determine for every $\Pi_2$-statement a function $f$ which determines the witness from the input. However, in the presence of postulated axioms, this function applied to an argument doesn't reduce necessarily to constructor head normal form, which means it doesn't produce a value. In this talk we discuss conditions which guarantee that the extracted function provide values in the presence of postulated axioms, and give a proof. This methodology will be applied to the extraction of alogrithms for exact real number computations. For this purpose the signed digit reals are introduced as a coalgebraic data type, and it is shown that the signed digit reals are closed under average, multiplication and rational numbers. Proofs have been carried out in the theorem prover Agda and the resulting programs can be executed effectively in this language.

1 0

Logic, religion and science
by Kensaku GOMI 08 Jan '15

08 Jan '15

Dear Sirs and Madams, Regarding conflicts among religions and between religion and science, and regarding the 1st World Congress on Logic and Religion http://www.uni-log.org/logic-and-religion.html, I would inform you of the paper entitled ``MATHEMATICAL THEOLOGY: A Proscience Concept of God with a Mathematical Model'' http://homepage3.nifty.com/gomiken/english/mathpsy.htm. I believe that it contributes to promoting harmony among religions and reconciling religion and science toward omniscience. Would you support it by forwarding this mail to your acquaintances who would be interested? With kind regards, The original sender: Kensaku Gomi, a retired professor of the Graduate School of Mathematical Sciences, University of Tokyo.

1 0

NLCS '15 Call for Papers
by Makoto Kanazawa 05 Jan '15

05 Jan '15

Third Workshop on Natural Language and Computer Science NLCS '15 July 5, 2015 Kyoto, Japan http://www.indiana.edu/~iulg/nlcs.html A workshop affiliated with 42nd International Colloquium on Automata, Languages and Programming (ICALP 2015) and 30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2015) Endorsed by the Association for Computational Linguistics Special Interest Group on Computational Semantics Paper submission deadline: April 2, 2015 AIMS AND SCOPE Formal tools coming from logic and category theory are important in both natural language semantics and in computational semantics. Moreover, work on these tools borrows heavily from all areas of theoretical computer science. In the other direction, applications having to do with natural language has inspired developments on the formal side. The workshop invites papers on both topics. Specific topics includes, but are not limited to: • logic for semantics of lexical items, sentences, discourse and dialog • continuations in natural language semantics • formal tools in textual inference, such as logics for natural language inference • applications of category theory in semantics • linear logic in semantics • formal approaches to unifying data-driven and declarative approaches to semantics INVITED SPEAKERS Makoto Kanazawa, National Institute of Informatics Gerard de Melo, Tsinghua University PROGRAM COMMITTEE • Heather Burnett, Université de Toulouse 2 • Robin Cooper, University of Gothenburg • Valeria de Paiva, Nuance Communications • Tim Fernando, Trinity College • Nissim Francez, The Technion • Makoto Kanazawa, National Institute of Informatics • Larry Moss, Indiana University • Aarne Ranta, University of Gothenburg • Christian Retoré, Université de Montpellier PAPER SUBMISSIONS Extended abstracts of up to 10 pages may be submitted through Easychair: https://easychair.org/conferences/?conf=nlcs15 ORGANIZERS Valeria de Paiva Nuance.com Email: Valeria.dePaiva at nuance .com Makoto Kanazawa National Institute of Informatics Email: kanazawa at nii.ac.jp Larry Moss Indiana University Email: lsm at cs.indiana . edu IMPORTANT DATES Paper submission deadline: April 2, 2015 Author notification: May 1, 2015 Electronic versions of papers due: May 14, 2015 Workshop: July 5, 2015

1 0

『第２回山陰基礎論・解析学研究集会』の御案内
by Horihata Yoshihiro 05 Jan '15

05 Jan '15

皆様米子高専の堀畑です．米子（鳥取県）にて下記要領で『第２回山陰基礎論・解析学研究集会』を開催いたします．分野を超えて，基礎論，関数解析，微分幾何，偏微分方程式の研究者が集まり，ざっくばらんに意見交換できる場にしたいと思っています．現在，発表１２件，参加者２０人前後となっています．講演をご希望される方は，少し詳しいアブストラクト（Texソース）と共に，１月１３日（火）までに堀畑までご連絡頂ければ幸いです．聴講のみご希望の方は１６日（金）頃までにご一報いただければ助かります．【日時】　１日目：１月２４日（土）１０時～１７時　２日目：１月２５日（日）１０時～１３時（時間については予定です．終了時間は発表件数によって変わる可能性があります）【場所】国際ファミリープラザ３Ｆ稲盛ホール（米子駅から徒歩１０分程）ＨＰ→ http://familyplaza.net/conference2 ※２３日（金）夜と２４日（土）夜に懇親会を行います．詳細は堀畑まで．会の詳細は下記ホームページで更新していきます： https://sites.google.com/site/yonagonctmath/slas2015 以上です．よろしくお願い申し上げます．堀畑佳宏 -- 米子工業高等専門学校教養教育科・数学〒683-8502 鳥取県米子市彦名町4448 E-mail: horihata(a)yonago-k.ac.jp

1 0

FW: UNILOG'2015 in Istanbul and 10th PLS in Samos Island
by Kensaku GOMI 05 Jan '15

05 Jan '15

From: jean-yves beziau [mailto:jyb.logician@gmail.com] Sent: Monday, January 5, 2015 3:44 AM To: Kensaku GOMI Forwarded to: Logic-ml Subject: UNILOG'2015 in Istanbul and 10th PLS in Samos Island Hope to see you at the 5th UNILOG - World Congress and School on Universal Logic to happen in Istanbul, June 20-30, 2015 http://www.uni-log.org/enter-istanbul As indicated in our website: The event is organized in combination with the 10th Panhellenic Logic Symposium that will happen June 11-15, 2015 in Samos Island, where Pythagoras was born. https://samosweb.aegean.gr/pls10/ A travel by bus from the nearby port of Kusadasi in Turkey up to Istanbul will be organized with stops on famous historical sites: Ephesus, Troy, etc. Special arrangements will exist for participants who wish to attend both conferences. I am sending you attached the posters for UNILOG'2015 and the related contest "The Future of Logic". I would be glad if you can print them (colour A3) and post them at your university /institute or if you prefer I can send them to you by post (then send me your exact mailing address) I wish you a happy new year 2015 Jean-Yves >----------------------------------------------------------------------> Jean-Yves Beziau Editor-in-Chief - Logica Universalis Latest Issue Scope of Logic Theorems - In Memoriam Adolf Lindenbaum http://link.springer.com/journal/11787/8/3/page/1

1 0

Logical Inference & Proof 学際会議（Jan 12-13th　Mita Campus Keio Univ）のお知らせ
by Mitsuhiro Okada 26 Dec '14

26 Dec '14

哲学、論理、計算、ソフトウエア科学基礎論、論理の認知・神経科学に関わるつぎのようなインフォーマルな会合を予定していますので、ご案内させていただきます。　慶應義塾大学哲学専攻　岡田光弘 “Logical Inference and Proofs”　Franco-Japanese Interdisciplinary Workshop　Jan 12-13^th 　“論理推論と証明”学際ワークショップ（１月１２日―１３日） (http://abelard.flet.keio.ac.jp/ilip2015/ ) 論理推論と証明に関する, 論理哲学、計算機科学、認知・神経科学などの学際的研究集会を案内させていただきます。(With Logic, Philosophy, Computer Science, Neuroscience, cognitive Science) 参加自由です。 (慶応大三田キャンパス、　Mita Campus, KeioUniversity) ―――――――――――――――――――――――――――――――― 日時：2015年1月1２日（月）13:00*〜18:00 / 1３日(火) 10:00*〜16:00 Date: January 12th (13:00-18:00) /13th (10:00-17:00), 201 東館6階G-Sec Lab () Place: G-Sec Lab, 6th Floor of East Research Building Mita campus of Keio University. http://www.keio.ac.jp/en/maps/mita.html (* 開始時間変更の可能性あり．プログラムは http://abelard.flet.keio.ac.jp/ilip2015/ でアップデートいたします。) ――――――――――――――――――――――――――― （ゲスト講演者リストやプログラム, abstracts情報はイベントページ http://ctj.keio.ac.jp/news/14 にアップデートされます．）参加方法：参加費無料。会場準備のため氏名、所属を明記して「Logical Inference集会参加希望」と件名を記したメールを事務局 logic(a)abelard.flet.keio.ac.jp 宛に1/10 までにお送りください。 (※12日セッション終了後のレセプションも参加自由です。) 主な講演者：フランス側主な講演者 Pierre Wagner ( University of Paris I and Institute of History and Philosophy of Science))　論理哲学 Jean-Baptiste Joinet（ University of Lyon III and Jean-Cavaiiles Institute, ENS-Paris ）論理哲学 Gilles Dowek (INRIA－Coq-Team Leader）タイプ理論・Coqシステム Jérôme Prado（University of Lyon I―CNRS　Language-Brain-Cognition Lab））推論の脳科学 Alberto Naibo (University of Paris I and Institute of History and Philosophy of Science)　証明と計算の論理 Discussantｓinclude Philippe Codognet （CNRS-Tokyo Joint Lab Director, and University of Paris VI）計算機科学日本側講演者 Shigeru Watanabe (Psychology, Keio University)　比較認知神経科学 Kazushige Terui (Mathematical Science Institute, Kyoto University)　情報論理学 Koji Mineshima (Center for Simulation Science, Ochanomizu University)　タイプ理論的言語学その他の日本側講演者は会合Web-siteでupdateします。 Tentative Program and tentative topics (See the conference website for further updated information.) １月１２日（月）１２th Jan. (Mon) １3；００PM　 Session on Proofs and Computation　 Baptiste-Joinet (Computatonal basis of semantics) Kazushige Terui (TBA) Pierre Wagner (Logical Pluralism) Gilles Dowek (Proof, type and Computation) Discussion (Discussion coordinator Phillipe Codognet Discussant Mitsuhiro Okada and others. To be announced. 18:30PM Reception １月１３日（火）13^th Jan. (Tue) 10:00AM Session on Logic and Types Alberto Naibo (Typed vs untyped proof theory) Koji Mineshima (Type theory and natural language) Discussion (Discussion coordinator, Mitsuhiro Okada) Discussants to be announced. 12:30AM-14:00PM Lunch Break 14:00pm Session on Logical Inference and Cognition Shigeru Watanabe (Comparative Cognitive-Neuroscientific Study of logical inference) Jerome Prado (Brain Imaging Study of Logical Inference) Yuri Sato (Cognitive Scientific Study of Logical Inference) Concluding Discussion (Discussion Coordinator Pierre Wagner) Discussants to be announced. 17:30PM Closing お問い合わせ先：慶應義塾大学「思考と行動判断」の研究拠点事務局（担当：高橋・小室） think-judge(a)abelard.flet.keio.ac.jp ―――――――――――――――――――――――――― 主催：慶應義塾大学「思考と行動判断」の研究拠点後援：慶應義塾大学論理と感性のグローバル研究センター後援：慶応義塾　「論理思考の次世代型研究と論理的思考力、発達支援への応用研究」プロジェクト後援：　新学術領域「予測と意思決定の論理と計算 ----------------------------------------------

1 0

42nd TRS Meeting - Final CFPart
by Naohi Eguchi 22 Dec '14

22 Dec '14

(Apologies for cross-posting) Final Call for Participation 42nd TRS Meeting February 7 - 9, 2015, Tokyo, Japan http://www.math.s.chiba-u.ac.jp/~neguchi/42trsmeeting/ The Term Rewriting Meeting (TRS Meeting) is a biannual informal workshop that aims at promoting the research on term rewriting and related areas. Every participant is highly encouraged to present recent works possibly in progress. It is perfectly acceptable to explain a paper written by someone else. Date: February 7th (Sat) – 9th (Mon), 2015 Venue: Harumi Grand Hotel 8-1, Harumi 3-chome, Chuo-ku, Tokyo 104-0053 Japan Lodging fees: 31812 yen (2 nights, non-smoking 2 persons' shared room) (breakfasts, banquet (Sat), lunch (Sun), dinner (Sun) included) Tentative Schedule: Meeting: Feb 7 (Sat) 14:00 - Feb 9 (Mon) 12:00 Banquet: Feb 7 (Sat) Registration: Deadline: January 5 (Mon), 2015 Please fill in the following registration form and send it to Naohi Eguchi (neguchi [at] g.math.s.chiba-u.ac.jp) by e-mail. (Items marked with * can be sent later) -------------------------------------------------------------------- Registration Form of the 42nd TRS Meeting name: affiliation: * title of talk: * approximate duration of talk (15 - 60 minutes): hotel reservation: (A)/(B) (A) Please accommodate me at Harumi Grand Hotel. February 7 (Sat): yes/no February 8 (Sun): yes/no additional request: (In case of partial accommodation) lunch (Sun): yes/no (B) I will attend without accommodation. February 7 (Sat): yes/no February 8 (Sun): yes/no February 9 (Mon): yes/no banquet (Sat): yes/no lunch (Sun): yes/no -------------------------------------------------------------------- In case of participation without accommodation: Registration fees: 2376 yen /day (for the use of meeting room) Banquet (Sat): 6000 yen Lunch (Sun): 1296 yen Further information can be found at the website of the meeting. 42nd TRS Meeting - Registration http://www.math.s.chiba-u.ac.jp/~neguchi/42trsmeeting/#registration

1 0

CFP: PPL2015 第17回プログラミングおよびプログラミング言語ワークショップ論文募集
by Makoto Hamana 15 Dec '14

15 Dec '14

皆様、群馬大学の浜名です．来年3月に愛媛県松山市道後温泉で開催される第17回プログラミングおよびプログラミング言語ワークショップのカテゴリ1 論文申込〆切まであと一週間ですので、最終のご案内です． * 新しく設けたカテゴリ4（サーベイ・チュートリアル発表）は発表は30分、申込みは簡単なアウトラインの提出のみで、新規の解説論文などは、なくてもよいものです。こちらの〆切は 1/23 でまだ先ですのでこちらもご検討ください。魅力的な招待講演もありますので、みなさまのご投稿、ご参加をお待ちしております。 -------------------------------------------------------------------------- 第17回プログラミングおよびプログラミング言語ワークショップ（PPL2015） http://www-kb.is.s.u-tokyo.ac.jp/ppl2015/ 論文募集主催: 日本ソフトウェア科学会プログラミング論研究会日程: 2015年3月4日(水)〜3月6日(金) 会場: 愛媛県松山市道後温泉「道後プリンスホテル」 http://www.dogoprince.co.jp/ PPL2015は、プログラミングおよびプログラミング言語に関する研究者が一堂に会し、最新の研究成果の発表、および新たな研究課題についての討論やアイディア交換等を行うことを目的とした、合宿形式のワークショップです．プログラミングおよびプログラミング言語の理論・設計・実装・処理系などに関する研究発表を、カテゴリ別に幅広く募集します．カテゴリ1: 国内外で未発表の論文の発表カテゴリ2: 国際会議・学術雑誌等で既発表であるが、国内では未発表の研究の紹介カテゴリ3: ポスター・デモ発表（既発表・未発表の別を問いません）カテゴリ4【新規】: サーベイ・チュートリアルの発表（既発表・未発表の別を問いません）カテゴリ1の採択論文の中から、特に独創的なアイディアや顕著な成果を含むものに対して論文賞を授与する予定です．また全論文発表と全ポスター・デモのなかから、聴衆の投票によりそれぞれ、最も優秀な論文プレゼンテーションには発表賞（一般の部、学生の部．既受賞者は除く）、最も優秀なポスター・デモにはポスター賞【新規】を授与する予定です．カテゴリ1（国内外未発表論文） ---------------------------- 完成した理論やシステムの研究発表のみならず、萌芽的なアイディアや問題点の提示等も歓迎します．発展途上の研究内容も積極的に採録する方針です（ただし、PPLでの発表として相応しくないと判断される場合は、この限りではありません）．また、カテゴリ1で発表された研究については、会場での討議や査読コメントをもとにその完成度を高め、将来の学術雑誌・会議等での業績に結び付けることを奨励しています．そのため、予稿集の配布は参加者のみへの限定的なものとする予定です．採録された論文は、PPL2015参加者に配布される予稿集に掲載され、参加者のみがアクセス可能な形でWeb上で公開されます（論文へのリンク集ページを作成し、閲覧に必要なパスワードを参加者に連絡します）．カテゴリ1で発表された研究のうち、PPL2015プログラム委員会により優れていると認めるものは、PPL2015終了後（2015年4月下旬予定）、「コンピュータソフトウェア」誌のPPL2015推薦論文としての投稿が可能です．推薦論文は、PPL プログラム委員が引き続き査読を行うことによる、迅速な査読プロセスを特長としています．カテゴリ2（国外既発表論文） -------------------------- 査読付の国際会議または学術雑誌等で既発表であるが国内では未発表である研究を紹介する場です．採録決定済みの研究も含みます．PPLへの関連をもとに採否を判定いたしますが、申し込み多数の場合はプログラム委員会での選考により、発表をご遠慮いただく可能性もございますので、その旨をご了承の上ご投稿ください．カテゴリ3（ポスター・デモ発表） ------------------------------ 2時間程度のセッション内でのポスター発表またはデモ発表です．既発表・未発表の別を問いません．PPLへの関連をもとに採録を判定いたします．また、申し込み多数の場合はプログラム委員会での選考により採否を決定します． ※ショートプレゼンテーションは行いませんカテゴリ4（サーベイ・チュートリアル発表）【新規】 ------------------------------------------------ サーベイはプログラミング言語に関連するトピックについての（発表者の研究も含め）研究動向を紹介する発表、チュートリアルはプログラミング言語に関連する基礎事項について解説する発表を募集します．既発表・未発表の別を問いません．プログラミング言語分野の学生、研究者に役立つような発表を想定しています．また、発表と同じ内容のサーベイ・解説論文の投稿も可能です (サーベイ、解説論文の投稿はオプショナルで必須ではありません)．本カテゴリは、分野間の相互理解と全体の底上げとなる事を期待し、新たに設置するものです．PPLへの関連および関連研究への言及をもとに採録を判定いたします．通常発表と同様の30分での発表を予定していますが、採択件数によっては発表者との相談で延長も考慮します．招待講演 -------- 橋本和幸 (NVIDIA. 元日本シンボリックス株式会社) 1980年代のLispマシンSymbolicsとその開発環境Genera 付属：NVIDIA GPUによる超並列コンピューティング Chung-Kil Hur (Seoul National University) Formal C semantics and LLVM compiler validation ====================================================================== 投稿・発表申込要領 4つのカテゴリそれぞれに対する投稿方法は以下の通りです．最新の情報は上記 Web ページでご確認ください．カテゴリ1（国内外未発表論文） ---------------------------- 投稿手続きは2段階です．発表申込を行った上で論文提出を行ってください．発表申込先： https://easychair.org/conferences/?conf=ppl2015 (EasyChairのアカウントが必要です) 発表申込締切：2014年12月22日(月) 17:00 (JST) 著者名、所属、論文タイトル、論文概要（日本語300〜400字程度もしくは英語 200 words 程度）を提出してください．論文提出締切：2015年1月8日(木) 17:00 (JST) 10ページ程度（最大15ページ）の論文（日本語もしくは英語、PDF形式）を提出してください．採否通知：2015年2月3日(火) 最終原稿提出締切：2015年2月16日(月) 17:00 (JST) 採録された論文の最終原稿の提出方法は、採否通知にてお知らせいたします． (注) カテゴリ1への投稿論文と類似の論文を、他の会議（予稿集を出版するもの）・論文誌などに同時投稿する場合は、査読の有無に関わらず、その旨を発表申込および論文提出の際に明記してください．PPLでは同時投稿の事実のみをもって論文を不採録とすることはありませんが、採否の決定に利用する場合があります（他の会議との重複を避けるため、発表内容についての条件付採録とすることもあります）．カテゴリ2（国外既発表論文） -------------------------- 発表申込時に採録が決定している国際会議および国際学術雑誌の発表論文が対象です．理論系だけではなく実装系の論文の投稿も歓迎いたします．発表申込先： ppl2015-submit [at] kb.is.s.u-tokyo.ac.jp ([at]を@に置き換えてください) 発表申込締切：2015年1月23日(金) 17:00 (JST) 原論文（ページ数不問、PDF形式）とabstract（テキスト形式）を、著者名、所属、論文タイトル、原論文の出典（発表会議名、掲載済／予定の別等）と併せてご提出ください．採否通知：2015年2月5日(木) カテゴリ3（ポスター・デモ発表） ------------------------------------------ ポスター・デモの区別を行わずに募集いたします．デモを行う場合は、発表概要においてその旨をご説明ください．発表申込先：https://easychair.org/conferences/?conf=ppl2015poster (EasyChairのアカウントが必要です) 発表申込締切：2015年2月6日(金) 17:00 (JST) 希望する発表形態（ポスター・デモの別）を明記して、著者名、所属、発表タイトル、発表概要（200〜300字程度）を abstract の部分に記入してご提出ください．論文提出のPDFファイルアップロード部分は無視してください．採否通知：2015年2月13日(金) カテゴリ4（サーベイ・チュートリアルの発表） ------------------------------------------ サーベイまたはチュートリアルの提案を募集いたします．発表申込み時に概要の提出を行ってください．概要の内容、PPLへの関連および関連研究への言及をもとに採録を判定いたします．発表申込先： ppl2015-submit [at] kb.is.s.u-tokyo.ac.jp ([at]を@に置き換えてください) 発表申込締切：2015年1月23日(金) 17:00 (JST) 著者名、所属、発表タイトル、発表の概要 (1〜3ページ、PDF形式．目的、カバーする話題、想定する聴衆、必要な知識の記述を含むもの)をご提出ください．新規にサーベイ論文・解説論文をご執筆される場合には、その原稿（ページ数不問・PDF形式）も併せてご提出ください．もし今回と同じ内容の既発表のサーベイ、チュートリアル、解説等があれば、その文書（ページ数不問、 PDF形式）、著者名、所属、タイトル、文書の出典（発表雑誌、掲載済／予定の別等）も併せてご提出ください．採否通知：2015年2月5日(木) 問い合わせ先：ppl2015-oc [at] kb.is.s.u-tokyo.ac.jp （[at]を@に置き換えてください） ====================================================================== プログラム委員会青戸等人東北大学浅田和之東京大学岩崎英哉電気通信大学鵜川始陽高知工科大学馬谷誠二京都大学 [プログラム共同委員長] 大岩寛産業技術総合研究所亀山幸義筑波大学河内谷清久仁日本IBM 久野靖筑波大学木村大輔国立情報学研究所宋剛秀神戸大学塚田武志 University of Oxford 中田景子 Tallinn University of Technology 浜名誠群馬大学 [プログラム共同委員長] 平井洋一 FireEye 平石拓京都大学藤田憲悦群馬大学星野直彦京都大学増原英彦東京工業大学渡部卓雄東京工業大学組織委員会松田一孝東京大学 [組織委員長] 浜名誠群馬大学 [プログラム共同委員長] 馬谷誠二京都大学 [プログラム共同委員長] 末永幸平京都大学上野雄大東北大学海野広志筑波大学木村大輔国立情報学研究所 [ポスターセッション幹事] --------------------------------------------------------------------------

1 0

クリスマス・ワークショップ「証明論・計算論とその周辺」
by Kazushige TERUI 14 Dec '14

14 Dec '14

みなさま下記の通り研究集会を開催します。クリスマス期間中ではありますが、よろしければぜひご参加ください。・RIMS研究集会「証明論・計算論とその周辺」　http://www.kurims.kyoto-u.ac.jp/~terui/proof2014.html ・日時：2014年12月24日（水）13:20 − 26日（金）15:40 ・場所：京都大学数理解析研究所１１１号室　（交通アクセス：http://www.kurims.kyoto-u.ac.jp/ja/access-01.html）・プログラム：http://www.kurims.kyoto-u.ac.jp/~terui/program2014.pdf ・懇親会：12月25日18時より「くれしま」にて。会費4,000円。　http://r.gnavi.co.jp/bvfb2hsb0000/ ・懇親会参加希望の方は12月18日（木）までにご連絡ください。 ------------------------------------------ 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

WoLLIC 2015 - Second Call for Papers
by 小野寛晰 10 Dec '14

10 Dec '14

[Please circulate. Apologies for cross-postings.] WoLLIC 2015 22nd Workshop on Logic, Language, Information and Computation July 20th-23rd, 2015 Bloomington, IN, USA SCIENTIFIC SPONSORSHIP Interest Group in Pure and Applied Logics (IGPL) The Association for Logic, Language and Information (FoLLI) Association for Symbolic Logic (ASL) European Association for Theoretical Computer Science (EATCS) European Association for Computer Science Logic (EACSL) Sociedade Brasileira de Computação (SBC) Sociedade Brasileira de Lógica (SBL) ORGANISATION Department of Computer Science, Indiana University, USA Program in Pure and Applied Logic, Indiana University, USA Centro de Informática, Universidade Federal de Pernambuco, Brazil HOSTED BY Department of Computer Science, Indiana University, USA CALL FOR PAPERS WoLLIC is an annual international forum on inter-disciplinary research involving formal logic, computing and programming theory, and natural language and reasoning. Each meeting includes invited talks and tutorials as well as contributed papers. The twenty-second WoLLIC will be held at the Department of Computer Science Indiana University, from July 20th to 23rd, 2015. It is sponsored by the Association for Symbolic Logic (ASL), the Interest Group in Pure and Applied Logics (IGPL), the The Association for Logic, Language and Information (FoLLI), the European Association for Theoretical Computer Science (EATCS), the European Association for Computer Science Logic (EACSL), the Sociedade Brasileira de Computação (SBC), and the Sociedade Brasileira de Lógica (SBL). PAPER SUBMISSION Contributions are invited on all pertinent subjects, with particular interest in cross-disciplinary topics. Typical but not exclusive areas of interest are: foundations of computing and programming; novel computation models and paradigms; broad notions of proof and belief; proof mining, type theory, effective learnability; formal methods in software and hardware development; logical approach to natural language and reasoning; logics of programs, actions and resources; foundational aspects of information organization, search, flow, sharing, and protection; foundations of mathematics; philosophical logic. Proposed contributions should be in English, and consist of a scholarly exposition accessible to the non-specialist, including motivation, background, and comparison with related works. They must not exceed 10 pages (in font 10 or higher), with up to 5 additional pages for references and technical appendices. The paper's main results must not be published or submitted for publication in refereed venues, including journals and other scientific meetings. It is expected that each accepted paper be presented at the meeting by one of its authors. Papers must be submitted electronically at the WoLLIC 2015 EasyChair website. (Please go to http://wollic.org/wollic2015/instructions.html <http://wollic.org/wollic2015/instructions.html> for instructions.) A title and single-paragraph abstract should be submitted by Feb 8, 2015, and the full paper by Feb 15, 2015 (firm date). Notifications are expected by Mar 22, 2015, and final papers for the proceedings will be due by Apr 5, 2015 (firm date). PROCEEDINGS The proceedings of WoLLIC 2015, including both invited and contributed papers, will be published in advance of the meeting as a volume in Springer's LNCS series. In addition, abstracts will be published in the Conference Report section of the Logic Journal of the IGPL, and selected contributions will be published as a special post-conference WoLLIC 2015 issue of Mathematical Structures in Computer Science, CUP (to be confirmed). INVITED SPEAKERS Adriana Compagnoni (Stevens Institute, USA) John Harrison (Intel, USA) Peter Jipsen (Chapman U, USA) Andre Joyal (U du Québec à Montreal, Canada) Chung-chieh Shan (Indiana U, USA) Alexandra Silva (Radboud U Nijmegen, The Netherlands) Mehrnoosh Sadrzadeh (Queen Mary, UK) STUDENT GRANTS ASL sponsorship of WoLLIC 2015 will permit ASL student members to apply for a modest travel grant (deadline: May 1st, 2015). See http://www.aslonline.org/studenttravelawards.html <http://www.aslonline.org/studenttravelawards.html> for details. IMPORTANT DATES Feb 8, 2015: Paper title and abstract deadline Feb 15, 2015: Full paper deadline Mar 22, 2015: Author notification Apr 5, 2015: Final version deadline (firm) PROGRAMME COMMITTEE Juliana Küster Filipe Bowles <https://risweb.st-andrews.ac.uk/portal/da/persons/juliana-kuster-filipe-bow…> (U St Andrews, Scotland) Guillaume Brunerie <http://www.eleves.ens.fr/home/brunerie/> (ENS Ulm, France) (TBC) Ann Copestake <http://www.cl.cam.ac.uk/~aac10/> (U Cambridge, UK) (TBC) Robin Cooper <http://www.ling.gu.se/~cooper/> (U Gothenburg, Sweden) Nikos Galatos <http://web.cs.du.edu/~ngalatos/>(U Denver, USA) Achim Jung <http://www.cs.bham.ac.uk/~axj/> (U Birmingham, UK) Sara <http://www2.warwick.ac.uk/fac/sci/dcs/people/sara_kalvala/> Kalvala <http://www2.warwick.ac.uk/fac/sci/dcs/people/sara_kalvala/> (U Warwick, UK) Elham Kashefi <http://www.inf.ed.ac.uk/people/staff/Elham_Kashefi.html> (Edinburgh U, Scotland) Peter Lefanu Lumsdaine <http://www.math.ias.edu/~plumsdaine/> (Institute for Advanced Study, USA) Ian Mackie <http://www.ianmackie.com/> (U Sussex, UK) Gerard de Melo <http://gerard.demelo.org/> (Tsinghua University, China) Vivek Nigam <http://www.nigam.info/> (Federal U of Paraíba, Brazil) Valeria de Paiva <http://www.cs.bham.ac.uk/~vdp/> (Nuance Comm, USA) (CHAIR) Luiz Carlos <http://buscatextual.cnpq.br/buscatextual/visualizacv.do?id=K4783548E2> Pereira <http://buscatextual.cnpq.br/buscatextual/visualizacv.do?id=K4783548E2> (PUC-Rio, Brazil) Elaine Pimentel <https://sites.google.com/site/elainepimentel/> (Federal U of Rio Grande do Norte, Brazil) Alexandra Silva <http://alexandrasilva.org/> (Radboud Nijmegen U, The Netherlands) Carolyn Talcott <http://www.sri.com/about/people/carolyn-talcott> (SRI International, USA) Josef Urban <http://cs.ru.nl/~urban/> (Radboud Nijmegen U, The Netherlands) Laure Vieu <http://www.irit.fr/~Laure.Vieu/> (IRIT-Toulouse, France) (TBC) Renata Wasserman <http://www.ime.usp.br/~renata/> (U São Paulo, Brazil) Anna Zamansky <http://mailng.hevra.haifa.ac.il/~annazam/> (U Haifa, Israel) STEERING COMMITTEE Samson Abramksy, Johan van Benthem, Anuj Dawar, Joe Halpern, Wilfrid Hodges, Ulrich Kohlenbach, Daniel Leivant, Leonid Libkin, Angus Macintyre, Luke Ong, Hiroakira Ono, Ruy de Queiroz. ORGANISING COMMITTEE Daniel Leivant (Indiana U) (Local co-chair) Larry Moss (Indiana U) (Local co-chair) Anjolina G. de Oliveira (U Fed Pernambuco) Ruy de Queiroz (U Fed Pernambuco) (co-chair) FURTHER INFORMATION Contact one of the Co-Chairs of the Organising Committee. WEB PAGE http://wollic.org/wollic2015/ <http://wollic.org/wollic2015/>

1 0

CFP: PPL2015 第17回プログラミングおよびプログラミング言語ワークショップ論文募集
by Makoto Hamana 09 Dec '14

09 Dec '14

皆様、群馬大学の浜名です．来年3月に愛媛県松山市道後温泉で開催される第17回プログラミングおよびプログラミング言語ワークショップご案内(2回目)です．論文申込〆切が近くなってきました。 * カテゴリ1への発表申込(タイトルと概要のみ)の締切は今年 12/22、論文の締切は1/8です。 * 新しく設けたカテゴリ4（サーベイ・チュートリアル発表）は発表は30分、申込みは簡単なアウトラインの提出のみで、新規の解説論文などは、なくてもよいものです。こちらの締切は 1/23 でまだ先ですのでこちらもご検討ください。また、魅力的な招待講演者も決定しました(詳細以下)。ぜひみなさまのご投稿、ご参加をお待ちしております。 -------------------------------------------------------------------------- 第17回プログラミングおよびプログラミング言語ワークショップ（PPL2015） http://www-kb.is.s.u-tokyo.ac.jp/ppl2015/ 論文募集主催: 日本ソフトウェア科学会プログラミング論研究会日程: 2015年3月4日(水)〜3月6日(金) 会場: 愛媛県松山市道後温泉「道後プリンスホテル」 http://www.dogoprince.co.jp/ PPL2015は、プログラミングおよびプログラミング言語に関する研究者が一堂に会し、最新の研究成果の発表、および新たな研究課題についての討論やアイディア交換等を行うことを目的とした、合宿形式のワークショップです．プログラミングおよびプログラミング言語の理論・設計・実装・処理系などに関する研究発表を、カテゴリ別に幅広く募集します．カテゴリ1: 国内外で未発表の論文の発表カテゴリ2: 国際会議・学術雑誌等で既発表であるが、国内では未発表の研究の紹介カテゴリ3: ポスター・デモ発表（既発表・未発表の別を問いません）カテゴリ4【新規】: サーベイ・チュートリアルの発表（既発表・未発表の別を問いません）カテゴリ1の採択論文の中から、特に独創的なアイディアや顕著な成果を含むものに対して論文賞を授与する予定です．また全論文発表と全ポスター・デモのなかから、聴衆の投票によりそれぞれ、最も優秀な論文プレゼンテーションには発表賞（一般の部、学生の部．既受賞者は除く）、最も優秀なポスター・デモにはポスター賞【新規】を授与する予定です．カテゴリ1（国内外未発表論文） ---------------------------- 完成した理論やシステムの研究発表のみならず、萌芽的なアイディアや問題点の提示等も歓迎します．発展途上の研究内容も積極的に採録する方針です（ただし、PPLでの発表として相応しくないと判断される場合は、この限りではありません）．また、カテゴリ1で発表された研究については、会場での討議や査読コメントをもとにその完成度を高め、将来の学術雑誌・会議等での業績に結び付けることを奨励しています．そのため、予稿集の配布は参加者のみへの限定的なものとする予定です．採録された論文は、PPL2015参加者に配布される予稿集に掲載され、参加者のみがアクセス可能な形でWeb上で公開されます（論文へのリンク集ページを作成し、閲覧に必要なパスワードを参加者に連絡します）．カテゴリ1で発表された研究のうち、PPL2015プログラム委員会により優れていると認めるものは、PPL2015終了後（2015年4月下旬予定）、「コンピュータソフトウェア」誌のPPL2015推薦論文としての投稿が可能です．推薦論文は、PPL プログラム委員が引き続き査読を行うことによる、迅速な査読プロセスを特長としています．カテゴリ2（国外既発表論文） -------------------------- 査読付の国際会議または学術雑誌等で既発表であるが国内では未発表である研究を紹介する場です．採録決定済みの研究も含みます．PPLへの関連をもとに採否を判定いたしますが、申し込み多数の場合はプログラム委員会での選考により、発表をご遠慮いただく可能性もございますので、その旨をご了承の上ご投稿ください．カテゴリ3（ポスター・デモ発表） ------------------------------ 2時間程度のセッション内でのポスター発表またはデモ発表です．既発表・未発表の別を問いません．PPLへの関連をもとに採録を判定いたします．また、申し込み多数の場合はプログラム委員会での選考により採否を決定します． ※ショートプレゼンテーションは行いませんカテゴリ4（サーベイ・チュートリアル発表）【新規】 ------------------------------------------------ サーベイはプログラミング言語に関連するトピックについての（発表者の研究も含め）研究動向を紹介する発表、チュートリアルはプログラミング言語に関連する基礎事項について解説する発表を募集します．既発表・未発表の別を問いません．プログラミング言語分野の学生、研究者に役立つような発表を想定しています．また、発表と同じ内容のサーベイ・解説論文の投稿も可能です (サーベイ、解説論文の投稿はオプショナルで必須ではありません)．本カテゴリは、分野間の相互理解と全体の底上げとなる事を期待し、新たに設置するものです．PPLへの関連および関連研究への言及をもとに採録を判定いたします．通常発表と同様の30分での発表を予定していますが、採択件数によっては発表者との相談で延長も考慮します．招待講演 -------- 橋本和幸 (NVIDIA. 元日本シンボリックス株式会社) 1980年代のLispマシンSymbolicsとその開発環境Genera 付属：NVIDIA GPUによる超並列コンピューティング Chung-Kil Hur (Seoul National University) Formal C semantics and LLVM compiler validation ====================================================================== 投稿・発表申込要領 4つのカテゴリそれぞれに対する投稿方法は以下の通りです．最新の情報は上記 Web ページでご確認ください．カテゴリ1（国内外未発表論文） ---------------------------- 投稿手続きは2段階です．発表申込を行った上で論文提出を行ってください．発表申込先： https://easychair.org/conferences/?conf=ppl2015 (EasyChairのアカウントが必要です) 発表申込締切：2014年12月22日(月) 17:00 (JST) 著者名、所属、論文タイトル、論文概要（日本語300〜400字程度もしくは英語 200 words 程度）を提出してください．論文提出締切：2015年1月8日(木) 17:00 (JST) 10ページ程度（最大15ページ）の論文（日本語もしくは英語、PDF形式）を提出してください．採否通知：2015年2月3日(火) 最終原稿提出締切：2015年2月16日(月) 17:00 (JST) 採録された論文の最終原稿の提出方法は、採否通知にてお知らせいたします． (注) カテゴリ1への投稿論文と類似の論文を、他の会議（予稿集を出版するもの）・論文誌などに同時投稿する場合は、査読の有無に関わらず、その旨を発表申込および論文提出の際に明記してください．PPLでは同時投稿の事実のみをもって論文を不採録とすることはありませんが、採否の決定に利用する場合があります（他の会議との重複を避けるため、発表内容についての条件付採録とすることもあります）．カテゴリ2（国外既発表論文） -------------------------- 発表申込時に採録が決定している国際会議および国際学術雑誌の発表論文が対象です．理論系だけではなく実装系の論文の投稿も歓迎いたします．発表申込方法につきましては PPL2015 のWeb ページをご確認ください．発表申込締切：2015年1月23日(金) 17:00 (JST) 原論文（ページ数不問、PDF形式）とabstract（テキスト形式）を、著者名、所属、論文タイトル、原論文の出典（発表会議名、掲載済／予定の別等）と併せてご提出ください．採否通知：2015年2月5日(木) カテゴリ3（ポスター・デモ発表） ------------------------------------------ ポスター・デモの区別を行わずに募集いたします．デモを行う場合は、発表概要においてその旨をご説明ください．発表申込方法につきましては PPL2015 の Web ページをご確認ください．発表申込締切：2015年2月6日(金) 17:00 (JST) 希望する発表形態（ポスター・デモの別）を明記して、著者名、所属、発表タイトル、発表概要（200〜300字程度）をご提出ください．採否通知：2015年2月13日(金) カテゴリ4（サーベイ・チュートリアルの発表） ------------------------------------------ サーベイまたはチュートリアルの提案を募集いたします．発表申込み時に概要の提出を行ってください．概要の内容、PPLへの関連および関連研究への言及をもとに採録を判定いたします．発表申込方法につきましては PPL2015 の Web ページをご確認ください．発表申込締切：2015年1月23日(金) 17:00 (JST) 著者名、所属、発表タイトル、発表の概要 (1〜3ページ、PDF形式．目的、カバーする話題、想定する聴衆、必要な知識の記述を含むもの)をご提出ください．新規にサーベイ論文・解説論文をご執筆される場合には、その原稿（ページ数不問・PDF形式）も併せてご提出ください．もし今回と同じ内容の既発表のサーベイ、チュートリアル、解説等があれば、その文書（ページ数不問、 PDF形式）、著者名、所属、タイトル、文書の出典（発表雑誌、掲載済／予定の別等）も併せてご提出ください．採否通知：2015年2月5日(木) 問い合わせ先：ppl2015-oc [at] kb.is.s.u-tokyo.ac.jp （[at]を@に置き換えてください） ====================================================================== プログラム委員会青戸等人東北大学浅田和之東京大学岩崎英哉電気通信大学鵜川始陽高知工科大学馬谷誠二京都大学 [プログラム共同委員長] 大岩寛産業技術総合研究所亀山幸義筑波大学河内谷清久仁日本IBM 久野靖筑波大学木村大輔国立情報学研究所宋剛秀神戸大学塚田武志 University of Oxford 中田景子 Tallinn University of Technology 浜名誠群馬大学 [プログラム共同委員長] 平井洋一 FireEye 平石拓京都大学藤田憲悦群馬大学星野直彦京都大学増原英彦東京工業大学渡部卓雄東京工業大学組織委員会松田一孝東京大学 [組織委員長] 浜名誠群馬大学 [プログラム共同委員長] 馬谷誠二京都大学 [プログラム共同委員長] 末永幸平京都大学上野雄大東北大学海野広志筑波大学木村大輔国立情報学研究所 [ポスターセッション幹事] --------------------------------------------------------------------------

1 0

Talk by John Power (U. Bath), Mon 15 Dec at UTokyo (Hongo)
by Ichiro Hasuo 09 Dec '14

09 Dec '14

Dear colleagues, John Power from U. Bath is visiting us and he is making a talk Monday next week. Feel free to join us. See you there! Best regards, Ichiro Hasuo http://www-mmm.is.s.u-tokyo.ac.jp/?plain=false&lang=en&pos=seminar ------------------------------ Mon 15 Dec 2014, 14:00-15:30 化学東館 236教室（理学部7号館の隣．ご存知ない方は先に理学部7号館415へお越しください） Room 236, Chemistry Building East (“Kagaku-Higashikan”). Next to our building (School of Science Bldg. No. 7) アクセス： https://www-mmm.is.s.u-tokyo.ac.jp/indexj.html （一番下） Access: http://www-mmm.is.s.u-tokyo.ac.jp/ (see bottom) John Power <http://www.bath.ac.uk/comp-sci/contacts/academics/john_power/> (U. Bath), Coalgebraic Logic Programming: from Semantics to Implementation; embracing the laxness (joint with Ekaterina Komendantskaya) Coinductive definitions, such as that of an infinite stream, may often be described by elegant logic programs, but ones for which SLD-refutation is of no value as SLD-derivations fall into infinite loops. Such definitions give rise to questions of lazy corecursive derivations and parallelism, as execution of such logic programs can have both recursive and corecursive features at once. Observational and coalgebraic semantics have been used to study them abstractly. However, the programming developments have often occurred separately and have usually been implementation-led. Here, we start to give a coherent semantics-led account of the issues, proceeding from abstract category theoretic semantics and developing coalgebra to try to characterise naturally arising trees. As part of the project but not presented in this talk, the work is proceeding towards implementation of a new dialect, CoALP, of logic programming, characterised by guarded lazy corecursion and parallelism.

1 0

QPL 2015: Call for papers
by Ichiro Hasuo 04 Dec '14

04 Dec '14

みなさま，来年7月の QPL 2015 @ Oxford の CFP をお送りします．ぜひ投稿・参加をご検討ください！（Tutorial もあります）蓮尾一郎東京大学コンピュータ科学専攻 http://www-mmm.is.s.u-tokyo.ac.jp/~ichiro/ ================ CALL FOR PAPERS The 12th International Workshop on Quantum Physics and Logic (QPL) July 13-17, Oxford, United Kingdom http://www.cs.ox.ac.uk/qpl2015 The 12th International Workshop on Quantum Physics and Logic (QPL) will take place at the Department of Computer Science of the University of Oxford between Wednesday 15 and Friday 17 July, 2015. The workshop will be preceded by tutorials on Monday 13 and Tuesday 14 July 2015. This workshop brings together researchers working on mathematical foundations of quantum physics, quantum computing, spatio-temporal causal structures, and related areas such as computational linguistics. Of particular interest are topics that use logical tools, ordered algebraic and category-theoretic structures, formal languages, semantical methods and other computer science methods for the study of physical behaviour in general. Previous QPL events were held in Kyoto (2014), Barcelona (2013), Brussels (2012), Nijmegen (2011), Oxford (2010), Oxford (2009), Reykjavik (2008), Oxford (2006), Chicago (2005), Turku (2004), and Ottawa (2003). INVITED SPEAKERS Paul Busch (University of York) Dan Browne (University College London) Chris Douglas (University of Oxford) TUTORIALS Paul Busch (University of York): Quantum uncertainty Dan Browne (University College London): Teleportation and measurement- based computation Oscar Dahlsten (University of Oxford): Entropy and majorisation in generalised probabilistic theories Pawel Sobocinski (University of Southampton): Graphical linear algebra IMPORTANT DATES Submission Deadline: May 1, 2015 Notification of Acceptance: June 1 Papers Ready: June 15 Tutorials: July 13-14 Workshop: July 15-17 SUBMISSIONS Prospective speakers are invited to submit a contribution to the workshop. - *Short contributions* consist of a 3 page description of the work, and a link to a paper published elsewhere. - Longer *original contributions* consist of a 5-12 page extended abstract which provides sufficient evidence of results of genuine interest and provides sufficient detail to allow the program committee to assess the merits of the work. Submissions of works in progress are encouraged but must be more substantial than a research proposal. Extended versions of accepted original research contributions will be published in Electronic Proceedings in Theoretical Computer Science (EPTCS) after the workshop. Submissions should be prepared using LaTeX, and must be submitted in PDF format. Use of the EPTCS style is encouraged. Submission is done via EasyChair: https://www.easychair.org/conferences/?conf=qpl2015 There will be an award for the best paper whose authors are all students, at the discretion of the programme committee. REGISTRATION Please visit the website to register. We encourage participation by graduate students, and will be able to provide limited reimbursement to partially support students for travel and accommodation. Further information is found on the workshop website. PROGRAMME COMMITTEE John Baez (University of California Riverside) Dan Browne (University College London) Giulio Chiribella (Tsinghua University) Bob Coecke (University of Oxford) Ross Duncan (University of Strathclyde) Tobias Fritz (Perimeter Institute) Simon Gay (University of Glasgow) Ichiro Hasuo (University of Tokyo) Chris Heunen (University of Oxford, co-chair) Matty Hoban (University of Oxford) Bart Jacobs (Radboud University Nijmegen) Viv Kendon (Durham University) Matt Leifer (Perimeter Institute) Prakash Panangaden (McGill University) Dusko Pavlovic (University of Hawaii) Simon Perdrix (CNRS Nancy) Mehrnoosh Sadrzadeh (Queen Mary University of London) Peter Selinger (Dalhousie University, co-chair) Rob Spekkens (Perimeter Institute) Bas Spitters (Aarhus University) Isar Stubbe (Universite du Littoral-Cote-d'Opale) Jamie Vicary (University of Oxford, co-chair) Mingsheng Ying (University of Technology Sydney, Tsinghua University) STEERING COMMITTEE Bob Coecke (University of Oxford) Prakash Panangaden (McGill University) Peter Selinger (Dalhousie University) LOCAL ORGANISATION Destiny Chen Chris Heunen Jamie Vicary

1 0

The 49th MLG Meeting: Program
by Katsuhiko Sano 01 Dec '14

01 Dec '14

$BBh(B49$B2s(B MLG $B?tM}O@M}3X8&5f=82q$N$40FFb(B $B!J=EJ#$7$F$*<u$1<h$j$N:]$O$4MF<O$/$@$5$$!#!K(B $BKLN&@hC<2J3X5;=QBg3X1!Bg3X$N:4Ln>!I'$G$9!#(B 2014$BG/EY(BMLG$B?tM}O@M}3X8&5f=82q!JBh(B49$B2s!K$r2<5-$NMWNN$G3+:E$7$^$9!#(B $B9V1i!&=IGq$N?=$79~$_$ODy$a@Z$j$^$7$?$,!$;22C$9$k$3$H$O2DG=$G$9!#(B $B$=$N>l9g!";22C?M?t$N4X78$G!$G0$N$?$a;d$^$G%a!<%k$G$40lJs$/$@$5$$(B $B!J;22CHq!J2q>lBe!K(B3000$B1_$r$$$?$@$/M=Dj$G$*$j$^$9!K!#(B $B$I$&$>$h$m$7$/$*4j$$$$$?$7$^$9!#(B ========================================= $BBh(B49$B2s(B MLG $B?tM}O@M}3X8&5f=82q3+:EMWNN(B ========================================= $B4|4V(B: 2014 $BG/(B 12 $B7n(B 5 $BF|(B($B6b(B) $B!A(B 12 $B7n(B 7 $BF|(B($BF|(B) $B>l=j(B: $B;3Cf29@t2O</Aq%m%$%d%k%[%F%k!J(BJR$B2C2l29@t1X$+$i<V$GLs(B20$BJ,!$2C2l29@t1X$+$iAw7^$"$j!K(B $B")(B922-0126 $B@P@n8)2C2l;T;3Cf29@t2O</D.%[(B100, URL : http://www.daiwaresort.jp/kajikasou/ $B%[!<%`%Z!<%8!'(Bhttps://sites.google.com/site/mlg2014kaga/ $B9V1i%W%m%0%i%`!'(B 12/5 (Fri) 1315--1325 $B3+2q(B (opening) 1325--1400 $B;3yu(B $B<S5*;R(B ($B<sETBg3XEl5~(B), Constructive Embedding from Logics of Strict Implication to Modal Logics via Cut-free and complete Labelled Sequent Calculus 1400--1435 $B6b;R(B $B<i(B ($BAa0pEDBg3X(B), Game Theoretic Decidability and Undecidability 1435--1510 $B4X(B $BN49((B ($B?73cBg3X(B), A Note on American Plan Semantics of Relevant Modal Logics 1530--1605 $B0KF#(B $B@.9'(B (JAIST), A relationship between classical and intuitionistic linear logic 1605--1640 $B>>ED(B $BD>M4(B ($BEl5~9)6HBg3X(B), Intuitionistic tree sequent calculus and intuitionistic lambda rho calculus 1640--1715 $BNkLZ(B $B?.9T(B ($B@E2,Bg3X(B), Two weak variants of existence property in intermediate predicate logics 12/6 (Sat) 0930--1005 $B2#9B(B $B63J?(B ($BF|K\Bg3X(B), $BCf4VO@M}$NItJ,BN7O$H$=$NJ]B83HBg$K$D$$$F(B 1005--1040 PREINING Norbert (JAIST), Separating intermediate predicate logics of well-founded and dually well-founded structures by monadic sentences 1100--1135 $B6bBt(B $B@?(B ($B9qN)>pJs3X8&5f=j(B), Toward a Logic of Cumulative Quantification 1135--1210 $B2#;3(B $B7<B@(B (JAIST), What is needed to characterize the natural number system? 1340--1415 $BEDCf(B $B5A?M(B ($B6e=#;:6HBg3X(B), Algebraic models for description logics 1415--1450 Jonni Virtema (JAIST), Tableau calculi for propositional dependence logics 1450--1510 $B:4!9LZ(B $B9nL&(B ($BFn;3Bg3X(B), The exact K4-models constructed from the exact S4-models 1530--1605 $BLnB<(B $B>0?7(B (JAIST), Revising a Labelled Sequent Calculus for Public Announcement Logic 1605--1640 $B5HB<(B $BOB?M(B (JAIST), A general analysis on proof structures 1900-- $B:)?F2q(B (Conference dinner) 12/7 (Sun) 0930--1005 $B2-:d(B $B>MJ?(B ($BElKLBg3X(B), Lindstrom extension on finite models 1005--1040 $B2CF#(B $BH%(B ($BEl5~9)6HBg3X(B), $BM-8B%U%l!<%`$K$*$1$kMMAjO@M}<0$N(Bvalidity$B$H7W;;NL$K$D$$$F(B 1100--1135 $BsnF#(B $B?.?C(B ($BEl5~9)6HBg3X(B), lambda-mu-calculus $B$N?d0\N'$N=|5n(B 1135--1210 $B:4F#(B $B2mI'(B ($B5~ETBg3XL>M@65<x(B), A name-free lambda-calculus 1210--1220 Closing --- MLG49 $B@$OC?M(B $B:4Ln>!I'!JKLN&@hC<2J3X5;=QBg3X1!Bg3X!K(B E-mail : mlg.logic.japan(a)gmail.com / katsuhiko.sano(a)gmail.com

1 0

千葉logic seminar
by arai toshiyasu 21 Nov '14

21 Nov '14

みなさま新井@千葉大学です。千葉 logic seminar の第4回のお知らせです。どなたでも参加できますのでどうぞ気軽にいらっしゃって下さい。問合せ先新井敏康（千葉大学） tosarai(a)faculty.chiba-u.jp ------------------------------------------ 日時：12月10日(水)13:30-15:300 場所：千葉大学理学部2号館105号室アクセスは http://www.chiba-u.ac.jp/campus_map/nishichiba/index.html の地図の黄色い理学部の中で数字2が付いている建物の1階です。講演者：秋吉亮太（京都大学）タイトル：ブラウワーのバー帰納法の証明論的分析アブストラクト: ブラウワーのバー帰納法は，直観主義数学において（ファン定理と並ぶ）根本原理の一つである．本発表では，バー帰納法をブフホルツのΩ規則によって分析し，いくつかの結果を紹介する．また，時間が許せば，この分析が，バー帰納法のブラワウー自身による正当化の再構成になっていることにもふれる． ------------------------------------------ -- 新井敏康

1 0

Workshop on Mathematical Logic on the Occasion of Sakae Fuchino's 60th Birthday
by Joerg Brendle 11 Nov '14

11 Nov '14

皆様、ブレンドレ＠神戸大学システム情報学研究科です。１１月１７日（月）から１１月１９日（水）まで神戸大学にて数理論理学やその関連のある分野についての研究集会「Workshop on Mathematical Logic on the Occasion of Sakae Fuchino's 60th Birthday」が開催されます。集会のウェブページは http://kurt.scitec.kobe-u.ac.jp/~brendle/sakae60/home.html にあります。また、１１月１８日（火）に１８：３０時からザ・ヒルサイド神戸（the Hillside Rokko Yamanote） http://www.hillsiderokko.com/party/ にて渕野昌先生の還暦お祝いのバンケットを開きます。バンケットの参加を希望される方は brendle(a)kurt.scitec.kobe-u.ac.jp までご連絡ください。皆様のご参加をお待ちしております。 jörg brendle

1 0

LENLS11: Call for Participation and Registration
by Koji Mineshima 06 Nov '14

06 Nov '14

（重複して受け取られた場合はご容赦ください）お茶の水女子大学の峯島と申します。 11月22日から24日にかけて東京で開催される国際ワークショップ LENLS 11のご案内をお送り致します。 Online Registrationの締め切りが 11月10日(月曜) に迫っております。 Registrationの方法につきましては、以下のページをご覧ください。 https://www.ai-gakkai.or.jp/isai/registration ワークショップの詳細につきましては、以下のページもご参照ください。 http://www.is.ocha.ac.jp/~bekki/lenls/ 皆さまのご参加をお待ちしております。峯島宏次（お茶の水女子大学・JST CREST） [Apologies for multiple copies] ================================================================= CALL FOR PARTICIPATION Logic and Engineering of Natural Language Semantics 11 (LENLS11) Dates : November 22-24, 2014 Workshop Site : (22nd) Ochanomizu University Room 207-209, Science Building 3, Tokyo, Japan http://www.ocha.ac.jp/en/index.html (23rd,24th) Raiousha Building, Keio University, Hiyoshi campus, Kanagawa, Japan http://www.keio.ac.jp/en/maps/hiyoshi.html Contact Person: Koji Mineshima (Ochanomizu University) Contact Email : lenls11[[at]]easychair.org Website : http://www.is.ocha.ac.jp/‾bekki/lenls/ ================================================================= Chair: Koji Mineshima (Ochanomizu University) Co-chair: Daisuke Bekki (Ochanomizu University /National Institute of Informatics/JST CREST) Eric McCready (Aoyama Gakuin University) Invited Speakers: - Chris Barkar (New York University) - Kimiko Nakanishi (Ochanomizu University) - Matthew Stone (Rutgers University) - Christopher Tancredi (Keio University) LENLS is an annual international workshop on formal syntax, semantics and pragmatics. It will be held as one of the workshops of the Sixth JSAI International Symposia on AI (isAI2014) (http://www.ai-gakkai.or.jp/isai/) sponsored by the Japan Society for Artificial Intelligence (JSAI) (http://www.ai-gakkai.or.jp/en). Important dates: ================ Deadline for onsite registration: November 10, 2014 LENLS11: November 22-24, 2014 We will also hold a one-day workshop at Kyoto University on November 28, 2014, with two invited speakers, Chris Barkar and Matthew Stone. The detailed information will be announced on the website. http://www.is.ocha.ac.jp/~bekki/lenls/ Registration: ============= The proceedings of the workshop will be available at the conference site for registered persons. Please follow the link below and register yourself until **10th November 2014**. https://www.ai-gakkai.or.jp/isai/registration Program: ======== 1st Day: November 22th (Sat), 2014 @Ochanomizu University ------------------------- 12:30-12:50: Reception 12:50-13:00: Opening Remarks 13:00-14:30: Session 1 * Kristina Liefke "Codability and Robustness in Formal Natural Language Semantics" * Alain Lecomte "An interaction framework for dialogue: combining Ludics and Type Theory with Records" * Yurie Hara "Radical Inquisitive Investigation into Cantonese Biased and Neutral Questions" 14:30-14:45: Coffee Break 14:45-16:15: Session 2 * Stergios Chatzikyriakidis and Zhaohui Luo "Using Signatures in Type Theory to Represent Situations" * Ribeka Tanaka, Koji Mineshima and Daisuke Bekki "Resolving Modal Anaphora in Dependent Type Semantics" * Krystian Jobczyk "Temporal verbs and adverbs: 'often' and 'many times' and their fuzzy-integral-logic based modelling" 16:15-16:30: Coffee Break 16:30-17:30: Invited Talk 1 * Kimiko Nakanishi "Scalarity of EVEN" 2nd Day: November 23th (Sun), 2014 @Keio University, Hiyoshi campus ------------------------- 9:00-9:30: Registration and Coffee Break 9:30-10:30: Invited Talk 2 * Mizoguchi Riichiro "Ontology engineering - Theory and practice -" (from the JURISIN workshop) 10:30-10:45: Coffee Break 10:45-12:00: Student Session * Daniel Tiskin "Specific Opaque Readings and Proportional Determiners" * Makiko Kato "Japanese plural marker 'tachi' and associativity" * Yu-Mi Jo "Temporal Pluractional Adverbs in Korean: Focusing on Tatali, Nanali, and Halwuhalwu" 12:00-13:00: Lunch 13:00-14:30: Session 3 * Daisuke Bekki and Eric McCready "CI via DTS" * Bruno Mery, Richard Moot and Christian Retore "Computing the Semantics of Massive Entities using Many-Sorted Types" * Oleg Kiselyov "Canonical Constituents and Non-canonical Coordination: Simple Categorial Grammar account" 14:30-14:45: Coffee Break 14:45-15:45: Session 4 * Eric McCready "Honorific Denotations" * Philippe de Groote and Yoad Winter "A type-logical account of quantification in event semantics" 15:45-16:00: Coffee Break 16:00-17:00: Invited Talk 3 * Matthew Stone "Logic and Probability in Grounded Semantics" (shared with the JURISIN workshop) 17:00-17:15: Coffee Break 17:15-18:15: Invited Talk 4 * Chris Tancredi "Focus and Givenness" 19:00-:Banquet 3rd Day: November 24th (Mon), 2014 @Keio University, Hiyoshi campus ------------------------- 9:30-10:00: Coffee Break 10:00-11:30: Session 5 * Lisa Bylinina, Natalia Ivlieva, Alexander Podobryaev and Yasutada Sudo "A Non-Superlative Semantics for Ordinals and the Syntax of Comparison Classes" * Laurent Prevot and Jan Gorisch "Crossing Empirical and Formal approaches for studying French feedback items" * Alastair Butler and Kei Yoshimoto "Semantic Visualisation with Flame Graphs" 11:30-13:00: Lunch 13:00-14:30: Session 6 * Lasha Abzianidze "Towards a Wide-coverage Tableau Method for Natural Logic" * Elena Castroviejo and Berit Gehrke "A good intensifier" * Shinya Okano and Yoshiki Mori "On CG management of Japanese weak necessity modal 'hazu'" 14:30-14:45: Coffee Break 14:45-16:15: Session 7 * Satoru Suzuki "Measurement-Theoretic Foundations of Observational-Predicate Logic" * Yasuo Nakayama "Formal Analysis of Epistemic Modalities and Conditionals based on Logic of Belief Structures" * Zhiguo Xie "An epistemic modal for strict comparison in Mandarin Chinese" 16:15-16:30: Coffee Break 16:30-17:30: Invited Talk 5 * Chris Barkar "The Logic of Scope" Alternates ---------- * Osamu Sawada "Polarity sensitivity and update refusal: the case of the Japanese negative 'totemo'" * Richard Zuber "On the logical reducibility of reflexives" Post Proceedings =========== Selected papers will be published in Springer's Lecture Notes in Artificial Intelligence (LNAI). Sponsor: ======== LENLS is being organized by an alliance of "Establishment of Knowledge-Intensive Structural Natural Language Processing and Construction of Knowledge Infrastructure" (http://nlp.ist.i.kyoto-u.ac.jp/CREST/?en) project, funded by JST CREST Programs "Advanced Core Technologies for Big Data Integration" (http://www.jst.go.jp/kisoken/crest/en/research_area/ongoing/areah25-6.html). Workshop Organizers/Program Committee: ====================================== - Koji Mineshima (Ochanomizu University) - Daisuke Bekki (Ochanomizu University/National Institute of Informatics) - Alastair Butler (Tohoku University) - Richard Dietz (University of Tokyo) - Eric McCready (Aoyama Gakuin University) - Yoshiki Mori (University of Tokyo) - Yasuo Nakayama (Osaka University) - Katsuhiko Sano (Japan Advanced Institute of Science and Technology) - Katsuhiko Yabushita (Naruto University of Education) - Tomoyuki Yamada (Hokkaido University) - Shunsuke Yatabe (Kyoto University) - Kei Yoshimoto (Tohoku University)

1 0

奈良女子大学Kowalski先生講演お知らせ
by 藤田恵 04 Nov '14

04 Nov '14

皆様、奈良女子大学の藤田です。今月11/10(月)に奈良女子大学にて、Robert Kowalski先生が講演を行ってくださいます。下記のような内容で行いますので、ぜひお越しください。 -------------------------------------------------------------------- Robert Kowalski先生講演のお知らせ 11月10日(月)に、本学科にて下記の要領でRobert Kowalski先生の講演を行います。記号論理学の分野では非常に有名な先生で、有益なお話を聞けると思いますので、ぜひお越し下さい。記演題: Towards a Science of Computing 時間: 13:00〜14:30 場所: 奈良女子大学G棟G302教室問い合わせ先: 新出 nide(a)ics.nara-wu.ac.jp [追記] 講演概要を http://www.ics.nara-wu.ac.jp/jp/event.html#seminars_and_lectures で案内しています。

1 0

再送：数学基礎論若手の会2014
by YOSHIDA Satoru 04 Nov '14

04 Nov '14

皆様重複して受け取られた場合はご容赦ください。数学基礎論若手の会2014について、参加申込み締切を下記の通り延長致しました：講演、参加、宿泊の申込み： 2014年11月18日15時（開催日前日）. 宿泊施設での食事の申込み：2014年11月13日15時. まだ多少時間がありますので、講演をご検討頂けたらと思います。また、講演プログラム（暫定版）および参加者リストを後述の若手の会webサイト内に掲載しました。以上、よろしくお願い致します。 2014年9月22日 19:04 YOSHIDA Satoru <satoru-y(a)kankyo-u.ac.jp>: > 皆様 > > 重複して受け取られた場合はご容赦ください。 > > 数学基礎論若手の会2014のご案内です。 > > 数学基礎論を専攻する学生および若手研究者の研究交流を目的とす > る合宿形式の研究集会です． > 講演はオリジナルの成果発表に限らず，研究の途中報告や研究内容の紹介など幅広く募集しております． > また，これから数学基礎論を勉強したいと思っている方のご参加も歓迎します． > 多くの方々のご参加およびご講演をお待ちしています． > > 日程：11月19日（水）午後－21日（金）午前 > 場所：鳥取市サイクリングターミナル砂丘の家（鳥取砂丘付近） > http://www.city.tottori.lg.jp/www/contents/1198114185831/ > 幹事：吉田聡（鳥取環境大学） satoru-y(a)kankyo-u.ac.jp > ホームページ： http://misc.kankyo-u.ac.jp/~satoru-y/wakate14/ > > 今年度若手の会申込み要領については上記ホームページをご参照ください。 > > > -- > 吉田聡<YOSHIDA, Satoru> > 鳥取環境大学 > -- 吉田聡<YOSHIDA, Satoru> 鳥取環境大学

1 0

WoLLIC 2015 - Call for Papers
by 小野寛晰 03 Nov '14

03 Nov '14

[Please circulate. Apologies for cross-postings.] WoLLIC 2015 22nd Workshop on Logic, Language, Information and Computation July 20th-23rd, 2015 Bloomington, IN, USA SCIENTIFIC SPONSORSHIP Interest Group in Pure and Applied Logics (IGPL) The Association for Logic, Language and Information (FoLLI) Association for Symbolic Logic (ASL) European Association for Theoretical Computer Science (EATCS) European Association for Computer Science Logic (EACSL) Sociedade Brasileira de Computação (SBC) Sociedade Brasileira de Lógica (SBL) ORGANISATION School of Informatics and Computing, Indiana University, USA Program in Pure and Applied Logic, Indiana University, USA Centro de Informática, Universidade Federal de Pernambuco, Brazil HOSTED BY School of Informatics and Computing, Indiana University, USA CALL FOR PAPERS WoLLIC is an annual international forum on inter-disciplinary research involving formal logic, computing and programming theory, and natural language and reasoning. Each meeting includes invited talks and tutorials as well as contributed papers. The twenty-second WoLLIC will be held at the School of Informatics and Computing, Indiana University, from July 20th to 23rd, 2015. It is sponsored by the Association for Symbolic Logic (ASL), the Interest Group in Pure and Applied Logics (IGPL), the The Association for Logic, Language and Information (FoLLI), the European Association for Theoretical Computer Science (EATCS), the European Association for Computer Science Logic (EACSL), the Sociedade Brasileira de Computação (SBC), and the Sociedade Brasileira de Lógica (SBL). PAPER SUBMISSION Contributions are invited on all pertinent subjects, with particular interest in cross-disciplinary topics. Typical but not exclusive areas of interest are: foundations of computing and programming; novel computation models and paradigms; broad notions of proof and belief; proof mining, type theory, effective learnability; formal methods in software and hardware development; logical approach to natural language and reasoning; logics of programs, actions and resources; foundational aspects of information organization, search, flow, sharing, and protection. Proposed contributions should be in English, and consist of a scholarly exposition accessible to the non-specialist, including motivation, background, and comparison with related works. They must not exceed 10 pages (in font 10 or higher), with up to 5 additional pages for references and technical appendices. The paper's main results must not be published or submitted for publication in refereed venues, including journals and other scientific meetings. It is expected that each accepted paper be presented at the meeting by one of its authors. Papers must be submitted electronically at the WoLLIC 2015 EasyChair website. (Please go to http://wollic.org/wollic2015/instructions.html <http://wollic.org/wollic2015/instructions.html> for instructions.) A title and single-paragraph abstract should be submitted by Feb 8, 2015, and the full paper by Feb 15, 2015 (firm date). Notifications are expected by Mar 22, 2015, and final papers for the proceedings will be due by Apr 5, 2015 (firm date). PROCEEDINGS The proceedings of WoLLIC 2015, including both invited and contributed papers, will be published in advance of the meeting as a volume in Springer's LNCS series. In addition, abstracts will be published in the Conference Report section of the Logic Journal of the IGPL, and selected contributions will be published as a special post-conference WoLLIC 2015 issue of a scientific journal (to be confirmed). INVITED SPEAKERS (tba) STUDENT GRANTS ASL sponsorship of WoLLIC 2015 will permit ASL student members to apply for a modest travel grant (deadline: May 1st, 2015). See http://www.aslonline.org/studenttravelawards.html <http://www.aslonline.org/studenttravelawards.html> for details. IMPORTANT DATES Feb 8, 2015: Paper title and abstract deadline Feb 15, 2015: Full paper deadline Mar 22, 2015: Author notification Apr 5, 2015: Final version deadline (firm) PROGRAMME COMMITTEE Juliana Küster Filipe Bowles <https://risweb.st-andrews.ac.uk/portal/da/persons/juliana-kuster-filipe-bow…> (U St Andrews, Scotland) Guillaume Brunerie <http://www.eleves.ens.fr/home/brunerie/> (ENS Ulm, France) (TBC) Ann Copestake <http://www.cl.cam.ac.uk/~aac10/> (U Cambridge, UK) (TBC) Robin Cooper <http://www.ling.gu.se/~cooper/> (U Gothenburg, Sweden) Nikos Galatos <http://web.cs.du.edu/~ngalatos/>(U Denver, USA) Achim Jung <http://www.cs.bham.ac.uk/~axj/> (U Birmingham, UK) Sara <http://www2.warwick.ac.uk/fac/sci/dcs/people/sara_kalvala/> Kalvala <http://www2.warwick.ac.uk/fac/sci/dcs/people/sara_kalvala/> (U Warwick, UK) Elham Kashefi <http://www.inf.ed.ac.uk/people/staff/Elham_Kashefi.html> (Edinburgh U, Scotland) Peter Lefanu Lumsdaine <http://www.math.ias.edu/~plumsdaine/> (Institute for Advanced Study, USA) Ian Mackie <http://www.ianmackie.com/> (U Sussex, UK) Gerard de Melo <http://gerard.demelo.org/> (Tsinghua University, China) Vivek Nigam <http://www.nigam.info/> (Federal U of Paraíba, Brazil) Valeria de Paiva <http://www.cs.bham.ac.uk/~vdp/> (Nuance Comm, USA) (CHAIR) Luiz Carlos <http://buscatextual.cnpq.br/buscatextual/visualizacv.do?id=K4783548E2> Pereira <http://buscatextual.cnpq.br/buscatextual/visualizacv.do?id=K4783548E2> (PUC-Rio, Brazil) Elaine Pimentel <https://sites.google.com/site/elainepimentel/> (Federal U of Rio Grande do Norte, Brazil) Alexandra Silva <http://alexandrasilva.org/> (Radboud Nijmegen U, The Netherlands) Carolyn Talcott <http://www.sri.com/about/people/carolyn-talcott> (SRI International, USA) Josef Urban <http://cs.ru.nl/~urban/> (Radboud Nijmegen U, The Netherlands) Laure Vieu <http://www.irit.fr/~Laure.Vieu/> (IRIT-Toulouse, France) (TBC) Renata Wasserman <http://www.ime.usp.br/~renata/> (U São Paulo, Brazil) Anna Zamansky <http://mailng.hevra.haifa.ac.il/~annazam/> (U Haifa, Israel) STEERING COMMITTEE Samson Abramksy, Johan van Benthem, Anuj Dawar, Joe Halpern, Wilfrid Hodges, Ulrich Kohlenbach, Daniel Leivant, Leonid Libkin, Angus Macintyre, Luke Ong, Hiroakira Ono, Ruy de Queiroz. ORGANISING COMMITTEE Daniel Leivant (Indiana U) (Local co-chair) Larry Moss (Indiana U) (Local co-chair) Anjolina G. de Oliveira (U Fed Pernambuco) Ruy de Queiroz (U Fed Pernambuco) (co-chair) FURTHER INFORMATION Contact one of the Co-Chairs of the Organising Committee. WEB PAGE http://wollic.org/wollic2015/ <http://wollic.org/wollic2015/>

1 0

第49回 MLG 数理論理学研究集会のご案内（再送：講演・宿泊の申し込み締め切り11/21）
by Katsuhiko Sano 30 Oct '14

30 Oct '14

第49回 MLG 数理論理学研究集会のご案内 (重複してお受け取りの際はどうぞご容赦ください。) 北陸先端科学技術大学院大学の佐野勝彦と申します。締め切りまで三週間程となりましたので、再度アナウンスさせていただきます。 2014年度MLG数理論理学研究集会（第49回）を下記の要領で開催いたします。多くの方のご講演・ご参加をお待ちしております。 ========================================= 第49回 MLG 数理論理学研究集会開催要領 ========================================= - 期間: 2014 年 12 月 5 日(金) 〜 12 月 7 日(日) - 場所: 山中温泉河鹿荘ロイヤルホテル（JR加賀温泉駅から車で約20分，加賀温泉駅から送迎あり） -- 〒922-0126 石川県加賀市山中温泉河鹿町ホ100 -- URL : http://www.daiwaresort.jp/kajikasou/ - 講演・宿泊申込締め切り: 2014 年 11 月 21 日（木） - 申し込みはこちらから --> http://goo.gl/RfZ5SE - ホームページ: https://sites.google.com/site/mlg2014kaga/ - 連絡先E-mail: mlg.logic.japan [at] gmail.com ============ 参加募集 ============ - 講演時間は原則40分を予定しています。 - 12月6日（土）の夜に懇親会を行います。 - 全日程参加の場合，参加費（宿泊代・食事代・会場代）は25000円前後になる予定です。 - ご講演をなさらなくても参加いただけます。山中温泉河鹿荘ロイヤルホテルで宿泊および食事をなさらない場合にも参加費（会場代）3000円をいただきます。 - 参加・講演申し込みは、http://goo.gl/RfZ5SE の registration form からお願い致します。世話人: 佐野勝彦〒923-1292 石川県能美市旭台1-1 北陸先端科学技術大学院大学情報科学研究科 MLG2014 に関するメールは，mlg.logic.japan [at] gmail.com まで。

1 0

TPP2014: 3rd Announcement and call for participation
by Jacques Garrigue 27 Oct '14

27 Oct '14

皆様、 TPP2014の参加募集案内をお送りします。参加される方、今週中に返事をいただければと思います。 Jacques Garrigue ========================================================================= TPP2014: 3rd Announcement and call for participation ========================================================================= 研究集会「高信頼な理論と実装のための定理証明および定理証明器」案内　　　　　　　　　　　　　　　　　　　(English version is below.) 12月3日(水)-5日(金)に九州大学西新プラザにて, 研究集会「高信頼な理論と実装のための定理証明および定理証明器」を開催します. 皆様のご参加をお待ちしています. 日時：2014年 12月3日(水)13:00 〜 12月5日(金)15:00 (予定) 場所：九州大学・西新プラザ (福岡市早良区西新2-16-23) http://bit.ly/QdaiNishijin 福岡空港から地下鉄で西新駅まで約20分, その後, 徒歩約10分. プログラム：詳細は未定ですが, 適宜HPを更新予定です. みなさまのご講演をお待ちしています. Adam Chlipala氏とCyril Cohen 氏をお招きして, ご講演頂く予定です. Correct-by-Construction Program Synthesis in Coq, Adam Chlipala (MIT, USA). Mathematical components and algebraic numbers, Cyril Cohen (INRIA Sophia-Antipolis, France). 御講演を頂く予定です. 参加者と講演の数を大体把握しておきたいと思いますので，参加される方は 10月末までに下の参加申し込みを下記メールアドレスまでお送りください．参加者には，できるだけ講演していただければと思います． TPPMARK: 形式証明のための問題を掲示し証明を募集しています. 皆で問題(PDF)を解いて, ワークショップ中に証明を比べようと思います. 証明支援系, 解き方を問わず, みなさまの多くの証明例を募集しています. 証明や質問は下記のメールアドレスに送って下さい. 都合で参加出来ない方の証明の応募も歓迎致します. 申込み・問い合わせ先: tpp2014(a)imi.kyushu-u.ac.jp (溝口佳寛(九州大学)) URL: http://imi.kyushu-u.ac.jp/lasm/tpp2014/index_ja.html (注. 作成途中です.「TPP2014 数学」で検索してみて下さい.) ------------------------------------------------------------------------- TPP 2014 参加申し込みお名前：ご所属：講演　：する／しない懇親会：参加する／参加しない講演する場合タイトル：（講演のタイトルが決まっていなければ，TBAでもかまいません．決まったらご連絡ください．）講演希望日: (○/×) 12/3 (○/×) 12/4 (○/×) 12/5 その他(ご意見/ご要望ありましたらお願いします): ------------------------------------------------------------------------- ========================================================================= Workshop: Theorem proving and provers for reliable theory and implementations (TPP2014) This is the call for participation for TPP2014, to be held on Dec. 3(Wed) - 5(Fri), 2014 at Kyushu University. Date: 2014/12/03 around 1pm to 12/05 around 3pm Venue: Nishijin Plaza, Kyushu University (2-16-23 Nishijin, Sawara-ku, Fukuoka City) http://bit.ly/QdaiNishijinPDF Invited Speakers: Correct-by-Construction Program Synthesis in Coq, Adam Chlipala (MIT, USA). Mathematical components and algebraic numbers, Cyril Cohen (INRIA Sophia-Antipolis, France). If you are planning to attend the meeting, please send the information slip below to the indicated address by the end of October. TPPMARK: A problem for a formal proof is attached in our HP. We would like you to solve a problem in your favorite theorem prover, and compare solutions at the workshop. Please send your proof to the email address below. Submission/questions to: 　　　tpp2014(a)imi.kyushu-u.ac.jp (Yoshihiro Mizoguchi) URL: http://imi.kyushu-u.ac.jp/lasm/tpp2014/ ------------------------------------------------------------------------- TPP 2014 Registration Name: Affiliation: Will give a talk: Yes/No Will attend the party: Yes/No Title of the talk: (If it is not decided yet, TBA is OK.) Which date do you prefer to talk ? 12/3 (OK/NG) 12/4 (OK/NG) 12/5 (OK/NG) Requests for the organizer (if any): ------------------------------------------------------------------------- =========================================================================

1 0

LICS 2015 - First Call for Papers
by Ichiro Hasuo 22 Oct '14

22 Oct '14

みなさま，来年行われる LICS 2015 の CFP をお送りします（なんと京都開催です！）． ICALP 2015 とも共催で，両方の情報をあわせたウェブページが http://www.kurims.kyoto-u.ac.jp/icalp-lics2015/index.html にあります．ぜひ，投稿また参加をご検討ください．京都でお会いできるのを楽しみにしております．蓮尾一郎東京大学情報理工コンピュータ科学専攻 http://www-mmm.is.s.u-tokyo.ac.jp/~ichiro/ =========================== CALL FOR PAPERS Thirtieth Annual ACM/IEEE Symposium on LOGIC IN COMPUTER SCIENCE (LICS) July 6–10, 2015, Kyoto, Japan http://lics.rwth-aachen.de/lics15/ VENUE LICS 2015 will be hosted in Kyoto, Japan during the week 6-10 July 2015 and will be colocated with ICALP 2015. SCOPE The LICS Symposium is an annual international forum on theoretical and practical topics in computer science that relate to logic, broadly construed. We invite submissions on topics that fit under that rubric. Suggested, but not exclusive, topics of interest include: automata theory, automated deduction, categorical models and logics, concurrency and distributed computation, constraint programming, constructive mathematics, database theory, decision procedures, description logics, domain theory, finite model theory, formal aspects of program analysis, formal methods, foundations of computability, higher-order logic, lambda and combinatory calculi, linear logic, logic in artificial intelligence, logic programming, logical aspects of bioinformatics, logical aspects of computational complexity, logical aspects of quantum computation, logical frameworks, logics of programs, modal and temporal logics, model checking, probabilistic systems, process calculi, programming language semantics, proof theory, real-time systems, reasoning about security and privacy, rewriting, type systems and type theory, and verification. IMPORTANT DATES Authors are required to submit a paper title and a short abstract of about 100 words in advance of submitting the extended abstract of the paper. The exact deadline time on these dates is given by AoE (anywhere on earth). Titles & Short Abstracts Due: January 12, 2015 Extended Abstracts Due: January 19, 2015 Author feedback/rebuttal period: March 12-16, 2015 Author Notification: March 30, 2015 Final Versions Due for Proceedings: April 27, 2015 Deadlines are firm; late submissions will not be considered. All submissions will be electronic via https://www.easychair.org/conferences/?conf=lics2015. SUBMISSION INSTRUCTIONS Every extended abstract must be submitted in the IEEE Proceedings 2-column 10pt format and may not be longer than 12 pages, including references. LaTeX style files are available on the conference website. The extended abstract must be in English and provide sufficient detail to allow the program committee to assess the merits of the paper. It should begin with a succinct statement of the issues, a summary of the main results, and a brief explanation of their significance and relevance to the conference and to computer science, all phrased for the non-specialist. Technical development directed to the specialist should follow. References and comparisons with related work must be included. (If necessary, detailed proofs of technical results may be included in a clearly-labeled appendix, to be consulted at the discretion of program committee members.) Extended abstracts not conforming to the above requirements will be rejected without further consideration. Paper selection will be merit-based, with no a priori limit on the number of accepted papers. Papers authored or co-authored by members of the program committee are not allowed. Results must be unpublished and not submitted for publication elsewhere, including the proceedings of other symposia or workshops. The program chair must be informed, in advance of submission, of any closely related work submitted or about to be submitted to a conference or journal. Authors of accepted papers are expected to sign copyright release forms. One author of each accepted paper is expected to present it at the conference. SHORT PRESENTATIONS A session of short presentations, intended for descriptions of student research, works in progress, and other brief communications, is planned. These abstracts will not be published. Dates and guidelines will be posted on the conference website. KLEENE AWARD FOR BEST STUDENT PAPER An award in honor of the late Stephen C. Kleene will be given for the best student paper(s), as judged by the program committee. SPECIAL ISSUES Full versions of up to three accepted papers, to be selected by the program committee, will be invited for submission to the Journal of the ACM. Additional selected papers will be invited to a special issue of Logical Methods in Computer Science. SPONSORSHIP The symposium is sponsored by ACM SIGLOG and the IEEE Technical Committee on Mathematical Foundations of Computing, in cooperation with the Association for Symbolic Logic and the European Association for Theoretical Computer Science. PROGRAM COMMITTEE CHAIR Catuscia Palamidessi, INRIA & E. Polytechnique PROGRAM COMMITTEE Pablo Barceló, U. Chile Gilles Barthe, IMDEA Andrej Bauer, IMFM Lev Beklemishev, Russian Ac. of Sci. Patricia Bouyer-Decitre, CNRS & ENS Cachan Adam Chlipala, MIT Agata Ciabattoni, TU Wien Véronique Cortier, CNRS Loria Pedro D'Argenio, UN Cordoba Anuj Dawar, U. Cambridge Mariangiola Dezani, U. Torino Yuxi Fu, SJTU Rob van Glabbeek, NICTA Ichiro Hasuo, U. Tokyo Martin Hofmann, LMU Delia Kesner, U. Paris Diderot Barbara König, U. Duisburg-Essen Laura Kovács, Chalmers UT Dexter Kozen, Cornell U. Manfred Kufleitner, U. Stuttgart Anthony W. Lin, Yale-NUS College Simone Martini, U. Bologna Madhavan Mukund, Chennai Math. Inst. Filip Murlak, U. Warsaw Gopalan Nadathur, U. Minnesota Frank Pfenning, CMU Ian Pratt-Hartmann, U. Manchester Albert Rubio, U. Barcelona Peter Selinger, Dalhousie U. Alessandra Silva, Radboud U. Tachio Terauchi, JAIST Ashish Tiwari, SRI Bow-Yaw Wang, Academia Sinica CONFERENCE CHAIR Masahito Hasegawa, RIMS, Kyoto U. WORKSHOP CHAIR Patricia Bouyer-Decitre, CNRS & ENS Cachan PUBLICITY CHAIR Andrzej Murawski, University of Warwick LICS ORGANIZING COMMITTEE M. Abadi, L. Aceto, R. Alur, M. P. Bonacina, P. Bouyer-Decitre, K. Chatterjee, A. Compagnoni, A. Dawar, N. Dershowitz, M. Fernandez, M. Grohe, O. Grumberg, T. Henzinger, P. Kolaitis, O. Kupferman, B. Larose, D. Miller, M. Mislove, A. Murawski, C. Palamidessi, L. Ong (chair), P. Panangaden, K. Rose, A. Scedrov, D. Shmoys, M. Valeriote

1 0

ICALP 2015 (Kyoto, 6-10 Jul, 2015)
by Shinya Katsumata 22 Oct '14

22 Oct '14

皆様、来年京都で開催されるICALP 2015 (LICS2015と共催)のご案内をお送りいたします。勝股 ----- ICALP 2015 http://www.kurims.kyoto-u.ac.jp/icalp2015/ First Call for Papers ====================== The 42nd International Colloquium on Automata, Languages, and Programming (ICALP) will take place in the period 6-10 July 2015 in Kyoto, Japan. The conference will co-locate with LICS 2015, the 30th ACM/IEEE Symposium on Logic in Computer Science. The ICALP 2015 conference chair is Kazuo Iwama (Kyoto University). ICALP is the main conference and annual meeting of the European Association for Theoretical Computer Science (EATCS). As usual, the main conference will be preceded and/or followed by a series of workshops. Important dates --------------- Submission deadline: Tuesday, 17 February 2015, 23:59 PST (Pacific Standard Time, UTC-8) Author notification: 15 April 2015 Final manuscript due: 30 April 2015 Deadlines are firm; late submissions will not be considered. Proceedings ----------- ICALP proceedings are published in the Springer-Verlag ARCoSS (Advanced Research in Computing and Software Science) subseries of LNCS (Lecture Notes in Computer Science). Invited Speakers ================= Ken Kawarabayashi, NII, Japan Valerie King, University of Victoria, Canada Thomas Moscibroda, MSR Asia, China Anca Muscholl, Universitè Bordeaux, France (Joint with LICS) Peter O'Hearn, Facebook, UK (Joint with LICS) Invited Tutorial Speakers (Joint with LICS) ------------------------------------------- Piotr Indyk, MIT, USA Andrew Pitts, University of Cambridge, UK Geoffrey Smith, Florida International University, USA Masterclass speaker ------------------- Ryuhei Uehara, JAIST, Japan Topics ====== Papers presenting original research on all aspects of theoretical computer science are sought. Typical but not exclusive topics of interest are: Track A: Algorithms, Complexity and Games ----------------------------------------- * Algorithmic Game Theory * Approximation Algorithms * Combinatorial Optimization * Combinatorics in Computer Science * Computational Biology * Computational Complexity * Computational Geometry * Cryptography * Data Structures * Design and Analysis of Algorithms * Machine Learning * Parallel, Distributed and External Memory Computing * Randomness in Computation * Quantum Computing Track B: Logic, Semantics, Automata and Theory of Programming ------------------------------------------------------------- * Algebraic and Categorical Models * Automata, Games, and Formal Languages * Emerging and Non-standard Models of Computation * Databases, Semi-Structured Data and Finite Model Theory * Principles and Semantics of Programming Languages * Logic in Computer Science, Theorem Proving and Model Checking * Models of Concurrent, Distributed, and Mobile Systems * Models of Reactive, Hybrid and Stochastic Systems * Program Analysis and Transformation * Specification, Refinement, Verification and Synthesis * Type Systems and Theory, Typed Calculi Track C: Foundations of Networked Computation: Models, Algorithms and Information Management ------------------------------------------------------ * Algorithmic Aspects of Networks and Networking * Formal Methods for Network Information Management * Foundations of Privacy, Trust and Reputation in Networks * Mobile and Wireless Networks and Communication * Network Economics and Incentive-Based Computing Related to Networks * Networks of Low Capability Devices * Network Mining and Analysis * Overlay Networks and P2P Systems * Specification, Semantics, Synchronization of Networked Systems * Theory of Security in Networks Submission Guidelines -------------------- Authors are invited to submit an extended abstract of no more than 12 pages, including references, in LNCS style presenting original research on the theory of Computer Science. All submissions will be electronic via the EasyChair page for the conference, with three tracks (A, B and C): https://easychair.org/conferences/?conf=icalp2015 Submissions should be made to the appropriate track of the conference. No prior publication or simultaneous submission to other publication outlets (either a conference or a journal) is allowed. Submissions must adhere to the specified format and length. Submissions that are too long or formatted incorrectly may be rejected immediately. All the technical details that are necessary for a proper scientific evaluation of a submission must be included in a clearly-labelled appendix, to be consulted at the discretion of program committee members. This includes, in particular, the proofs of all the key theorems in a paper. Should I submit my paper to Track A or Track C? ------------------------------------------------ While the scope of Tracks A and B are generally well understood given their long history, the situation for Track C may be less obvious. In particular, some clarifications may be helpful regarding areas of potential overlap, especially between Tracks A and C. The aim for Track C is to be the leading venue for theory papers truly motivated by networking applications, and/or proposing theoretical results relevant to real networking, certified analytically, but not necessarily tested practically. The motivation for the track was the lack of good venues for theory papers motivated by applications in networking. On the one hand, the good networking conferences typically ask for extended experiments and/or simulations, while the TCS community is hardly able to do such experiments or simulations. On the other hand, the good conferences on algorithms tend to judge a paper based only on its technical difficulty and on its significance from an algorithmic perspective, which may not be the same as when judging the paper from the perspective of impact on networks. Several areas of algorithmic study of interest to track C have a broad overlap with track A. Graph algorithmics can belong in either, though if the work is not linked to networking, it is more appropriate in track A. Algorithmic game theory is another area of major overlap. Aspects involving complexity, the computation of equilibria and approximations, belong more in Track A, while results with applications in auctions, networks and some aspects of mechanism design belong in Track C. Finally, it should be noted that algorithms and complexity of message-passing based distributed computing belong squarely in track C, while certain other aspects of distributed computing do not fall under its scope. Best Paper Awards ----------------- As in previous editions of ICALP, there will be best paper and best student paper awards for each track of the conference. In order to be eligible for a best student paper award, a paper should be authored only by students and should be marked as such upon submission. Committees ========== Track A: Algorithms, complexity, and games ------------------------------------------ Peyman Afshani, Aarhus University, Denmark Hee-Kap Ahn, POSTECH, South Korea Hans Bodlaender Utrecht University, The Netherlands Karl Bringmann, Max-Planck Institut für Informatik, Germany Sergio Cabello, University of Ljubljana, Slovenia Ken Clarkson, IBM Almaden Research Center, USA Éric Colin de Verdière, École Normale Supérieure Paris, France Stefan Dziembowski, University of Warsaw, Poland David Eppstein, University of California at Irvine, USA Dimitris Fotakis, National Technical University of Athens, Greece Paul Goldberg, University of Oxford, UK MohammadTaghi Hajiaghayi, University of Maryland at College Park, USA Jesper Jansson, Kyoto University, Japan Andrei Krokhin, Durham University, UK Asaf Levin, Technion, Israel Inge Li Gørtz, Technical University of Denmark, Denmark Pinyan Lu, Microsoft Research Asia, China Frédéric Magniez, Université Paris Diderot, France Kazuhisa Makino, Kyoto University, Japan Elvira Mayordomo, Universidad de Zaragoza, Spain Ulrich Meyer, Goethe University Frankfurt am Main, Germany Wolfgang Mulzer, Free University Berlin, Germany Viswanath Nagarajan, University of Michigan, USA Vicky Papadopoulou, European University Cyprus, Cyprus Michał Pilipczuk, University of Bergen, Norway Liam Roditty, Bar-Ilan University, Israel Ignaz Rutter, Karlsruhe Institute of Technology, Germany Rocco Servedio, Columbia University, USA Jens Schmidt, TU Ilmenau, Germany Bettina Speckmann (chair), TU Eindhoven, The Netherlands Csaba D. Tóth, California State University Northridge, USA Takeaki Uno, National Institute of Informatics, Japan Erik Jan van Leeuwen, Max-Planck Institut für Informatik, Germany Rob van Stee, University of Leicester, UK Ivan Visconti, University of Salerno, Italy Track B: Logic, semantics, automata and theory of Programming ------------------------------------------------------------- Andreas Abel, Chalmers and Gothenburg University, Sweden Albert Atserias, Universitat Politècnica de Catalunya, Spain Christel Baier, TU Dresden, Germany Lars Birkedal, Aarhus University, Denmark, Luís Caires, Universidade Nova de Lisboa, Portugal James Cheney, University of Edinburgh, UK Wei Ngan Chin, National University of Singapore, Singapore Ugo Dal Lago, University of Bologna, Italy Thomas Ehrhard, CNRS, Université Paris Diderot, France Zoltán Ésik, University of Szeged, Hungary Xinyu Feng, University of Science and Technology of China, China Wan Fokkink, VU University Amsterdam, The Netherlands Shin-ya Katsumata, Kyoto University, Japan Naoki Kobayashi (chair), The University of Tokyo, Japan Eric Koskinen, New York University, USA Antonín Kučera, Masaryk University, Czech Republic Orna Kupferman, Hebrew University, Israel Annabelle Mclver, Macquarie University, Australia Dale Miller, INRIA Saclay, France Markus Müller-Olm, University of Münster, Germany Andrzej Murawski, Univeristy of Warwick, UK Joel Ouaknine, Univeristy of Oxford, UK Prakash Panangaden, McGill University, Canada Pawel Parys, University. of Warsaw, Poland Reinhard Pichler, TU Vienna, Austria Simona Ronchi Della Rocca, University of Torino, Italy Jeremy Siek, Indiana University, USA Track C: Foundations of networked computation: Models, algorithms and information management ------------------------------------------------------ Ioannis Caragiannis, Univ. Patras, Greece Katarina Cechlarova, Pavol Jozef Safarik Univ., Slovakia Shiri Chechik, Tel Aviv Univ., Israel Yuval Emek, Technion, Israel Sándor Fekete, TU Braunschweig, Germany Pierre Fraigniaud, CNRS and Paris Diderot, France Leszek Gąsieniec, Univ. Liverpool, UK Aristides Gionis, Aalto Univ., Finland Magnús M. Halldórsson (chair), Reykjavik Univ, Iceland Monika Henzinger, Univ. Wien, Austria Bhaskar Krishnamachari, USC, USAL Fabian Kuhn, Freiburg, Germany Michael Mitzenmacher, Harvard Univ, USA Massimo Merro, Univ. Verona, Italy Gopal Pandurangan, NTU, Singapore Pino Persiano, Salerno, Italy R. Ravi, CMU, USA Ymir Vigfusson, Emory Univ., USA Roger Wattenhofer, ETH Zurich, Switzerland Masafumi Yamashita, Kyushu Univ., Japan

1 0

再送：数学基礎論若の手会（10/29締切）
by YOSHIDA Satoru 17 Oct '14

17 Oct '14

皆様重複して受け取られた場合はご容赦ください。数学基礎論若手の会2014のご案内です。数学基礎論を専攻する学生および若手研究者の研究交流を目的とする合宿形式の研究集会です．講演はオリジナルの成果発表に限らず，研究の途中報告や研究内容の紹介など幅広く募集しております．また，これから数学基礎論を勉強したいと思っている方のご参加も歓迎します．多くの方々のご参加およびご講演をお待ちしています．日程：11月19日（水）午後－21日（金）午前場所：鳥取市サイクリングターミナル砂丘の家（鳥取砂丘付近） http://www.city.tottori.lg.jp/www/contents/1198114185831/ 幹事：吉田聡（鳥取環境大学） satoru-y(a)kankyo-u.ac.jp ホームページ： http://misc.kankyo-u.ac.jp/~satoru-y/wakate14/ 申込み要領については上記ホームページをご参照ください。 -- 吉田聡<YOSHIDA, Satoru> 鳥取環境大学

1 0

PSSJ Symposium
by takeuti＠kuis.kyoto-u.ac.jp 16 Oct '14

16 Oct '14

各位科学哲学会シンポジウムの宣伝を致します。シンポジウム「数学を巡る思索」日時：11月15日（土）14:15〜16:45 会場：南山大学名古屋キャンパスＢ棟B11教室ウェブ：http://pssj.info/program/program.html 会費が1000円掛かります。論理学の観点からは、野本和幸氏のデデキントの数概念に関する講演があります。数学としての話はありません。計算機科学としては、蓮尾さんに会えます。産総研竹内泉 takeuti(a)ni.aist.go.jp

1 0

第101回プログラミング研究会開催案内
by Rei Odaira 13 Oct '14

13 Oct '14

Logic-mlの皆さま、 IBMの大平です。＊＊＊＊複数受け取られた方はご容赦ください＊＊＊＊情報処理学会第101回プログラミング研究発表会開催のご案内をさせて頂きます． 11月10日(月)・11日(火)に東京都文京区にて開催されます．最新情報は以下のWEBページに掲載致します． http://staff.aist.go.jp/reynald.affeldt/pro101/index.htm 皆様のご参加をお待ちしております．担当: 大平怜 (日本アイ・ビー・エム東京基礎研究所) AFFELDT Reynald (産業技術総合研究所) ================================================================= 情報処理学会第101回プログラミング研究発表会プログラム ================================================================= 日程: 2014年11月10日(月)・11日(火) 会場: 東京大学創造情報学専攻 I-REF 棟 6階 Hilobby 　　　東京都文京区弥生 1-1-1 　　　http://www.ci.i.u-tokyo.ac.jp/site/?access-j ※ 1件あたり45分 (発表25分，質疑・討論20分) 発表の順番につきましてはまだ確定ではありませんのでご了承ください． 11月10日（月） 2014-3-(1) 10:00-10:45 Unified Memoryを利用したCUDAプログラミングと性能評価土井淳, 今井晴基 (日本アイ・ビー・エム株式会社東京基礎研究所) 2014-3-(2) 10:45-11:30 Ruby向けトレース方式Just-in-timeコンパイラの設計と実装井出真広 (横浜国立大学大学院) 2014-3-(3) 11:30-12:15 Rubyにおけるライトバリアのないオブジェクトを考慮した世代別インクリメンタル GCの実装笹田耕一, 松本行弘 (Heroku, Inc.) 12:15-13:30 昼食 2014-3-(4) 13:30-14:15 A Simple Sufficient Condition for the Completeness of a Heuristic Procedure for Inverse Unfold Problem 長島正憲, 加藤友郁, 酒井正彦, 西田直樹 (名古屋大学) 2014-3-(5) 14:15-15:00 挿抜可能メソッドに基づく統一的な抽象単位複合機構久野靖 (筑波大学ビジネスサイエンス系) 15:00-15:15 休憩 15:15-16:30 CS領域奨励賞授与式パネルセッション「PROのこれまで目指したことと目指すべきもの」登壇者（予定）：　萩谷昌己（東京大学）　上田和紀（早稲田大学）　河内谷清久仁（日本アイ・ビー・エム株式会社）　南出靖彦（筑波大学；主査）　西崎真也（東京工業大学；司会） 18:00-20:00 懇親会 11月11日（火） 2014-3-(6) 09:30-10:15 CとLuaを容易に埋め込むための言語LuCa 谷村明, 岩崎英哉 (電気通信大学大学院情報理工学研究科) 2014-3-(7) 10:15-11:00 C#プログラム実行時書き換えによるコンテキスト指向プログラミングの実現谷川郁太 (東海大学), 小倉信彦 (東京都市大学), 菅谷みどり (芝浦工業大学 ), 渡辺晴美 (東海大学) 11:00-11:15 休憩 2014-3-(8) 11:15-12:00 グラフ問題を効率的に解くためのハードウェアトランザクショナルメモリの利用小林哲, 佐藤重幸, 岩崎英哉 (電気通信大学大学院情報理工学研究科) 2014-3-(9) 12:00-12:45 Tracing Packrat Parsing 倉光君郎 (横浜国立大学) ================================================================= 大平　怜 (Rei Odaira), Ph.D. IBM Research - Tokyo Phone: +81-3-5144-2847

1 0

TPP2014: 2nd Announcement and call for participation
by Jacques Garrigue 09 Oct '14

09 Oct '14

皆様、 TPP2014の案内をお送りします。更新点は - TPP2014のHPにAdam Chlipala氏の講演タイトル等を掲示しました. http://imi.kyushu-u.ac.jp/lasm/tpp2014/index_ja.html - TPPMARKの問題を掲示し証明を募集しています. 　証明支援系, 解き方を問わず, みなさまの多くの証明例を募集しています. 　よろしく, お願いします. 投稿された証明はclosedなrepositoryに投稿者のみ見えるようにしています. 開催時には全てをopenにさせて頂きます. - 学生の講演者へ若干の旅費の援助を計画しています. 援助を希望される学生の方は, 溝口 tpp2014(a)imi.kyushu-u.ac.jp までご相談下さい. その際には, 手続きの都合上, 10月末までに講演申し込みをお願いします. みなさまの参加をお待ちしています. お気づきの点, ご質問等ありましたら, お知らせ下さい. TPP2014幹事 (溝口佳寛) ========================================================================= 研究集会「高信頼な理論と実装のための定理証明および定理証明器」案内　　　　　　　　　　　　　　　　　　　(English version is below.) 12月3日(水)-5日(金)に九州大学西新プラザにて, 研究集会「高信頼な理論と実装のための定理証明および定理証明器」を開催します. 皆様のご参加をお待ちしています. 日時：2014年 12月3日(水)13:00 〜 12月5日(金)17:00 (予定) 場所：九州大学・西新プラザ (福岡市早良区西新2-16-23) http://bit.ly/QdaiNishijin 福岡空港から地下鉄で西新駅まで約20分, その後, 徒歩約10分. プログラム：詳細は未定(準備中)です. みなさまのご講演をお待ちしています. Adam Chlipala氏 (MIT, USA), Cyril Cohen 氏 (Univ. Gothenburg, Sweden) をお招きして, Coqおよび Ssreflect, MathCompに関する御講演を頂く予定です. 参加者と講演の数を大体把握しておきたいと思いますので，参加される方は 10月末までに下の参加申し込みを下記メールアドレスまでお送りください．参加者には，できるだけ講演していただければと思います．申込み・問い合わせ先: tpp2014(a)imi.kyushu-u.ac.jp (溝口佳寛(九州大学)) URL: http://imi.kyushu-u.ac.jp/lasm/tpp2014/index_ja.html (注. 作成途中です.「TPP2014 数学」で検索してみて下さい.) ------------------------------------------------------------------------- TPP 2014 参加申し込みお名前：ご所属：講演　：する／しない懇親会：参加する／参加しない講演する場合タイトル：（講演のタイトルが決まっていなければ，TBAでもかまいません．決まったらご連絡ください．）講演希望日: (○/×) 12/3 (○/×) 12/4 (○/×) 12/5 その他(ご意見/ご要望ありましたらお願いします): ------------------------------------------------------------------------- ========================================================================= Workshop: Theorem proving and provers for reliable theory and implementations (TPP2014) This is the call for participation for TPP2014, to be held on Dec. 3(Wed) - 5(Fri), 2014 at Kyushu University. Date: 2014/12/03 around 1pm to 12/05 around 3pm Venue: Nishijin Plaza, Kyushu University (2-16-23 Nishijin, Sawara-ku, Fukuoka City) http://bit.ly/QdaiNishijinPDF Invited Speakers: Adam Chlipala (MIT, USA) Cyril Cohen (Univ. Gothenburg, Sweden) If you are planning to attend the meeting, please send the information slip below to the indicated address by the end of October. Submission/questions to: 　　　tpp2014(a)imi.kyushu-u.ac.jp (Yoshihiro Mizoguchi) URL: http://imi.kyushu-u.ac.jp/lasm/tpp2014/ ------------------------------------------------------------------------- TPP 2014 Registration Name: Affiliation: Will give a talk: Yes/No Will attend the party: Yes/No Title of the talk: (If it is not decided yet, TBA is OK.) Which date do you prefer to talk ? 12/3 (OK/NG) 12/4 (OK/NG) 12/5 (OK/NG) Requests for the organizer (if any): ------------------------------------------------------------------------- ========================================================================= -- 〒819-0395 福岡市西区元岡744 九州大学　マス・フォア・インダストリ研究所数理棟B1階 (120室) 准教授　溝口　佳寛 Email. ym(a)imi.kyushu-u.ac.jp http://imi.kyushu-u.ac.jp/~ym/ Tel. 092(802)4402 (事務室)

1 0

ACSI 2015: Deadline extended
by Kohei SUENAGA 26 Sep '14

26 Sep '14

皆様，（複数お受け取りの際はご容赦ください．）京都大学の末永と申します．来年1月につくばで開催されるSACSISの後継のACSI 2015につきまして，登録締切，原稿締切がそれぞれ2週間延長されました．論文登録の時点で未発表の論文はもちろん，他の会議・雑誌に投稿中でも採否未決定であればこれらの論文に含まれる研究成果の投稿が可能とのことです．（ACSIではプロシーディングスを出さないとのことです．）投稿をどうぞご検討くださいませ．末永幸平 -- 2015年1月につくば市で開催するACSI2015につきまして，一般論文の登録〆切，アップロード〆切をそれぞれ二週間延長することにいたしましたので，ご連絡いたします．変更後の日時は下記の通りです． 2014年10月10日(金) 17:00 一般論文登録〆切（延長しました） 2014年10月17日(金) 17:00 一般論文アップロード〆切（延長しました）皆さまからのご投稿をお待ちしています．本メールの末尾に投稿サイトのURL，CFPを記載しています．適宜，ご参照ください．なお，本メールではACSIへの論文投稿に関してよくある質問に回答させて頂きます． Q.　ACSIで投稿可能な論文（研究成果）はどのようなものでしょうか？ A.　ACSI2015の論文登録の時点で未発表の論文や，他の会議・雑誌に投稿中でも採否が未決定の論文については，これらの論文に含まれる研究成果の投稿が可能です．ACSI登録後，開催日までに別会議・雑誌に採録された場合でも，ACSIにおいて発表することができます．詳細は末尾のCFPをご確認ください． Q.　ACSIで発表するメリットはなんでしょうか？研究会との違いはどこにありますか？ A.　ACSIに投稿することによって，査読者から論文や研究に関するコメントをもらうことができます．ACSIのHP（http://acsi.hpcc.jp/2015/committee.html.ja）に記載の通り，ACSI2015のPCは関連分野における当代のエキスパートにより構成されています．こうした専門家に自身の論文を読んでもらい，客観的なコメントをもらえることは研究会では得られないメリットです．また，査読のない研究会とは異なり，PCによって良質な研究であると認定を受けた上で発表できることは，将来の国際会議・学術雑誌への投稿に向けて著者らの自信を深めるものとなりますし，より幅広い聴衆に興味を持って聞いてもらえる可能性もでてきます． Q.　ACSIでの発表論文は引用可能でしょうか？ A.　ACSIでは会議録を発行しませんが，会議参加者に論文のコピーが配布されます．会議録が発行されていない会議における発表を引用している論文は公に見られるものであり，同様の引用形態は可能と考えます．具体的には， XXX, YYY, ZZZ, "Performance.......", ACSI2015, (2015). のような形で引用することができると考えています．どうぞよろしくお願いします． --------------------------------------------------------------------------------- ACSI2015は論文投稿システムにEasyChairを用います． ACSI2015 EasyChairサイトは以下のURLになります． https://www.easychair.org/conferences/?conf=acsi2015 投稿方法の詳細な説明は以下のURLに記載してあります． http://acsi.hpcc.jp/2015/submission_instruction.html.ja (日本語) http://acsi.hpcc.jp/2015/submission_instruction.html.en (English) 重要日程 2014年10月10日(金) 17:00 一般論文登録〆切（NEW） 2014年10月17日(金) 17:00 一般論文アップロード〆切（NEW） 2014年12月上旬一般論文採否通知 2014年12月中旬ポスター論文〆切 2014年12月下旬ポスター論文採否通知（予定） 2015年1月26日(月)～28日(水) ACSI2015開催 ---------------------------------------------------------------------------------------------------- Call for Papers Annual Meeting on Advanced Computing System and Infrastructure: ACSI2015 (http://acsi.hpcc.jp/) 日時: 2015年1月26日(月)－28日(水) 会場: つくば国際会議場主催（予定）（順不同）　（社）情報処理学会・計算機アーキテクチャ研究会 (ARC) 　同・システムソフトウェアとオペレーティングシステム研究会 (OS) 　同・ハイパフォーマンスコンピューティング研究会 (HPC) 　同・プログラミング研究会 (PRO) 【概要】　ACSI (Annual Meeting on Advanced Computing System and Infrastructure)はJSPP, SACSISの系譜を受け継ぐ，情報処理学会のARC, HPC, OS, PROの4研究会が主催する国内会議です．これらの4つの研究会が対象とする研究分野を中心に，広い意味での先進的な計算を支えるシステムや基盤技術を対象分野とします．　ACSIは，従来のSACSISが担っていた対象研究分野における国内最高峰の研究に関する発表や議論の機会を与えるという目的に加え，これらの良質な研究成果を国際的に発信することを支援し，主催4研究会を中心としたコミュニティの国際発信力を高めることを目的とします．その結果，従来のSACSISから以下のような大きな変更があります．　－SACSISからの変更点－　・論文は英語論文とする　・会議録は会議参加者のみに配布し，一般には公開しない．上記の通り，ACSIにおける発表論文は一般公開されません．そこで，ACSIで発表される研究成果は，別途，国際会議や学術論文誌において英語により発表されることを強く推奨いたします．【査読について】　ACSIにおいて募集する一般論文では査読を行います．査読の主たる目的は，ACSIにおける発表の質を一定水準以上に保つこと，限られた発表枠に対する発表の選定，表彰論文の選出となります．これらに加え，研究に対する客観的な評価やコメントを投稿者が自身の研究において活用し，将来の国際会議・学術論文投稿へ生かすことも目的とします．　なお，査読結果報告に使用する言語は日本語または英語としますが，投稿時に英語による報告を希望する選択を可能とする予定です．【会議録について】　ACSI2015では，一般に公開する会議録を発行しません．但し，各採録論文は，会議参加者のみに対して一定期間（本会議の前後あわせて一週間程度を予定），閲覧可能とします．【一般論文の募集内容】　下記のテーマに関連するオリジナリティ溢れる論文，実装・開発事例等も含め有用性の高い論文，実用性を重視した基盤に関する論文を広く募集します．計算科学アプリケーション数値計算アルゴリズム, ライブラリ大規模データ処理高性能計算環境(スパコン・クラスタ・クラウド) プログラミング言語オペレーティングシステム高速ネットワーキングコンピュータアーキテクチャより詳細な対象研究分野は下記のトラック毎のキーワードをご参照ください．【一般論文の投稿規定・規定スタイル】 (1) IEEEのフォーマット（IEEE conference style，用紙サイズはLetterまたはA4）を用いた10ページ以内の英文による研究論文を募集します．募集対象は，国内外の査読付き雑誌・査読付き会議に既発表/採録決定済みでない論文とします．レターやテクニカルノートなどの，通常の論文とは異なる基準で査読されるカテゴリの発表/投稿も同様の基準で取り扱います．なお，雑誌・会議で既発表/採録決定済みであっても予稿集等がISBN番号あるいはISSN番号を有しない配布物の場合には未発表とみなします． (2) 原稿のテンプレートはhttp://www.ieee.org/conferences_events/conferences/publishing/tem… (3) ページ数は最大で10ページとしますが，将来の投稿予定等の理由から4ページ程度の論文を投稿して頂くことも可能です．ページ数の多寡に関わらず，積極的なご応募をお待ちしています．但し，査読の基準は一律であるため，ページ数が少ないことに起因して提案する内容やその有効性が十分に説明されていない場合には，評価が下がる可能性があります．その点はご留意ください． (4) 使用言語が異なっている，ページ数が大幅に超過している等，規定のフォーマットに従っていない場合にはプログラム委員長の判断で不採択となることがありますのでご注意ください．【一般論文に関する発表】　採択された一般論文の各々について，本会議中に口頭発表を行って頂きます．口頭発表に使用する言語は日本語，英語のいずれでも構いません．また，スライドについても同様とします．聴衆への配慮，国際会議への投稿予定等を総合的に勘案し，発表者各自で適宜使用する言語を選択してください. 【一般論文における表彰】　一般論文では，トラック毎に最大一件のOutstanding Research Awardを選出し，表彰します．　また，学生が第一著者である論文の中からOutstanding Student Research Award一件を選出し，表彰します．なお，Student Research Awardについては，会議における発表者が第一著者でなかった場合，理由を問わず表彰の対象とならないことを付記します．　両賞はいずれも研究内容の質の高さに加え，研究の将来性，実用性を総合的に評価して選出します．論文の完成度よりも研究内容の評価をより重視しますが，論文における論旨の確かさ等，研究内容を他者に的確に伝えているかどうかは評価の対象となります．【ACS論文誌における連携号】　ACSI2015採録通知3週間後頃を目途に投稿を募集する，ACS論文誌（ACSI連携号）を企画します．本連携号では，ACSIへの投稿論文を元にした一般論文の審査をACSIのプログラム委員会がACS編集委員会に協力して行い，通常の投稿論文よりもさらに迅速な審査を目指します．ACSIで発表される研究成果に関する論文投稿先の一つとしてご検討ください．なお，同連携号ではACS論文誌としての基準で審査が行われ，ACSIの論文採録基準と同一ではないことにご留意ください．【ポスター論文】 (1) 一般論文採否決定後，ポスター論文を募集します．投稿受付開始は2014年12月初旬を予定しており，一般論文に準じた形式で分量は英文1～2ページとします．ポスター論文では，構想段階の研究，問題提起などを含めた研究を広く募集し，将来の国際会議への投稿等を視野に入れた参加者間の議論の場を提供します． (2) ポスター論文は英文としますが，会場で貼付するポスターに使用する言語は日本語・英語のいずれでも構いません． (3) 優秀なポスター発表を対象とした表彰を予定しています．プログラム正副委員長および審査を担当するプログラム委員により，ポスター論文の内容およびポスター発表時の審査に基づき選出します．【論文の投稿方法】　投稿方法の詳細な説明を以下のURLに記載しています．　　http://acsi.hpcc.jp/2015/submission_instruction.html.ja (日本語) 　　http://acsi.hpcc.jp/2015/submission_instruction.html.en (English) 　なお，投稿時には，論文の内容に応じて以下の3つの査読トラックのうちの1つを選択していただきます．ただし，列挙されているテーマに属さないなど，トラックの選択が難しい場合には指定しなくてもかまいません．この場合，プログラム委員会で適切なトラックを選択します．また，投稿時にトラックが指定された場合でも，査読に際してプログラム委員会の判断で異なるトラックに移動することもあります．トラックA: アプリケーション, アルゴリズム（トラックチェア: 高橋大介）　計算科学・シミュレーション　数値計算アルゴリズム　数値計算ライブラリ　自動チューニング　大規模データ処理アルゴリズム　省電力アルゴリズム　アルゴリズム耐故障トラックB: プログラミング・システムソフトウェア（トラックチェア: 合田憲人）　オペレーティングシステム　プログラミング言語設計・実装　仮想化技術　データ集約的計算基盤(MapReduce, KVS) 　ファイルシステム　データベース　クラウドコンピューティング　サイバーフィジカルシステム　グリッドコンピューティング　セキュリティ　通信ライブラリ　広域ネットワーキング　大規模システム運用・評価トラックC: システムアーキテクチャ（トラックチェア: 吉瀬謙二）　プロセッサアーキテクチャ　メモリアーキテクチャ　ネットワークアーキテクチャ　ヘテロジニアスアーキテクチャ(GPU, メニーコア) 　リコンフィギャラブルシステム　省電力設計　ディペンダブルシステム　アプリケーション専用アーキテクチャ　組み込みシステム【運営・組織委員】　組織委員長　　朴泰祐（筑波大学）　組織副委員長　　八杉昌宏（九州工業大学）　プログラム委員長　　岩下武史（北海道大学）　プログラム副委員長（一般論文）　　嶋田創（名古屋大学）　プログラム副委員長（ポスター）　　池上努（産業技術総合研究所）　プログラム副委員長（ＡＣＳ論文誌連携）　　鯉渕道紘（情報学研究所）　ローカルアレンジメント委員長　　高野了成（産業技術総合研究所）　会計委員長　　横山大作（東京大学）　広報委員長　　児玉祐悦（筑波大学）　企画展示委員長　　池上努（産業技術総合研究所）　総務委員長　　多田野寛人（筑波大学）【お問い合わせ】　ACSI2015組織委員会 acsi2015 .at. ccs.tsukuba.ac.jp -- 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

HSCC 2014: Call for Papers
by Kohei SUENAGA 26 Sep '14

26 Sep '14

皆様，京都大学の末永と申します．先日お知らせしましたハイブリッドシステムに関する国際会議 HSCC 2014 の締切 (10月20日) まで一ヶ月を切りましたので，再度 CFP をお送りします．アブストラクト締切が 10月13日です．どうぞ投稿をご検討くださいませ．末永幸平 -- 18th International Conference on Hybrid Systems: Computation and Control April 14-16, 2015, Seattle, USA. URL: http://2015.hscc-conference.org/ Important dates Abstract Submission deadline: October 13, 2014. Full Paper Submission deadline: October 20, 2014. (no extensions possible). Rebuttal phase: December 4 to December 7, 2014. Author notification: December 17, 2014. Camera-ready submission: February 3, 2015. Conference dates: April 14-16, 2015. Conference Scope Hybrid Systems: Computation and Control (HSCC) has long been a leading, single-track conference on foundations, techniques, and tools for analysis, control, synthesis, implementation, and applications of dynamical systems that exhibit continuous and discrete (hybrid) dynamics. Applications include cyber-physical systems (CPS), mixed signal circuits, robotics, large-scale infrastructure networks, as well as natural systems such as biochemical and physiological models. In particular, we solicit theoretical as well as applied research papers that present original work combining ideas from computer science and control systems. Topics of interest include, but are not limited to: - Design, synthesis and control - Analysis and verification - Computability and complexity - Programming languages, specification formalisms - Software tool engineering and experimentation - Real-time and resource-aware control for embedded systems - Network science and control over networks - Applications in automotive, avionics, energy, mobile robotics, medical devices, manufacturing, systems biology, transportation, and other areas HSCC 2015 will be part of the 8th CPSWeek (Cyber-Physical Systems Week) to be held in Seattle, USA, collocating 5 conferences: HSCC, the International Conference on Cyber-Physical Systems (ICCPS), the International Conference on Information Processing in Sensor Networks (IPSN), the Conference on High Confidence Networked Systems (HiCoNS), and the Real-Time and Embedded Technology and Applications Symposium (RTAS). Special Issue: Authors of distinguished papers will be invited to submit an extended version of their work for possible publication in a special issue of the journal Nonlinear Analysis: Hybrid Systems. Best Student Paper Award: As established in the previous years, a best student paper award will be given to a contribution which has been primarily authored by a student. Each paper nominated for this award should be co-authored primarily by a student (as certified by the student’s faculty advisor). Repeatability Evaluation: HSCC has a history of publishing strong papers emphasizing computational contributions; however, recreating these computational elements is hard, because details of the implementation are unavoidably absent in the paper. Following a successful inaugural run in 2014, authors of papers accepted to HSCC (in any track) that contain a computational component will be invited to participate in an optional repeatability evaluation process after final submission of the paper in February. Papers that pass will be highlighted at the conference, and all submissions will receive confidential feedback from independent reviewers on any challenges faced in recreating the computational results. Review criteria and suggestions on how to get started on reproducible research are posted at the conference web page (http://2015.hscc-conference.org). Submission Guidelines Submitted papers should present original research that is unpublished and not submitted elsewhere. Regular papers: maximum 10 pages in the 10pt, two-column ACM format. Submission by October 20, 2014 through the EasyChair system. Regular papers should present original research or industrial applications of techniques for design and/or analysis of hybrid systems, or their integration into industrial design flows. Tool and Case-Study papers: maximum 6 pages in the 10pt, two-column ACM format. Submission by October 20, 2014 through the EasyChair system. Tool Papers should describe an implemented tool and its novel features. Case studies should present hybrid systems tools or techniques. Submissions of Regular, Tool and Case-Study papers should be made through the HSCC 2015 EasyChair submission website: https://www.easychair.org/conferences/?conf=hscc2015 Demo/poster abstracts: Approximately 2 pages. Submission by January 10, 2015 through email to hscc2015(a)easychair.org with “HSCC demo/poster submission” in the subject line. Questions should be directed to the same address. Demo/poster abstracts serve the sole purpose of selecting contributions for the demo and poster session and will not be published in the conference proceedings. Program Chairs Antoine Girard, University of Grenoble, France. Sriram Sankaranarayanan, University of Colorado, Boulder, USA. Publicity Chair Sayan Mitra, University of Illinois, Urbana-Champaign, USA. Repeatability Evaluation Chair Ian Mitchell, University of British Columbia, Vancouver, Canada. Program Committee Erika Abraham, RWTH Aachen University, Germany Matthias Althoff , TU Ilmenau, Germany Shun-ichi Azuma, Kyoto University, Japan Hamsa Balakrishnan, MIT, USA Mireille Broucke, University of Toronto, Canada Krishnendu Chatterjee , IST Austria, Austria Thao Dang, VERIMAG, France Jyotirmoy Deshmukh, Toyota Motors, USA Alexandre Donzé , UC Berkeley, USA Georgios Fainekos, Arizona State University, USA Eric Feron, Georgia Institute of Technology, USA Martin Fränzle, Carl von Ossietzky Universität Oldenburg, Germany Eric Goubault, CEA France and Ecole Polytechnique, France Radu Grosu, Vienna University of Technology, Austria Maurice Heemels, TU Eindhoven, Netherlands Jun-ichi Imura, Tokyo Institute of Technology, Japan (Samuel) Qing-Shan Jia, Tsinghua University, PR China Marta Kwiatkowska, Oxford University, England Kim Larsen, Aalborg University, Denmark Javad Lavaei, Columbia University, USA John Lygeros, ETH Zurich, Switzerland Sayan Mitra, University of Illinois at Urbana Champaign, USA Jens Oehlerking , Robert Bosch GmbH, Germany Meeko Oishi, University of New Mexico, USA Necmiye Ozay, University of Michigan, USA Carla Piazza, University of Udine, Italy Andre Platzer , Carnegie Mellon University, USA Pavithra Prabhakar, IMDEA Software Institute, Spain Maria Prandini, Politecnico di Milano, Italy Daniel Quevedo, University of Newcastle, Australia Jörg Raisch, TU Berlin, Germany S Ramesh, General Motors, USA Kohei Suenaga, Kyoto University, Japan Danielle Tarraf, Johns Hopkins University, USA P.S. Thiagarajan, National University of Singapore, Singapore Ufuk Topcu, University of Pennsylvania, USA Ashuthosh Trivedi, IIT Bombay, India Jana Tumova, KTH, Sweden Majid Zamani, Technical University of Munich, Germany Naijun Zhan, Chinese Academy of Sciences, PR China\ Steering Committee Rajeev Alur, University of Pennsylvania, USA Bruce Krogh, Carnegie-Mellon University, USA Oded Maler, Verimag, France Claire Tomlin, University of California Berkeley, USA Werner Damm, OFFIS, Germany -- 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

CFP: PPL2015 第17回プログラミングおよびプログラミング言語ワークショップ論文募集
by Makoto Hamana 25 Sep '14

25 Sep '14

皆様、群馬大学の浜名と申します．来年3月に愛媛県松山市道後温泉で開催される第17回プログラミングおよびプログラミング言語ワークショップのご案内です．より詳細な投稿方法などは決定次第，下記ワークショップ Webページにてお知らせしますので，ぜひご投稿，ご参加をご検討ください． -------------------------------------------------------------------------- 第17回プログラミングおよびプログラミング言語ワークショップ（PPL2015） http://www-kb.is.s.u-tokyo.ac.jp/ppl2015/ 論文募集主催: 日本ソフトウェア科学会プログラミング論研究会日程: 2015年3月4日(水)〜3月6日(金) 会場: 愛媛県松山市道後温泉「道後プリンスホテル」 http://www.dogoprince.co.jp/ PPL2015は，プログラミングおよびプログラミング言語に関する研究者が一堂に会し，最新の研究成果の発表，および新たな研究課題についての討論やアイディア交換等を行うことを目的とした，合宿形式のワークショップです．プログラミングおよびプログラミング言語の理論・設計・実装・処理系などに関する研究発表を，カテゴリ別に幅広く募集します．カテゴリ1: 国内外で未発表の論文の発表カテゴリ2: 国際会議・学術雑誌等で既発表であるが，国内では未発表の研究の紹介カテゴリ3: ポスター・デモ発表（既発表・未発表の別を問いません）カテゴリ4【新規】: サーベイ・チュートリアルの発表（既発表・未発表の別を問いません）カテゴリ1の採択論文の中から，特に独創的なアイディアや顕著な成果を含むものに対して論文賞を授与する予定です．また全論文発表と全ポスター・デモのなかから，聴衆の投票によりそれぞれ，最も優秀な論文プレゼンテーションには発表賞（一般の部，学生の部．既受賞者は除く），最も優秀なポスター・デモにはポスター賞【新規】を授与する予定です．カテゴリ1（国内外未発表論文） ---------------------------- 完成した理論やシステムの研究発表のみならず，萌芽的なアイディアや問題点の提示等も歓迎します．発展途上の研究内容も積極的に採録する方針です（ただし，PPLでの発表として相応しくないと判断される場合は，この限りではありません）．また，カテゴリ1で発表された研究については，会場での討議や査読コメントをもとにその完成度を高め，将来の学術雑誌・会議等での業績に結び付けることを奨励しています．そのため，予稿集の配布は参加者のみへの限定的なものとする予定です．採録された論文は，PPL2015参加者に配布される予稿集に掲載され，参加者のみがアクセス可能な形でWeb上で公開されます（論文へのリンク集ページを作成し，閲覧に必要なパスワードを参加者に連絡します）．カテゴリ1で発表された研究のうち，PPL2015プログラム委員会により優れていると認めるものは，PPL2015終了後（2015年4月下旬予定），「コンピュータソフトウェア」誌のPPL2015推薦論文としての投稿が可能です．推薦論文は，PPL プログラム委員が引き続き査読を行うことによる，迅速な査読プロセスを特長としています．カテゴリ2（国外既発表論文） -------------------------- 査読付の国際会議または学術雑誌等で既発表であるが国内では未発表である研究を紹介する場です．採録決定済みの研究も含みます．PPLへの関連をもとに採否を判定いたしますが，申し込み多数の場合はプログラム委員会での選考により，発表をご遠慮いただく可能性もございますので，その旨をご了承の上ご投稿ください．カテゴリ3（ポスター・デモ発表） ------------------------------ 2時間程度のセッション内でのポスター発表またはデモ発表です．既発表・未発表の別を問いません．PPLへの関連をもとに採録を判定いたします．また，申し込み多数の場合はプログラム委員会での選考により採否を決定します． ※ショートプレゼンテーションは行いませんカテゴリ4（サーベイ・チュートリアル発表）【新規】 ------------------------------------------------ サーベイはプログラミング言語に関連するトピックについての(発表者の研究も含め)研究動向の紹介，チュートリアルはプログラミング言語に関連する基礎事項についての解説を募集します．既発表・未発表の別を問いません．プログラミング言語分野の学生，研究者の研究に役立つような発表を想定しています．分野間の相互理解と全体の底上げとなる事を期待し，新たに設置するものです．PPLへの関連および関連研究への言及をもとに採択を判定いたします．通常発表と同様の30分での発表を予定していますが，採択件数によっては発表者との相談で延長も考慮します． ====================================================================== 投稿・発表申込要領 4つのカテゴリそれぞれに対する投稿方法は以下の通りです．最新の情報は上記 Web ページでご確認ください．カテゴリ1（国内外未発表論文） ---------------------------- 投稿手続きは2段階です．発表申込を行った上で論文提出を行ってください．発表申込先： EasyChair による申込み受付を予定しています．発表申込締切：2014年12月22日(月) 17:00 (JST) 著者名，所属，論文タイトル，論文概要（日本語300〜400字程度もしくは英語 200 words 程度）を提出してください．論文提出締切：2015年1月8日(木) 17:00 (JST) 10ページ程度（最大15ページ）の論文（日本語もしくは英語，PDF形式）を提出してください．採否通知：2015年2月3日(火) 最終原稿提出締切：2015年2月16日(月) 17:00 (JST) 採録された論文の最終原稿の提出方法は，採否通知にてお知らせいたします． (注) カテゴリ1への投稿論文と類似の論文を，他の会議（予稿集を出版するもの）・論文誌などに同時投稿する場合は，査読の有無に関わらず，その旨を発表申込および論文提出の際に明記してください．PPLでは同時投稿の事実のみをもって論文を不採録とすることはありませんが，採否の決定に利用する場合があります（他の会議との重複を避けるため，発表内容についての条件付採録とすることもあります）．カテゴリ2（国外既発表論文） -------------------------- 発表申込時に採録が決定している国際会議および国際学術雑誌の発表論文が対象です．理論系だけではなく実装系の論文の投稿も歓迎いたします．発表申込方法につきましては PPL2015 の Web ページをご確認ください．発表申込締切：2015年1月23日(金) 17:00 (JST) 原論文（ページ数不問，PDF形式）とabstract（テキスト形式）を，著者名，所属，論文タイトル，原論文の出典（発表会議名，掲載済／予定の別等）と併せてご提出ください．採否通知：2015年2月5日(木) カテゴリ3（ポスター・デモ発表） ------------------------------------------ ポスター・デモの区別を行わずに募集いたします．デモを行う場合は，発表概要においてその旨をご説明ください．発表申込方法につきましては PPL2015 の Web ページをご確認ください．発表申込締切：2015年2月9日(月) 17:00 (JST) 希望する発表形態（ポスター・デモの別）を明記して，著者名，所属，発表タイトル，発表概要（200〜300字程度）をご提出ください．採否通知：2015年2月16日(月) カテゴリ4（サーベイ・チュートリアルの発表） ------------------------------------------ サーベイまたはチュートリアルの提案を募集いたします．発表申込み時に概要の提出を行ってください．概要の内容，PPLへの関連および関連研究への言及をもとに採録を判定いたします．発表申込締切：2015年1月23日(金) 17:00 (JST) 著者名，所属，発表タイトル，発表の概要 (1〜3ページ，PDF形式．目的，カバーする話題，想定する聴衆，必要な知識の記述を含むもの)をご提出ください．またもしその内容の既発表のサーベイ，チュートリアル，解説等があれば，その文書（ページ数不問，PDF形式），著者名，所属，タイトル，文書の出典（発表雑誌，掲載済／予定の別等）も併せてご提出ください．採否通知：2015年2月5日(木) 問い合わせ先：ppl2015-oc [at] kb.is.s.u-tokyo.ac.jp （[at]を@に置き換えてください） ====================================================================== プログラム委員会青戸等人東北大学浅田和之東京大学岩崎英哉電気通信大学鵜川始陽高知工科大学馬谷誠二京都大学 [プログラム共同委員長] 大岩寛産業技術総合研究所亀山幸義筑波大学河内谷清久仁日本IBM 久野靖筑波大学木村大輔国立情報学研究所宋剛秀神戸大学塚田武志 University of Oxford 中田景子 Tallinn University of Technology 浜名誠群馬大学 [プログラム共同委員長] 平井洋一 FireEye 平石拓京都大学藤田憲悦群馬大学星野直彦京都大学増原英彦東京工業大学渡部卓雄東京工業大学組織委員会松田一孝東京大学 [組織委員長] 浜名誠群馬大学 [プログラム共同委員長] 馬谷誠二京都大学 [プログラム共同委員長] 末永幸平京都大学上野雄大東北大学海野広志筑波大学木村大輔国立情報学研究所 [ポスターセッション幹事] --------------------------------------------------------------------------

1 0

数学会からのお知らせ
by shioya＠math.tsukuba.ac.jp 22 Sep '14

22 Sep '14

日本数学会数学基礎論および歴史分科会会員の皆様今週の数学会に関するお知らせが２件あります。（重複投稿をご容赦ください）１．台風16号への対応について２．プロジェクターの利用とバス便に関してよろしくお願いいたします。塩谷真弘（2014年度分科会連絡責任評議員） %%%%%%%%%%%%%%%%% １．台風16号への対応について以下の文書はWeb上　　　　　http://mathsoc.jp/meeting/hiroshima14sept/typhoon16.html でも公開しています。 2014年度秋季総合分科会における台風第16号への対応について　　　　　　　　　　　　　　　　　　　　　　　　　　　　　2014年9月21日会員各位台風第16号（フォンウォン）が西日本に接近しつつあります．日本数学会理事会では9月25日（木）から広島大学東広島キャンパスで開催されます秋季総合分科会への影響について懸念をしておりますが、まず以下のようにこの件に関わる広報、周知のチャンネルを確立しておきたいと思います．以下の対応が杞憂で終わってくれたらと祈っておりますが、念のために会員内で周知をお願いいたします．秋季総合分科会の開催に関して重要なお知らせは以下の手段によって会員にお知らせします．（１）スマートフォンでない携帯電話でも読めるページ　　　http://mathsoc.jp/i/ （２）大会の公式ページ　　　http://mathsoc.jp/meeting/hiroshima14sept/ また極めて重要なお知らせはニュースレターの号外でもご案内いたします．このとき同時に、講演者にも講演申し込みに際して登録されたアドレスにメールをお送りします．秋季総合分科会に参加される方は可能な限りActivation Systemからニュースレターの購読を選択してくださいますようお願いいたします．また台風の交通機関への影響により講演をキャンセルされる場合は、大会本部に電子メールアドレス　　program14sept(a)mathsoc.jp または電話番号 090-1791-3483　までご連絡ください．　　　　　　　　　　　　　　　　　　　　　　日本数学会理事長　舟木　直久 %%%%%%%%%%%%%%%%% ２．プロジェクターの利用とバス便に関してウェブページ http://mathsoc.jp/meeting/hiroshima14sept/news20140920.html に同様の告知が準備してあり、続報はこのページに記載することになっています。 (1) 講演に関するお願い：USBメモリに講演ファイルを入れてご持参ください． 9月19日まで広島大学総合科学部で日本分析化学会が開催されていましたが，会場の総合科学部の設備が最新の機器に対応していないせいもあり，コンピュータとプロジェクタの接続トラブルが頻繁に起こったとの報告がありました．（ノートパソコンのうちおおよそ9割以上は正常に接続されていますが，特に新しいコンピュータ，Mac，との接続トラブルが絶えなかったそうです．なお， HDMIケーブルは使用できません．）そのため，多くの会場では，USBメモリを使って予備のコンピュータに講演ファイルを移し，対応したとのことです．つきましては，可能な限り，次のことをお願いできないでしょうか？＊トラブルに備えて，講演ファイルをpdfファイル化し，USBメモリに入れてご持参　頂き，講演時にはUSBを携行してください．プロジェクタ接続に困難が生じたときに　予備機にUSBをつなぐことにより講演ができるようにするためです．　（ただしpdf ファイルに埋め込んだ動画の動作については保証しかねます．）　なお，ファイル名はプログラムの講演番号（2桁）から始めてご自分のお名前も入れて 01数学太郎.pdf 　のようにしてください．＊接続に不安がある方や，（追伸2）に記した接続上の注意に対応できない方は，　講演開始時間前や休憩時間に，実行委員会で用意するコンピュータに講演ファイル　を移し，そちらのコンピュータをご使用ください． (2) JR西条駅と広島大学を結ぶバス：小銭２９０円をご用意ください．日本数学会開催中，JR西条駅と広島大学を結ぶバスは，同時期に開催する他学会があるため，混雑することが予想されており，臨時バスが増発されます．バスの時刻表は下記URLに掲載されていますので，印刷してお持ちください．　　http://mathsoc.jp/meeting/hiroshima14sept/bus_timetable.pdf 講演会場である総合科学部の最寄りのバス停は「広大西口」であり，広島大学内の最初のバス停である「広大中央口」ではありません．また，西条駅から広島大学までのバス運賃は290円です．両替による混雑を避けるために，小銭をご用意いただければ幸いです．なおバスで利用できるICカードは PASPYとICOCAのみです（Suicaなど他のICカードはご利用になれません）．以上，どうぞ宜しくお願い申し上げます．　　　　　　　　　　　　　　　　　　秋季総合分科会実行委員長　作間　誠追伸1 学会開催直前の時期ですので，この件に関して個別にお問い合わせ頂きましても，ご対応はいたしかねますのでご了承ください．ただし、今後新たな注意事項がでてきましたら，ウェブページ http://mathsoc.jp/meeting/hiroshima14sept/news20140920.html を通して会員の皆様にお知らせする予定です．追伸2 （接続上の注意）＊HDMIケーブルには対応していません．こちらで準備したRGBケーブルをご使用ください．＊パソコンの解像度を1024 × 768に設定してください．＊液晶プロジェクターとパソコンは，ミニD-sub15ピンコネクタ（ピンが5本×3段の　通常のもの）で接続します．　パソコン側にメスコネクタがない場合，接続に必要なアダプタは各自ご持参ください．　薄型WindowsノートやMacを使用される方は，接続変換コネクタを必ずご持参ください．追伸3（パソコンとプロジェクターの不適合について　　　　　　　　　　　　　　　　　--接続トラブルに関する日本分析化学会からの連絡）多くのPCはプロジェクターに正しく信号が入り問題なく投影できましたが，いくつかのパソコンではトラブルが発生しています．その例を下記にしるしておきます． a.　最近のノートＰＣでは昔のVGA出力（D-sub15コネクタ）ではなくHDMIという規格のモニター出力のノートPCがあります．この場合はHDMIとD-sub15の変換コネクタを使うことになりますがこのようなケースでかなりの確率でプロジェクターへの出力がうまくいかないようです．またVGA出力（D-sub15コネクタ）とHDMIの両方をもつノートPC（例えばPanasonicのレッツノートのシリーズ）でもHDMI優先でVGAをまともに認識しないものがあるそうです. 有効な対策はないようで、別のPCへデータを移して映写する他ないようです． b.　MacBookAirの一部では時としてプロジェクターへ映写が大変暗くほとんど見えない程度にしか写らないことがあります（これはまれな現象です）．私の座長中にも1件発生し、いろいろやったのですが結果的にうまく映写することはできませんでした．しかし、これについては、Macがバッテリ駆動の時ではモニター出力信号が弱くなるためであり「ACアダプタを接続すると回避できる可能性がある」そうです． c.接触不良などの物理的な問題うまく写らない場合の一つの原因としてコネクタの接触不良もあるようです．差し直すとうまくいったとの話も何件かあったようです．Macのアダプタを差し直すとうまくいったとの話もありました．

1 0

再送：数学基礎論若手の会
by YOSHIDA Satoru 22 Sep '14

22 Sep '14

皆様重複して受け取られた場合はご容赦ください。数学基礎論若手の会2014のご案内です。数学基礎論を専攻する学生および若手研究者の研究交流を目的とする合宿形式の研究集会です．講演はオリジナルの成果発表に限らず，研究の途中報告や研究内容の紹介など幅広く募集しております．また，これから数学基礎論を勉強したいと思っている方のご参加も歓迎します．多くの方々のご参加およびご講演をお待ちしています．日程：11月19日（水）午後－21日（金）午前場所：鳥取市サイクリングターミナル砂丘の家（鳥取砂丘付近） http://www.city.tottori.lg.jp/www/contents/1198114185831/ 幹事：吉田聡（鳥取環境大学） satoru-y(a)kankyo-u.ac.jp ホームページ： http://misc.kankyo-u.ac.jp/~satoru-y/wakate14/ 今年度若手の会申込み要領については上記ホームページをご参照ください。 -- 吉田聡<YOSHIDA, Satoru> 鳥取環境大学

1 0

QIT31口頭発表締切延長
by NISHIMURA Harumichi 22 Sep '14

22 Sep '14

logic-mlの皆様，第31回量子情報技術研究会口頭発表申込の締切が 10月3日（金）に延長されました．詳しくは以下のご案内をご覧ください．ご応募のほどよろしくお願いいたします．名古屋大学大学院情報科学研究科西村治道 ---------------------------------------------------------- 第31回量子情報技術研究会(QIT31) ※口頭講演の申込締切を10/3(金)まで延長しましたので，奮ってご応募ください．研究会の内容情報科学と量子力学を融合させた新しい分野，量子情報科学に関する研究会です．情報を担う物理系の量子力学的側面を積極的に活かした新しい情報処理原理の研究とそこから開かれる新しい学問体系の構築および新しい情報技術パラダイムの創生を目指して，情報科学，物理学，光エレクトロニクスを含む理学，工学，数理科学に携わる研究者間に自由な討論の場を提供し，この研究分野の発展を図ることを目的としています．第31回研究会を下記のように開催いたします．現在この分野で活躍する研究者は勿論，自分の研究資産が何らかの形で使えそうだと予感している研究者・技術者など，広く関連する分野の研究者・技術者からの発表を募集致します．聴講のみの参加も歓迎致しますので，奮ってお申し込みください．日時: 2014年11月17日(月)～18日(火) 会場: 東北大学さくらホール (〒980-8577 仙台市青葉区片平２－１－１東北大学片平キャンパス内) 発表募集分野 (申し込み状況によっては査読の可能性あり) 量子情報，量子計算，量子暗号など広く量子情報技術に関わる理論的研究，実験的研究，計算機科学的研究，数学的研究，および，その他関連分野．定員: 200名参加費: 事前振込み一般4,000円，学生1,000円 (当日会場払いは一般5,000円，学生2,000円) (懇親会は別途) 研究会参加申込要領参加申込は下記 Web にて受付けます： http://staff.aist.go.jp/s-kawabata/qit/ 講演 (口頭，ポスター) の申込，予稿集原稿 PDF の提出は，電子情報通信学会の Web システムを使用する予定．【口頭講演申込締切】 2014年10月3日(金) ※延長しました．なお，申込数が予定数に達した時点で締め切る場合があります．【ポスター講演申込締切】 2014年10月3日(金) 【予稿原稿提出締切】 2014年10月3日(金) 【参加申込締切】 2014年10月24日(金) 【問合せ先】枝松圭一 (東北大学電気通信研究所) 三森康義 (東北大学電気通信研究所) 吉田真人 (東北大学電気通信研究所) Email: qit31(a)quantum.riec.tohoku.ac.jp 主催: 量子情報技術時限研究専門委員会 (委員長: 枝松圭一 (東北大学)) 共催: 応用物理学会量子エレクトロニクス研究会東北大学電気通信研究所 ―――――――――――――――――――――――――――――

1 0

Prof. Aleksy Schubert at NII Logic Seminar
by Makoto Tatsuta 22 Sep '14

22 Sep '14

Prof. Aleksy Schubert at NII Logic Seminar Date: September 26, 2014, 14:00--16:00 Place: National Institute of Informatics, Room 1716 (17th floor) 場所: 国立情報学研究所 17階 1716室 (半蔵門線,都営地下鉄三田線・新宿線神保町駅または東西線竹橋駅より徒歩5分) (地図 http://www.nii.ac.jp/about/access/) Speaker: Prof. Aleksy Schubert (University of Warsaw) (1) Title: Undecidability and complexity in fragments of first-order intuitionistic logic Abstract: In case of classical first-order logic there is a full characterisation of decidable and undecidable classes of formulae depending on the quantifier prefix and the vocabulary that is used. First-order logic in intuitionistic case lacks this kind of classification since there is no prefix normal form and actually the prenex fragment of the logic is in many cases much weaker than the general calculus. However, there is one meaningful stratification of the intuitionistic logic similar to the prenex form. We can consider classes of formulae that would result in a particular prefix of quantifiers when transformed using classical equivalences. The status of decidable and undecidable cases within this stratification will be presented as well as the complexity of known subcases. (2) Title: Verification of programs using Frama-C and Why3 Abstract: Frama-C is a tool that makes it possible to do a variety of analyses for C programs annotated with C specification language called ACSL (The ANSI/ISO C Specification Langage). One of the possible ways to use Frama-C is to generate verification conditions for appropriately defined Hoare logic that is in line with C programming language semantics. These verification conditions can subsequently be discharged by Why3 tool that makes it possible to manage the proving of necessary properties. During the talk I will present an overview of the tools and show a number of interesting examples to demonstrate how these tools work together to make possible verification of practical programs. 問合せ先: 龍田真 (国立情報学研究所) e-mail: tatsuta(a)nii.ac.jp http://research.nii.ac.jp/~tatsuta

1 0

研究集会「高信頼な理論と実装のための定理証明および定理証明器」案内
by Yoshihito Tanaka 22 Sep '14

22 Sep '14

九州大学マス・フォア・インダストリ研究所の溝口先生の代理で投稿いたします． ========================================================================= 研究集会「高信頼な理論と実装のための定理証明および定理証明器」案内　　　　　　　　　　　　　　　　　　　(English version is below.) 12月3日(水)-5日(金)に九州大学西新プラザにて, 研究集会「高信頼な理論と実装のための定理証明および定理証明器」を開催します. 皆様のご参加をお待ちしています. 日時：2014年 12月3日(水) 〜 12月5日(金) 場所：九州大学・西新プラザ (福岡市早良区西新2-16-23) http://bit.ly/QdaiNishijin 福岡空港から地下鉄で西新駅まで約20分, その後, 徒歩約10分. プログラム：詳細は未定(準備中)です. みなさまのご講演をお待ちしています. Adam Chlipala氏 (MIT, USA), Cyril Cohen 氏 (Univ. Gothenburg, Sweden) をお招きして, Coqおよび Ssreflect, MathCompに関する御講演を頂く予定です. 参加者と講演の数を大体把握しておきたいと思いますので，参加される方は 10月半ばまでに下の参加申し込みを下記メールアドレスまでお送りください．参加者には，できるだけ講演していただければと思います．申込み・問い合わせ先: tpp2014(a)imi.kyushu-u.ac.jp (溝口佳寛(九州大学)) URL: http://coop-math.ism.ac.jp/event/2014E04 (注. 作成途中です.「TPP2014 数学」で検索してみて下さい.) ------------------------------------------------------------------------- TPP 2014 参加申し込みお名前：ご所属：講演　：する／しない懇親会：参加する／参加しない講演する場合タイトル：（講演のタイトルが決まっていなければ，TBAでもかまいません．決まったらご連絡ください．）講演希望日: (○/×) 12/3 (○/×) 12/4 (○/×) 12/5 その他(ご意見/ご要望ありましたらお願いします): ------------------------------------------------------------------------- ========================================================================= Workshop: Theorem proving and provers for reliable theory and implementations (TPP2014) This is the call for participation for TPP2014, to be held on Dec. 3(Wed) - 5(Fri), 2014 at Kyushu University. Date: 2014/12/03 around 1pm to 12/05 around 3pm Venue: Nishijin Plaza, Kyushu University (2-16-23 Nishijin, Sawara-ku, Fukuoka City) http://bit.ly/QdaiNishijinPDF Invited Speakers: Adam Chlipala (MIT, USA) Cyril Cohen (Univ. Gothenburg, Sweden) If you are planning to attend the meeting, please send the information slip below to the indicated address by mid-October. Submission/questions to: 　　　tpp2014(a)imi.kyushu-u.ac.jp (Yoshihiro Mizoguchi) URL: http://coop-math.ism.ac.jp/event/2014E04 (Tentative Japanese HP. Revised English HP will be notified later.) ------------------------------------------------------------------------- TPP 2014 Registration Name: Affiliation: Will give a talk: Yes/No Will attend the party: Yes/No Title of the talk: (If it is not decided yet, TBA is OK.) Which date do you prefer to talk ? 12/3 (OK/NG) 12/4 (OK/NG) 12/5 (OK/NG) Requests for the organizer (if any): ------------------------------------------------------------------------- =========================================================================

1 0

Prof. Aart Middeldorp at NII Logic Seminar
by Makoto Tatsuta 17 Sep '14

17 Sep '14

Prof. Aart Middeldorp at NII Logic Seminar Date: September 22, 2014, 14:00--16:00 Place: National Institute of Informatics, Room 2005 (20th floor) 場所: 国立情報学研究所 20階 2005室 (半蔵門線,都営地下鉄三田線・新宿線神保町駅または東西線竹橋駅より徒歩5分) (地図 http://www.nii.ac.jp/about/access/) Speaker: Prof. Aart Middeldorp (University of Innsbruck) Title: Proving AC Termination by Knuth-Bendix Orders Abstract: Equational theories that contain axioms expressing associativity and commutativity (AC) of certain operators are ubiquitous. Theorem proving methods in such theories rely on well-founded orders that are compatible with the AC axioms. In this talk we consider various definitions of AC-compatible Knuth-Bendix orders. The orders of Steinbach and of Korovin and Voronkov are revisited. The former is enhanced to a more powerful AC-compatible order and we modify the latter to amend its lack of monotonicity on non-ground terms. We present new complexity results and compare the various orders on problems in termination and completion. The talk is based on joint work with Nao Hirokawa, Sarah Winkler, and Akihisa Yamada. 問合せ先: 龍田真 (国立情報学研究所) e-mail: tatsuta(a)nii.ac.jp http://research.nii.ac.jp/~tatsuta

1 0

JAIST Logic Seminar Series (18th Sep. 2014: Tadeusz Litak on Relational lattices)
by Katsuhiko Sano 14 Sep '14

14 Sep '14

皆様、 FAU Erlangen-Nürnberg の Tadeusz Litak さんの講演のお知らせです。ふるってご参加ください。問い合わせ先：佐野勝彦北陸先端科学技術大学院大学情報科学研究科 e-mail: v-sano(a)jaist.ac.jp ---------------------------------------------------------------------------------------------------- * JAIST Logic Seminar Series * Date: Thursday, 18th September, 2014, 15:10-17:00 Place: JAIST Collaboration Room 6 (I57-g) (Access:http://www.jaist.ac.jp/english/location/access.html) Speaker: Tadeusz Litak (Department Informatik, Technische Fakultät, FAU Erlangen-Nürnberg, Germany) Title: Relational lattices Abstract: We study an interpretation of lattice connectives as natural join and inner union between database relations with non-uniform headers. We show that this interpretation proposed by database experts (Vadim Tropashko from Oracle) yields a class of lattices which has not been considered in the existing lattice-theoretical literature. We discuss axiomatizability and decidability of their (quasi-)equational theory and propose an equational axiomatization for a corresponding abstract algebraic class. It turns out that addition of just the “header constant” to the lattice signature already allows mimicking the Maddux technique for cylindric algebras and encode the word problem for semigroups in the quasiequational theory. Relational lattices, however, are not as intangible as one may fear: for example, they do form a pseudoelementary class. We also apply the tools of Formal Concept Analysis and investigate standard contexts of relational lattices, obtaining, e.g., results on their subdirect irreducibility. This is a joint work with Szabolcs Mikulas and Jan Hidders ----------------------------------------------------------------------------------------------------

1 0

$B?t3X4pACO@%5%^!<%9%/!<%k(B 2014
by fuchino＠diamond.kobe-u.ac.jp 12 Sep '14

12 Sep '14

皆様他の場所での掲示で既に御存知のことと思いますが，今年の数学基礎論サマースクールが 9月16日(火)から 9月19日(金) にかけて神戸大学で開催されます．今年のテーマは集合論，特に強制法理論の入門です．詳しくは： http://kurt.scitec.kobe-u.ac.jp/~fuchino/set-theory2014/kisoron-summerschoo… をごらんください．参加費参加登録等は必要ありません．興味のある方はぜひ御参加ください．この集会のプログラム： http://kurt.scitec.kobe-u.ac.jp/~fuchino/set-theory2014/program-summerschl1… なお，9月18日(木) 18:00--20:00 に立食の懇親会を予定しております (子細については上のプログラムを御覧ください)．参加を御希望の方はサマースクールの最初の二日の間に参加登録と実費 (3000円) の支払をお願いします．懇親会のみに参加される方も歓迎します．ただし，その場合には，レストランへの人数の登録の関係上，私 fuchino(a)diamond.kobe-u.ac.jp と懇親会のアレンジメントを担当している酒井拓史さん hsakai(a)people.kobe-u.ac.jp の両方に，9月23日午後までにメールで御連絡ください． -- best regards Saka\'e Fuchino (渕野昌) ------------------------------------------------------------------------- Kobe University Graduate School of System Informatics Rokko-dai 1-1, Nada, Kobe 657-8501 Japan e-mail: fuchino(a)diamond.kobe-u.ac.jp web page: http://kurt.scitec.kobe-u.ac.jp/~fuchino/ -------------------------------------------------------------------------

1 0

CFP: JURISIN2014 〆切延長
by Satoshi Tojo 09 Sep '14

09 Sep '14

Apologies if you receive this CFP multiple times. -------------------------------------------- !!Deadline Extention!! Due to many requests, we will extend the deadline for Eighth International Workshop on Juris-informatics (JURISIN 2014). New Submission Deadline: September 17, 2014 Conference date: November 23 - 24, 2014 venue: Raiosha Building, Keio University Kanagawa, Japan Aims and Scope Juris-informatics is a new research area which studies legal issues from the perspective of informatics. The purpose of this workshop is to discuss both the fundamental and practical issues among people from the various backgrounds such as law, social science, information and intelligent technology, logic and philosophy, including the conventional "AI and law" area. We solicit unpublished papers on theories, technologies and applications on juris-informatics. Topics Relevant topics include, but are not limited to, the following: Model of legal reasoning Argumentation / Negotiation / Argumentation agent Legal term ontology Formal legal knowledge-base / Intelligent management of legal knowledge-base Translation of legal documents Information retrieval of legal texts Computer-aided law education Use of Informatics and AI in law Legal issues on ubiquitous computing / multi-agent system / the Internet Social implications of use of informatics and AI in law Natural language processing for legal knowledge Verification and validation of legal knowledge systems Any theories and technologies which is not directly related with juris-informatics but has a potential to contribute to this domain Bar Exam Competition This year, JURISIN invites participation in a legal information extraction and entailment competition. Previous conferences/workshops have not conducted such a shared task on a large legal data collection, so we hope that the 2014 workshop will help establish a major experimental effort in the legal information extraction/retrieval field. The motivation for the competition is to help create a research community of practice for the capture and use of legal information. Please visit the homepage of the bar exam competition. http://webdocs.cs.ualberta.ca/~miyoung2/jurisin_task/index.html Invited Speakers Bart Verheij (Stanford University/ University of Groningen) Riichiro Mizoguchi (Japan Advanced Institute of Science and Technology) Submissions: the submission site via EasyChair is now open. We welcome and encourage the submission of high quality, original papers, which are not simultaneously submitted for publication elsewhere except as a submission to JURIX 2014 (The 27th International Conference on Legal Knowledge and Information Systems). The double submission policy with JURIX 2014 is as follows: Papers being submitted both to JURISIN2014 and JURIX2014 must note this on the title page. A paper to be presented at JURISIN2014 must be withdrawn from JURIX2014 and vice versa according to the choice by the authors. If the authors do not follow this double submission policy, the paper by the authors will not be included in the proceedings of JURISIN 2014. Post Proceedings: Selected papers will be published via Springer Verlag LNAI. In addition, the authors have an opportunity to submit their full versions to the special issue of Journal of New Generation Computing. The detail will be announced soon. Workshop Chair Satoshi Tojo, Japan Advanced Institute of Science and Technology(JAIST), Japan Organizing Committee Members Katsumi Nitta, Tokyo Institute of Technology, Japan Ken Satoh, National Institute of Informatics and Sokendai, Japan Satoshi Tojo, Japan Advanced Institute of Science and Technology(JAIST), Japan Katsuhiko Sano, Japan Advanced Institute of Science and Technology(JAIST), Japan Advisory Committee Members Trevor Bench-Capon, The University of Liverpool, UK Tomas Gordon, Fraunfoher FOKUS, Germany Henry Prakken, University of Utrecht & Groningen, The Netherlands John Zeleznikow, Victoria University, Australia Robert Kowalski, Imperial College London, UK Kevin Ashley, University of Pittsburgh, USA Program Committee Members Satoshi Tojo, Japan Advanced Institute of Science and Technology(JAIST), Japan Tokuyasu Kakuta, Nagoya University, Japan Hanmin Jung, Korea Institute of Science and Technology Information(KISTI), Korea Minghui Xiong, Sun Yat-sen University, China Minghui Ma, Southwest University, China Nguyen Le Minh, Japan Advanced Institute of Science and Technology(JAIST), Japan Katsuhiko Toyama, Nagoya University, Japan Makoto Nakamura, Nagoya University, Japan Marina De Vos, University of Bath, UK Guido Governatori, NICTA, Australia Paulo Novais, University of Minho, Portugal Seiichiro Sakurai, Meiji Gakuin University, Japan Ken Satoh, National Institute of Informatics and Sokendai, Japan Thomas Ågotnes, University of Bergen, Norway Robert Kowalski, Imperial College London, UK Katsuhiko Sano, Japan Advanced Institute of Science and Technology(JAIST), Japan Katumi Nitta, Tokyo Institute of Technology, Japan Katie Atkinson, University of Liverpool, UK Philip T H Chung, Australasian Legal Information Institute (AustLII), Australia Masahiro Kozuka, Okayama University, Japan Fumihiko Takahashi, Meiji Gakuin University, Japan Baosheng Zhang, China University of Political Science and Law, China Akira Shimazu, Japan Advanced Institute of Science and Technology(JAIST), Japan Home page of JURISIN 2014 http://www.jaist.ac.jp/org/jurisin2014/ ------------------------------------------------------ Satoshi Tojo Japan Advanced Institute of Science and Technology (JAIST)

1 0

CSセミナーin桐生
by Fujita Kenetsu 09 Sep '14

09 Sep '14

(* Apologies for any cross-postings. *) 皆様，群馬大学の藤田と申します．コンピュータ・サイエンスのセミナーのご案内です．どなたでも参加できますので，どうぞお気軽にお越し下さい．問い合わせ先：藤田憲悦 fujita(a)cs.gunma-u.ac.jp *********************************************************************** +++++ CS seminar in Kiryu: Programme +++++ URL: http://www.cs.gunma-u.ac.jp/~fujita/research/20140918Seminar.html Thursday, September 18, 2014 14:00--15:30 in the J3 lecture room (the building no. 6 of the map below), Kiryu campus, Gunma University Title: "Verification of programs using Frama-C and Why3" Speaker: Dr. Aleksy Schubert The University of Warsaw, Poland Abstract: Frama-C is a tool that makes it possible to do a variety of analyses for C programs annotated with C specification language called ACSL (The ANSI/ISO C Specification Language). One of the possible ways to use Frama-C is to generate verification conditions for appropriately defined Hoare logic that is in line with C programming language semantics. These verification conditions can subsequently be discharged by Why3 tool that makes it possible to manage the proving of necessary properties. During the talk I will present an overview of the tools and show a number of interesting examples to demonstrate how these tools work together to make possible verification of practical programs. ************************************************************************** Access to Kiryu campus, Gunma University: http://www.st.gunma-u.ac.jp/other/14.html Map of Kiryu campus: http://www.st.gunma-u.ac.jp/other/13.html For more information, please contact at: fujita(a)cs.gunma-u.ac.jp (Ken-etsu Fujita, Gunma University) -----

1 0

APLAS 2014: Call for Participation
by Jacques Garrigue 06 Sep '14

06 Sep '14

皆様、 APLASの参加募集案内をお送ります。 Jacques Garrigue ======================================================================= 12th Asian Symposium on Programming Languages and Systems (APLAS) November 17-19, 2014, Singapore http://loris-7.ddns.comp.nus.edu.sg/~aplas14 ======================================================================= C A L L F O R P A R T I C I P A T I O N C A L L F O R P O S T E R S APLAS aims to stimulate programming language research by providing a forum for the presentation of latest results and the exchange of ideas in programming languages and systems. APLAS is based in Asia, but is an international forum that serves the worldwide programming language community. APLAS is sponsored by the Asian Association for Foundation of Software (AAFS), founded by Asian researchers in cooperation with many researchers from Europe and the USA. Past APLAS symposiums were successfully held in Melbourne ('13), Kyoto ('12), Kenting ('11), Shanghai ('10), Seoul ('09), Bangalore ('08), Singapore ('07), Sydney ('06), Tsukuba ('05), Taipei ('04) and Beijing ('03) after three informal workshops. Proceedings of the past symposiums were published in Springer's LNCS. The symposium is devoted to foundational and practical issues in programming languages and systems. Invited Speakers ---------------- Zhenjiang Hu NII, Japan Dexter Kozen Cornell University, USA Julien Verlaguet Facebook, USA Program Committee ----------------- General chair Wei-Ngan Chin National University of Singapore, Singapore Program chair Jacques Garrigue Nagoya University, Japan Program committee Xiaojuan Cai Shanghai Jiao Tong University, China James Chapman Institute of Cybernetics, Estonia Cristian Gherghina Singapore University of Technology and Design Eric Goubault CEA LIST and Ecole Polytechnique, France Fei He Tsinghua University, China Gerwin Klein NICTA and UNSW, Australia Raghavan Komondoor Indian Institute of Science, Bangalore Paddy Krishnan Oracle, Australia Daan Leijen Microsoft Research, USA Yasuhiko Minamide University of Tsukuba, Japan Shin-Cheng Mu Academia Sinica, Taiwan Sungwoo Park Pohang University of Science and Technology, Korea Julian Rathke University of Southampton, UK Sukyoung Ryu KAIST, Korea Alexandra Silva Radboud University Nijmegen, Netherlands Martin Sulzmann Karlsruhe University of Applied Sciences, Germany Munehiro Takimoto Tokyo University of Science, Japan Jan Vitek Purdue University, USA Hongwei Xi Boston University, USA Venue ----- The conference will be held at the Kent Ridge Guild House of the National University of Singapore. Local information and registration are available at the following web site: http://loris-7.ddns.comp.nus.edu.sg/~aplas14 Call for Poster (Deadline 15th Sept 2014) http://loris-7.ddns.comp.nus.edu.sg/~aplas14/cfposters.html Poster Chair: Cristian Gherghina ============================= Monday, November 17th ============================= 08:30-09:00 Registration 09:00-10:00 ** Invited Talk: What is the Essence of Bidirectional Programming? Zhenjiang Hu (NII, Japan) 10:00-10:30 Coffee break 10:30-12:00 Session 1 Optimized Compilation of Multiset Rewriting with Comprehensions Edmund Soon Lee Lam, Iliano Cervesato (CMU, Qatar) Logic Programming and Logarithmic Space Clément Aubert, Marc Bagnol, Paolo Pistone (Institut de Mathématiques de Marseille, France),Thomas Seiller (Institut des Hautes Études Mathématiques,France) Automatic Memory Management Based on Program Transformation using Ownerships Tatsuya Sonobe, Kohei Suenaga, Atsushi Igarashi (Kyoto Univ., Japan) 12:00-13:30 Lunch and Posters 13:30-14:30 Session 2 The Essence of Ruby Katsuhiro Ueno, Yutaka Fukasawa (Tohoku University, Japan),Akimasa Morihata (Univ. of Tokyo, Japan), Atsushi Ohori (Tohoku Univ., Japan) Types for Flexible Objects Zachary Palmer, Scott Smith, Hari Menon, Alexander Rozenshteyn (The Johns Hopkins Univ., USA) 14:30-16:00 Posters and Tea 16:00-17:30 Session 3 A Translation of Intersection and Union Types for the lambda-mu Calculus Kentaro Kikuchi (RIEC, Tohoku Univ., Japan), Takafumi Sakurai (Chiba Univ., Japan) A Formalized Proof of Strong Normalization for Guarded Recursive Types Andreas Abel (Gothenburg Univ., Sweden), Andrea Vezzosi (Chalmers Univ. of Technology, Sweden) Functional Pearl: Nearest Shelters in Manhattan Shin-Cheng Mu (Academia Sinica, Taiwan), Ting-Wei Chen (National Taiwan Univ., Taiwan) ============================= Tuesday, November 18th ============================= 08:30-09:30 ** Invited Talk: Incremental Adoption of Static-Typing Julien Verlaguet (Facebook, USA) 09:30-10:00 Session 4 SUPPL: A flexible language for policies Robert Dockins and Andrew Tolmach (Portland State Univ., USA) 10:00-10:30 Coffee break 10:30-12:00 Session 5 A Method for Scalable and Precise Bug Finding Using Program Analysis and Model Checking Manuel Valdiviezo, Cristina Cifuentes and Padmanabhan Krishnan (Oracle Labs Brisbane, Australia) Model-checking for Android Malware Detection Fu Song (East China Normal Univ., China), Tayssir Touili (LIAFA, CNRS & Univ. Paris Diderot, France) Necessary and Sufficient Preconditions via Eager Abstraction Mohamed Nassim Seghir (Univ. of Edinburgh, UK), Peter Schrammel (Univ. of Oxford, UK) 12:00-13:30 Lunch 13:30-15:00 Session 6 Resource Protection using Atomics: Patterns and Verifications Afshin Amighi, Stefan Blom, Marieke Huisman (Univ. of Twente, Netherlands) Resource Analysis of Complex Programs with Cost Equations Antonio Flores Montoya, Reiner Hähnle (Technische Univ. Darmstadt, Germany) Simple and Efficient Algorithms for Octagons Aziem Chawdhary, Edward Robbins, Andy King (Univ. of Kent, UK) 15:00-15:30 Coffee break 15:30-17:00 Session 7 Compositional Entailment Checking for a Fragment of Separation Logic Constantin Enea (LIAFA, CNRS & Univ. of Paris, France), Ondrej Lengal (Brno Univ. of Technology, Czech Republic),Mihaela Sighireanu (LIAFA, CNRS & Univ. of Paris, France), Tomas Vojnar (Brno Univ. of Technology, Czech Republic) Automatic Constrained Rewriting Induction Towards Verifying Procedural Programs Cynthia Kop (Univ. of Innsbruck, Austria), Naoki Nishida (Nagoya Univ., Japan) A ZDD-based Efficient Higher-order Model Checking Algorithm Taku Terao, Naoki Kobayashi (Univ. of Tokyo, Japan) 18:00- APLAS Banquet ============================ Wednesday, November 19th ============================ 08:30-10:00 Session 8 Inferring Grammatical Summaries of String Values Se-Won Kim, Wooyoung Chin, Jimin Park, Jeongmin Kim, Sukyoung Ryu (KAIST, Korea) Syntax-Directed Divide-and-Conquer Data-Flow Analysis Shigeyuki Sato (The Univ. of Electro-Communications, Japan), Akimasa Morihata (Univ. of Tokyo, Japan) Address Chain: Profiling Java Objects without Overhead in Java Heaps Xiaohua Shi, Junru Xie, Hengyang Yu (Beihang Univ., China) 10:00-10:30 Coffee break 10:30-12:00 Session 9 Call-by-Value in a Basic Logic for Interaction Ulrich Schäpp (Ludwig-Maximilians-Univ. München, Germany) A precise and abstract memory model for C using symbolic values Frédéric Besson (Inria, France), Sandrine Blazy, Pierre Wilke (IRISA, France) Hereditary history-preserving bisimilarity: logics and automata Paolo Baldan, Silvia Crafa (Universita' di Padova, Italy) 12:00-13:00 Lunch 13:00-14:00 ** Invited Talk: NetKAT: A formal system for the verification of networks Dexter Kozen (Cornell Univ., USA)

1 0

第３１回量子情報技術研究会（QIT31）のご案内
by NISHIMURA Harumichi 05 Sep '14

05 Sep '14

logic-mlの皆様，第31回量子情報技術研究会のご案内を代理投稿させていただきます．よろしくお願いいたします．名古屋大学大学院情報科学研究科西村治道 ---------------------------------------------------------- 第31回量子情報技術研究会(QIT31) 研究会の内容情報科学と量子力学を融合させた新しい分野，量子情報科学に関する研究会です．情報を担う物理系の量子力学的側面を積極的に活かした新しい情報処理原理の研究とそこから開かれる新しい学問体系の構築および新しい情報技術パラダイムの創生を目指して，情報科学，物理学，光エレクトロニクスを含む理学，工学，数理科学に携わる研究者間に自由な討論の場を提供し，この研究分野の発展を図ることを目的としています．第31回研究会を下記のように開催いたします．現在この分野で活躍する研究者は勿論，自分の研究資産が何らかの形で使えそうだと予感している研究者・技術者など，広く関連する分野の研究者・技術者からの発表を募集致します．聴講のみの参加も歓迎致しますので，奮ってお申し込みください．日時: 2014年11月17日(月)～18日(火) 会場: 東北大学さくらホール (〒980-8577 仙台市青葉区片平２－１－１東北大学片平キャンパス内) 発表募集分野 (申し込み状況によっては査読の可能性あり) 量子情報，量子計算，量子暗号など広く量子情報技術に関わる理論的研究，実験的研究，計算機科学的研究，数学的研究，および，その他関連分野．定員: 200名参加費: 事前振込み一般4,000円，学生1,000円 (当日会場払いは一般5,000円，学生2,000円) (懇親会は別途) 研究会参加申込要領参加申込は下記 Web にて受付けます： http://staff.aist.go.jp/s-kawabata/qit/ 講演 (口頭，ポスター) の申込，予稿集原稿 PDF の提出は，電子情報通信学会の Web システムを使用する予定．【口頭講演申込締切】 2014年9月19日(金) 【ポスター講演申込締切】 2014年10月3日(金) 【予稿原稿提出締切】 2014年10月3日(金) 【参加申込締切】 2014年10月24日(金) 【問合せ先】枝松圭一 (東北大学電気通信研究所) 三森康義 (東北大学電気通信研究所) 吉田真人 (東北大学電気通信研究所) Email: qit31(a)quantum.riec.tohoku.ac.jp 主催: 量子情報技術時限研究専門委員会 (委員長: 枝松圭一 (東北大学)) 共催: 応用物理学会量子エレクトロニクス研究会東北大学電気通信研究所 ----------------------------------------------------------

1 0

[CFP] 情報処理学会第101回プログラミング研究発表会発表募集
by Rei Odaira 01 Sep '14

01 Sep '14

Logic-mlの皆さま、 IBMの大平です。締切約10日前ということで再度送らせて頂きます。＊＊＊＊複数受け取られた方はご容赦ください＊＊＊＊情報処理学会第101回プログラミング研究発表会発表募集今回は第101回記念ということでプログラミング研究会の初期に活躍された方を招いてのパネルセッションも催す予定です．プログラミング研究会(PRO)は，・プログラミング言語の設計，処理系の実装・プログラミングの理論，基本概念・プログラミング環境，支援システム・プログラミング方法論，パラダイム・これらを応用したシステムの開発事例・その他，プログラミングに関する面白い話題を対象とした研究発表の場で，1998年度から毎年3?4回のペースで論文誌を発行しています．PRO論文誌は研究会と密接にリンクしており，研究会で発表されたもののうちあらかじめ論文投稿を希望し，論文原稿を提出されているものが査読の対象となっています (論文誌投稿を希望しない発表も歓迎します)．おおむね研究会から3週間で論文の採否が決定されるという迅速さも大きな特徴です． 2014年11月の研究会も多くの発表ならびに論文投稿をお待ちしております．参加費は無料です．申込締切は9月12日金曜日(投稿締切は10月10日金曜日)ですので，よろしくご検討ください．なお，多数の発表申込みがある場合には，発表をお断りすることがございますので，お早めにお申し込みください．発表申込時で必要なのはタイトルと概要などとなっております．また，今回も和文として投稿された論文の英語化を支援する試みを実施します．和文原稿にて採録を判断し，(著者が希望する場合は) 採録決定後に英語化していただいてから掲載致します．この英語化に関する詳細については， http://www.ipsj.or.jp/sig/pro/english-paper-encouragement.html をご覧ください．第101回プログラミング研究会(PRO-2014-3)発表募集日程: 2014年11月10日(月)・11日(火) 会場: 東京大学創造情報学専攻 I-REF 棟 6階 Hilobby 東京都文京区弥生 1-1-1 　　交通案内: http://www.ci.i.u-tokyo.ac.jp/site/?access-j 発表申込締切:　　　　　　 2014年9月12日(金) 投稿論文原稿提出締切: 2014年10月10日(金) 申込先: 大平怜（日本アイ・ビー・エム東京基礎研究所） E-mail: odaira [at] jp.ibm.com 案内ページ: https://staff.aist.go.jp/reynald.affeldt/pro101/ ・申込みに当たっての注意はプログラミング研究会のページ http://www.ipsj.or.jp/sig/pro/を参照してください．・著者のための手引き: http://www.ipsj.or.jp/sig/pro/trans-author.html ・申込みの際には整理のために，Subject欄に以下をご指定頂けると助かります．　「PRO2014-3発表申込み」(カッコ不要) ・できるだけE-mailでお願いします．・申込み後3日以内に返信がない場合はご連絡下さい．大平　怜 (Rei Odaira), Ph.D. IBM Research - Tokyo Phone: +81-3-5144-2847

1 0

第49回 MLG 数理論理学研究集会のご案内
by Katsuhiko Sano 29 Aug '14

29 Aug '14

第49回 MLG 数理論理学研究集会のご案内 (重複してお受け取りの際はどうぞご容赦ください。) 北陸先端科学技術大学院大学の佐野勝彦と申します。少し先にはなりますが、2014年度MLG数理論理学研究集会（第49回）を下記の要領で開催いたします。多くの方のご講演・ご参加をお待ちしております。 ========================================= 第49回 MLG 数理論理学研究集会開催要領 ========================================= - 期間: 2014 年 12 月 5 日(金) 〜 12 月 7 日(日) - 場所: 山中温泉河鹿荘ロイヤルホテル（JR加賀温泉駅から車で約20分，加賀温泉駅から送迎あり） -- 〒922-0126 石川県加賀市山中温泉河鹿町ホ100 -- URL : http://www.daiwaresort.jp/kajikasou/ - 講演・宿泊申込締め切り: 2014 年 11 月 21 日（木） - 申し込みはこちらから --> http://goo.gl/RfZ5SE - ホームページ: https://sites.google.com/site/mlg2014kaga/ - 連絡先E-mail: mlg.logic.japan [at] gmail.com ============ 参加募集 ============ - 講演時間は原則40分を予定しています。 - 12月6日（土）の夜に懇親会を行います。 - 全日程参加の場合，参加費（宿泊代・食事代・会場代）は25000円前後になる予定です。 - ご講演をなさらなくても参加いただけます。山中温泉河鹿荘ロイヤルホテルで宿泊および食事をなさらない場合にも参加費（会場代）3000円をいただきます。 - 参加・講演申し込みは、http://goo.gl/RfZ5SE の registration form からお願い致します。世話人: 佐野勝彦〒923-1292 石川県能美市旭台1-1 北陸先端科学技術大学院大学情報科学研究科 MLG2014 に関するメールは，mlg.logic.japan [at] gmail.com まで。

1 0

September 1st - research talks by Yves Bertot, Pierre Casteran and Assia Mahboubi at University of Tokyo
by Jacques Garrigue 28 Aug '14

28 Aug '14

名古屋大学のGarrigueです。来る月曜日（9月1日）Coqの専門家三人による講演会を東京大学本郷キャンパスで開きます。皆様をお待ちしています。 On Monday, September 1st, three of the lecturers of the Shonan School on Coq will give talks at the University of Tokyo (Hongo Campus). We are waiting for you. David Nowak and Jacques Garrigue —— Date: September 1st, 2014 (Monday) Time: 14:00 - 16:30 Place: room 007, Faculty of Science Bldg. 7, Hongo Campus, The University of Tokyo URL: http://jfli.cnrs.fr/index.php/special-jfli-seminar-coq On the occasion of the NII Shonan School on Coq, JFLI organizes a special seminar on formal proofs in Coq with talks by three of the school's lecturers: Yves Bertot and Pierre Castéran (two of the 2013 ACM Software System Award laureates) will present some of their recent work. And Assia Mahboubi will present the formalization in Coq of the Feit-Thompson theorem (a.k.a. odd order theorem) achieved in 2012 under the direction of Georges Gonthier. 14:00 - 14:45: Yves Bertot PI, Arithmetic geometric means, and formal verification in Coq using Coquelicot In an experiment spanning over several months, we formally verified an abstract model of an algorithm to compute PI to a large number of digits using arithmetic geometric means. The proof that we used relies on a few non elementary aspects, like reasoning about improper integrals or deriving under the integral sign, and revolved around manipulating real numbers. This is why we call this an abstract model. Then we used the recent extension of Coq with native compilation to test the algorithm on a concrete setting, using large integers. As a result we are able to compute in the order of a million of decimals of PI within the theorem prover. We also proved the correctness of this implementation. This involves bounding the cumulated errors brought by multiplication, division, and square-root during fixed-point multiplications. This work benefits from the overall quality of the Coq system and the following recent contributions: the coquelicot library by Boldo & al., the psatzl tactic by F. Besson, and native compilation by M. Dénès. 14:45 - 15:30: Pierre Castéran Formal Proofs of Local Computation Systems Local Computations (LC) are an abstract model for distributed algorithms based on message passing. Each processor can only interact with its neighbours. The current configuration of a static network is represented as a labelling of the vertices and edges of a graph. This model allows us to study the importance of such hypotheses on the network's behaviour such as synchrony, anonymity, initial knowledge of the processors. Algorithms are splitted into several classes, according to the precise way in which every processor interacts with its neighbours. LoCo is a formalization of LC in the Coq proof assistant. This library allows us to simulate algorithms, to prove their correctness, and also to prove more abstract results: • Impossibility results, i.e., proving that some task is not realisable within a given subclass of LC; • Certified transformations, that are functions that map one or several proved algorithms into a new proved algorithm; • Analysis of some simple random distributed algorithms. The talk will show how Coq's rich type system and computation rules allowed us to build this library. Perspective of future work will also be discussed. 15:30 - 15:45: break 15:45 - 16:30: Assia Mahboubi Computer-checked mathematics: a formal proof of the Odd Order theorem The Odd Order Theorem is a landmark result in finite group theory, famous for its crucial role in the classification of finite simple groups, for the novel methods introduced by its original proof but also for the striking contrast between the simplicity of its statement and the unusual length and complexity of its proof. This talk presents the six-year collaborative work that led to a complete formalization of this theorem, using the Coq proof assistant. The resulting collection of libraries of formalized mathematics covers a wide variety of topics as this proof relies on a sophisticated combination of different flavours of mathematics. These libraries and the underlying methodology can be reused for a wider spectrum of applications. This is a joint work with the Mathematical Components group at the Inria Microsoft Joint Centre.

1 0

第5回松山TGSAセミナーのお知らせ
by Hiroshi Fujita 26 Aug '14

26 Aug '14

LOGICメーリングリストの皆さま、愛媛大学の藤田です。このほど下記のセミナーを愛媛大学理学部において開催することとなりましたのでお知らせいたします。 ============================================== 第5回松山TGSAセミナー ============================================== 日時: 2014年9月8日(月) 16時30分〜17時30分会場: 愛媛大学理学部 2号館201号室 (数学科大演習室) 講演者: 南裕明さん（神戸大学）演題: Mathias-Prikry forcing and dominating reals ============================================== Abstract: For a countable set X, we call $\mathcal{I}$ an ideal on X if $\mathcal{I}$ is a family of subsets of X closed under the taking subsets and unions. We assume all ideals on X contains the family of finite subsets of X. The Mathias-Prikry forcing associated with an ideal $\mathcal{I}$ on a countable subset X, denoted by $\mathbb{M}_{\mathcal{I}}$, consist of pairs (s,A) such that s is a finite subsets of X, A in $\mathcal{I}$ and $s\cap A=\emptyset$. The ordering is given by $(s,A)\leq (t,B)$ if t is a subset of s and B is a subset of A and $(s\setminus t)\cap B=\emptyset$. The Mathias-Prikry forcing adds a new subset of X which diagonalize ideal $\mathcal{I}$, that is, $\mathbb{M}_{\mathcal{I}}$ adds a new subset $\dot{A}$ of X such that $X\cap I$ is finite for every I in $\mathcal{I}$. So Mathias-Prikry forcing plays significant role when we investigate ultrafilter, ideal or mad family. Some additional nice properties of the Mathias-Prikry forcing depends on $\mathcal{I}$. For example, $\mathcal{U}$ is a Ramsey ultrafilter if and only if $\mathbb{M}_{\mathcal{U}^{*}}$ does not add Cohen real. The speaker and Michael Hru\v{s}\'{a}k give a characterization of ideals $\mathcal{I}$ such that $\mathbb{M}_{\mathcal{I}}$ adds no dominating real. We say a forcing notion $\mathbb{P}$ adds dominating reals if $\mathbb{P}$ adds a new function $\dot{g}$ from $\omega$ to $\omega$ such that for $f\in\omega^{\omega}\cap V$, $f(n)<\dot{g}(n)$ for all but finitely many $n\in\omega$. We show that $\mathbb{M}_{\mathcal{I}^{*}}$ adds dominating reals if and only if $\mathcal{I}^{<\omega}$ is $P^{+}$-ideal. Recently, David Chodounsk\'{y}, and Du\v{s}an Repov\v{s} and Lyubomyr Zdomskyy give another characterization of ideal $\mathcal{I}$ with covering property such that $\mathbb{M}_{\mathcal{I}}$ adds no dominating real. We will talk about recent development of these result and application. ============================================== 松山TGSAセミナー（Matsuyama Seminar on Topology, Geometry, Set Theory and their Applications)は、位相空間論・幾何学・集合論およびその関連分野を広く扱うセミナーで、愛媛大学のスタッフが中心となって定期的に開催しています。今後の予定についてはWebサイト <http://www.math.sci.ehime-u.ac.jp/MTGSA.html> をご覧ください。 -- 藤田博司 <fujita.hiroshi.mh(a)ehime-u.ac.jp> 愛媛大学理学部／大学院理工学研究科数理物質科学専攻

1 0

The Kyoto Summer School in Logic, Language and Information (KSSLLI)のお知らせ
by Shunsuke Yatabe 25 Aug '14

25 Aug '14

重複して受け取られたかたはご容赦ください。下記のとおりに哲学的論理学に関するサマースクールを開催いたします。どうぞふるってご参加ください。矢田部俊介＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊記日時：2014年8月30日（土）～31日（日）場所：京都大学文学部第７講義室（下地図のNo.8） http://www.kyoto-u.ac.jp/en/access/campus/main.htm 開催趣旨と内容：近年、哲学や人文学と論理学や形式的言語学、情報科学との間の垣根は低くなり、哲学や人文学の研究にも形式的な論理学等の手法の知識が必要となるケースも増えてきた。欧州や北米では、人文学・哲学の研究者とこれら三分野の研究者が国を超えて共に集い、それら手法を学び、意見交換を通じて共同研究の芽を用意するサマースクール（ESSLI、NASSLLI等）が毎年行われ、多くの成果を上げている。しかし、アジア太平洋地域では、研究者は自身の専門分野に籠もり、欧米のような共同の試みはあまり行われてこなかった。本サマースクールは、アジア太平洋地域の、論理学が専門ではない哲学の大学院生が多数参加する国際会議CCPEAのサテライトとして開催され、院生への最先端の論理学的手法等の紹介を通して、異分野同志の協業をスタートさせることを目指す。今回は、8月30日にブリストル大学のLeon Horsten教授に、公理的真理理論の論理学的、および哲学的意義（特に真理に関するデフレ主義との関連で）についてご講演頂く。 8月31日は、矢田部・秋吉が非古典論理上の素朴集合論や形式算術の順序数解析などの話題について、入門的な説明と最新の結果説明を同時に行う。また、夕方は、お茶の水女子大学の田中と叢が、言語学における論理学的・計算機科学的手法の最新の応用例について、発展的な解説を行う。参加費は無料、事前登録は不要です。講演は英語で行われます。問い合わせ先：CAPE(a)bun.kyoto-u.ac.jp ***************************************** The Kyoto Summer School in Logic, Language and Information (KSSLLI) The Kyoto Summer School in Logic, Language and Information (KSSLLI) is planned to be an annual event under the support of the Center for Applied Philosophy and Ethics, graduate school of letters, Kyoto University (CAPE) and brings together logicians, linguists, computer scientists, and philosophers to study language, logic, and information, and their interconnections. This is a satellite workshop of the 2nd conference on Contemporary Philosophy in East Asia (CCPEA). There will be about several courses at introductory and advanced invited lectures and a student session to foster interdisciplinary discussion among philosophers, logicians and computer scientists. Venue: The 7th lecture room, faculty of letters main building (the bulding no.8 of the map below), Kyoto University http://www.kyoto-u.ac.jp/en/access/campus/main.htm Conference url: http://www.cape.bun.kyoto-u.ac.jp/capes/ws/ Fee: free Submission: no submission is needed. Schedule: 30, August（Saturday） Mini lecture course on Axiomatic Truth Theories : Leon Horsten (University of Bristol) This is one day tutorial course on axiomatic truth theory (as FS) and deflationism for wide range audience. 10:00-12:00 Session 1 "Axiomatic approaches to truth" 12:00-14:00 Lunch 14:00-16:00 Session 2 "Implications for deflationism about truth" 31, August（Sunday） Short lectures and introductions of advanced results This session provides introductions to new results in philosophical logics 10:00-11:30 Session 1 Naive set theories on non-classical logics: Shunsuke Yatabe (Kyoto University) 11:30-13:30 Lunch 13:30-15:00 Session 2 An Introduction to Proof Theory of First-Order Arithmetic: Ryota Akiyoshi (JSPS) Talks on formal linguistics This session provides introductions to new results in formal linguistics 15:00-16:00 "A Proof-Theoretic Approach to Generalized Quantifiers in Dependent Type Semantics" Ribeka Tanaka (Ochanomizu University) 16:00-17:00 "Analysis and Implementation of Focus and Inverse Scope by Delimited Continuations" Youyou Cong (Ochanomizu University) Abstracts: Session 1 Naive set theories on non-classical logics: Shunsuke Yatabe (Kyoto University) It is well-known that naive set theories within many non-classical logics do not imply a contradiction. And, in these set theories, there are very different from classical set theories with respect to the concept of infinity because these theories are highly circular. In this lecture, we introduce these set theories and such difference. Session 2 An Introduction to Proof Theory of First-Order Arithmetic: Ryota Akiyoshi (JSPS) Gentzen proved the consistency of Peano arithmetic on 1936 after Goedel’s incompleteness theorems. Moreover, he showed that the epsilon_0 is the least ordinal for proving it. His fundamental work was the beginning of the modern proof theory called “ordinal analyais”. In 1951, Schuette used an infinitary inference called “the omega-rule” for obtaining a more perspicuous proof of Gentzen’s result. This approach is not only technically simpler and elegant, but historically (or philosophically) interesting for the following reason; Brouwer already suggested the possibility of using of infinitary inference for Hilbertian proof theory. In this talk, we explain the basic results of infinitary proof theory via the omega-rule for Peano arithmetic. Additionally, we discuss the relationship between finitary proof theory (Gentzen) and infinitary proof theory (Schuette). Talks on formal linguistics (1) A Proof-Theoretic Approach to Generalized Quantifiers in Dependent Type Semantics: Ribeka Tanaka (Ochanomizu University) The main aim of this study is to give semantic representations of generalized quanti fiers (GQs) in the framework of dependent type semantics (DTS), a proof-theoretic semantics for natural language. Quantifier "most" is known as a crucial example of GQs. In this talk, we introduce the framework of DTS, propose a definition of "most" that accounts for dynamic linguistic phenomena, and extend the definition to numerical quantifiers. We also show that the definitions satisfy logical properties of GQs, conservativity and monotonicity. (2) Analysis and Implementation of Focus and Inverse Scope by Delimited Continuations: Youyou Sou (Ochanomizu University) Focus and inverse scope are known as phenomena that require the context surrounding a particular lexical item for the semantic representation of the whole sentence. The context of a given lexical item in a natural language sentence can be regarded as its continuation. Continuation is a notion in programming languages that represents the rest of the computation. In this talk, we will present an analysis of focus and inverse scope by means of the control operators shift/reset (Danvy and Filinski 1990). We also discuss the interaction between these phenomena. For more information, please contact at CAPE(a)bun.kyoto-u.ac.jp

1 0

セミナー案内
by KASHIMA Ryo 25 Aug '14

25 Aug '14

数理論理学セミナーのお知らせ日時：8月28日(木) 16:00 から場所：東京工業大学大岡山西８号館Ｗ棟10階 W1008 話者：横山啓太（JAIST）題目：ヒルベルトは悪夢を見るか概要：ゲーデルの不完全性定理によれば、十分な自然数論を含む無矛盾かつ再帰的な公理系は必ず証明できない文を持つ。それでは、二つの（ゲーデルの不完全性定理の条件を満たすような）公理系T,T'を用意して次を成り立たせることは可能だろうか？全ての文 A に対して T が A で証明できるかまたは T が A で証明できないことが T' で証明できる。 6月にシンガポールで行われた研究集会において、Mingzhong Cai 氏が Hilbert's nightmare の名で上を一般化した問題を提示した。ここではその問題に対する Beklemishev/Vissar の答えを紹介し、さらなる一般化についても考える。 ------ 本セミナーは定期的に東工大で開催しているものです。初めて参加を希望される方はご一報ください。 ----- 鹿島亮東京工業大学大学院情報理工学研究科数理・計算科学専攻 kashima(a)is.titech.ac.jp

1 0

日本ソフトウェア科学会第31回大会参加募集案内
by Atsushi Igarashi 22 Aug '14

22 Aug '14

京都大学の五十嵐です．　9月7日(日)～10日(水)に名古屋大学東山キャンパスにて開催されます日本ソフトウェア科学会第31回大会の暫定プログラムを公開し，参加申し込みの受付も開始いたしましたのでご案内いたします．様々な企画と研究発表があり，特に9/7(日)に行われる FTD 2014 (Future Technology Design) は参加費無料ですので，ぜひ参加をご検討ください． -- 五十嵐淳 (IGARASHI Atsushi) E-mail: igarashi(a)kuis.kyoto-u.ac.jp url: http://www.fos.kuis.kyoto-u.ac.jp/~igarashi/ ------------------------------------------------------------------------- 日本ソフトウェア科学会第 31 回大会開催案内・参加募集 ------------------------------------------------------------------------- 大会ホームページ： http://jssst2014.wordpress.com Twitter： @jssst2014 日時： 2014 年 9 月 7 日(日)～ 10 日(水) 会場：名古屋大学東山キャンパス IB電子情報館名古屋市営地下鉄名城線名古屋大学駅３番「西地区出口」１分参加申込ページ: http://jssst2014.wordpress.com/participation/ 本年も，2件の招待講演に加えて，著名な国際会議での発表論文を紹介していただくトップカンファレンス特別講演，未来につくるソフトウェアについて語る FTD，新たな知識を身に着けるためのチュートリアルなどの様々な企画が開催されます．また，一般セッション，研究会セッション，ソフトウェア論文セッション，デモ・ポスターセッションとしてソフトウェア科学全般に渡る多数の研究発表も行われますので，最新の研究成果についての議論と情報収集の場として，皆様の参加をお待ちしております． ------------------------------------------------------------------------- 大会ハイライト ------------------------------------------------------------------------- 招待講演 9/8(月) スマートステーションを実現する屋内空間情報サービス河口信夫（名古屋大学） 9/9(火) プログラム検証とインバリアント生成寺内多智弘（北陸先端科学技術大学院大学）トップカンファレンス特別講演 9/8(月)～9/10(水) ACM ICFP, ACM POPL, USENIX ATC, AAAI-14, AAMAS 2014 など 2013年から 2014年のトップカンファレンスで発表された論文について紹介していただきます．各講演はそれぞれ研究発表セッションにて実施されます． FTD 2014 (Future Technology Design) 9/7(日) ～未来をつくる素晴らしいソフトウェアのアイデアを世界に～「小学生」，「笑顔」，「命」，そして「飛行ロボット」，さまざまな分野でソフトウェアに関する素晴らしいアイデアをもっている７組の講演者たちが登場予定です．この講演者たちの記憶に残る１０分間のプレゼンを身近で経験してみませんか？ http://jssst2014.wordpress.com/events/ftd/ チュートリアル 9/7(日) (1) 定理証明支援系Coq入門講師：アフェルトレナルド（産業技術総合研究所） http://jssst2014.wordpress.com/events/coq-tutorial/ (2) ソフトウェア品質向上活動におけるプロダクトレビューの役割と効果講師：森崎修司（名古屋大学） http://jssst2014.wordpress.com/events/product-review-tutorial/ 併設企画・PPLサマースクール2014 9/7(日) 高性能計算のプログラミングの最前線講師：遠藤敏夫（東京工業大学） http://ppl.jssst.or.jp/index.php?ss2014 ------------------------------------------------------------------------- 参加申し込み方法 ------------------------------------------------------------------------- 参加申し込みページ http://jssst2014.wordpress.com/participation/ をご参照のうえ，お申し込みください．参加費については，9月4日（木）までに銀行振込にてお支払い下さるようにお願いいたします． ------------------------------------------------------------------------- プログラム（HTML版 http://jssst2014.wordpress.com/program/ ） ------------------------------------------------------------------------- [招待講演] (1) スマートステーションを実現する屋内空間情報サービス河口信夫（名古屋大学） 9月8日(月) 13:30-14:30 名古屋大学東山キャンパス IB電子情報館大講義室講演概要：屋外での位置情報サービスは広く普及しているが、屋内空間での位置情報サービスには、まだまだ発展の余地がある。本講演では、駅や地下街などの公共空間を対象として屋内空間のスマート化を目指す「スマートステーションなごや」プロジェクトを紹介する。 (2) プログラム検証とインバリアント生成寺内多智弘（北陸先端科学技術大学院大学） 9月9日(火) 14:00-15:00 名古屋大学東山キャンパス IB電子情報館大講義室講演概要： CEGAR によるソフトウェアモデル検査など多くの近年のプログラム検証において共通して使われる技術の一つが、有限の深さまで展開されたプログラムスライスを解析し（帰納的）インバリアント候補を推論する、というプロセスである。本講演では、この技術について基本的な解説を行い、またいくつかの課題についても述べる。特に、近年主流となりつつある「ホーン節制約解消」による手法に焦点を置き解説を行う。 [トップカンファレンス特別講演] 2013年から2014年のトップカンファレンスで発表された論文について紹介していただきます．各講演はそれぞれ研究発表セッションにて実施されます． (1) A Short Cut to Parallelization Theorems ○Akimasa Morihata （The University of Tokyo） (ACM ICFP 2013にて発表) 発表セッション：PPL (1) (2) Structural Recursion for Querying Ordered Graphs ○Soichiro Hidaka （National Institute of Informatics） Kazuyuki Asada （The University of Tokyo） Zhenjiang Hu （National Institute of Informatics） Hiroyuki Kato （National Institute of Informatics） Keisuke Nakano （University of Electro-Communications） (ACM ICFP 2013にて発表) 発表セッション：PPL (3) (3) Parametric Effect Monads and Semantics of Effect Systems ○Shin-ya Katsumata (Kyoto Univeristy) (ACM POPL 2014にて発表) 発表セッション：PPL (4) (4) GPUvm: Why Not Virtualizing GPUs at the Hypervisor? Yusuke Suzuki （Keio University） Shinpei Kato （Nagoya University） Hiroshi Yamada （Tokyo University of Agriculture and Technology） ○Kenji Kono （Keio University） (USENIX ATC ’14にて発表) 発表セッション：一般 (5) (5) SML# in Industry: A Practical ERP System Development ○Atsushi Ohori （Tohoku University） Katsuhiro Ueno （Tohoku University） Kazunori Hoshi （NEC Solution Innovators, Ltd.） Shinji Nozaki （NEC Solution Innovators, Ltd.） Takashi Sato （NEC Solution Innovators, Ltd.） Tasuku Makabe （NEC Solution Innovators, Ltd.） Yuki Ito （NEC Solution Innovators, Ltd.） (ACM ICFP 2014にて発表) 発表セッション：PPL (6) (6) Two Case Studies for Trading Multiple Indivisible Goods with Indifferences Akihisa Sonoda （Kyushu University） Etsushi Fujita （Kyushu University） ○Taiki Todo （Kyushu University） Makoto Yokoo （Kyushu University） (AAAI-14にて発表) 発表セッション：一般 (6) (7) Intelligence Arms Race: Delayed Reward Increases Complexity of Agent Strategies ○Hirotaka Osawa （University of Tsukuba） (AAMAS 2014にて発表) 発表セッション：一般 (6) [企画セッション] FTD2014 (Future Technology Design) ～未来をつくる素晴らしいソフトウェアのアイデアを世界に～ http://jssst2014.wordpress.com/events/ftd/ 9月7日(日) 13:20-17:00 名古屋大学東山キャンパス IB電子情報館 IB014 日本ソフトウェア科学会は、昨年創立３０周年を迎え、本学会で議論され生み出されてきたアイデアや、日本で生まれた広める価値のある素晴らしいソフトウェアのアイデアを広げる大会特別企画として、FTD (Future Technology Design)を実施しました。FTD 2013では、すばらしいアイデアを持った8名の講演があり、大盛況のもと改めてソフトウェアの面白さを再確認することができました。そして、FTD 特別企画から１年、未来につくるソフトウェアのアイデアをもっと広めたいという思いを再認識し、2014年の第３１回大会でもFTDを継続することにしました。FTD 2014では、映像、そして講演の両面からさらにパワーアップします。映像面では、講演の映像配信のさきがけ的コミュニティであるWISSとコラボし、リアルタイム映像合成+配信にチャレンジします。そして、講演面では、素晴らしいソフトウェアを産み出す人財を発掘する未踏事業とコラボレーションします。名付けてFTD 2014 ≒ FTD x WISS x 未踏。どうぞご期待ください。 [チュートリアル] (1) 定理証明支援系Coq入門講師：アフェルトレナルド（産業技術総合研究所） http://jssst2014.wordpress.com/events/coq-tutorial/ 9月7日(日) 14:00-18:00 名古屋大学東山キャンパス IB電子情報館 IB015 数学とソフトウェア科学の両方の分野において，定理証明支援系への関心が高まっています．なかでも，フランス国立情報学自動制御研究所（INRIA）で開発が進められている定理証明支援系Coqは，ACM SIGPLAN Programming Languages Software 2013 AwardとACM Software System 2013 Awardの受賞を契機に，より多くの研究者や技術者の注目を集めていす． Coqは，四色定理の証明に代表される数学分野での貢献だけでなく，ソフトウェア開発への応用においても大きな役割を果たしてきました．本チュートリアルでは，産業技術総合研究所のアフェルトレナルド氏をお招きし，モダンなCoq入門の観点から，Coqの拡張であるSSReflectを使った証明の初歩を紹介していただきます．SSReflectはタクティクスの表現力が向上し，数学の膨大な証明が可能になっただけでなく，プログラムの検証でも伝統的なCoqに代わって使われるようになっています．定理証明支援系を使った証明に関心を持つ研究者や学生の方，ソフトウェアの形式検証に関心を持つ研究者や技術者の方など，多くの方々の参加をお待ちしております．（本チュートリアルは日本語で行います） (2) ソフトウェア品質向上活動におけるプロダクトレビューの役割と効果講師：森崎修司（名古屋大学） http://jssst2014.wordpress.com/events/product-review-tutorial/ 9月7日(日) 13:00-16:00 名古屋大学東山キャンパス IB 電子情報館 IB014 ソフトウェア品質向上活動はプログラムの完成前に実施できる活動(静的解析技法を用いた活動)とプログラムの完成後に実施できる活動(動的解析技法を用いた活動)に大別できます。本チュートリアルでは、両方の品質向上活動を概観し、静的解析技法としてプロダクトレビューを紹介します。プロダクトレビューの技法を紹介した上で、ソフトウェアテストをはじめとする動的解析技法との役割分担やバランスを考えるヒントを紹介します。 [併設企画] PPLサマースクール2014 高性能計算のプログラミングの最前線講師：遠藤敏夫（東京工業大学） http://ppl.jssst.or.jp/index.php?ss2014 9月7日 (日) 10:00-13:00 名古屋大学東山キャンパス IB電子情報館 IB015 コンピュータの性能を最大限に活かすソフトウェアを作成するためには記憶階層や並列プログラミングの知識が必須であるが、学ぶべき知識は近年膨大となっている。古典的なOpenMPやMPIに加え、CUDA, OpenCL, OpenACC, Intel offload API, SSE/AVX…などである。その増大の多くは計算機アーキテクチャの複雑化・異種混合化に起因している。マルチコアや、 GPU・Xeon Phiなどのアクセラレータのアーキテクチャの動向も踏まえて、高性能計算のためのプログラミングの道具を概説する。 [研究発表プログラム（暫定版）] ◎一般セッション (1)：形式手法 9月8日（月） 10:00-12:00 （IB011）座長：田辺良則（国立情報学研究所） [一般1-1] 形式言語CSP#によるSysMLステートマシン図の形式化 ○安藤崇央（九州大学大学院システム情報科学研究院）谷津弘一（九州大学大学院システム情報科学研究院）孔維強（九州大学大学院システム情報科学研究院）久住憲嗣（九州大学システムLSI研究センター）福田晃（九州大学大学院システム情報科学研究院） [一般1-2] スマホ・アプリの電力消費振る舞いと検査性質の表現 ○中島震（国立情報学研究所） [一般1-3] 協調的リアクティブシステムの合成手法 ○冨田尭（東京工業大学大学院情報理工学研究科）上野篤史（東京工業大学大学院情報理工学研究科）萩原茂樹（東京工業大学大学院情報理工学研究科）米崎直樹（東京工業大学大学院情報理工学研究科） [一般1-4] 情報制御システムにおける段階的検査法を用いたモジュラ検証 ○宮島卓巳（茨城大学）小飼敬（茨城工業高等専門学校）上田賀一（茨城大学）山形知行（株式会社　日立製作所）武澤隆之（株式会社　日立製作所） ◎rePiTセッション (1) 9月8日（月） 10:30-12:00 （IB013）座長：楠本真二（大阪大学） [rePiT1-1] 女性IT技術者の育成を目指して―enPiT女性部会WiTの活動を中心に― ○櫻井浩子（大阪大学）森本千佳子（東京工業大学）渡辺知恵美（筑波大学）木塚あゆみ（公立はこだて未来大学）永瀬美穂（産業技術大学院大学）中島明日香（NTTセキュアプラットフォーム研究所） [rePiT1-2] RDFとユーザプロファイルを用いたPBL向け情報推薦手法 ○藤原哲（公立はこだて未来大学大学院）大場みち子（公立はこだて未来大学）山口琢（公立はこだて未来大学）奥野拓（公立はこだて未来大学）伊藤恵（公立はこだて未来大学） [rePiT1-3] IoTを題材としたPBLの実施と分析細合晋太郎（九州大学大学院システム情報科学研究院システム情報科学府高度ICT 人材教育開発センター）石田繁巳（九州大学大学院システム情報科学研究院システム情報科学府高度ICT 人材教育開発センター）亀井靖高（九州大学大学院システム情報科学研究院システム情報科学府高度ICT 人材教育開発センター） ○大迫周平（九州大学大学院システム情報科学研究院システム情報科学府高度ICT 人材教育開発センター）井垣宏（大阪大学）鵜林尚靖（九州大学大学院システム情報科学研究院システム情報科学府高度ICT 人材教育開発センター）福田晃（九州大学大学院システム情報科学研究院システム情報科学府高度ICT 人材教育開発センター） ◎PPLセッション (1)：並列処理 9月8日（月） 10:00-12:00 （IB014） [PPL1-1]（特別講演）A Short Cut to Parallelization Theorems 　　○Akimasa Morihata （The University of Tokyo）　　(ACM ICFP 2013にて発表) [PPL1-2] 限定継続演算子の拡張およびそれを用いた並列向け領域特化言語群の実現 ○山口洋（東京大学）千葉滋（東京大学） [PPL1-3] Locality-Aware Parallel Iterative Tree Traversal ○Shigeyuki Sato（The University of Electro-Communications） [PPL1-4] 依存関係をもった並列タスクのための動的グループバリア同期とその効率的な実装 ○夏澄彦（東京大学）佐藤芳樹（東京大学）千葉滋（東京大学） ◎一般セッション (2)：プログラミング学習 9月8日（月） 14:45-16:15 （IB011）座長：脇田建（東京工業大学） [一般2-1] LablGtk2を用いたuniverse teach packの実装 ○上原千裕（お茶の水女子大学理学部情報科学科）浅井健一（お茶の水女子大学理学部情報科学科） [一般2-2] プログラミング作業過程の動画を用いたプログラミング学習の試み ○杉本識吏（公立はこだて未来大学）伊藤恵（公立はこだて未来大学） [一般2-3] Schemeによる3D図形の構成的制作 ○古川孝太郎（京都大学大学院）坂東宜昭（京都大学大学院）糸山克寿（京都大学大学院）吉井和佳（京都大学大学院）奥乃博（京都大学大学院） ◎rePiTセッション (2) 9月8日（月） 14:45-16:15 （IB013）座長：粂野文洋（日本工業大学） [rePiT2-1] OJLによる実践的組込みシステム教育 ○舘　伸幸（名古屋大学）山本雅基（名古屋大学）吉田則裕（名古屋大学）高嶋博之（名古屋大学）海上智昭（名古屋大学）安藤友樹（名古屋大学）松原　豊（名古屋大学）本田晋也（名古屋大学）高田広章（名古屋大学） [rePiT2-2] ハイブリッド人材育成のための基礎学習に関する一考察 ○野尻梢（慶應義塾大学）廣瀬雅治（慶應義塾大学）山内正人（慶應義塾大学）砂原秀樹（慶應義塾大学） [rePiT2-3] モダンなソフトウエア開発者育成のための技術教育 ○中鉢欣秀（産業技術大学院大学） ◎PPLセッション (2)：文脈指向プログラミングと制約プログラミング 9月8日（月） 14:45-16:15 （IB014） [PPL2-1] Visibility of Context-oriented Behavior and State in L ○Robert Hirschfeld（Hasso-Plattner-Institute, University of Potsdam） Hidehiko Masuhara（Tokyo Institute of Technology） Atsushi Igarashi（Kyoto University） Tim Felgentreff（Hasso-Plattner-Institute, University of Potsdam） [PPL2-2] アクターモデルに基づく並行文脈指向プログラミング機構の実装と評価 ○竹野創平（東京工業大学）渡部卓雄（東京工業大学） [PPL2-3] 制約解集合プログラミングシステムの設計方式に関する考察 ○宋剛秀（神戸大学情報基盤センター）則武治樹（神戸大学大学院システム情報学研究科）番原睦則（神戸大学情報基盤センター）田村直之（神戸大学情報基盤センター）井上克巳（国立情報学研究所） ◎一般セッション (3)：ユーザ支援 9月8日（月） 16:30-18:00 （IB011）座長：丸山勝久（立命館大学） [一般3-1] コード生成を用いたフレームワーク向けWebアプリケーション開発支援ツールの作成 ○京谷和明（公立はこだて未来大学）伊藤恵（公立はこだて未来大学） [一般3-2] 研究エピソードネットワークに基づくスライド検索 ○加藤雄大（名古屋工業大学大学院工学研究科情報工学専攻）白松俊（名古屋工業大学大学院情報工学専攻）大囿忠親（名古屋工業大学大学院情報工学専攻）新谷虎松（名古屋工業大学大学院情報工学専攻） [一般3-3] ドキュメントレビュー結果を利用したテスト項目作成システムの開発 ○加藤武文（公立はこだて未来大学）大場みち子（公立はこだて未来大学）藤原哲（公立はこだて未来大学） ◎rePiTセッション (3) 9月8日（月） 16:30-18:00 （IB013）座長：井垣宏（大阪大学） [rePiT3-1] ハッカソン形式の実践的IT教育の実施報告 ○坂本一憲（国立情報学研究所）田辺良則（国立情報学研究所） [rePiT3-2] 筑波大学大学院におけるIT実践力育成の施策と評価 ○山戸昭三（筑波大学大学院システム情報工学研究科コンピュータサイエンス専攻）北川博之（筑波大学大学院システム情報工学研究科コンピュータサイエンス専攻）田中二郎（筑波大学大学院システム情報工学研究科コンピュータサイエンス専攻） [rePiT3-3] enPiT SecCap: Comparison of Japanese Practical Security Education with one of the US ○Takao Okubo（Institute of Information Security） ◎PPLセッション (3)：グラフ処理 9月8日（月） 16:30-18:00 （IB014） [PPL3-1]（特別講演）Structural Recursion for Querying Ordered Graphs 　　○Soichiro Hidaka （National Institute of Informatics）　　Kazuyuki Asada （The University of Tokyo）　　Zhenjiang Hu （National Institute of Informatics）　　Hiroyuki Kato （National Institute of Informatics）　　Keisuke Nakano （University of Electro-Communications）　　(ACM ICFP 2013にて発表) [PPL3-2] Engineering Shortest Regular Category-Path Queries ○Le-Duc Tung（The Graduate University for Advanced Studies (SOKENDAI)） Kento Emoto（Kyushu Institute of Technology） Zhenjiang Hu（National Institute of Informatics） [PPL3-3] パターン定義によるマッチングを導入したグラフ書換え言語とその実装 ○奈良耕太（早稲田大学理工学研究科）上田和紀（早稲田大学理工学術院） ◎ソフトウェア論文セッション (1) 9月9日（火） 10:30-12:00 （IB011）座長：馬谷誠二（京都大学） [ソフト1-1] Scala上で実現されたSAT型制約プログラミングシステムのための開発ツール ○宋剛秀（神戸大学情報基盤センター）番原睦則（神戸大学情報基盤センター）田村直之（神戸大学情報基盤センター） [ソフト1-2] Code2Xml：ソースコードと構文木の相互変換を実現するパーサコレクション ○坂本一憲（国立情報学研究所） [ソフト1-3] まねっこダンス：真似て覚えるプログラミング学習ツール ○坂本一憲（国立情報学研究所）高野孝一（株式会社オービック）本田澄（早稲田大学）音森一輝（早稲田大学）山崎頌平（早稲田大学）鷲崎弘宣（早稲田大学）深澤良彰（早稲田大学） ◎rePiTセッション (4) 9月9日（火） 10:30-12:00 （IB013）座長：吉岡信和（国立情報学研究所） [rePiT4-1] 過去のPBLの開発履歴を活用したPBL運用支援 ○伊藤恵（公立はこだて未来大学）木塚あゆみ（公立はこだて未来大学）奥野拓（公立はこだて未来大学）大場みち子（公立はこだて未来大学） [rePiT4-2] テキストマイニングによるPBL発表会評価アンケート傾向分析 ○大迫周平（九州大学）孔維強（九州大学）亀井靖高（九州大学）細合晋太郎（九州大学）石田繁巳（九州大学）鵜林尚靖（九州大学）福田晃（九州大学） [rePiT4-3] enPiTにおける教育効果測定の実践と評価 ○山本雅基（名古屋大学）小林隆志（東京工業大学）宮地充子（北陸先端科学技術大学院大学）奥野拓（公立はこだて未来大学）粂野文洋（日本工業大学）櫻井浩子（大阪大学）海上智昭（名古屋大学）春名修介（大阪大学）井上克郎（大阪大学） ◎PPLセッション (4)：型システム 9月9日（火） 10:00-12:00 （IB014） [PPL4-1]（特別講演）Parametric Effect Monads and Semantics of Effect Systems 　　○Shin-ya Katsumata (Kyoto Univeristy) 　　(ACM POPL 2014にて発表) [PPL4-2] 分割できながら等価：型レベル・エイリアス ○Jacques Garrigue（名古屋大学） [PPL4-3] 代数的データ構造を扱う関数型プログラムの検証法 ○岡本大輔（筑波大学）海野広志（筑波大学） [PPL4-4] コード生成のための自然演繹 ○須藤悠斗（筑波大学コンピュータサイエンス専攻） Oleg Kiselyov（筑波大学コンピュータサイエンス専攻）亀山幸義（筑波大学コンピュータサイエンス専攻） ◎ソフトウェア論文セッション (2) 9月9日（火） 15:15-16:45 （IB011）座長：小宮常康 (電気通信大学) [ソフト2-1] REMViewer:複数回実行されたJavaメソッドの実行経路可視化ツール ○松村俊徳（大阪大学大学院情報科学研究科）石尾　隆（大阪大学大学院情報科学研究科）鹿島　悠（大阪大学大学院情報科学研究科）井上　克郎（大阪大学大学院情報科学研究科） [ソフト2-2] シーケンス図を用いたモデル検査支援ツール ○後藤隼弐（フェリカネットワークス株式会社）吉岡信和（国立情報学研究所） [ソフト2-3] RepositoryProbe: リポジトリマイニングのためのデータセット作成支援ツール ○高澤亮平（早稲田大学）坂本一憲（国立情報学研究所）鷲崎弘宜（早稲田大学）深澤良彰（早稲田大学） ◎一般セッション (4)：データ構造とプログラミング 9月9日（火） 15:15-16:45 （IB013）座長：南出靖彦（筑波大学） [一般4-1] Towards A Trace-based Approach to Increasing the Comprehensibility and Predictability of Bidirectional Graph Transformations ○Soichiro Hidaka（National Institute of Informatics） Martin Billes（Augsburg University） Quang Minh Tran（Daimler Center for IT Innovations, Technical University of Berlin） [一般4-2] RePair流高階圧縮アルゴリズムの最適化 ○武田広太郎（東京大学大学院情報理工学系研究科）小林直樹（東京大学大学院情報理工学系研究科）松田一孝（東京大学大学院情報理工学系研究科） [一般4-3] SGL Hierarchical Bridging Model for Parallel Programming ○LI Chong（National Institute of Informatics / Université Paris-Est, France） HAINS Gaétan（Université Paris-Est, France / INSA Centre, France） ◎PPLセッション (5)：非決定性とスケジューリング 9月9日（火） 15:15-16:45 （IB014） [PPL5-1] 公平な並列実行のためのゲーム意味論 ○西村進（京都大学大学院理学研究科） [PPL5-2] Observational Equivalence Using Schedulers for Quantum Processes Kazuya Yasuda（University of Tokyo） Takahiro Kubota（University of Tokyo） ○Yoshihiko Kakutani（University of Tokyo） [PPL5-3] Prolog再考: 急がないで推測 ○Oleg Kiselyov（Tsukuba）亀山幸義（Tsukuba） ◎一般セッション (5)：システムソフトウェア実装 9月10日（水） 10:00-12:00 （IB011）座長：光来健一（九州工業大学） [一般5-1]（特別講演）GPUvm: Why Not Virtualizing GPUs at the Hypervisor? 　　Yusuke Suzuki （Keio University）　　Shinpei Kato （Nagoya University）　　Hiroshi Yamada （Tokyo University of Agriculture and Technology）　　○Kenji Kono （Keio University）　　(USENIX ATC '14にて発表) [一般5-2] 仮想マシンモニタによるマルウェアプロセスの実行抑止 ○本田惇（電気通信大学情報理工学研究科総合情報学専攻）高橋一志（電気通信大学情報理工学研究科総合情報学専攻）大山恵弘（電気通信大学情報理工学研究科総合情報学専攻） [一般5-3] Silhouettes: ディスプレイ間を移動可能な人物の実像を用いた情報通知システムの試作 ○丹羽佑輔（名古屋工業大学大学院情報工学専攻）白松俊（名古屋工業大学大学院情報工学専攻）大囿忠親（名古屋工業大学大学院情報工学専攻）新谷虎松（名古屋工業大学大学院情報工学専攻） [一般5-4] 既存プレゼンテーション支援システムのWeb連携に基づく双方向プレゼンテーションの実現 ○井上良太（名古屋工業大学）丹羽佑輔（名古屋工業大学）白松俊（名古屋工業大学）大囿忠親（名古屋工業大学）新谷虎松（名古屋工業大学） ◎FOSEセッション 9月10日（水） 10:30-12:00 （IB013）座長：杉山安洋（日本大学） [FOSE-1] 過去のPBLの情報を用いた工数見積り支援ツールの開発 ○齋藤尊（公立はこだて未来大学）新美礼彦（公立はこだて未来大学）伊藤恵（公立はこだて未来大学） [FOSE-2] プログラム理解のためのコードリーディング支援ツールの提案と実装 ○大村裕（東京工業大学・大学院情報理工学研究科・計算工学専攻）渡部卓雄（東京工業大学・大学院情報理工学研究科・計算工学専攻） ◎PPLセッション (6)：言語実装 9月10日（水） 10:00-12:00 （IB014） [PPL6-1]（特別講演）SML# in Industry: A Practical ERP System Development 　　○Atsushi Ohori （Tohoku University）　　Katsuhiro Ueno （Tohoku University）　　Kazunori Hoshi （NEC Solution Innovators, Ltd.）　　Shinji Nozaki （NEC Solution Innovators, Ltd.）　　Takashi Sato （NEC Solution Innovators, Ltd.）　　Tasuku Makabe （NEC Solution Innovators, Ltd.）　　Yuki Ito （NEC Solution Innovators, Ltd.）　　(ACM ICFP 2014にて発表) [PPL6-2] Processingアプリケーション開発のための視覚的ドメイン特化言語の実装 ○栗原あずさ（法政大学大学院情報科学研究科）佐々木晃（法政大学情報科学部）脇田建（東京工業大学大学院情報理工学研究科）細部博史（法政大学情報科学部） [PPL6-3] 高レベルLLVMマクロとしてのMetaOCaml ○高島尚希（筑波大学コンピュータサイエンス専攻） Oleg Kiselyov（筑波大学コンピュータサイエンス専攻）亀山幸義（筑波大学コンピュータサイエンス専攻） [PPL6-4] Implementing a subset of Lambda Prolog in HyperLMNtal ○Alimujiang Yasen（Waseda University） Kazunori Ueda（Waseda University） ◎一般セッション (6)：知能，ユーザビリティ 9月10日（水） 13:15-15:15 （IB011）座長：櫻井祐子（九州大学） [一般6-1]（特別講演）Two Case Studies for Trading Multiple Indivisible Goods with Indifferences 　　Akihisa Sonoda （Kyushu University）　　Etsushi Fujita （Kyushu University）　　○Taiki Todo （Kyushu University）　　Makoto Yokoo （Kyushu University）　　(AAAI-14にて発表) [一般6-2]（特別講演）Intelligence Arms Race: Delayed Reward Increases Complexity of Agent Strategies 　　○Hirotaka Osawa （University of Tsukuba）　　(AAMAS 2014にて発表) [一般6-3] ASIRRAシステムに対する機械的な突破の検証 ○飯田貴章（東京電機大学）藤本衡（東京電機大学） [一般6-4] リモート・ユーザビリティテストの実施容易性と有効性の評価実験 ○西本光司（公立はこだて未来大学）南部美砂子（公立はこだて未来大学）伊藤恵（公立はこだて未来大学） ◎PPLセッション (7) 9月10日（水） 13:15-15:15 （IB014） [PPL7-1] 対話的修正と対象プログラムとの合成手法 ○森口　草介（関西学院大学）高橋　和子（関西学院大学） [PPL7-2] 検証済みのコードによるCoqからScalaへのコード抽出 ○逸見港（東京大学）田辺良則（国立情報学研究所）今井宜洋（有限会社ITプランニング）萩谷昌己（東京大学） [PPL7-3] Weak HOASを用いたFeatherweight JavaとFeatherweight GJのCoq上での形式化 ○奥村健太郎（京都大学大学院情報学研究科）五十嵐淳（京都大学大学院情報学研究科） [PPL7-4] Aπ計算のCoqによる形式化 ○安武祥平（東京工業大学）渡部卓雄（東京工業大学） ◎一般セッション (7)：分散システム，言語処理系 9月10日（水） 15:30-17:00 （IB011）座長：細部博史（法政大学） [一般7-1] 関数型言語SML#における64ビット対応への取り組み ○逢坂美冬（東北大学）佐々木智啓（東北大学） Charles Mejia Cruz（東北大学）上野雄大（東北大学）大堀淳（東北大学） [一般7-2] 通信制約を考慮した遠隔介護のための適応型コミュニケーション支援システムの実現 ○片山真也（名古屋工業大学）白松俊（名古屋工業大学）大囿忠親（名古屋工業大学）新谷虎松（名古屋工業大学） [一般7-3] 数式処理に基づくハイブリッドシステムシミュレータHyroseの大規模モデルシミュレーションに向けた拡張 ○河野文彦（早稲田大学大学院基幹理工学研究科）小林輝哉（早稲田大学大学院基幹理工学研究科）松本翔太（早稲田大学大学院基幹理工学研究科）上田和紀（早稲田大学理工学術院） ◎一般セッション (8)：ソフトウェア工学 9月10日（水） 15:30-17:00 （IB014）座長：花川典子（阪南大学） [一般8-1] BABOKを活用したチェックシートによるRFP評価の試み ○斉藤篤史（公立はこだて未来大学）伊藤恵（公立はこだて未来大学） [一般8-2] When Project Centralization and Random Testing Meet --Efficient Automatic Testing of Multiple Software Product Variants-- ○Lei Ma（The University of Tokyo） Cyrille Artho（AIST / RISEC） Cheng Zhang（The University of Waterloo） Hiroyuki Sato（The University of Tokyo） [一般8-3] 開発のためのCMMIの成熟度レベルごとの関連プロセス領域ネットワークの中心性可視化 ○日下部茂（九州大学）林信宏（九州大学）大森洋一（九州大学）荒木啓二郎（九州大学） ◎デモ・ポスターセッション 9月9日（火） 17:00-18:00 （講義室前プレゼンスペース） [ポスター-1] Coqを使ったライン型ネットワークトポロジー上でのCCNのモデル化と検証について森嶋崇（関西学院大学）後藤瑞貴（関西学院大学）高橋和子（関西学院大学） [ポスター-2] ページ回収によるOSノイズを削減するシステム高橋秀明（電気通信大学）高橋一志（電気通信大学 / JST, CREST）大山恵弘（電気通信大学 / JST, CREST） [ポスター-3] 拡張可能で安全な統合言語クエリ鈴木健一（筑波大学コンピュータサイエンス専攻）オレッグ・キセリョーヴ（筑波大学コンピュータサイエンス専攻）亀山幸義（筑波大学コンピュータサイエンス専攻） [ポスター-4] PBL向けフォーマル/インフォーマルをまたがる学習サービス大場　みち子（公立はこだて未来大学）山口　琢（公立はこだて未来大学） [ポスター-5] 妥当なPCLA表現の帰納的定義とその正当性について後藤瑞貴（関西学院大学）高橋和子（関西学院大学） [ポスター-6] FOSE2014の開催と目的尾花将輝（大阪工業大学）花川典子（阪南大学）杉山安洋（日本大学） [ポスター-7] Shiranui: テストフレンドリーなライブプログラミング言語環境今井朝貴（東京工業大学理学部情報科学科）増原英彦（東京工業大学大学院情報理工学研究科数理・計算科学専攻）青谷知幸（東京工業大学大学院情報理工学研究科数理・計算科学専攻） [ポスター-8] シェルコマンドを型安全に利用するための領域特化言語OCommand 朝倉泉（東京工業大学大学院情報理工学研究科数理・計算科学専攻）増原英彦（東京工業大学大学院情報理工学研究科数理・計算科学専攻）青谷知幸（東京工業大学大学院情報理工学研究科数理・計算科学専攻） [ポスター-9] LLVMを活用した例外処理の実現のためのコンパイラ基盤COINS の拡張産一傑（広島市立大学）川端英之（広島市立大学）北村俊明（広島市立大学） [ポスター-10] 分析・モニタリングのために作文活動を測定するシステムの設計山口琢（公立はこだて未来大学大学院）大場みち子（公立はこだて未来大学）高橋修（公立はこだて未来大学）

1 0

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Logic-ml