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

早稲田大学高等研究所 / 慶應義塾大学論理と感性のグローバル研究センター共催「Workshop in Logic and Philosophy of Mathematics」(7月14-15日)のご案内
by Makoto Fujiwara 10 Jul '17

10 Jul '17

早稲田大学の藤原誠です。先日ご案内させていただいた早稲田大学高等研究所 / 慶應義塾大学論理と感性のグローバル研究センター共催「Workshop in Logic and Philosophy of Mathematics」について最新の情報を流させていただきます。 14日15日ともに参加自由です。どうぞふるってご参加ください。 ------------------------------------------------------------------- We apologize if you receive this message more than once. --------------------------------------------------------------------- We announce the following “Workshop in Logic and Philosophy of Mathematics”. The first day is at Mita campus of Keio University and the second day is at Waseda campus of Waseda University. 7月14日は慶應義塾大学三田キャンパス、7月15日は早稲田大学早稲田キャンパスでの開催になりますのでご注意下さい。 ---- Workshop in Logic and Philosophy of Mathematics Date: July 14 (Fri) and 15 (Sat), 2017 日時: 2017年7月14日(金), 7月15日(土) Place: G-Lab, 6th floor, East Building, Mita campus of Keio University (14th); Meeting Room #1, 5th Floor, Bldg. 9, Waseda campus of Waseda University (15th). 場所: 慶應義塾大学三田キャンパス東館6階G-Lab (14日); 早稲田大学早稲田キャンパス9号館5階第一会議室 (15日). For more details, please see the following page: 詳細は以下をご覧ください。 https://www.waseda.jp/inst/wias/news/2017/07/04/4467/ ---- Program: 1. July 14 (Friday, G-Lab, 6th floor, East Building, Mita campus of Keio University): Time: 13:00-18:00 Speakers: Andrew Arana (Université Paris 1 Panthéon-Sorbonne, IHPST), Kengo Okamoto (Tokyo Metropolitan University), Ryota Akiyoshi (Waseda University), Makoto Fujiwara (Waseda University) The details will be announced soon at the following page: https://abelard.flet.keio.ac.jp/jindex.php <https://abelard.flet.keio.ac.jp/jindex.php> 2. July 15 (Saturday, Meeting Room #1, 5th Floor, Bldg. 9, Waseda Campus of Waseda University) Talk 1: 13:00-14:00 Ryoma Shinya (The University of Tokyo) Title: Almost every simply typed λ-term has a long β-reduction sequence Abstract: It is well known that the length of a β-reduction sequence of a simply typed λ-term of order k can be huge; it is as large as k-fold exponential in the size of the λ-term in the worst case. We consider the following relevant question about quantitative properties, instead of the worst case: how many simply typed λ-terms have very long reduction sequences? We provide a partial answer to this question, by showing that asymptotically almost every simply typed λ-term of order k has a reduction sequence as long as (k − 2)-fold exponential in the term size, under the assumption that the arity of functions and the number of variables that may occur in every subterm are bounded above by a constant. The work has been motivated by quantitative analysis of the complexity of higher-order model checking. Talk 2: 14:00-15:00 Taishi Kurahashi (National Institute of Technology, Kisarazu College) Title: On partial disjunction properties of theories containing PA Abstract: It is well-known that intuitionistic predicate logic and Heyting Arithmetic have the disjunction property (DP). For intuitionistic logic, DP seems to reflect its constructivity. In classical logic, DP plays a different role. If a theory T in classical logic has DP, then T is complete because the law of excluded middle is valid. Thus in classical logic, every \Sigma_1-definable consistent extension of Peano Arithmetic PA does not have DP by the Gödel–Rosser first incompleteness theorem. On the other hand, PA enjoys a partial disjunction property. Let \Gamma be a class of formula. We say that a theory T has the \Gamma-disjunction property (\Gamma-DP) iff for any \Gamma sentences \varphi and \psi, at least one of \varphi or \psi is provable in T whenever \varphi \lor \psi is provable in T. It is known that PA has \Sigma_1-DP but does not have \Pi_1-DP. In this talk, we present several results concerning partial disjunction properties and other related properties of theories containing PA which is not necessarily \Sigma_1-definable. Talk 3: 15:20-16:20 Naosuke Matsuda (Kanagawa University) Title: Some extensions of de Jongh's theorem Abstract: It is obvious that if a propositional formula A is provable in intuitionistic propositional calculus, then each arithmetical instance is provable in Heyting Arithmetic. The converse of this statement is known as de Jongh's theorem. In this talk, I give an introduction to de Jongh's theorem and introduce some extensional works. Talk 4: 16:20-17:20 Masahiko Sato (Kyoto University) Title: A common notation system for lambda calculus and combinatory logic Abstract: We present a notation system which can be used to faithfully represent both the terms of lambda calculus and combinatory logic. We show the faithfullness of the representations by observing that the representations respect the beta and eta reduction rules. We also argue that Curry's Last Problem (J.R.Hindley, Curry's Last Problem: Imitating lambda-beta-reduction in Combinatory Logic) in its original form is an ill-posed problem, and can be solved naturally by expressing the problem in our notation system. --------------------------------------------------------------------- Organizers: Ryota Akiyoshi (Waseda Institute for Advanced Study, Waseda University) Makoto Fujiwara (Waseda Institute for Advanced Study, Waseda University) Mitsuhiro Okada (Global Research Center for Logic and Sensibility, Keio University) Co-host: Waseda Institute for Advanced Study (Waseda University), Global Research Center for Logic and Sensibility (Keio University) Contact: Ryota Akiyoshi georg.logic(a)gmail.com <mailto:georg.logic@gmail.com> ============================================ 藤原誠 (Makoto Fujiwara) 早稲田大学高等研究所 (Waseda Institute for Advanced Study, Waseda University) E-mail: makoto_fujiwara(a)aoni.waseda.jp ============================================

2 1

47th TRS meeting (参加者募集)
by Munehiro Iwami 07 Jul '17

07 Jul '17

皆様島根大学の岩見と申します。 9月25～27日に開催される「第47回 TRS Meeting」の参加者募集をご案内致します。今回は水の都とよばれる松江の宍道湖岸のホテルで開催します。皆様、ぜひ参加をご検討下さい。講演題目と講演時間は後程連絡して頂く形で構いません。和室シングルルームは宍道湖眺望ありです。通常のシングルルームは宍道湖眺望なしです。 7月14日（金）までに岩見へメールにて連絡してください。 -- 岩見宗弘島根大学総合理工学研究科情報システム学領域 E-mail: munehiro(a)cis.shimane-u.ac.jp ----------------------------------------- 47th TRS Meeting September 25 - 27, 2017 Matsue, Japan http://www.cis.shimane-u.ac.jp/~munehiro/trs-meeting47/ About TRS Meeting Term Rewriting Meeting (TRS Meeting) is a biannual informal workshop that aims at promoting the research on rewriting and related areas. Participants are requested to give a talk(s) of approximately 15 - 60 minutes in English on their research activities. The subject of the talk may not be one's original result; for example, explaining an interesting paper is perfectly OK. (See Rewriting Researchers Forum for further information: http://www.jaist.ac.jp/~hirokawa/trs-meeting/). Basic Information Date September 25 (Mon) - 27 (Wed), 2017 Venue Matsue New Urban Hotel (webpage in Japanese) 40-1, Nishicha-machi, Mstsue-shi, Shimane, 690-0845, Japan Fee Registration: 6,000 JPY (includes coffee breaks and meeting room) Accomodation: 8,400 JPY (Sep. 25) (includes breakfast and dinner) and 12,560 JPY (Sep. 26) (includes breakfast and bunquet) Tentative Schedule Room Koto (we will have a screen and a whiteboard) Opening 13:30, September 25 Closing 12:00, September 27 Timetable Tentative Registration Deadline July 14th (Fri), 2017 Please fill in the following registration form and send it to Munehiro Iwami (munehiro [at] cis.shimane-u.ac.jp) by e-mail. Items marked with * can be sent later. -------------------------------------------------------------------------------------------- Registration Form of the 47th TRS Meeting name: affiliation: * title of talk: * approximate duration of talk (15 - 60 minutes): preference on your room: [standard single room / Japanese style single room] (choose one) (In case of partial participation, please contact us) --------------------------------------------------------------------------------------------

1 0

FLOPS 2018: Call for Papers
by koba＠kb.is.s.u-tokyo.ac.jp 04 Jul '17

04 Jul '17

皆様、東京大学の小林です。 FLOPS 2018 の論文募集案内をお送りいたします。小林直樹東京大学大学院情報理工学系研究科コンピュータ科学専攻〒113-0033 東京都文京区本郷7-3-1 Phone: 03-5841-4124 Fax: 03-5841-4124 email: koba(a)is.s.u-tokyo.ac.jp ----------------- FIRST Call For Papers FLOPS 2018: 14th International Symposium on Functional and Logic Programming 9-11 May, 2018, Nagoya, Japan http://www.sqlab.jp/FLOPS2018/ Writing down detailed computational steps is not the only way of programming. The alternative, being used increasingly in practice, is to start by writing down the desired properties of the result. The computational steps are then (semi-)automatically derived from these higher-level specifications. Examples of this declarative style include functional and logic programming, program transformation and re-writing, and extracting programs from proofs of their correctness. FLOPS aims to bring together practitioners, researchers and implementors of the declarative programming, to discuss mutually interesting results and common problems: theoretical advances, their implementations in language systems and tools, and applications of these systems in practice. The scope includes all aspects of the design, semantics, theory, applications, implementations, and teaching of declarative programming. FLOPS specifically aims to promote cross-fertilization between theory and practice and among different styles of declarative programming. Scope FLOPS solicits original papers in all areas of the declarative programming: * functional, logic, functional-logic programming, re-writing systems, formal methods and model checking, program transformations and program refinements, developing programs with the help of theorem provers or SAT/SMT solvers; * foundations, language design, implementation issues (compilation techniques, memory management, run-time systems), applications and case studies. FLOPS promotes cross-fertilization among different styles of declarative programming. Therefore, submissions must be written to be understandable by the wide audience of declarative programmers and researchers. Submission of system descriptions and declarative pearls are especially encouraged. Submissions should fall into one of the following categories: * Regular research papers: they should describe new results and will be judged on originality, correctness, and significance. * System descriptions: they should contain a link to a working system and will be judged on originality, usefulness, and design. * Declarative pearls: new and excellent declarative programs or theories with illustrative applications. System descriptions and declarative pearls must be explicitly marked as such in the title. Submissions must be unpublished and not submitted for publication elsewhere. Work that already appeared in unpublished or informally published workshops proceedings may be submitted. See also ACM SIGPLAN Republication Policy. Proceedings The proceedings will be published by Springer International Publishing in the Lecture Notes in Computer Science (LNCS) series, as a printed volume as well as online in the digital library SpringerLink. Post-proceedings: The authors of 4-7 best papers will be invited to submit the extended version of their FLOPS paper to a special issue of the journal Science of Computer Programming (SCP). Important dates 13 November 2017 (any time zone): Abstract Submission 20 November 2017 (any time zone): Submission deadline 15 January 2018: Author notification 9-11 May 2018: FLOPS Symposium Invited Talks To be announced Submission Submissions must be written in English and can be up to 15 pages long including references, though pearls are typically shorter. The formatting has to conform to Springer's guidelines. Regular research papers should be supported by proofs and/or experimental results. In case of lack of space, this supporting information should be made accessible otherwise (e.g., a link to a Web page, or an appendix). Papers should be submitted electronically at https://easychair.org/conferences/?conf=flops2018 Program Committee Andreas Rossberg Google, Germany Atsushi Ohori Tohoku University, Japan Bruno C. D. S. Oliveira The University of Hong Kong, China Carsten Fuhs Birkbeck, University of London, UK Chung-chieh Shan Indiana University, USA Didier Remy INRIA, France Harald Sondergaard The University of Melbourne, Australia Jacques Garrigue Nagoya University, Japan Jan Midtgaard Technical University of Denmark, Denmark Joachim Breitner University of Pennsylvania, USA John Gallagher Roskilde University, Denmark and IMDEA Software Institute, Spain (co-chair) Jorge A Navas SRI International, USA Kazunori Ueda Waseda University, Japan Kenny Zhuo Ming Lu School of Information Technology, Nanyang Polytechnic, Singapore María Alpuente Universitat Politècnica de València, Spain María Garcia De La Banda Monash University, Australia Martin Sulzmann Karlsruhe University of Applied Sciences, Germany (co-chair) Meng Wang University of Kent, UK Michael Codish Ben-Gurion University of the Negev, Israel Michael Leuschel University of Düsseldorf, Germany Naoki Kobayashi University of Tokyo, Japan Nikolaj Bjørner Microsoft Research, USA Robert Glück University of Copenhagen, Denmark Samir Genaim Universidad Complutense de Madrid, Spain Siau Cheng Khoo National University of Singapore, Singapore Organizers Martin Sulzmann Karlsruhe University of Applied Sciences (co-chair) John Gallagher Roskilde University and IMDEA Software Institute (co-chair) Makoto Tatsuta National Institute of Informatics, Japan (General Chair) Koji Nakazawa Nagoya University, Japan (Local Chair)

1 0

ARANA博士パリ第1大哲学科准教授Geometrical knowledge and　geometrical　legitimacy7月４、１１、１９日慶応大三田
by Mitsuhiro Okada 03 Jul '17

03 Jul '17

次の3回の連続セミナートークを予定しています。アナウンスが第1回目の開催日に間に合わないかもしれませんが、次の内容をこのメールリストに流させて頂きけるとありがたいです。よろしくお願いいたします。岡田光弘　慶應義塾大学文学部哲学専攻 ─────────────────────────────── ＜Andrew ARANA パリ第1大学哲学科准教授　数学の哲学連続トークと討論 7月4日、11日、19日、Geometrical knowledge and　geometrical　 legitimacy ＞　July 4th, 11th,19th, Mita Campus, Keio University 次のようなPhilosophy of mathematics 連続セミナートークを Andrew ARANA 博士にお願いしています。連続セミナートーク・テーマ　Theme Geometrical knowledge and geometrical legitimacy I, II, III 初回Iはoverview的講演をお願いしてます。この告知メールは初回のトークのあとに届く可能性が高いですが、 2回目、3回目の内容は初回と独立にお聴きいただくこともできますので2回目以降からのご参加も歓迎いたします。スピーカー Speaker Andrew Arana, パリ第1大学哲学科准教授、Dept of Philosophy, University of Paris-1 場所：慶應大三田キャンパス大学院棟３１３番教室 Room 313, Graduate School Building, Mita Campus, Keio university (構内図 Campus Mapの8番です。　#8 of this map.) https://www.keio.ac.jp/ja/maps/mita.html One hour talk and 30 minutes discussion 第1回7月4日 (火) July 4th (Tues) 18;00-19:30 第2回　7月11日(火)　July 11th (Tues) 18:00-19:30 第3回 7月１９日（火）July 19th (Tues) 18:00-19:30 ---------------------------------------------------------------- この会合とは別に、早稲田大学高等研究所―慶應義塾大学論理と感性のグローバル研究センター共催の「論理と数学の哲学」会合(7月14日三田キャンパス、１５日早稲田キャンパス)でもArana先生が14日に話されます。) Ａｎｄｒｅｗ　Arana, Proofs and Meaning in Arithmetic 14日、15日とも13:00に開始を予定しています。こちらの案内はプログラムが決まり次第追ってお知らせします。14日は慶應大三田キャンパス東館６階G-Lab　Ａｌｓｏ　the Waseda-U=Keio U Joint Workshop on “Logic and Philosophy of Mathematics” Is acheduled. Prof. Arana is going to give another talk there on 14th at G-Lab, 6th floor, East Building, Mita Campus, Keio University. We will announce the program soon. ------------------------------------------- 論理と感性のグローバル研究センター(論理班)、三田ロジックセミナー共催お問い合わせ Contact: logic(a)abelard.flet.keio.ac.jp (セミナー事務局専用アドレス)　慶応義塾大学文学部哲学専攻岡田光弘研究室内 ----------------------------------------

1 0

3rd CFP +++ extended deadline +++ IWC 2017 (with FSCD in Oxford)
by Fujita Kenetsu 01 Jul '17

01 Jul '17

皆様，群馬大学の藤田と申します． 9月の IWC 2017(Oxford)の締切が7/5まで延長されましたのでご案内をさせていただきます．どうぞ宜しくお願い致します． ----- (* Apologies for any cross-postings. *) ===================================================================== Call for Papers IWC 2017 6th International Workshop on Confluence September 8th, 2017, Oxford, United Kingdom Collocated with FSCD 2017 http://cl-informatik.uibk.ac.at/events/iwc-2017/ ===================================================================== Confluence provides a general notion of determinism and is widely viewed as one of the central properties of rewriting. Confluence relates to many topics of rewriting (completion, modularity, termination, commutation, etc.) and has been investigated in many formalisms of rewriting such as first-order rewriting, lambda-calculi, higher-order rewriting, constrained rewriting, conditional rewriting, etc. Recently there is a renewed interest in confluence research, resulting in new techniques, tool support, certification as well as new applications. The International Workshop on Confluence (IWC) aims at promoting further research in confluence and related properties. IWC 2017 is collocated with FSCD 2017. Previous editions of the workshop were held in Nagoya (2012), Eindhoven (2013), Vienna (2014), Berlin (2015), and Obergurgl (2016). During the workshop, the 6th Confluence Competition (CoCo 2017) takes place. IMPORTANT DATES: * submission Wednesday, July 5th, 2017 (extended) * notification Saturday, July 22nd, 2017 * final version Saturday, August 5th, 2017 * workshop Friday, September 8th, 2017 (deadlines are AoE) TOPICS: Specific topics of interest include: * confluence and related properties (unique normal forms, commutation, ground confluence) * completion * critical pair criteria * decidability issues * complexity issues * system descriptions * certification * applications of confluence INVITED SPEAKERS: * Stefan Kahrs (University of Kent) * Patrick Bahr (IT University of Copenhagen) PROGRAM COMMITTEE: * Beniamino Accattoli (INRIA) * Jörg Endrullis (Vrije Universiteit Amsterdam) * Bertram Felgenhauer (University of Innsbruck) * Ken-Etsu Fujita (Gumma University) * Philippe Malbos (Université Claude Bernard Lyon 1) * Jakob Grue Simonsen (University of Copenhagen) SUBMISSION: We solicit short papers or extended abstracts of at most five pages. There will be no formal reviewing. In particular, we welcome short versions of recently published articles and papers submitted elsewhere. The program committee checks relevance and may provide additional feedback. The accepted papers will be made available electronically before the workshop. The page limit for papers is 5 pages in EasyChair style. Short papers or extended abstracts must be submitted electronically through the EasyChair system at: https://www.easychair.org/conferences/?conf=iwc2017 EasyChair style: http://easychair.org/publications/for_authors -----

1 0

第52回MLG数理論理学研究集会のご案内
by Suzuki, Nobu-Yuki 30 Jun '17

30 Jun '17

皆さま静岡大学の鈴木信行と申します。今年度の　MLG 数理論理学研究集会　の世話人（代表）をいたします。今年度、第52回MLG 数理論理学研究集会は、以下の要領で開催する予定です。・期間: 2017年12月1日(金)午後 -- 12月3日(日)午前・場所: 静岡大学　静岡キャンパス　〒422-8529　静岡県静岡市駿河区大谷836 　 (JR静岡駅よりバスで約30分) ご予定にお加えいただけますよう、お願いいたします。ご案内も随時送信しますが、次のHPでも最新のご案内を申し上げまので、ご覧ください。（現時点では、まだあまり情報はありません） https://wwp.shizuoka.ac.jp/logic-suzuki-mlg/ よろしくお願い致します。

1 0

First CFP: Eleventh International Workshop on Juris-informatics (JURISIN 2017)
by Ken Satoh 28 Jun '17

28 Jun '17

First CFP: Eleventh International Workshop on Juris-informatics (JURISIN 2017) (associated with JSAI International Symposia on AI 2017 (IsAI-2017)) homepage: http://research.nii.ac.jp/~ksatoh/jurisin2017 ** Workshop dates November 13 - 15, 2017 ** Venue Tokyo Campus, University of Tsukuba, Tokyo, Japan http://www.tsukuba.ac.jp/en/access/tokyocampus-access ** Important Dates Submission Deadline: August 28, 2017 Notification: October 1, 2017 Camera-ready due: October 13, 2017 ** 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. ** 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 applications of robotics and AI to society 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 ** Invited Speakers Kevin D. Ashley (University of Pittsburgh) Katsumi Nitta (Tokyo Institute of Technology) ** Submissions We welcome and encourage the submission of high quality, original papers, which are not simultaneously submitted for publication elsewhere Papers should be written in English, formatted according to the Springer Verlag LNCS style in a pdf form, which can be obtained from http://www.springeronline.com and not exceed 14 pages including figures, references, etc. If you use a word file, please follow the instruction of the format, and then convert it into a pdf form and submit it at the paper submission page. If a paper is accepted, at least one author of the paper must register the workshop and present it. We strongly encourage an online registration. You can submit your paper at "https://easychair.org/conferences/?conf=jurisin2017". If you cannot submit a paper by EasyChair System by some trouble, please send email to "ksatoh[at]nii.ac.jp" ** Post Proceedings Selected papers will be published as a post-proceedings via Springer Verlag LNAI series after the second round of review after the workshop. ** Workshop Chair Ken Satoh, National Institute of Informatics and Sokendai, Japan ** Steering Committee Members Takehiko Kasahara, Toin Yokohama University Makoto Nakamura, Nagoya University, Japan Katsumi Nitta, Tokyo Institute of Technology, Japan Seiichiro Sakurai, Meiji Gakuin University, Japan Ken Satoh, National Institute of Informatics and Sokendai, Japan Satoshi Tojo, Japan Advanced Institute of Science and Technology(JAIST), Japan Katsuhiko Toyama, Nagoya University, 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 Thomas Agotnes, University of Bergen, Norway Ryuta Arisaka, National Institute of Informatics, Japan Kristijonas Cyras Imperial College London Marina De Vos, University of Bath, UK Tatsuhiko Inatani, Kyoto University, Japan Phan Minh Dung, AIT, Thailand Guido Governatori, Data61, Australia Tokuyasu Kakuta, Nagoya University, Japan Yoshinobu Kano, Shizuoka University, Japan Nguyen Le Minh, JAIST, Japan Beishui Liao, Zhejiang University, China Hatsuru Morita, Tohoku University, Japan Makoto Nakamura, Nagoya University, Japan Yoshiaki Nishigai, Nihon University, Japan Konatsu Nishigai, Tokyo Metropolitan University, Japan Katsumi Nitta, Titech, Japan Paulo Novais, University of Minho, Portugal Julian Padget, University of Bath, UK Ginevra Peruginelli, ITTIG-CNR, Italy Katsuhiko Sano, Hokkaido University, Japan Giovanni Sartor, EUI/CIRSFID, Italy Seiichiro Sakurai, Meiji Gakuin University, Japan Ken Satoh, National Institute of Informatics and Sokendai, Japan Akira Shimazu, JAIST, Japan Fumio Shinpo, Keio University, Japan Satoshi Tojo, JAIST, Japan Katsuhiko Toyama, Nagoya University, Japan Rob van den Hoven van Genderen, VU University Amsterdam, The Netherlands Leon van der Torre, University of Luxembourg, Luxembourg Bart Verheij, University of Groningen, The Netherlands Harumichi Yuasa, Institute of Information Security, Japan Yueh-Hsuan Weng, Tohoku University, Japan For any inquiry concerning the workshop, please send it to "ksatoh[at]nii.ac.jp"

1 0

Workshop in Logic and Philosophy of Mathematics
by Makoto Fujiwara 28 Jun '17

28 Jun '17

皆様早稲田大学の藤原誠です。標記ワークショップのご案内をさせていただきます。 ------------------------------------------------------------------- We apologize if you receive this message more than once. --------------------------------------------------------------------- We announce the following “Workshop in Logic and Philosophy of Mathematics” 次のようなワークショップ「Workshop in Logic and Philosophy of Mathematics」を予定しております。参加自由です。 The exact list of speakers and places will be announced later. The first day is at Mita campus of Keio University and the second day is at Waseda campus of Waseda University. スピーカーや開催場所の詳細につきましては後ほど改めてご連絡させていただきます。（7月14日は慶應義塾大学三田キャンパス，7月15日は早稲田大学早稲田キャンパスでの開催になります） ---- Workshop in Logic and Philosophy of Mathematics Date: July 14 (Fri) and 15 (Sat), 2017 日時: 2017年7月14日(金), 7月15日(土) Place: Mita campus of Keio University (14th) and Waseda campus of Waseda University (15th). 場所: 慶應義塾大学三田キャンパス（14日），早稲田大学早稲田キャンパス（15日） ---- Program: 1. July 14 (Friday, Mita campus of Keio University): Time: 13:00-18:00 Speakers: Andy Arana (Université Paris 1 Panthéon-Sorbonne, IHPST), Kengo Okamoto (Tokyo Metropolitan University), Ryota Akiyoshi (Waseda University), Makoto Fujiwara (Waseda University) 2. July 15 (Saturday, Waseda campus of Waseda University ) Time: 13:00-18:00 Speakers: Ryoma Shinya (The University of Tokyo), Taishi Kurahashi (National Institute of Technology, Kisarazu College), Naosuke Matsuda (Kanagawa University), Masahiko Sato (Kyoto University) --------------------------------------------------------------------- Organizers: Ryota Akiyoshi (Waseda Institute for Advanced Study, Waseda University) Makoto Fujiwara (Waseda Institute for Advanced Study, Waseda University) Mitsuhiro Okada (Global Research Center for Logic and Sensibility, Keio University) Co-host: Waseda Institute for Advanced Study (Waseda University), Global Research Center for Logic and Sensibility (Keio University) Contact: Ryota Akiyoshi georg.logic(a)gmail.com

1 0

CALL FOR PAPERS: Logic and Engineering of Natural Language Semantics 14 (LENLS 14)
by Katsuhiko Sano 27 Jun '17

27 Jun '17

[Apologies for multiple copies] ================================================================= CALL FOR PAPERS Logic and Engineering of Natural Language Semantics 14 (LENLS 14) Workshop Site : Bunkyo School Building in University of Tsukuba, Tokyo Campus Bunkyo-ku, Tokyo, Japan http://www.tsukuba.ac.jp/en/access/tokyocampus-access Dates : November 13-15, 2017 Contact Person: Katsuhiko Sano (Hokkaido University) Contact Email : lenls14[[at]]easychair.org Website : http://www.is.ocha.ac.jp/~bekki/lenls/ ================================================================= Chair: Katsuhiko Sano (Hokkaido University) Co-chair: Eric McCready (Aoyama Gakuin University) Daisuke Bekki (Ochanomizu University/JST CREST) Koji Mineshima (Ochanomizu University/JST CREST) Invited Speakers: - Craige Roberts (The Ohio State University) - Ivano Ciardelli (University of Amsterdam) - Shoichi Takahashi (Aoyama Gakuin University) LENLS is an annual international workshop on formal syntax, semantics and pragmatics. It will be held as one of the workshops of the JSAI International Symposia on AI (isAI2017) (https://www.ai-gakkai.or.jp/isai/) sponsored by the Japan Society for Artificial Intelligence (JSAI). Aims and Topics: ================ We invite submissions to this year's workshop on topics in formal syntax, semantics and pragmatics, and related fields, including but in no way limited to the following: - Formal syntax, semantics and pragmatics of natural language - Model-theoretic and/or proof-theoretic semantics of natural language - Computational Semantics - Game-theoretic/Bayesian approaches to pragmatics - Nonclassical Logic and its relation to natural language (especially Substructural/Fuzzy/Categorical/Topological logics) - Formal Philosophy of language - Scientific methodology and/or experimental design for linguistics Submissions: ============ Abstracts (anonymous, up to 4 pages, including figures and references, A4 size, with 12 point font) must be submitted electronically in PDF format at: https://easychair.org/conferences/?conf=lenls14 When the abstract is accepted, the author is expected to submit a full paper (10-14 pages) before the workshop. The online proceedings of the workshop will be available at the conference site. Important dates: ================ Abstract submission deadline: August 31, 2017 Notification of acceptance: September 30, 2017 Deadline for camera-ready copy: mid-October, 2017 LENLS14: November 13-15, 2017 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: ====================================== - Katsuhiko Sano (Hokkaido University) - Eric McCready (Aoyama Gakuin University) - Daisuke Bekki (Ochanomizu University/JST CREST) - Koji Mineshima (Ochanomizu University/JST CREST) - Alastair Butler (National Institute for Japanese Language and Linguistics) - Richard Dietz (iCLA, Yamanashi Gakuin University) - Naoya Fujikawa (Tokyo Metropolitan University) - Yoshiki Mori (University of Tokyo) - Yasuo Nakayama (Osaka University) - David Y. Oshima (Nagoya University) - Osamu Sawada (Mie University) - Wataru Uegaki (Leiden University) - Katsuhiko Yabushita (Naruto University of Education) - Tomoyuki Yamada (Hokkaido University) - Shunsuke Yatabe (Kyoto University) - Kei Yoshimoto (Tohoku University)

1 0

Talk by Georgios Fainekos on June 30
by urabenatsuki＠is.s.u-tokyo.ac.jp 26 Jun '17

26 Jun '17

Dear all (apologies for multiple copies), Let me advertise a talk by Georgios Fainekos on 30th June, 15:00-. Please find the title and the abstract below. You are all invited. Sincerely, -- Natsuki Urabe urabenatsuki(a)is.s.u-tokyo.ac.jp The University of Tokyo ---------- https://docs.google.com/document/d/1Qrg4c8XDkbO3tmns6tQwxn5l GHOrBON5LtHXXTpXDeA/edit?usp=sharing Fri 30 June 2017, 15:00–17:00 NII meeting room 2010 https://www.nii.ac.jp/en/about/access/ Georgios Fainekos <http://www.public.asu.edu/%7Egfaineko/> (Arizona State University), Beyond Requirements Falsification : Semi-formal methods and tools for the analysis of Cyber-Physical Systems Correct-by-design synthesis methods for Cyber-Physical Systems (CPS) are still in their infancy for CPS with complex physical dynamics. For that reason, a combination of design theories for simpler systems and/or ad-hoc design approaches are utilized. Hence, numerous design and implementation errors are discovered while CPS are operational in the field. Such errors can have catastrophic effects to human life and to the economy. Over the last few years, requirements guided falsification methods have proven to be a practical approach to the verification problem of industrial size CPS. However, requirements falsification is just one component of the necessary tools for the development of safe and reliable CPS. In this talk, we provide an overview of our research in providing support for all the stages of the development for CPS, from formal requirements elicitation and mining to system conformance to on-line monitoring. Most of our methods have been implemented in a Matlab (TM) toolbox called S-TaLiRo (System's TemporAl LogIc Robustness). Finally, in this talk, we demonstrate that S-TaLiRo can provide answers to challenge problems from the automotive industry. Bio: Georgios Fainekos is an Associate Professor at the School of Computing, Informatics and Decision Systems Engineering (SCIDSE) at Arizona State University (ASU). He is director of the Cyber-Physical Systems (CPS) Lab and he is currently affiliated with the NSF I/UCRC Center for Embedded Systems (CES) at ASU. He received his Ph.D. in Computer and Information Science from the University of Pennsylvania in 2008 where he was affiliated with the GRASP laboratory. He holds a Diploma degree (B.Sc. & M.Sc.) in Mechanical Engineering from the National Technical University of Athens and an M.Sc. degree in Computer and Information Science from the University of Pennsylvania. Before joining ASU, he held a Postdoctoral Researcher position at NEC Laboratories America in the System Analysis & Verification Group. He is currently working on Cyber-Physical Systems (CPS) and robotics. In particular, his expertise is on formal methods, logic, control theory, artificial intelligence, and optimization. His research has applications to automotive systems, medical devices, autonomous (ground and aerial) robots and human-robot interaction (HRI). In 2013, Dr. Fainekos received the NSF CAREER award. He was also recipient of the SCIDSE Best Researcher Junior Faculty award for 2013 and of the 2008 Frank Anger Memorial ACM SIGBED/SIGSOFT Student Award. Two of his conference papers have been nominated for student best paper awards. In 2016, Dr. Fainekos was the program co-Chair for the ACM International Conference on Hybrid Systems: Computation and Control.

1 0

国際会議 : 2nd CFP IWC 2017 (with FSCD in Oxford )
by Fujita Kenetsu 20 Jun '17

20 Jun '17

皆様，群馬大学の藤田と申します． 9月の IWC 2017 のご案内をさせていただきます．どうぞよろしくお願いいたします． ----- (* Apologies for any cross-postings. *) ===================================================================== Call for Papers IWC 2017 6th International Workshop on Confluence September 8th, 2017, Oxford, United Kingdom Collocated with FSCD 2017 http://cl-informatik.uibk.ac.at/events/iwc-2017/ ===================================================================== Confluence provides a general notion of determinism and is widely viewed as one of the central properties of rewriting. Confluence relates to many topics of rewriting (completion, modularity, termination, commutation, etc.) and has been investigated in many formalisms of rewriting such as first-order rewriting, lambda-calculi, higher-order rewriting, constrained rewriting, conditional rewriting, etc. Recently there is a renewed interest in confluence research, resulting in new techniques, tool support, certification as well as new applications. The International Workshop on Confluence (IWC) aims at promoting further research in confluence and related properties. IWC 2017 is collocated with FSCD 2017. Previous editions of the workshop were held in Nagoya (2012), Eindhoven (2013), Vienna (2014), Berlin (2015), and Obergurgl (2016). During the workshop, the 6th Confluence Competition (CoCo 2017) takes place. IMPORTANT DATES: * submission Saturday, July 1st, 2017 * notification Saturday, July 22nd, 2017 * final version Saturday, August 5th, 2017 * workshop Friday, September 8th, 2017 (deadlines are AoE) TOPICS: Specific topics of interest include: * confluence and related properties (unique normal forms, commutation, ground confluence) * completion * critical pair criteria * decidability issues * complexity issues * system descriptions * certification * applications of confluence INVITED SPEAKERS: * Stefan Kahrs (University of Kent) * tba PROGRAM COMMITTEE: * Beniamino Accattoli (INRIA) * Jörg Endrullis (Vrije Universiteit Amsterdam) * Bertram Felgenhauer (University of Innsbruck) * Ken-Etsu Fujita (Gumma University) * Philippe Malbos (Université Claude Bernard Lyon 1) * Jakob Grue Simonsen (University of Copenhagen) SUBMISSION: We solicit short papers or extended abstracts of at most five pages. There will be no formal reviewing. In particular, we welcome short versions of recently published articles and papers submitted elsewhere. The program committee checks relevance and may provide additional feedback. The accepted papers will be made available electronically before the workshop. The page limit for papers is 5 pages in EasyChair style. Short papers or extended abstracts must be submitted electronically through the EasyChair system at: https://www.easychair.org/conferences/?conf=iwc2017 EasyChair style: http://easychair.org/publications/for_authors -----

1 0

[LORI-VI] 1st Call for Participation
by Katsuhiko Sano 20 Jun '17

20 Jun '17

[Please circulate. Apologies for multiple copies] The Sixth International Conference on Logic, Rationality and Interaction September 11-14, 2017, Hokkaido University, Sapporo, Japan http://golori.org/lori2017/ [About LORI] The International Conference on Logic, Rationality and Interaction (LORI) conference series aims at bringing together researchers working on a wide variety of logic-related topics that concern the understanding of rationality and interaction. The series aims at fostering a view of Logic as an interdisciplinary endeavour, and supports the creation of an East-Asian community of interdisciplinary researchers. [Invited Speakers] Mike Dunn: Indiana University, U.S.A. Alan Hajek: Australian National University, Australia Nina Gierasimczuk: Technical University of Denmark, Denmark Natasha Alechina: University of Nottingham, UK Sara Negri: University of Helsinki, Finland Hiroakira Ono: JAIST, Japan [PC Chairs] Alexandru Baltag: University of Amsterdam, The Netherlands Jeremy Seligman: University of Auckland, New Zealand [Conference Organiser] Tomoyuki Yamada: Hokkaido University, Japan [News] ****** ASL Sponsorship ****** Student ASL members may apply for (limited) ASL travel funds that ASL is making available for sponsored meetings. For more on this, see http://www.aslonline.org/studenttravelawards.html . The deadline for student travel grant applications and recommendations for LORI VI is kindly extended to June 30th, 2017. [Website] For detailed conference information and registration, please visit http://golori.org/lori2017/ . [Sponsors] LORI Tsinghua University - University of Amsterdam Joint Research Centre for Logic Graduate School of Letters, Hokkaido University Association for Symbolic Logic [Contacts] Programme: The PC Chairs <lori6(a)easychair.org> Conference: Tomoyuki Yamada <tomoyuki.s.yamada(a)gmail.com>

1 0

教員公募（東北大学電気通信研究所教授）
by Atsushi Ohori 16 Jun '17

16 Jun '17

sonoteno皆様，PPLの皆様，logic-mlの皆様，メーリングリストをお借りして、教員公募の案内をお送りいたします．教授１名（理論計算機科学等を含む基礎研究分野），応募締切 6月30日です．(重複して受信された場合はご容赦ください) 東北大学大堀淳 ------------------------------------------------------------------------- 教員公募情報東北大学大電気通信研究所では、教授職の教員を下記により公募いたします。募集人員：教授１名所　　属：　システム・ソフトウェア研究部門コンピューティング情報理論研究分野専門分野：　　本分野では、情報の意味や計算の構造に関する基礎研究の飛躍的発展とその応用的展開を通じて、複雑で多様な情報のより高速、より安全、より効率的な処理の実現を目指します。　この実現のため、計算理論分野の基礎研究を対象とし、プログラム検証や自動証明、高度コミュニケーションシステム、人工知能などへの応用に資する計算理論への展開なども視野にいれた研究と教育を行います。着任時期：平成30年4月以降のなるべく早い時期応募資格：博士の学位を持つ者応募期限：平成29年6月30日（消印有効）なお、提出書類や書類送付先などの詳細につきましては以下をご覧ください。 http://www.riec.tohoku.ac.jp/ja/information/proposals/2017/04/post-14412/ -------------------------------------------------------------------------

1 1

24th WoLLIC 2017 - Call for Participation
by 小野寛晰 13 Jun '17

13 Jun '17

[Please circulate. Apologies for multiple copies] Call for Participation WoLLIC 2017 24th Workshop on Logic, Language, Information and Computation July 18-21, 2017 University College London (UCL), London, UK SPECIAL SESSION: Screening of Navajo Math Circles <http://www.zalafilms.com/navajo/about.html> (Directed by George Paul Csicsery, 2016, 58min) 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) IN COOPERATION WITH ACM Special Interest Group on Logic and Computation (ACM-SIGLOG) ORGANISATION Department of Computer Science, University College London, London, UK School of Electronic Engineering and Computer Science, Queen Mary College, London, UK Centro de Informática, Universidade Federal de Pernambuco, Brazil HOSTED BY Department of Computer Science, University College London, London, UK INVITED SPEAKERS Hazel Brickhill (Bristol) (University of Bristol) Michael Detlefsen (University of Notre Dame) Alexander Kurz (University of Leicester) Frederike Moltmann (New York University) David Pym (University College London) Nicole Schweikardt (Humboldt Universität) Fan Yang (Delft University) Boris Zilber (University of Oxford) STUDENT GRANTS ASL sponsorship of WoLLIC 2017 will permit ASL student members to apply for a modest travel grant (deadline: May 1st, 2017). See http://www.aslonline.org/studenttravelawards.html <http://www.aslonline.org/studenttravelawards.html> for details. PROGRAMME COMMITTEE Matthias Baaz <http://www.logic.tuwien.ac.at/staff/baaz/home.html> (University of Technology, Vienna, Austria) John Baldwin <http://homepages.math.uic.edu/~jbaldwin/> (University of Illinois at Chicago, USA) Dana Bartozová <http://www.math.toronto.edu/bartosov/> (Universidade de São Paulo, Brazil) Agata Ciabattoni <https://www.logic.at/staff/agata/> (University of Technology, Vienna, Austria) Walter Dean <http://www2.warwick.ac.uk/fac/soc/philosophy/people/dean/> (University of Warwick, UK) Erich Grädel <https://logic.rwth-aachen.de/~graedel/> (RWTH Aachen, Germany) Volker Halbach <http://users.ox.ac.uk/~sfop0114/> (University of Oxford, UK) Juliette Kennedy <http://www.math.helsinki.fi/logic/people/juliette.kennedy/> (Helsinki University, Finland) (Chair) Dexter Kozen <http://www.cs.cornell.edu/~kozen/> (Cornell University, USA) Janos Makowsky <http://www.cs.technion.ac.il/~janos/> (Technion - Israel Institute of Technology, Israel) Larry Moss <http://www.indiana.edu/~iulg/moss/> (indiana University, USA) Alessandra Palmigiano <http://www.appliedlogictudelft.nl/alessandra-palmigiano/> (Delft University, The Netherlands) Mehrnoosh Sadrzadeh <http://www.eecs.qmul.ac.uk/people/view/33472/dr-mehrnoosh-sadrzadeh> (Queen Mary, UK) Sonja Smets <http://sonja.tiddlyspot.com/#HOME> (Amsterdam University, The Netherlands) Asger Törnquist <http://www.math.ku.dk/~asgert/> (Københavns Universitet, Denmark) Rineke Verbrugge <http://www.rinekeverbrugge.nl/> (University of Groningen, The Netherlands) Andrés Villaveces <https://avillavecesn.net/> (Universidad Nacional, Colombia) Philip Welch <http://www.maths.bris.ac.uk/~mapdw/> (University of Bristol, UK) STEERING COMMITTEE Samson Abramsky, Johan van Benthem, Anuj Dawar, Joe Halpern, Wilfrid Hodges, Ulrich Kohlenbach, Daniel Leivant, Leonid Libkin, Angus Macintyre, Luke Ong, Hiroakira Ono, Valeria de Paiva, Ruy de Queiroz, Jouko Väänänen. ORGANISING COMMITTEE Alexandra Silva <http://www.alexandrasilva.org/#/main.html> (Univ College London, UK) (Local co-chair) Mehrnoosh Sadrzadeh <http://www.eecs.qmul.ac.uk/people/view/33472/dr-mehrnoosh-sadrzadeh> (Queen Mary, UK) (Local co-chair) Paulo Oliva <http://www.eecs.qmul.ac.uk/~pbo/> (Queen Mary, UK) James Brotherston <http://www0.cs.ucl.ac.uk/staff/J.Brotherston/> (Univ College London, UK) Anjolina G. de Oliveira <http://www.cin.ufpe.br/~ago> (U Fed Pernambuco) Ruy de Queiroz <http://www.cin.ufpe.br/~ruy> (U Fed Pernambuco) (co-chair) FURTHER INFORMATION Contact one of the Co-Chairs of the Organising Committee. WEB PAGE http://wollic.org/wollic2017/ <http://wollic.org/wollic2017/> ACCEPTED PAPERS Fausto Barbero, Lauri Hella and Raine Rönnholm. Independence-Friendly logic without Henkin quantification. Fedor Pakhomov. Solovay completeness without fixed points. Paola Bruscoli and Lutz Strassburger. On the length of Medial-Switch-Mix derivations. Almudena Colacito and George Metcalfe. Proof Theory and Ordered Groups. Rohit Parikh. An Epistemic Generalization of Rationalizability. Lev Beklemishev. On the reflection calculus with partial conservativity operators. Arnold Beckmann and Jean Jose Razafindrakoto. Total Search Problems in Bounded Arithmetic and Improved Witnessing. Flavio Ferrarotti, Senén González and Jose Turull-Torres. On Fragments of Higher Order Logics that on Finite Structures Collapse to Second Order. Michał Tomasz Godziszewski and Joel David Hamkins. Computable quotient presentations of models of arithmetic and set theory. Nathanael L. Ackerman and Cameron E. Freer. On the Computability of Graph Turing Machines. Ian Mackie. A Geometry of Interaction Machine for Gödel's System T. Zhaohui Luo and Serguei Soloviev. Dependent Event Types. Igor Sedlar. Substructural logics with a reflexive transitive closure modality. Stepan Kuznetsov. The Lambek calculus with iteration: two variants. Willem Conradie, Andrew Craig, Alessandra Palmigiano and Zhiguang Zhao. Constructive canonicity for lattice-based fixed point logics. Karin Cvetko Vah, Mehrnoosh Sadrzadeh, Dimitri Kartsaklis and Benjamin Blundell. Non-commutative logic for compositional distributional semantics. Daniyar Shamkanov. Global Neighbourhood Completeness of the Gödel-Löb Provability Logic. Vít Punčochář. Knowledge is a Diamond. Gijs Wijnholds. Coherent Diagrammatic Reasoning in Compositional Distributional Semantics. Zhiguang Zhao. Algorithmic Sahlqvist Preservation for Modal Compact Hausdorff Spaces. Marcin Mostowski and Marek Czarnecki. Concrete mathematics. Finitistic approach to foundations. Denis I. Saveliev and Nikolai L. Poliakov. On two concepts of ultrafilter extensions of first-order models and their generalizations. Yury Savateev and Daniyar Shamkanov. Cut-elimination for the modal Grzegorczyk logic via non-well-founded proofs. Sérgio Marcelino and Carlos Caleiro. Disjoint fibring of non-deterministic matrices. Fei Liang, Giuseppe Greco, Andrew Moshier and Alessandra Palmigiano. Multi-type display caculus for Semi De Morgan Logic. Dan Marsden, Fabrizio Genovese, Bob Coecke and Martha Lewis. Applications of Generalized Relations in Linguistics and Cognition. Bjørn Kjos-Hanssen. Shift registers fool finite automata. Giuseppe Greco and Alessandra Palmigiano. Lattice logic properly displayed.

1 0

Kyoto Philosophical Logic Workshop IIのご案内
by Hitoshi Omori 12 Jun '17

12 Jun '17

Kyoto Philosophical Logic Workshop IIのご案内 (重複してお受け取りの際はご容赦ください。) 京都大学の大森仁です。直前の案内になってしまいましたが、以下の通りワークショップを開催いたします。概要などの詳細はウェブサイトをご覧下さい。 ------------------------------------- Kyoto Philosophical Logic Workshop II 【日時】2017年6月19日、20日【場所】京都大学文学部校舎地下大会議室【ウェブサイト】https://sites.google.com/site/hitoshiomori/home/workshops/kplw2017-2 【プログラム】 19日: 11:00--12:30 Eduardo Barrio "What is a Paraconsistent Logic?" 12:30--14:00 Lunch 14:00--15:00 Damian Szmuc "On all Weak Kleene generalizations of Classical Logic" 15:00--16:00 Takuro Onishi "Routley’s American plan revisited" 16:00--16:15 Coffee break 16:15--17:15 Yosuke Fukuda "On a computational interpretation of Rumfitt's bilateral natural deduction" 17:15--18:45 Shunsuke Yatabe "Deflationism, logical notion of truth and proof theoretic semantics" 19:00-- Dinner 20日: 11:00--12:30 Wen-fang Wang "Three-Valued Semantic Pluralism: A Defense of A Three-Valued Solution to the Sorites Paradox" 12:30--14:00 Lunch 14:00--15:00 Ryosuke Igarashi "Kant's Transcendental Logic and Antinomies of Pure Reason" 15:00--16:00 Ryo Ito "Classes, Fusions and Russell's original theory of types" 16:00--16:15 Coffee break 16:15--17:15 Timo Weiss "Logic, Probability, Belief" 17:15--18:45 Graham Priest "Logical Theory-Choice: the Case of Vacuous Counterfactuals" 19:00-- Dinner ------------------------------------- どうぞよろしくお願いいたします。大森仁

1 0

ERATO MMSD キックオフワークショップのご案内
by Shin-ya KATSUMATA 01 Jun '17

01 Jun '17

国立情報学研究所の勝股です。 ERATO蓮尾メタ数理システムデザインプロジェクトでは、プロジェクトの紹介と研究交流のためのキックオフワークショップを以下の要領で行います。お気軽にお越しください。名称 ERATO MMSD キックオフワークショップ日時 6月15日(木) 14:30開始 17:15終了場所東京都千代田区一ツ橋2-1-2 国立情報学研究所12階 1208-1210 参加をご希望の方は文末のフォームにご記入の上、s.katsumata+kickoff(a)gmail.com に6月8日午前中までにご連絡下さいますようお願い申し上げます。また、ワークショップ後に研究交流会を行います。こちらもお気軽にお越しください。名称 ERATO MMSD 研究交流会日時 6月15日(木) 18:00開始場所東京都千代田区一ツ橋1-1-1 パレスサイドビルディング3階 ERATO蓮尾プロジェクト (http://group-mmm.org/eratommsd/accessj.html 東エレベータをご利用下さい) 参加費一般 3000円程度学生割引あり ========== ワークショッププログラム(発表は英語です) ========== 14:30-14:35 Introduction 14:35-14:55 Kengo Kido Nonstandard Static Analysis (Metatheoretical Transfer via Logic) 15:00-15:20 Natsuki Urabe Coalgebraic Unfolding in Forward and Backward Simulations (Metatheoretical Transfer via Category Theory) 15:25-15:45 Shin-ya Katsumata Simulations and Fibrational Liftings (Categorical Foundation for System Approximation) 15:45-16:00 Break 16:00-16:05 Interlude 16:05-16:25 Takamasa Okudono Generating Polynomial Interpolant with Semidefinite Programming (Numerical Optimization and Formal Methods) 16:30-16:50 Masaki Waga Efficient Timed Pattern Matching by Automata-Based Skipping (Automata Theory in Light-Weight Formal Methods) 16:55-17:15 Fuyuki Ishikawa Insights into Verification of Complex Systems from Software Testing Research (Formal Methods and Intelligence) ========== s.katsumata+kickoff(a)gmail.com 宛ワークショップ参加連絡フォーム ========== ERATO MMSD キックオフワークショップにご出席します。お名前: 研究交流会の参加：するしない (該当しないものを消去して下さい) 研究交流会の参加区分：一般学生 (該当しないものを消去して下さい) ========== ERATOプロジェクトホームページ ========== http://www.jst.go.jp/erato/research_area/ongoing/16816853.html 国立情報学研究所勝股審也

1 0

名古屋ロジックセミナー (UC Berkeley校Antonio Montalban氏の講演 6/12)
by Takayuki Kihara 26 May '17

26 May '17

皆様，名古屋大学の木原貴行です．この度，UC BerkeleyのAntonio Montalban氏の日本訪問の折に，下記の要領で名古屋ロジックセミナーを開催することとなりました．多数のご参加をお待ちしております．名古屋ロジックセミナー http://www.math.mi.i.nagoya-u.ac.jp/~kihara/logic-seminar.html 日時：6月12日 (月) 15:00〜場所：名古屋大学大学院情報学研究科棟 322号室講演者：Antonio Montalbán (カリフォルニア大学バークレー校) 題目：A classification of the natural many-one degrees アブストラクト： A common phenomenon in mathematics is that naturally-occurring objects behave better than general objects. This is definitely the case of the many-one degrees within Computability Theory. Our theorem, in a sense, completely classifies the natural many-one degrees and sets them apart from the non-natural ones. The theorem is a version of the uniform Martin's conjecture, but for the case of the many-one degrees. 講演終了後に夕食会を予定しています．夕食会にご参加いただける方は木原貴行 kihara(a)i.nagoya-u.ac.jp <mailto:kihara@i.nagoya-u.ac.jp> までご一報お願い致します． -------- Takayuki Kihara Graduate School of Informatics, Nagoya University, Japan URL: http://math.mi.i.nagoya-u.ac.jp/~kihara/ Email: kihara(a)i.nagoya-u.ac.jp

1 0

ALGIについての重要なお知らせ３件と第二十八回ALGIの開催について
by 西澤弘毅 25 May '17

25 May '17

logic-mlメーリングリストの皆様，神奈川大学の西澤弘毅と申します。 ALGI（代数，論理，幾何と情報科学研究集会）について重要なお知らせ３件と、第二十八回 ALGIの開催に関する告知をさせていただきます。 < 重複してお受け取りの節はご容赦願います。> 【重要なお知らせ３件】 1. 現在の algi メーリングリストのアドレスは algi(a)sakura.imi.kyushu-u.ac.jp ですが、googleグループを利用したメーリングリストへの移行を計画しています。近いうちに、現在ご登録いただいているメールアドレスに招待メールが届く予定ですので、ぜひ承認作業をお願いいたします。 2. ALGIのウェブサイトが新しくなりました。新しいURLはこちらです。 https://sites.google.com/site/algimeeting/home 一部のコンテンツは旧サイトへのリンクになっていますが、順次移行いたしますので、ブックマークには新サイトをご登録ください。 3. 昨年度まで長きにわたり幹事を務めていただきました鹿児島大学の古澤仁さんに代わりまして、今年から崇城大学の津曲紀宏さんに幹事をお願いすることにいたしました。西澤も引き続き幹事を務めさせていただきます。よろしくお願いいたします。【第二十八回 ALGIの開催について】 **************************************************************** * 第二十八回 ALGI（代数，論理，幾何と情報科学研究集会） * * * * 2017年8月28日（月）午後～8月29日（火） * * 鹿児島大学郡元キャンパス理学部 1号館 101講義室 * * * * 開催のお知らせと講演の募集 * **************************************************************** ALGI (Algebra, Logic, Geometry and Informatics) は、代数学や論理学、幾何学の情報科学への応用について、および情報科学の代数学や論理学、幾何学への応用についての研究集会で、年一回の頻度で開催されています。このたび、第二十八回ALGIを開催することになりました。会場の手配などは、昨年度まで幹事を務めていただきました鹿児島大学の古澤仁先生にお願いしています。開催場所は下記のとおりです。鹿児島大学郡元キャンパス理学部 1号館 101講義室 http://www.kagoshima-u.ac.jp/about/campusmap.html 講演を希望される方は、・題目・講演者名・e-mail address ・所属・梗概・希望時間・講演に必要な道具などの情報を nishizawa(a)kanagawa-u.ac.jp までお寄せください。「講演したいと思っている」程度の不完全情報でも結構です。時間の空きがある限り、開催直前まで講演申込を受け付けるつもりですが、申込順に発表時間を割り当てていきますので、講演をお考えの方は、なるべくお早めにお知らせいただけますようにお願い致します。初日は午後から開催いたします。夕方には懇親会を計画しています。 ALGIは申し込み不要で自由にご参加いただけます。ただし懇親会については事前に詳細を告知し参加申し込みを受け付けます。できるだけ多くの皆さんのご講演・ご参加をお待ちしております。西澤弘毅（神奈川大学）津曲紀宏（崇城大学） ----------------------------------------------------------- -- 西澤弘毅神奈川大学工学部情報システム創成学科〒221-8686 神奈川県横浜市神奈川区六角橋3-27-1 nishizawa(a)kanagawa-u.ac.jp TEL（代表）045-481-5661 （内線：3378）

1 0

LFCS 2018 Call for Papers
by Hajime Ishihara 23 May '17

23 May '17

FIRST CALL FOR PAPERS Symposium on LOGICAL FOUNDATIONS OF COMPUTER SCIENCE (LFCS '18), Deerfield Beach, Florida, January 8-11, 2018. LFCS GENERAL CHAIR: Anil Nerode. LFCS STEERING COMMITTEE: Anil Nerode, (Ithaca); Stephen Cook (Toronto); Dirk van Dalen (Utrecht); Yuri Matiyasevich (St. Petersburg); Samuel Buss (San Diego); Gerald Sacks (Cambridge, MA); Dana Scott, (Pittsburgh, PA - Berkeley, CA). LFCS ’18 PROGRAM COMMITTEE: Sergei Artemov (New York, NY) - PC Chair; Eugene Asarin (Paris); Steve Awodey (Pittsburgh, PA); Matthias Baaz (Vienna); Lev Beklemishev (Moscow); Andreas Blass (Ann Arbor, MI); Samuel Buss (San Diego, CA); Robert Constable (Ithaca, NY); Thierry Coquand (Göteborg); Michael Fellows (Bergen), Melvin Fitting (New York); Sergey Goncharov (Novosibirsk); Denis Hirschfeldt (Chicago, IL); Martin Hyland (Cambridge); Rosalie Iemhoff (Utrecht); Hajime Ishihara (JAIST - Kanazawa); Bakhadyr Khoussainov (Auckland); Roman Kuznets (Vienna); Daniel Leivant (Bloomington, IN); Robert Lubarsky (Boca Raton, FL); Victor Marek (Lexington, KY); Lawrence Moss (Bloomington, IN); Anil Nerode (Ithaca, NY) - General LFCS Chair; Hiroakira Ono (JAIST - Kanazawa); Alessandra Palmigiano (Delft); Ramaswamy Ramanujam (Chennai); Michael Rathjen (Leeds); Jeffrey Remmel (San Diego); Andre Scedrov (UPenn); Helmut Schwichtenberg (Munich); Philip Scott (Ottawa); Alex Simpson (Ljubljana); Sonja Smets (Amsterdam); Sebastiaan Terwijn(Nijmegen). LFCS ’18 LOCAL ORGANIZING COMMITTEE CHAIR: Robert Lubarsky. LFCS TOPICS of interest include, but are not limited to: constructive mathematics and type theory; homotopy type theory; logic, automata, and automatic structures; computability and randomness; logical foundations of programming; logical aspects of computational complexity; parameterized complexity; logic programming and constraints; automated deduction and interactive theorem proving; logical methods in protocol and program verification; logical methods in program specification and extraction; domain theory logics; logical foundations of database theory; equational logic and term rewriting; lambda and combinatory calculi; categorical logic and topological semantics; linear logic; epistemic and temporal logics; intelligent and multiple agent system logics; logics of proof and justification; nonmonotonic reasoning; logic in game theory and social software; logic of hybrid systems; distributed system logics; mathematical fuzzy logic; system design logics; other logics in computer science. SUBMISSION DETAILS. Proceedings will be published in the Springer LNCS series. There will be a post-conference volume of selected works published. Submissions should be made electronically via http://www.easychair.org/LFCS18/. Submitted papers must be in pdf/12pt format and of no more than 15 pages, present work not previously published, and must not be submitted concurrently to another conference with refereed proceedings. LFCS issues the BEST STUDENT PAPER AWARD named after John Barkley Rosser Sr. (1907-1989), a prominent American logician with fundamental contributions in both Mathematics and Computer Science. IMPORTANT DATES. Submissions deadline: September 10, 2017, any time zone. Notification: October 10, 2017. LOCAL ARRANGEMENTS. The venue of LFCS ’18 will be the spectacular Wyndham Deerfield Beach Resort, 2096 NE 2nd Street, Deerfield Beach, Florida 33441. Website: http://www.wyndhamdeerfieldresort.com Further Information about LFCS symposia: http://lfcs.ws.gc.cuny.edu/ About LFCS. The LFCS series provides an outlet for the fast-growing body of work in the logical foundations of computer science, e.g., areas of fundamental theoretical logic related to computer science. The LFCS series began with Logic at Botik, Pereslavl-Zalessky, 1989 and was co-organized by Albert R. Meyer (MIT) and Michael Taitslin (Tver), after which organization passed to Anil Nerode in 1992. LFCS has enjoyed support and endorsements from a number of bodies, including the US National Science Foundation (NSF) and the City University of New York Research Foundation.

1 0

2017年度数学基礎論サマースクール案内第１報
by Toshio Suzuki 19 May '17

19 May '17

皆様首都大学東京の鈴木登志雄です。 2017年度数学基礎論サマースクールの案内第１報です。今年度のテーマは「計算理論」です。日時：８月５日（土）から７日（月）初日午後、２日目以降午前・午後（時間割は後日、ウェブに掲載）会場：明治大学駿河台キャンパス　リバティタワー1073 http://www.meiji.ac.jp/koho/campus_guide/suruga/access.html 世話人：鈴木登志雄（首都大学東京），隈部正博（放送大学），河村彰星（東京大学），宮部賢志（明治大学）参加費：無料講師・テーマ：河村彰星「はじめての計算可能性」，宮部賢志「チューリング次数」，隈部正博「ジェネリック次数」，鈴木登志雄「ＨＦデルタ１関係」ウェブサイト： toshio-suzuki-logic.jp/meeting/summer2017.html 近い日程の集会：サマースクールの翌日から，SLACS 2017（記号論理と情報科学）が開催されます（千葉工業大学）。 -- 鈴木登志雄首都大学東京理工学研究科　数理情報科学専攻 toshio-suzuki(a)tmu.ac.jp

1 0

Talk by Prof. Sebastian Maneth
by Keisuke Nakano 18 May '17

18 May '17

皆様， (複数のメーリングリストに送信しています．重複して受信された場合はご容赦願います) 電気通信大学の中野と申します．来る5月26日(金)，ブレーメン大学のSebastian Maneth先生がご講演を行います．木トランスデューサ理論とその応用についてお話ししていただきますので，お時間のある方は是非ご参加ください．日時： 2017年5月26日(金) 15:00-17:00 場所：電気通信大学西9号館3階AVホール http://www.uec.ac.jp/about/profile/access/pdf/map.pdf 　　　 (こちらの地図の68番の建物です．地図にはありませんが68番の南側に　　　　門が設置されましたので，そちらをご利用されると便利です) 講演者：Prof. Sebastian Maneth (University of Bremen) タイトル：View-Query Determinacy for Tree Transducers 概要： This talk consists of two parts each with a duration of approximately 40 minutes. The first part focuses on the view-query determinacy problem. Given transformations v and q, the problem asks whether there exists a function f such that f(v(s))=q(s) for all possible inputs s. View-query determinacy is a strong static analysis with many important applications; for instance, it was used by Buneman, Davidson and Frey for data citation [CACM 59 (2016)]. For tree transducers, Hashimoto, Sawada, Ishihara, Seki, and Fujiwara showed in 2013 that determinacy is decidable for views realized by extended linear bottom-up tree transducers, and queries realized by single-valued bottom-up tree transducers. Their solution tests functionality of the inverse of the view composed with the query. We extend this result using known results about transducers and properties of uniformizers. A uniformizer of a relation R is a function that has the same domain as R. A query q is determined by a view v if and only if the composition v ; u ; q is equivalent to q, where u is a uniformizer of the inverse of v. Thus, our technique reduces the determinacy problem to the existence of uniformizers and to the decidability of equivalence. Henceforth, recent new results on decidability of equivalence immediately give rise to new results about determinacy. These results about transducer determinacy only work for views given by linear (extended) transducers. It is easy to see that even if a view transducer copies once, at the input root node, then determinacy becomes undecidable. This is unfortunate, because some very basic translations cannot be realized by linear transducers but require copying. Consider for instance a view that regroups a list of publications into sublists of books, articles, etc. A tree transducer realizing this view needs copying (i.e., it needs to process the original list multiple times). The issue that we cannot deal with non-linear views lead us to study transducers with origin (Part 2 of the talk). Under origin semantics, transducers that produce their output in "different ways" are considered different, even if they realize the same tree translation. Under this more rigid semantics, determinacy can be decided even for non-linear views. In particular, origin determinacy is decidable if the view and query are either both given by deterministic top-down tree transducers with look-ahead, or, if they are both given by deterministic MSO definable transducers. Intuitively, the world becomes safer with origin, but more restrictive (e.g., the query “is book X before article Y in the original list?” becomes determined under origin semantics). -- 中野圭介 <ksk(a)cs.uec.ac.jp> 電気通信大学大学院情報理工学研究科 http://millsmess.cs.uec.ac.jp/~ksk/

1 0

SLACS2017講演募集のお知らせ
by 安部達也 17 May '17

17 May '17

皆様（複数のメイリングリストに送信しています。重複して受信の際はご容赦ください。） SLACS 2017（記号論理と情報科学）幹事の千葉工業大学の安部達也です。今年度の講演募集を以下のとおり行います。ご検討よろしくお願いいたします。 SLACS 2017（記号論理と情報科学） http://super.para.media.kyoto-u.ac.jp/~abet/slacs2017/ 日時 2017年8月8日（火）から2017年8月9日（水）場所千葉県習志野市津田沼2-17-1 千葉工業大学津田沼キャンパス6号館3階633室参加費無料。ただし、懇親会（初日夕方に開催予定）費は別途徴収します。幹事千葉工業大学人工知能・ソフトウェア技術研究センター安部達也連絡先 abet(a)stair.center SLACSとは以下はSLACSのページの冒頭からの抜粋です。 http://www.math.s.chiba-u.ac.jp/SLACS/ 「SLACS（スラックス）は，記号論理学と情報科学の境界領域に関する研究発表・研究討論の場を提供することを目的にして開催されている研究集会です． 1985年1月に第１回が開催されて以来，毎年１回のペースで開催されています． SLACS は，堅苦しい研究会ではなく，その年の幹事を中心とした参加者自らの手作りによるフレンドリーな雰囲気を持った集会です．気軽に発表できる場ですから，研究が進行中の話題を持ってきて議論したり，学生さんが発表する場としても適当です．もちろん，発展を続けるこの分野の最先端の研究テーマに関する発表も数多く聞くことができます．参加者の資格は問いませんので，原則として，どなたでも講演発表・聴講いただけます．発表はごく少数の例外を除いて日本語です．」より詳しい情報はSLACSのページや最近の開催情報をご確認ください。 SLACS 2016 (名古屋大学) http://www.st.nanzan-u.ac.jp/info/sasaki/2016slacs/SLACS2016.html SLACS 2015 (南山大学) https://sites.google.com/site/ptslacs2015/ SLACS 2014 (東京工業大学) http://www.jaist.ac.jp/~y-keita/2014SLACS-NSA/ 講演・聴講・懇親会申込方法講演を希望される方は、幹事に連絡をお願いいたします。その際、以下について回答をお願いいたします。Subject を「SLACS2017講演申込」にしておいていただけるとありがたいです。講演申込期限は2017年7月31日としますが、講演する意思があるという方は早目にご連絡いただけると幸いです。 ----- 8< ----- 8< ----- 8< ----- 8< ----- 8< ----- 8< ----- 8< ----- 1. 氏名：（例）安部達也 2. 所属：（例）千葉工業大学人工知能・ソフトウェア技術研究センター 3. 区分：一般/学生 ← プログラム作成・懇親会費設定に利用する場合があります 4. 演題：（例）TBA 5. 懇親会：参加する/追って連絡する/参加できない 6. 要望等：（例）初日しか参加できませんので初日の枠に入れてください ----- 8< ----- 8< ----- 8< ----- 8< ----- 8< ----- 8< ----- 8< ----- 講演を伴わない聴講のみを希望される場合、事前連絡は不要です。当日、会場に直接お越しください。懇親会に参加を希望される方は、幹事に連絡をお願いいたします。その際、講演申込と同様のフォーマット（演題不要）での回答をお願いいたします。 Subject を「SLACS2017懇親会参加申込」にしておいていただけるとありがたいです。申込期限は2017年7月31日としますが、参加する意思があるという方は早目にご連絡いただけると幸いです。

1 0

JAIST Logic Seminar Series
by Takako Nemoto 15 May '17

15 May '17

皆様インスブリア大学（イタリア）の Marco Benini 先生の講演のお知らせです。どうぞふるってご参加ください。問い合わせ先：根元　多佳子北陸先端科学技術大学院大学　情報科学系 email: t-nemoto(a)jaist.ac.jp --------------------------------------------- *JAIST Logic Seminar Series* Date: Tuesday, 6 June, 2017, 15:30-17:00 Place: JAIST, Collaboration room 7 (I-56) (Access: http://www.jaist.ac.jp/english/location/access.html) Speaker: Marco Benini (Università degli Studi dell'Insubria) Title: The Graph Minor Theorem: a walk on the wild side of graphs Abstract: The Graph Minor Theorem says that the collection of finite graphs ordered by the minor relation is a well quasi order. This apparently innocent statement hides a monstrous proof: the original result by Robertson and Seymour is about 500 pages and twenty articles, in which a new and deep branch of Graph Theory has been developed. The theorem is famous and full of consequences both on the theoretical side of Mathematics and in applications, e.g., to Computer Science. But there is no concise proof available, although many attempts have been made. In this talk, arising from one such failed attempts, an analysis of the Graph Minor Theorem is presented. Why is it so hard? Assuming to use the by-now standard Nash-Williams's approach to prove it, we will illustrate a number of methods which allow to solve or circumvent some of the difficulties. Finally, we will show that the core of this line of thought lies in a coherence question which is common to many parts of Mathematics: elsewhere it has been solved, although we were unable to adapt those solutions to the present framework. So, there is hope for a short proof of the Graph Minor Theorem but it will not be elementary.

1 0

訃報：竹内外史先生
by Makoto Kikuchi 11 May '17

11 May '17

皆様，昨日，竹内外史先生がお亡くなりになられたそうです．菊池誠

2 1

ランダムネス集中講義
by Toshio Suzuki 28 Apr '17

28 Apr '17

ランダムネス集中講義のご案内（重複して受け取られた折はご容赦ください）お世話になっております。首都大学東京の鈴木登志雄です。さて５月・６月に首都大で，明治大学の宮部先生にランダムネスの集中講義をしていただきます。公式にオープンセミナーとうたっているわけではありませんが，当専攻ではこの種の集中講義に数名程度まで学外の院生等が聴きに来ても黙認する慣習のようです。お近くに関心のありそうな方がいらっしゃいましたら、お知らせいただければ幸いです。 %%%%%%% ここから＊＊担当者宮部賢志先生（明治大学理工学部講師）　＊＊授業科目名情報数理科学２ (博士前期課程、Ｒ０７９）、情報数理科学特論２(博士後期課程、Ｒ０８０）タイトルランダムネス入門場所　首都大学東京（南大沢キャンパス）８号館６階６１０時期５月１８日（木），５月２５日（木），６月　８日（木），６月１５日（木）の１４：４０−１７：５０（途中休憩あり）当専攻での連絡係鈴木登志雄 toshio-suzuki[atmark]tmu.ac.jp 概要アルゴリズム的ランダムネスの理論では，科学の基本概念であるランダムについて，計算論を使って厳密な定義を与え，その性質を調べる。本講義では，計算論の再帰定理やTuring次数などの概念の復習から始める。その後，MLランダムネスの定義といくつかの性質を見る。特に，ランダムな列の構成技術に焦点を当てて解説する。 %%%%%%% ここまで首都大学東京南大沢キャンパスへの交通 http://www.tmu.ac.jp/university/campus_guide/access.html 同・構内図 http://www.tmu.ac.jp/university/campus_guide/map.html -- 鈴木登志雄首都大学東京理工学研究科数理情報科学専攻 toshio-suzuki(a)tmu.ac.jp

1 0

早稲田大学高等研究所セミナー「Logic and Game Theory」 (5/16)のご案内
by Makoto Fujiwara 28 Apr '17

28 Apr '17

皆様 (English follows) 以下の通り、5/16(火)に金子守先生(早稲田大学政治経済学術院、特任教授)に非専門家向けのご講演(英語)をしていただきます。事前申込みは不要ですので、どうぞふるってご参加ください。詳細は下記ホームページをご覧ください。 https://www.waseda.jp/inst/wias/news/2017/04/25/4250/ <https://www.waseda.jp/inst/wias/news/2017/04/25/4250/> 問い合わせ先：藤原誠(早稲田大学高等研究所) makoto_fujiwara(a)aoni.waseda.jp <mailto:makoto_fujiwara@aoni.waseda.jp> Dear all, It is our pleasure to announce WIAS Seminar "Logic and Game Theory" (May 16, 2017). The talk by Professor Mamoru Kaneko and the following discussion would be held in English. It is free for charge and the prior registration for your attendance is not needed. You are welcome to join us. Best regards, Coordinators ================================================================== WIAS Seminar "Logic and Game Theory" Date & Time: Tuesday, 16 May 2017, 11:00 - 12:15 Venue: Meeting room. 1 on the 5th floor, Building #9, Waseda University Speaker: Mamoru KANEKO（Professor, Waseda University） Title: Logic and Game Theory Abstract: In this presentation, I make conceptual connections between logic and game theory. First, I give a small introduction to each filed. Then, a Japanese comic story called “Konnyaku Mondo” is introduced to describe a basic problem on one’s understanding about the other person’s thought. The Konnyaku Mondo phenomena are often observed in our real lives. It is indicative of the distinction between a symbolic expression and its intended meaning; this is a very basic distinction in the modern logic. The story leads also to a new field in game theory called “Inductive Game Theory” that I and several collaborators have developed. Indeed, we construct a game theory example having the feature of the Konnyaku Mondo that two players are playing a game with mutual misunderstanding of the situation, but they cannot correct their mutual misunderstanding even after they have played the game several times. Coordinators: Makoto FUJIWARA （Assistant Professor, Waseda University） Ryota AKIYOSHI （Associate Professor, Waseda University） Kazuto OHTSUKI （Assistant Professor, Waseda University） For more information, please see the following page: https://www.waseda.jp/inst/wias/news-en/2017/04/25/4251/ <https://www.waseda.jp/inst/wias/news-en/2017/04/25/4251/> Contact: Makoto FUJIWARA E-mail: makoto_fujiwara(a)aoni.waseda.jp <mailto:makoto_fujiwara@aoni.waseda.jp> ================================================================== ============================================ 藤原誠 (Makoto Fujiwara) 早稲田大学高等研究所 (Waseda Institute for Advanced Study, Waseda University) E-mail: makoto_fujiwara(a)aoni.waseda.jp ============================================

1 0

Project colloquium talk by Sean Sedwards on 28 April
by Akira Yoshimizu 27 Apr '17

27 Apr '17

Dear colleagues, (apology for multiple copies) Let us advertise the next ERATO MMSD project colloquium talk by Sean Sedwards. Please find the title and abstract of the talk below. You are all cordially invited. Remote attendance is also welcome (Polycom is available in the room). Please let us know beforehand if you would like to join remotely. Sincerely, Akira Yoshimizu Technical Assistant at ERATO MMSD project ---------- https://docs.google.com/document/d/1Qrg4c8XDkbO3tmns6tQwxn5lGHOrBON5LtHXXTp… <https://docs.google.com/document/d/1Qrg4c8XDkbO3tmns6tQwxn5lGHOrBON5LtHXXTp…> Fri 28 April 2017, 15:15–17:00 NII meeting room 2010 https://www.nii.ac.jp/en/about/access/ <https://www.nii.ac.jp/en/about/access/> Sean Sedwards (ERATO MMSD), Rare Event Simulation for Statistical Model Checking Statistical model checking (SMC) avoids the intractable number of states associated with numerical model checking by estimating the probability of a property from a number of execution traces (simulations). Rare events nevertheless pose an important challenge to SMC because interesting properties, such as bugs and optima, are often very rare and occur infrequently in simulations. A key objective for SMC is thus to reduce the number and length of simulations necessary to produce an estimate with a given level of statistical confidence. In this talk I will describe two variance reduction approaches that address this problem: importance sampling and importance splitting. Importance sampling weights the probabilities of a system to make a rare property occur more frequently in simulations, then compensates the results by the weights. Importance splitting decomposes a rare property into the product of sub-properties that are less rare and easier to simulate. I will outline the challenges of using these techniques in SMC and highlight some practical solutions, including the recent successful application of importance sampling to stochastic timed automata.

1 0

JAIST Logic Seminar Series
by Takako Nemoto 25 Apr '17

25 Apr '17

皆様インスブリア大学（イタリア）の Marco Benini 先生の講演のお知らせです。どうぞふるってご参加ください。問い合わせ先：根元　多佳子北陸先端科学技術大学院大学　情報科学系 email: t-nemoto(a)jaist.ac.jp --------------------------------------------- *JAIST Logic Seminar Series* Date: Friday, 12 May, 2017, 15:30-17:00 Place: JAIST, Collaboration room 7 (I-56) (Access: http://www.jaist.ac.jp/english/location/access.html) Speaker: Marco Benini (Università degli Studi dell'Insubria) Title: Explaining the Kruskal's Tree Theorem Abstract: The famous Kruskal's tree theorem states that the collection of finite trees labelled over a well quasi order and ordered by homeomorphic embedding, forms a well quasi order. Its intended mathematical meaning is that the collection of finite, connected and acyclic graphs labelled over a well quasi order is a well quasi order when it is ordered by the graph minor relation. Oppositely, the standard proof(s) shows the property to hold for trees in the Computer Science's sense together with an ad-hoc, inductive notion of embedding. The mathematical result follows as a consequence in a somewhat unsatisfactory way. In this talk, a variant of the standard proof will be illustrated explaining how the Computer Science and the graph-theoretical statements are strictly coupled, thus explaining why the double statement is justified and necessary.

1 0

国際会議 IWC 2017 (with FSCD at Oxford)
by Fujita Kenetsu 19 Apr '17

19 Apr '17

(* Apologies for any cross-postings. *) ===================================================================== Call for Papers IWC 2017 6th International Workshop on Confluence September 8th, 2017, Oxford, United Kingdom Collocated with FSCD 2017 http://cl-informatik.uibk.ac.at/events/iwc-2017/ ===================================================================== Confluence provides a general notion of determinism and is widely viewed as one of the central properties of rewriting. Confluence relates to many topics of rewriting (completion, modularity, termination, commutation, etc.) and has been investigated in many formalisms of rewriting such as first-order rewriting, lambda-calculi, higher-order rewriting, constrained rewriting, conditional rewriting, etc. Recently there is a renewed interest in confluence research, resulting in new techniques, tool support, certification as well as new applications. The International Workshop on Confluence (IWC) aims at promoting further research in confluence and related properties. IWC 2017 is collocated with FSCD 2017. Previous editions of the workshop were held in Nagoya (2012), Eindhoven (2013), Vienna (2014), Berlin (2015), and Obergurgl (2016). During the workshop, the 6th Confluence Competition (CoCo 2017) takes place. IMPORTANT DATES: * submission Saturday, July 1st, 2017 * notification Saturday, July 22nd, 2017 * final version Saturday, August 5th, 2017 * workshop Friday, September 8th, 2017 (deadlines are AoE) TOPICS: Specific topics of interest include: * confluence and related properties (unique normal forms, commutation, ground confluence) * completion * critical pair criteria * decidability issues * complexity issues * system descriptions * certification * applications of confluence INVITED SPEAKERS: tba PROGRAM COMMITTEE: * Beniamino Accattoli (INRIA) * Jörg Endrullis (Vrije Universiteit Amsterdam) * Bertram Felgenhauer (University of Innsbruck) * Ken-Etsu Fujita (Gumma University) * Philippe Malbos (Université Claude Bernard Lyon 1) * Jakob Grue Simonsen (University of Copenhagen) SUBMISSION: We solicit short papers or extended abstracts of at most five pages. There will be no formal reviewing. In particular, we welcome short versions of recently published articles and papers submitted elsewhere. The program committee checks relevance and may provide additional feedback. The accepted papers will be made available electronically before the workshop. The page limit for papers is 5 pages in EasyChair style. Short papers or extended abstracts must be submitted electronically through the EasyChair system at: https://www.easychair.org/conferences/?conf=iwc2017 EasyChair style: http://easychair.org/publications/for_authors -------

1 0

JAIST Logic Seminar Series
by Hajime Ishihara 16 Apr '17

16 Apr '17

皆様バーミンガム大学のSteve Vickers先生の講演のお知らせです。どうぞふるってご参加ください。問合せ先：石原　哉北陸先端科学技術大学院大学情報科学系 e-mail: ishihara(a)jaist.ac.jp ----------------------------------------------- * JAIST Logic Seminar Series * * The seminar below is held as a part of JSPS Core-to-Core Program, A. Advanced Research Networks, EU FP7 Marie Curie Actions IRSES project CORCON. (http://www.jaist.ac.jp/logic/ja/core2core, https://corcon.net/), and EU Horizon 2020 Marie Skłodowska-Curie actions RISE project CID. Date: Monday 17, April, 2017, 15:20-17:00 Place: JAIST, Collaboration room 6 (I-57g) (Access: http://www.jaist.ac.jp/english/location/access.html) Speaker: Steve Vickers (University of Birmingham) Title: Arithmetic universes as generalized point-free spaces Abstract: Point-free topology in all its guises (e.g. locales, formal topology) can be understood as presenting a space as a _logical theory_, for which the points are the models and the opens are the formulae. The logic in question is geometric logic, its connectives being finite conjunctions and arbitrary disjunctions, and then the Lindenbaum algebra (formulae modulo equivalence) for a theory T is a frame O[T], a complete lattice with binary meet distributing over all joins. Locales are frames but with the morphisms reversed. Grothendieck proposed Grothendieck toposes as the generalized point-free spaces got when one moves to the first-order form of geometric logic. Then the opens (giving truth values for each point) are not enough, and one must move to sheaves (giving sets for each point). The Lindenbaum algebra now becomes a Grothendieck topos Set[T], the classifying topos for T, constructed using presheaves with a pasting condition, and closed under finite limits and arbitrary colimits in accordance with Giraud's theorem. The topos Set[T] canonically represents the generalized space of models of T. Grothendieck used the category Set of classical sets, but we now know that it can be replaced by any elementary topos S. This base will determine the infinities available for "arbitrary" disjunctions, as well as governing the construction of the classifier S[T]. However, for theories in which all the disjunctions are countable (such as the formal space of reals) it doesn't matter which S is used, as long as it has a natural numbers object (nno). Thus the generalized space of models of T is not absolutely fixed as a mathematical object. In my talk I shall present the idea of using Joyal's _arithmetic universes_ (AUs), pretoposes with parameterized list objects, as a base-independent substitute for Grothendieck toposes in which countable disjunctions are intrinsic to the logic rather than being supplied extrinsically by a base S. In [1] I have defined a 2-category Con whose objects ("contexts") serve as geometric theories that are sufficiently countable in nature, and whose morphisms are the maps of models. In [2] I showed how to use Con to prove results for Grothendieck toposes, fibred over choice of base topos. Thus we start to see AUs providing a free-standing foundations for a significant fragment of geometric logic and Grothendieck toposes, independent of base S. My two papers - [1] "Sketches for arithmetic universes" (arXiv:1608.01559) [2] "Arithmetic universes and classifying toposes" (arXiv:1701.04611)

2 1

Continuity, Computability, Constructivity 2017; second call for submission; extended deadline
by Hajime Ishihara 12 Apr '17

12 Apr '17

*Continuity, Computability, Constructivity – From Logic to Algorithms* * (CCC 2017)* * Loria, 26-30 June 2017* *Call for papers* http://ccc2017.loria.fr/ CCC is a workshop series bringing together researchers from exact real number computation, computable analysis, effective descriptive set theory, constructive analysis, and related areas. The overall aim is to apply logical methods in these disciplines to provide a sound foundation for obtaining exact and provably correctalgorithms for computations with real numbers and related analytical data, which are of increasing importance in safety critical applications and scientific computation. Previous workshops have been held in Cologne 2009, Trier 2012, Gregynog 2013, Ljubljana 2014, and Kochel 2015. The conference series has always been linked with EU-funded international research projects, with COMPUTAL (Computable Analysis) in the years 2012-2015 and now with CID (Computing with Infinite Data), a research network between Europe, Chile, Japan, New Zealand, Russia, Singapore, South Africa, South Korea, and the USA. This conference is the first CID event, but is open to all researchers in the area. The workshop will take place in Nancy, France. *Scope: *The workshop specifically invites contributions in the areas of * Exact real number computation, * Correctness of algorithms on infinite data, * Computable analysis, * Complexity of real numbers, real-valued functions, etc. * Effective descriptive set theory * Scott's domain theory, * Constructive analysis, * Category-theoretic approaches to computation on infinite data, * Weihrauch degrees, * And related areas. *Invited Speakers:* * Matthew de Brecht (Kyoto, Japan) * Bernhard Reus (Brighton, UK) * Matthias Schröder (Darmstadt, Germany) * Alex Simpson (Ljubljana, Slovenia) * * *Submission:* * * Extended abstracts (1-2 pages) of original work are welcome. * * ** *Extended Deadline:* *10 May 2017* ** *Upload your submission via EasyChair:* https://easychair.org/conferences/?conf=ccc20170 *Programme Committee:* * Ulrich Berger (Swansea) * Pieter Collins (Maastricht) * Mathieu Hoyrup (Nancy) (co-chair) * Erik Palmgren (Stockholm) * Victor Selivanov (Novosibirsk) * Dieter Spreen (Siegen) (co-chair) * Martin Ziegler (Daejeon). *Organizing Committee:* * Anne-Lise Charbonnier (Nancy) * Mathieu Hoyrup (Nancy)

2 1

FW: 松山 TGSAセミナーのお知らせ（４月１９日）
by FUJITA Hiroshi 11 Apr '17

11 Apr '17

こんにちは。愛媛大学の藤田です。次回のTGSAセミナーの案内を転送します。藤田博司 <fujita.hiroshi.mh(a)ehime-u.ac.jp> ________________________________ 差出人: Dmitri SHAKHMATOV <dmitri.shakhmatov(a)dmitri.math.sci.ehime-u.ac.jp> 送信日時: 2017年4月11日 10:55 宛先: FUJITA Hiroshi CC: dmitri.shakhmatov(a)dmitri.math.sci.ehime-u.ac.jp 件名: 松山 TGSAセミナーのお知らせ（４月１９日）皆様、「Matsuyama Seminar on Topology, Geometry, Set Theory and their Applications」（松山TGSAセミナー）のお知らせです。 ***** 第30回のセミナー日時: 2017年4月19日（水） 16:30〜17:30 場所: 愛媛大学理学部2号館2階，大演習室 (201号室) 講演者: Alejandro Dorantes-Aldama (愛媛大学) 題目: Selective sequential pseudcompactness 概要： We say that a topological space $X$ is {\em selectively sequentially pseudcompact} if for every family $\{U_n:n\in\mathbb{N}\}$ of non-empty open subsets of $X$, one can choose a point $x_n\in U_n$ for each $n\in\mathbb{N}$ in such a way that the sequence $\{x_n:n\in \mathbb{N}\}$ has a convergent subsequence. We show that the class of selectively sequentially pseudcompact spaces is closed under arbitrary products and continuous images, contains the class of all dyadic spaces and forms a proper subclass of the class of strongly pseudocompact spaces introduced recently by Garc\'ia-Ferreira and Ortiz-Castillo. We prove, under the Singular Cardinal Hypothesis SCH, that if $G$ is an Abelian group admitting a pseudocompact group topology, then it can also be equipped with a selectively sequentially pseudcompact group topology. Since selectively sequentially pseudcompact spaces are strongly pseudocompact, this provides a strong positive answer to a question of Garc\'ia-Ferreira and Tomita. This is a joint work with Dmitri Shakhmatov. 講演終了後に交流会を予定しています。交流会にご参加いただける方はシャクマトフ<dmitri.shakhmatov(a)ehime-u.ac.jp>までご一報お願い致します。以上、よろしくお願い申し上げます。世話人（五十音順）井上友喜尾國新一シャクマトフディミトリ野倉嗣紀平出耕一平田浩一藤田博司山内貴光 --- ウェブページ： http://www.math.sci.ehime-u.ac.jp/MTGSA.ja.html

1 0

論文募集：「プログラミングおよびプログラミング言語」特集
by Isao Sasano 10 Apr '17

10 Apr '17

皆様芝浦工業大学の篠埜です。論文誌「コンピュータソフトウェア」の特集「プログラミングおよびプログラミング言語」の論文募集のご案内です。 PPL2017の論文に限らず募集いたします。是非論文のご投稿をお願いいたします。 ----------------------------------------------------------------------- 論文募集：「プログラミングおよびプログラミング言語」特集 (論文投稿締切: 2017年6月16日(金) 17:00) http://www.jssst.or.jp/edit_news/detail/id=274 日本ソフトウェア科学会プログラミング論研究会は，毎年「プログラミングおよびプログラミング言語ワークショップ (PPL)」を開催しており，2017年3 月には第19回シンポジウム PPL2017 を開催しました．本「プログラミングおよびプログラミング言語」特集号は，PPL2017 に連動した企画であり，プログラミングに関する最先端の研究成果を掲載することを目的にしています．PPL2017 の発表論文を発展させた論文，PPL2017 での発表論文の中から推薦された論文（PPL2017 推薦論文），あるいはそれに限らず下記の対象分野に関連した論文を広く募集します．なお，PPL2017 との連携を強化するために，PPL2017 のプログラム共同委員長・篠埜功 (芝浦工業大学) 氏，番原睦則 (神戸大学) 氏を中心として特集号編集委員を構成しています．PPL2017 での発表論文を発展させた論文，および， PPL2017 推薦論文の査読にあたっては，PPL2017 の論文およびその査読結果を参考とさせていただきますので，迅速で一貫した査読が期待できます． <対象分野> プログラミングおよびプログラミング言語に関する研究成果 <募集論文> プログラミングおよびプログラミング言語に関する研究論文・解説論文・ソフトウェア論文 <執筆要領> 日本ソフトウェア科学会誌「コンピュータソフトウェア」の関連諸規定をご参照の上，投稿論文の PDF ファイルと「投稿メモ」を ppl2017si[at]org.kobe-u.ac.jp 宛てにお送りください．([at]を@に置換下さい) * PPL2017 で発表した論文を改訂して投稿する場合はその旨をお知らせください．学会誌関連諸規定は以下でご参照いただけます． http://www.jssst.or.jp/edit/kitei/ * レター論文による投稿を歓迎します． * レター論文は，査読者 1名による査読を行い，「照会後判定」は行わず，一度の査読で採否を判定します．刷り上がりで 6ページ以下の速報性を重視した論文です．レター論文を発展させたものは通常論文として投稿可能です． * 特集号に投稿された論文の査読基準は，一般投稿論文の査読基準と同じです． * 二重投稿にならないよう，十分ご注意下さい．（国際会議であっても，査読期間が重複する場合は二重投稿に該当します．） * 特集号への投稿に限り，日本ソフトウェア科学会の非会員による投稿も受け付けております．詳しくは上記より論文投稿規定をご覧ください． <スケジュール> 論文投稿締切り： 2017年6月16日(金) 17:00 特集号刊行予定： 2018年11月号査読プロセスの進行状況により掲載予定号に間に合わない場合があります．その場合でも特集論文として扱われます． <特集号編集委員> 青谷知幸 (東京工業大学)，馬谷誠二 (京都大学)，篠埜功 (芝浦工業大学)，番原睦則 (代表者，神戸大学) <企画母体> 日本ソフトウェア科学会プログラミング論研究会 <問合せ先> 篠埜功，番原睦則 (ppl2017si[at]org.kobe-u.ac.jp) ([at]は@で置き換えて下さい) ----------------------------------------------------------------------- 篠埜　功 -- Isao Sasano <sasano(a)sic.shibaura-it.ac.jp>

1 0

Talk by Marc Bagnol (13 Apr 11:00-)
by Tetsuya Sato 07 Apr '17

07 Apr '17

京都大学数理解析研究所の佐藤です。 4月13日11:00から、東京大学のMarc Bagnol氏に以下の講演をしていただくことになりましたので、ご連絡いたします。どうぞお気軽にお越しください。 ========== Time: 11:00-12:00, 13 Apr, 2017 Place: Rm 478, Research Building 2, Main Campus, Kyoto University 京都大学本部構内総合研究2号館 4階478号室 http://www.kyoto-u.ac.jp/en/access/yoshida/main.html (Building 34) http://www.kyoto-u.ac.jp/ja/access/campus/map6r_y.htm (34番の建物) Speaker: Marc Bagnol (JSPS Postdoctoral Fellow, University of Tokyo) Title: A Free Trace Construction and the Embedding Problem Abstract: The notion of traced category allows to model feedback situations in the language of category theory. Traces are ubiquitous in mathematics and serve as the basis for the categorical formulation of Girard's Geometry of Interaction. The notion was extended to partially-defined traces by Scott and Haghverdi, and a representation theorem was later shown: any partially traced category can be embedded in a fully traced one. A related problem we are currently investigating with some RIMS members is understanding when a monoidal category can be embedded into a traced one, or equivalently when it can be equipped with a partial trace. This "embedding problem" has already seen a few tentative solutions, conditions that are necessary but turned out not to be sufficient which I will present and discuss. I will also present a construction of a free trace for monoidal categories that both can be used to prove the representation theorem mentioned above (this was its original purpose) and gives an angle to look at the embedding problem.

1 0

Autumn school "Proof and Computation"
by Hajime Ishihara 07 Apr '17

07 Apr '17

Autumn school "Proof and Computation" Herrsching, Germany, 23rd to 26th September 2017 http://www.mathematik.uni-muenchen.de/~schwicht/pc17.php An international autumn school "Proof and Computation" will be held from 23rd to 26th September 2017 at Haus der bayerischen Landwirtschaft Herrsching in Herrsching near Munich. Its aim is to bring together young researchers in the field of Foundations of Mathematics, Computer Science and Philosophy. SCORE -------------------- - Predicative Foundations - Constructive Mathematics and Type Theory - Computation in Higher Types - Extraction of Programs from Proofs - Algorithmic Aspects in Financial Mathematics COURSES -------------------- - Mark Bickford on Constructive Analysis in NuPrl - Laura Crosilla on Foundations of Predicative Mathematics - Hajime Ishihara on Constructive Reverse Mathematics - Ulrich Kohlenbach on Proof Mining - Davide Rinaldi on Constructivising Transfinite Algebra - Andrei Rodin on Foundations of Axiomatic Mathematics - Gregor Svindland on Algorithmic Aspects in Financial Mathematics WORKING GROUPS -------------------- There will be an opportunity to form ad-hoc groups working on specific projects, but also to discuss in more general terms the vision of constructing correct programs from proofs. APPLICATIONS -------------------- Graduate or PhD students and young postdoctoral researches are invited to apply. Applications must be accompanied by a letter of recommendation, preferably from the thesis adviser, and should be sent to Chuangjie Xu (xu(a)math.lmu.de). DEADLINE for applications: **30th May 2017**. Applicants will be notified by 30th June 2017. FINANCIAL SUPPORT -------------------- The workshop is supported by the Udo Keller Stiftung (Hamburg), the CID (Computing with Infinite Data) programme of the European Commission and a JSPS core-to-core project. Successful applicants will be offered full-board accommodation for the days of the autumn school. There are no funds, however, to reimburse travel or further expenses, which successful applicants will have to cover otherwise. Klaus Mainzer Peter Schuster Helmut Schwichtenberg

1 0

Third Call for Papers ***** extended deadline ***** [LORI-VI] The Sixth International Conference on Logic, Rationality and Interaction
by Katsuhiko Sano 26 Mar '17

26 Mar '17

Third Call for Papers ***** extended deadline ***** [LORI-VI] The Sixth International Conference on Logic, Rationality and Interaction September 11-14, 2017, Hokkaido University, Sapporo, Japan http://golori.org/lori2017/ [About LORI] The International Conference on Logic, Rationality and Interaction (LORI) conference series aims at bringing together researchers working on a wide variety of logic-related topics that concern the understanding of rationality and interaction. The series aims at fostering a view of Logic as an interdisciplinary endeavour, and supports the creation of an East-Asian community of interdisciplinary researchers. [News] ****** Submission Deadline extended to Friday April 14 ****** [Call for Papers] We invite submission of contributed papers on any of the broad themes of LORI series; specific topics of interest include, but are not limited to, formal approaches to · agency · argumentation and agreement · belief representation · cooperation · belief revision and belief merging · strategic reasoning · games · decision making and planning · knowledge and action · epistemology · dynamics of informational attitudes · speech acts · knowledge representation · interaction · norms and normative systems · natural language · rationality · philosophy and philosophical logic · preference and utility · social choice · probability and uncertainty · social interaction · intentions, plans, and goals Submitted papers should be at most 12 pages long, with one additional page for references, in PDF format following the Springer LNCS style. Please submit your paper by Friday April 14, 2017, via EasyChair : http://easychair.org/conferences/?conf=lori6 . [Publication] Accepted papers will be collected as a volume in the FoLLI Series on Logic, Language and Information, and authors may be later invited to submit extended versions of their papers in a special issue of a prestigious journal. [Best Student Paper] The best student paper will be selected from the contributed student papers accepted for presentation at LORI VI, and be awarded the prize of 60,000 Japanese Yen (approximately 500 Euro). For more details, see http://golori.org/lori2017/award.html . [Website] For detailed conference information and registration, please visit http://golori.org/lori2017/ . [Invited Speakers] Mike Dunn: Indiana University, U.S.A. Alan Hájek: Australian National University, Australia Nina Gierasimczuk: Technical University of Denmark, Denmark Willemien Kets: Northwestern University, U.S.A Sara Negri: University of Helsinki, Finland Hiroakira Ono: JAIST, Japan [PC Chairs] Alexandru Baltag: University of Amsterdam, The Netherlands Jeremy Seligman: University of Auckland, New Zealand [Conference Organiser] Tomoyuki Yamada: Hokkaido University, Japan [Sponsors] LORI Tsinghua University - University of Amsterdam Joint Research Centre for Logic Hokkaido University [Contacts] Programme: The PC Chairs <lori6(a)easychair.org> Conference: Tomoyuki Yamada <tomoyuki.s.yamada(a)gmail.com>

1 0

Computability and Complexity in Analysis (CCA 2017): Final Call for Papers
by Daniel Graça 22 Mar '17

22 Mar '17

______________________________________________________________ Final Call for Papers Fourteenth International Conference on Computability and Complexity in Analysis (CCA 2017) http://cca-net.de/cca2017/ July 24-27, 2017, Daejeon, Republic of Korea (South Korea) Submission deadline: April 3, 2017 ______________________________________________________________ Topics * Computable analysis * Complexity on real numbers * Constructive analysis * Domain theory and analysis * Effective descriptive set theory * Theory of representations * Computable numbers, subsets and functions * Randomness and computable measure theory * Models of computability on real numbers * Realizability theory and analysis * Reverse analysis * Real number algorithms * Implementation of exact real number arithmetic Invited Speakers * Hee-Kap Ahn (Pohang, Republic of Korea) * Verónica Becher (Buenos Aires, Argentina) * Anders Hansen (Cambridge, UK) * Takayuki Kihara (Berkeley, USA) * Amaury Pouly (Max Planck Institute, Germany) * Linda Brown Westrick (Connecticut, USA) Funding Funding opportunities for student members of the Association for Symbolic Logic (ASL) are available. Applications should be directed to the Association for Symbolic Logic three months prior to the meeting, following the instructions here: http://www.aslonline.org/studenttravelawards.html Scientific Programme Committee * Johanna Franklin (Hempstead, USA) * Daniel Graça, chair (Faro, Portugal) * Vassilios Gregoriades (Turin, Italy) * Peter Hertling (Munich, Germany) * Gyesik Lee (Anseong, Republic of Korea) * Alexander Melnikov (Auckland, New Zealand) * Takako Nemoto (Ishikawa, Japan) * Arno Pauly (Brussells, Belgium) * Cristóbal Rojas (Santiago, Chile) * Frank Stephan (Singapore) * Klaus Weihrauch (Hagen, Germany) Organising Committee * Sunyoung Kim (Yonsei University, Republic of Korea) * Sewon Park (KAIST, Republic of Korea) * Martin Ziegler, chair (KAIST, Republic of Korea) Submissions Authors are invited to submit 1-2 pages abstracts in PDF format, including references via the following web page: https://easychair.org/conferences/?conf=cca2017 If full versions of papers are already available as technical report or arXiv version, then corresponding links should be added to the reference list. Final versions of abstracts might be distributed to participants in hardcopy and/or in electronic form. Dates * Submission deadline: April 3, 2017 * Notification of authors: May 1, 2017 * Final version: May 29, 2017 Conference Web Page http://cca-net.de/cca2017/ A co-located "Workshop on Real Verification" will take place on Friday, July 28, jointly organized by: * Gyesik Lee (Hankyong National University, Republic of Korea) * Martin Ziegler (KAIST, Republic of Korea) https://complexity.kaist.edu/CCA2017/workshop.html

1 0

RIMS共同研究（公開型）「証明論と証明活動」のご案内
by Katsumi Sasaki 16 Mar '17

16 Mar '17

みなさま　標記の共同研究として，以下の研究集会を開催します．　　　研究題目：証明論と証明活動　　　日程：2017年12月25日(月)〜27日(水) 　　　場所：京都大学数理解析研究所420号室　証明論・計算論・証明活動に関連する話題の講演を広く募集します．お忙しい時期かと思いますが，是非とも、講演・参加をご計画ください．　講演される学生の方には，旅費の援助があります．　詳細は， http://www.st.nanzan-u.ac.jp/info/sasaki/2017rims/rims2017.html で案内していく予定です．世話人：南山大学　佐々木克巳佐々木克巳 -- sasaki <sasaki(a)nanzan-u.ac.jp>

1 0

ITP 2017 - Final Call for Papers
by Nao Hirokawa 13 Mar '17

13 Mar '17

皆様 ITP 2017 の論文募集案内（最終）をお送り致します。ぜひ論文投稿をご検討下さい。廣川 (JAIST) ---------------------------------------------------------------------- FINAL CALL FOR PAPERS ITP 2017 8th International Conference on Interactive Theorem Proving Brasilia, Brazil September 26-29, 2017 http://itp2017.cic.unb.br SUBMISSION DEADLINES * April 3, 2017 (abstracts) * April 10, 2017 (full papers) GENERAL INFORMATION The ITP conference series is concerned with all topics related to interactive theorem proving, ranging from theoretical foundations to implementation aspects and applications in program verification, security, and formalization of mathematics. ITP is the evolution of the TPHOLs conference series to the broad field of interactive theorem proving. TPHOLs meetings took place every year from 1988 until 2009. The eighth ITP conference, ITP 2017, will be held at Universidade de Brasilia, September 26-29, 2017. SCOPE OF CONFERENCE ITP welcomes submissions describing original research on all aspects of interactive theorem proving and its applications. Suggested topics include but are not limited to the following: * formal aspects of hardware and software * formalizations of mathematics * improvements in theorem prover technology * user interfaces for interactive theorem provers * formalizations of computational models * verification of security algorithms * use of theorem provers in education * industrial applications of interactive theorem provers * concise and elegant worked examples of formalizations (proof pearls) PUBLICATION DETAILS The proceedings of the symposium will be published in the Springer's LNCS series. ** After the conference the authors of selected papers will be invited to submit revised papers for a special issue of the Journal of Automated Reasoning. ** PAPER SUBMISSIONS All submissions must be original, unpublished, and not submitted concurrently for publication elsewhere. Furthermore, when appropriate, submissions are expected to be accompanied by verifiable evidence of a suitable implementation, such as the source files of a formalization for the proof assistant used. Submissions should be no more than 16 pages in length and are to be submitted in PDF via EasyChair at the following address: https://easychair.org/conferences/?conf=itp2017 Submissions must conform to the LNCS style in LaTeX. Authors of accepted papers are expected to present their paper at the conference and will be required to a sign copyright release form. In addition to regular papers, described above, there will be a rough diamond section. Rough diamond submissions are limited to 6 pages and may consist of an extended abstract. They will be refereed and be expected to present innovative and promising ideas, possibly in an early form and without supporting evidence. Accepted diamonds will be published in the main proceedings and will be presented as short talks. IMPORTANT DATES Abstract submission deadline: April 3, 2017 Full paper submission deadline: April 10, 2017 Author notification: June 2, 2017 Camera-ready papers: June 30, 2017 Workshops & Tutorials: September 23-25, 2017 Conference: September 26-29, 2017 INVITED SPEAKERS Moa Johansson, Chalmers University of Technology, Sweden Leonardo de Moura, Microsoft Research Cezary Kaliszyk, Universitaet Innsbruck, Austria (joint with TABLEAUX and FroCos) Katalin Bimbo, University of Alberta, Canada (joint with TABLEAUX and FroCos) Jasmin Blanchette, Inria and LORIA, Nancy, France (joint with TABLEAUX and FroCos) WORKSHOPS AND TUTORIALS There will be a three-day programme of four workshops and four tutorials from 23-25 September. Workshops: 12th Logical and Semantic Frameworks with Applications (LSFA 2017) Sandra Alves, Renata Wassermann, Flavio L. C. de Moura 23 and 24 September 2017 Proof eXchange for Theorem Proving (PxTP) Catherine Dubois, Bruno Woltzenlogel Paleo 23 and 24 September 2017 EPS - Encyclopedia of Proof Systems Giselle Reis, Bruno Woltzenlogel Paleo 24 and 25 September 2017 DaLi - Dynamic Logic: new trends and applications Mario Benevides, Alexandre Madeira 24 September 2017 Tutorials: General methods in proof theory for modal and substructural logics Bjoern Lellmann, Revantha Ramanayake 23 September 2017 From proof systems to complexity bounds Anupam Das 24 September 2017 Proof Compressions and the conjecture NP =3D PSPACE Lew Gordeev, Edward Hermann Haeusler 25 September 2017 PVS for Computer Scientists Cesar Munoz, Mauricio Ayala-Rincon, Mariano Moscato 25 September 2017 Details will be published in separate calls and on the conference website. PROGRAM COMMITTEE CHAIRS Mauricio Ayala-Rincon, U. Brasilia Cesar Munoz, NASA PROGRAM COMMITTEE Maria Alpuente, T.U. Valencia Vander Alves, U. Brasilia June Andronick, Data61, CSIRO, UNSW Jeremy Avigad, Carnegie Mellon U. Sylvie Boldo, INRIA LRI Ana Bove, Chalmers & Gothenburg U. Adam Chlipala, MIT Gilles Dowek, INRIA, ENS Cachan Aaron Dutle, NASA Amy Felty, U. Ottawa Marcelo Frias, I.T. Buenos Aires Ruben Gamboa, U. Wyoming Herman Geuvers, Radboud U. Elsa Gunter, U. Illinois U.C. John Harrison, Intel Corporation Nao Hirokawa, JAIST Matt Kaufmann, U. Texas Austin Mark Lawford, McMaster U. Andreas Lochbihler, ETH Zurich Assia Mahboubi, INRIA Panagiotis Manolios, Northeastern U. Gopalan Nadathur, U. Minnesota Keiko Nakata, SAP Potsdam Adam Naumowicz, U. Bialystok Tobias Nipkow, T.U. Munich Scott Owens, U. Kent Sam Owre, SRI Lawrence Paulson, U. Cambridge Leila Ribeiro, U.F. Rio Grande do Sul Claudio Sacerdoti Coen, U. Bologna Augusto Sampaio, U.F. Pernambuco Monika Seisenberger, Swansea U. Christian Sternagel, U. Innsbruck Sofiene Tahar, Concordia U. Christian Urban, King's College London Josef Urban, Czech T.U. Prague CONTACT INFORMATION itp2017(a)easychair.org http://itp2017.cic.unb.br

1 0

[FINAL CALL FOR PAPERS] TABLEAUX 2017, University of Brasilia, Brazil, September 25-28, 2017
by Katsuhiko Sano 13 Mar '17

13 Mar '17

************************************************************************ FINAL CALL FOR PAPERS TABLEAUX 2017 26th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods University of Brasilia, Brazil September 25-28, 2017 Deadlines: 18 Apr 2017 (abstract), 25 Apr 2017 (paper) http://tableaux2017.cic.unb.br/ GENERAL INFORMATION TABLEAUX is the main international conference at which research on all aspects, theoretical foundations, implementation techniques, systems development and applications, of the mechanization of tableau-based reasoning and related methods is presented. As the first TABLEAUX workshop was held in Lautenbach in 1992, this year's conference will include special events celebrating 25 years of TABLEAUX. The conference will be held in Brasilia from 25-28 September 2017. It will be co-located with both the 11th International Symposium on Frontiers of Combining Systems (FroCoS 2017) and the 8th International Conference on Interactive Theorem Proving (ITP 2017). TOPICS Tableau methods offer a convenient and flexible set of tools for automated reasoning in classical logic, extensions of classical logic, and a large number of non-classical logics. For large groups of logics, tableau methods can be generated automatically. Areas of application include verification of software and computer systems, deductive databases, knowledge representation and its required inference engines, teaching, and system diagnosis. Topics of interest include but are not limited to: * tableau methods for classical and non-classical logics (including first-order, higher-order, modal, temporal, description, hybrid, intuitionistic, substructural, relevance, non-monotonic logics) and their proof-theoretic foundations; * related methods (SMT, model elimination, model checking, connection methods, resolution, BDDs, translation approaches); * sequent calculi and natural deduction calculi for classical and non-classical logics, as tools for proof search and proof representation; * flexible, easily extendable, light weight methods for theorem proving; * novel types of calculi for theorem proving and verification in classical and non-classical logics; * systems, tools, implementations, empirical evaluations and applications (provers, logical frameworks, model checkers, ...); * implementation techniques (data structures, efficient algorithms, performance measurement, extensibility, ...); * extensions of tableau procedures with conflict-driven learning, generation of proofs; compact (or humanly readable) representation of proofs; * decision procedures, theoretically optimal procedures; * applications of automated deduction to mathematics, software development, verification, deductive and temporal databases, knowledge representation, ontologies, fault diagnosis or teaching. We also welcome papers describing applications of tableau procedures to real world examples. Such papers should be tailored to the tableau community and should focus on the role of reasoning, and logical aspects of the solution. CELEBRATING 25 YEARS To celebrate 25 years TABLEAUX the conference will include a special session of invited talks by: Reiner Haehnle Technische Universitaet Darmstadt, Germany Wolfgang Bibel Technische Universitaet Darmstadt, Germany INVITED SPEAKERS: Carlos Areces FaMAF - Universidad Nacional de Cordoba, Argentina Katalin Bimbo University of Alberta, Canada (with FroCoS and ITP) Jasmin Blanchette Inria and LORIA, Nancy, France (with FroCoS and ITP) Cezary Kaliszyk Universitaet Innsbruck, Austria (with FroCoS and ITP) WORKSHOPS AND TUTORIALS There will be a three-day programme of four workshops and four tutorials from 23-25 September. Workshops: 12th Logical and Semantic Frameworks with Applications (LSFA 2017) Sandra Alves, Renata Wassermann, Flavio L. C. de Moura 23 and 24 September 2017 Proof eXchange for Theorem Proving (PxTP) Catherine Dubois, Bruno Woltzenlogel Paleo 23 and 24 September 2017 EPS - Encyclopedia of Proof Systems Giselle Reis, Bruno Woltzenlogel Paleo 24 and 25 September 2017 DaLi - Dynamic Logic: new trends and applications Mario Benevides, Alexandre Madeira 24 September 2017 Tutorials: General methods in proof theory for modal and substructural logics Bjoern Lellmann, Revantha Ramanayake 23 September 2017 From proof systems to complexity bounds Anupam Das 24 September 2017 Proof Compressions and the conjecture NP = PSPACE Lew Gordeev, Edward Hermann Haeusler 25 September 2017 PVS for Computer Scientists Cesar Munoz, Mauricio Ayala-Rincon, Mariano Moscato 25 September 2017 Details will be published in separate calls and on the conference website. POSTER SESSION There will be a joint poster session for TABLEAUX 2017, FroCos 2017, and ITP 2017. The session is intended for descriptions of work in progress, student projects and relevant research being published elsewhere. The deadline for posters submission is June 15, 2017. More details can be found at http://tableaux2017.cic.unb.br/#postersession. PUBLICATION DETAILS The conference proceedings will published in the Springer LNAI/LNCS series, as in previous editions. SUBMISSIONS Submissions are invited in two categories: A Research papers, which describe original theoretical research, original algorithms, or applications, with length up to 15 pages. B System descriptions, with length up to 9 pages. Submissions will be reviewed by the PC, possibly with the help of external reviewers, taking into account readability, relevance and originality. For category A, theoretical results and algorithms must be original, and not submitted for publication elsewhere. Submissions will be reviewed taking into account correctness, theoretical elegance, and possible implementability. For category B submissions, a working implementation must be accessible via the internet, which includes sources. The aim of a system description is to make the system available in such a way that users can use it, understand it, and build on it. Accepted papers in both categories will be published in the conference proceedings. Papers must be edited in LaTeX using the llncs style and must be submitted electronically as PDF files via the EasyChair system: https://easychair.org/conferences/?conf=tableaux2017. For all accepted papers at least one author is required to attend the conference and present the paper. A paper title and a short abstract of about 100 words must be submitted before the paper submission deadline. Further information about paper submissions will be made available at the conference website. Be aware that neither plagiarism, nor self-plagiarism, nor duplicate publication is acceptable. Formatting instructions and the LNCS style files can be obtained via http://www.springer.com/br/computer-science/lncs/conference-proceedings-gui… BEST PAPER AWARD The TABLEAUX 2017 Best Paper Award will be presented to the best submission nominated and chosen by the Program Committee among the accepted papers. The eligibility criteria will place emphasis on the originality and significance of the contribution, but readability and the overall technical quality, including correctness and completeness of results, will also be considered. The TABLEAUX Best Paper Award was established in 2015 and is a permanent initiative of TABLEAUX. IMPORTANT DATES 18 Apr 2017 Abstract submission 25 Apr 2017 Paper submission 8 Jun 2017 Notification of paper decisions 3 Jul 2017 Camera-ready papers due 23-25 Sep 2017 Workshops & Tutorials 25-28 Sep 2017 TABLEAUX Conference PROGRAM COMMITTEE Peter Baumgartner National ICT Australia, Canberra Maria Paola Bonacina Universita degli Studi di Verona Laura Bozzelli Universidad Politecnica de Madrid Torben Brauener Roskilde University Serenella Cerrito Ibisc, Universite d'Evry Val d'Essonne Agata Ciabattoni Technische Universitaet Wien Clare Dixon University of Liverpool Pascal Fontaine LORIA, INRIA, Universite de Lorraine Didier Galmiche LORIA, Universite de Lorraine Martin Giese Universitetet i Oslo Laura Giordano DISIT, Universita del Piemonte Orientale Rajeev Gore The Australian National University Volker Haarslev Concordia University George Metcalfe Universitaet Bern Angelo Montanari Universita degli Studi di Udine Barbara Morawska Technische Universitaet Dresden Boris Motik University of Oxford Leonardo de Moura Microsoft Research Neil Murray SUNY at Albany Claudia Nalon Universidade de Brasilia Linh Anh Nguyen Uniwersytet Warszawski Hans de Nivelle Uniwersytet Wroclawski Nicola Olivetti LSIS, Aix-Marseille Universite Jens Otten Universitetet i Oslo Valeria de Paiva Nuance Communications Nicolas Peltier Centre National de la Recherche Scientifique, Laboratoire d'Informatique de Grenoble Elaine Pimentel Universidade Federal do Rio Grande do Norte Giselle Reis Carnegie Mellon University-Qatar Philipp Ruemmer Uppsala Universitet Katsuhiko Sano Hokkaido University Renate Schmidt The University of Manchester Cesare Tinelli The University of Iowa Alwen Tiu Nanyang Technological University David Toman University of Waterloo Josef Urban Ceske vysoke uceni technicke v Praze LOCAL CONFERENCE ORGANIZATION COMMITTEE Claudia Nalon, Universidade de Brasilia, Brazil Daniele Nantes Sobrinho, Universidade de Brasilia, Brazil Elaine Pimentel, Universidade Federal do Rio Grande do Norte, Brazil Joao Marcos, Universidade Federal do Rio Grande do Norte, Brazil CONFERENCE CHAIR Claudia Nalon, University of Brasilia, Brazil PC CHAIRS Claudia Nalon, University of Brasilia, Brazil Renate Schmidt, The University of Manchester, UK

1 0

[Second Call for Paper] LORI-VI: The Sixth International Conference on Logic, Rationality and Interaction, September 11-14, 2017, Hokkaido University, Sapporo, Japan
by Katsuhiko Sano 13 Mar '17

13 Mar '17

Second Call for Papers LORI-VI: The Sixth International Conference on Logic, Rationality and Interaction September 11-14, 2017, Hokkaido University, Sapporo, Japan http://golori.org/lori2017/ [About LORI] The International Conference on Logic, Rationality and Interaction (LORI) conference series aims at bringing together researchers working on a wide variety of logic-related topics that concern the understanding of rationality and interaction. The series aims at fostering a view of Logic as an interdisciplinary endeavour, and supports the creation of an East-Asian community of interdisciplinary researchers. [News] *** 60,000 yen (approx 500 Euro) prize for best student paper *** The best student paper will be selected from the contributed student papers accepted for presentation at LORI VI, and be awarded the prize of 60,000 Japanese Yen (approximately 500 Euro). For more details, see http://golori.org/lori2017/award.html . [Call for Papers] We invite submission of contributed papers on any of the broad themes of LORI series; specific topics of interest include, but are not limited to, formal approaches to ・ agency ・ argumentation and agreement ・ belief representation ・ cooperation ・ belief revision and belief merging ・ strategic reasoning ・ games ・ decision making and planning ・ knowledge and action ・ epistemology ・ dynamics of informational attitudes ・ speech acts ・ knowledge representation ・ interaction ・ norms and normative systems ・ natural language ・ rationality ・ philosophy and philosophical logic ・ preference and utility ・ social choice ・ probability and uncertainty ・ social interaction ・ intentions, plans, and goals Submitted papers should be at most 12 pages long, with one additional page for references, in PDF format following the Springer LNCS style. Please submit your paper by Friday March 31, 2017, via EasyChair : http://easychair.org/conferences/?conf=lori6 . [Publication] Accepted papers will be collected as a volume in the FoLLI Series on Logic, Language and Information, and authors may be later invited to submit extended versions of their papers in a special issue of a prestigious journal. [Website] For detailed conference information and registration, please visit http://golori.org/lori2017/ . [Invited Speakers] Mike Dunn: Indiana University, U.S.A. Alan Hajek: Australian National University, Australia Nina Gierasimczuk: Technical University of Denmark, Denmark Willemien Kets: Northwestern University, U.S.A Sara Negri: University of Helsinki, Finland Hiroakira Ono: JAIST, Japan [PC Chairs] Alexandru Baltag: University of Amsterdam, The Netherlands Jeremy Seligman: University of Auckland, New Zealand [Conference Organiser] Tomoyuki Yamada: Hokkaido University, Japan [Sponsors] LORI Tsinghua University - University of Amsterdam Joint Research Centre for Logic Hokkaido University [Contacts] Programme: The PC Chairs <lori6(a)easychair.org> Conference: Tomoyuki Yamada <tomoyuki.s.yamada(a)gmail.com>

1 0

JAIST Logic Seminar Series
by Takako Nemoto 10 Mar '17

10 Mar '17

皆様 Ludwig-Maximilians-Universität München の Josef Berger 博士の講演のお知らせです。どうぞふるってご参加ください。問い合わせ先：根元　多佳子北陸先端科学技術大学院大学　情報科学系 email: t-nemoto(a)jaist.ac.jp --------------------------------------------- *JAIST Logic Seminar Series* Date: Thursday 16 March, 2017, 15:20-17:00 Place: JAIST, Collaboration room 7 (I-56) (Access: http://www.jaist.ac.jp/english/location/access.html) Speaker: Josef Berger (udwig-Maximilians-Universität München, Germany) (joint work with Gregor Svindland) Brouwer's fan theorem and convexity In the framework of Bishop's constructive mathematics, we introduce a correspondence between sets B of finite binary sequences on the one hand and uniformly continuous functions f on the unit interval on the other hand. This correspondence is compatible with basic properties of the involved objects as follows: i) B is a bar if and only if the corresponding f is positive-valued ii) B is a uniform bar if and only if f has positive infimum iii) B is weakly convex if and only f is weakly convex. This simplifies and generalises a result in William H. Julian and Fred Reichmann, A uniformly continuous function on [0, 1] that is everywhere different from its infimum. Pacific Journal of Mathematics 111, No 2 (1984) 333–340

1 0

QIT36のご案内
by NISHIMURA Harumichi 08 Mar '17

08 Mar '17

logic-mlの皆様 QIT36世話人に代わりまして第36回量子情報技術研究会(QIT36)の会告を以下の通り投稿させていただきます．どうぞよろしくお願いいたします．名古屋大学大学院情報科学研究科西村治道 ---------------- 第36回量子情報技術研究会(QIT36) 研究会の内容：情報科学と量子力学を融合させた新しい分野，量子情報科学に関する研究会です．情報を担う物理系の量子力学的側面を積極的に活かした新しい情報処理原理の研究とそこから開かれる新しい学問体系の構築および新しい情報技術パラダイムの創生を目指して，情報科学，物理学，光エレクトロニクスを含む理学，工学，数理科学に携わる研究者間に自由な討論の場を提供し，この研究分野の発展を図ることを目的としています．第36回研究会を下記のように開催いたします．現在この分野で活躍する研究者は勿論，自分の研究資産が何らかの形で使えそうだと予感している研究者・技術者など，広く関連する分野の研究者・技術者からの発表を募集致します．聴講のみの参加も歓迎致しますので，奮ってお申し込みください．日時: 2017年5月29日(月)～30日(火) 会場: 立命館大学朱雀キャンパス５階大講義室（ホール） (〒604-8520 京都市中京区西ノ京朱雀町１）発表募集分野 (申し込み状況によっては査読の可能性あり)：量子情報，量子計算，量子暗号など広く量子情報技術に関わる理論的研究，実験的研究，計算機科学的研究，数学的研究，および，その他関連分野．定員: 200名参加費: 事前振込み一般2,000円，学生1,000円（当日会場払いは一般3,000円，学生2,000円．学生に限り予稿集なしで当日無料参加可能です．）懇親会費：事前振り込み一般4,000円，学生2,000円．（当日会場払いは一般5,000円，学生3,000円．）招待・チュートリアル講演：笹川崇男（東京工業大学）：CRESTプロジェクト「トポロジカル量子計算の基盤技術構築」の研究構想について田家慎太郎（京都大学）：光格子を用いた実験による、量子磁性や高温超伝導といった固体電子系の物理に対する量子シミュレーションに関した最近の成果と展望について谷誠一郎（NTT）：機能制限された量子計算モデルの能力について並木亮（学習院大学）：連続量量子チャンネルの最近の理論展開について研究会参加申込要領：参加申込は下記 Web にて受付けます： http://staff.aist.go.jp/s-kawabata/qit/ 講演 (口頭，ポスター) の申込，予稿集原稿 PDF の提出は，電子情報通信学会の Web システムを使用する予定．【口頭講演申込締切】2017年4月7日(金) 【ポスター講演申込締切】2017年4月21日(金) 【予稿原稿提出締切】2017年4月21日(金) 【参加申込締切】2017年4月28日(金) 【問合せ先】山下茂（立命館大学）中西正樹（山形大学) 添田彬仁（東京大学) Email: qit36(a)ngc.is.ritsumei.ac.jp 主催: 量子情報技術時限研究専門委員会 (委員長: 竹内繁樹 (京都大学)) 共催: 応用物理学会量子エレクトロニクス研究会立命館大学情報理工学部

1 0

First NII Programming and Logic Workshop
by Makoto Tatsuta 27 Feb '17

27 Feb '17

First NII Programming and Logic Workshop Date: March 2--3, 2017 Place: National Institute of Informatics, Room 2006 (20th floor) 場所: 国立情報学研究所 20階 2006室 (半蔵門線,都営地下鉄三田線・新宿線神保町駅または東西線竹橋駅より徒歩5分) (地図 http://www.nii.ac.jp/about/access/) Program: March 2 10:20--11:00 Wei-Ngan Chin (National University of Singapore) Title: Automated Verification and Analysis of Expressive Specifications 11:00--11:40 Zhenjiang Hu (National Institute of Informatics) Title: Towards Change-Oriented Programming 11:40--11:55 Break 11:55--12:35 Makoto Tatsuta (National Institute of Informatics) Title: Presburger and Mutual Inductive Definitions 12:35--14:00 Lunch Break 14:00--14:40 Quang Loc Le (Singapore University of Technology and Design / National University of Singapore) Title: A Decidable Fragment in Separation Logic with Inductive Predicates and Arithmetic 14:40--15:20 Hsiang-Shang Ko (National Institute of Informatics) Title: An Axiomatic Basis for Bidirectional Programming 15:20--15:35 Break 15:35--16:15 Daisuke Kimura (Toho University) Title: Decidability of Entailments in Separation Logic with Arrays 16:15--16:55 Mahmudul Faisal Al Ameen (National University of Singapore) Title: Separation-Logic-Based Analyzer for Detecting Memory Errors March 3 10:15--10:55 Koji Nakazawa (Nagoya University) Title: Cyclic-Proof-Based Decision Procedure for Symbolic Heaps and Inductive Definitions 10:55--11:35 Shin-Cheng Mu (Academia Sinica) Title: Towards Derivation of Monadic Programs: A Case Study of States and Nondeterminism 11:35--11:50 Break 11:50--12:30 Andreea Costea National University of Singapore) Title: Automated Reasoning for Race-Free Channels with Explicit Synchronization and Precise Disjunction Abstracts: ---------------------------------------------------------------------- Speaker: Wei-Ngan Chin (National University of Singapore) Title: Automated Verification and Analysis of Expressive Specifications Abstract: The last two decades have seen a proliferation of research activities in methodologies, techniques and systems for automated verification and analysis of software programs. One driving force in this direction has been the deployment of expressive logics that are able to capture specifications of programs in a concise and precise manner. One of these logics that my research group has been pre-occupied with in the last decade is separation logic itself, made popular by seminal works of John Reynolds and Peter O’Hearn. Separation logic is a sub-structural which treats memory locations as resources that can be transferred, borrowed or consumed. Such a resource logic allows must-aliasing and updates to be succinctly expressed. We have looked into various extensions to support expressive specification logics. We have also explored automated verification techniques that work with inductive predicates. We have proposed and evaluated decision procedures on satisfiability and entailment on some fragments of our logics. We have moreover extended our approach to support incremental specification inference with the help of second-order unknown predicates. These works have challenged us to go beyond properties that guarantee memory safety and correctness, to include also termination, immutability infinity, deeper sharing, communication and concurrency. We shall describe several aspects of our recent endeavours here. ---------------------------------------------------------------------- Speaker: Zhenjiang Hu (National Institute of Informatics) Title: Towards Change-Oriented Programming Abstract: Change is essential and expensive in software development. Although a significant amount of work has been done on software change, its status as a scientific discipline is still an open challenge. In this talk, I will show that it is possible to treat software change as a first-class citizen in software development. The success of this work could lead to change-oriented programming, a new programming paradigm that can effectively cope with software dynamics. ---------------------------------------------------------------------- Speaker: Makoto Tatsuta (National Institute of Informatics) Title: Presburger and Mutual Inductive Definitions Abstract: This talk proposes some restrictions for a system of Presburger arithmetic and mutual inductive definitions and proves the decidability of truth in the system. To prove it, this talk shows that every inductively defined predicate in the system represents a semilinear set. Since inductively defined predicates can be eliminated, the truth is decided in the arithmetic. This system is an extension of the system given in our APLAS 2016 paper but more expressive as it can handle mutual inductive definitions and more than one induction steps in inductive definitions. ---------------------------------------------------------------------- Speaker: Quang Loc Le (Singapore University of Technology and Design / National University of Singapore) Title: A Decidable Fragment in Separation Logic with Inductive Predicates and Arithmetic Abstract: We consider the satisfiability problem for a fragment of separation logic including inductive predicates with shape and arithmetic properties. We show that the fragment is decidable if the arithmetic properties can be represented as semilinear sets. Our decision procedure is based on a novel algorithm to infer a finite representation for each inductive predicate which precisely characterises its satisfiability. Our analysis shows that the proposed algorithm runs in exponential time in the worst case. To show the feasibility of our proposal, we have implemented our decision procedure, integrated it into an existing verification system and evaluated the solver on a set of satisfiability problems which is generated from the verification of heap-manipulated programs. ---------------------------------------------------------------------- Speaker: Hsiang-Shang Ko (National Institute of Informatics) Title: An Axiomatic Basis for Bidirectional Programming Abstract: Among the frameworks of bidirectional transformations proposed for addressing various synchronisation problems, Foster et al.’s lenses have influenced the design of a generation of bidirectional programming languages. Most of these languages are highly declarative, and only allow the programmer to specify a consistency relation with limited control over the behaviour of the automatically derived consistency restorer. However, synchronisation problems are diverse and require vastly different consistency restoration strategies, and the programmer must be empowered to fully control and reason about the consistency restoration behaviour of their bidirectional programs. The putback-based approach to bidirectional programming was proposed to address this issue once and for all, and this talk will present the latest result along this line of research: a Hoare-style logic for the putback-based language BiGUL. With this Hoare-style logic, the BiGUL programmer can precisely understand the bidirectional behaviour of their programs by reasoning solely in the putback direction. The theory underlying the Hoare-style logic has been formalised and checked in the dependently typed language Agda, but this talk will give a semi-formal presentation of the logic suitable for human reasoning. ---------------------------------------------------------------------- Speaker: Daisuke Kimura (Toho University) Title: Decidability of Entailments in Separation Logic with Arrays Abstract: We show decidability of validity of entailments in symbolic-heap fragment of separation logic with arrays, which is designed for verifying array-manipulating imperative programs. Our proof is given by translating entailments into formulas of Presburger Arithmetic, which is known to be decidable. Finally we provide an implementation of our decision procedure, in which Presburger-formulas are decided by an internally called SMT-solver. ---------------------------------------------------------------------- Speaker: Mahmudul Faisal Al Ameen (National University of Singapore) Title: Separation-Logic-Based Analyzer for Detecting Memory Errors Abstract: This talk discusses an implementation of a separation-logic-based analyzer for memory errors. This system is based on symbolic heap with presburger arithmetic. This implementation extracts errors by analyzing the strongest postcondition. The system abstracts all the existentially quantified pointers. A while loop is analyzed using fixed point analysis and it uses an arithmetic decision procedure. It is also intended to analyze array and inter-procedure analysis. ---------------------------------------------------------------------- Speaker: Koji Nakazawa (Nagoya University) Title: Cyclic-Proof-Based Decision Procedure for Symbolic Heaps and Inductive Definitions Abstract: We introduce a new cyclic-proof system CSLID_omega for separation logic with inductively defined predicates. CSLID_omega is complete and gives decision procedure for entailment checking based on the unfold-match approach. ---------------------------------------------------------------------- Speaker: Shin-Cheng Mu (Academia Sinica) Title: Towards Derivation of Monadic Programs: A Case Study of States and Nondeterminism Abstract: Equational reasoning is among the most important tools that functional programming provides us. Curiously, relatively little attention has been paid on reasoning about monadic programs. In this talk we propose some theorems and patterns useful for derivation of monadic programs, focusing on non-determinism and states. ---------------------------------------------------------------------- Speaker: Andreea Costea National University of Singapore) Title: Automated Reasoning for Race-Free Channels with Explicit Synchronization and Precise Disjunction Abstract: The usage of the message passing for inter-process communication leveraged the performance and scalability of computing platforms leading to a rise in the level of concurrency. Together with its benefits though, message passing also places a burden on the safety and correctness verification process of concurrent system, which was already a challenging task even in the absence of message passing. The current state of the art tackles this problem of safe message communication assuming the systems rely solely of message passing in order to obtain concurrency. However, this is generally not true, since existing software tend to use a combination of synchronization mechanisms. Our aim is to break the assumption of unique synchronization mechanisms, and step further into reasoning about hybrid communication system, where different concurrency instruments intermingle. We therefore present a multiparty session logic which vows to marry the message passing model with explicit synchronization mechanisms, such as CountDownLatch. In this context, we consider how to ensure well-formedness of the session logic, and how to build summaries that can help ensure race-freedom and type safety amongst shared channels. ---------------------------------------------------------------------- 問合せ先　龍田 (tatsuta(a)nii.ac.jp)

1 0

DICE-FOPARA 2017: deadline extension
by Nao Hirokawa 21 Feb '17

21 Feb '17

皆様 DICE-FOPARA 2017 の論文募集の案内をお送り致します。投稿締切が延長され、3月5日になっております。廣川 [Apologies for cross-postings.] ------------------------------------------------------------------------------------------- 8th Workshop on Developments in Implicit Computational complExity and 5th Workshop on Foundational and Practical Aspects of Resource Analysis (DICE-FOPARA 2017) Affiliated with ETAPS 2017 April 22 - 23, 2017, Uppsala, Sweden http://cbr.uibk.ac.at/events/dice-fopara ------------------------------------------------------------------------------------------- OBJECTIVES The first joint international workshop on Developments in Implicit Computational complExity and FOundational and Practical Aspects of Resource Analysis (DICE-FOPARA) will be held in Uppsala, Sweden, from April 22-23, 2017 as part of ETAPS. DICE-FOPARA serves as a forum for presenting results relevant to the implicit computational complexity theory *and* to the analysis of resource consumption by computer programs (e.g. time, space, energy). The workshop brings together researchers that work on foundational issues with researchers that focus more on practical results. For further information, kindly see the workshop's website. INVITED SPEAKERS Elvira Albert (Complutense University of Madrid) Kerstin I. Eder (University of Bristol) Lars Kristiansen (University of Oslo) Jan Reinecke (Universität Saarland) SUBMISSIONS We ask for submission of *regular papers* describing original work (10-15 pages) or *extended abstracts* (2-6 pages) presenting already published work or work in progress. Regular papers must be prepared using the LaTeX EPTCS class (see http://eptcs.org/). Accepted regular papers will appear in an EPTCS volume. Papers should be submitted electronically via the submission page: https://easychair.org/conferences/?conf=dicefopara2017 IMPORTANT DATES Paper submission March 5, 2017 (extended) Notification March 19, 2017 Final versions due March 26, 2017 Workshop date April 22-23, 2017 CONFERENCE VENUE The workshop will be held as a satellite workshop of European Joint Conferences on Theory and Practice of Software 2017 (ETAPS 2017) which takes place in Uppsala, Sweden. PROGRAM COMMITTEE Beniamino Accattoli (Paris) Guillaume Bonfante (Nancy, co-chair) Marko van Eekelen (Nijmegen) Marco Gaboardi (Buffalo) Dan Ghica (Birmingham) Clemens Grelck (Amsterdam) Charles Grellois (Bologna) Nao Hirokawa (JAIST) Jan Hoffmann (CMU) Thomas Jensen (Rennes) Björn Lisper (Mälardalen) Hans-Wolfgang Loidl (Edinburgh) Georg Moser (Innsbruck, co-chair) Kazushige Terui (Kyoto) Simon Wegener (Saarbrücken) Florian Zuleger (Vienna)

1 0

JAIST Logic Seminar Series
by Takako Nemoto 14 Feb '17

14 Feb '17

皆様ベルン大学の Silvia Steila 博士の講演のお知らせです。どうぞふるってご参加ください。問い合わせ先：根元　多佳子北陸先端科学技術大学院大学　情報科学系 email: t-nemoto(a)jaist.ac.jp --------------------------------------------- *JAIST Logic Seminar Series* Date: Tuesday 28 February, 2017, 15:20-17:00 Place: JAIST, Collaboration room 7 (I-56) (Access: http://www.jaist.ac.jp/english/location/access.html) Speaker: Silvia Steila (University of Bern, Switzerland) Title: The strength of the SCT criterion (Joint work with Emanuele Frittaion and Keita Yokoyama). In 2001 Lee, Jones and Ben-Amram introduced the notion of size-change termination (SCT) for first order functional programs, a sufficient condition for termination. They proved that a program is size-change terminating if and only if it satisfies a certain property which can be statically verified from the recursive definition of the program. We call this equivalence SCT criterion. We undertake the study of size-change analysis in the context of Reverse Mathematics. In particular, we prove that the SCT criterion is equivalent to $\Sigma_2$-induction over RCA$_{0}$.

1 0

CCA 2017 (Computability and Complexity in Analysis): 2nd call for papers
by Daniel Graça 10 Feb '17

10 Feb '17

______________________________________________________________ Second Call for Papers Fourteenth International Conference on Computability and Complexity in Analysis (CCA 2017) http://cca-net.de/cca2017/ July 24-27, 2017, Daejeon, Republic of Korea (South Korea) Submission deadline: April 3, 2017 ______________________________________________________________ Topics * Computable analysis * Complexity on real numbers * Constructive analysis * Domain theory and analysis * Effective descriptive set theory * Theory of representations * Computable numbers, subsets and functions * Randomness and computable measure theory * Models of computability on real numbers * Realizability theory and analysis * Reverse analysis * Real number algorithms * Implementation of exact real number arithmetic Invited Speakers * Hee-Kap Ahn (Pohang, Republic of Korea) * Verónica Becher (Buenos Aires, Argentina) * Anders Hansen (Cambridge, UK) * Takayuki Kihara (Berkeley, USA) * Amaury Pouly (Max Planck Institute, Germany) * Linda Brown Westrick (Connecticut, USA) Scientific Programme Committee * Johanna Franklin (Hempstead, USA) * Daniel Graça, chair (Faro, Portugal) * Vassilios Gregoriades (Turin, Italy) * Peter Hertling (Munich, Germany) * Gyesik Lee (Anseong, Republic of Korea) * Alexander Melnikov (Auckland, New Zealand) * Takako Nemoto (Ishikawa, Japan) * Arno Pauly (Brussells, Belgium) * Cristóbal Rojas (Santiago, Chile) * Frank Stephan (Singapore) * Klaus Weihrauch (Hagen, Germany) Organising Committee * Sunyoung Kim (Yonsei University, Republic of Korea) * Sewon Park (KAIST, Republic of Korea) * Martin Ziegler, chair (KAIST, Republic of Korea) Submissions Authors are invited to submit 1-2 pages abstracts in PDF format, including references via the following web page: https://easychair.org/conferences/?conf=cca2017 If full versions of papers are already available as technical report or arXiv version, then corresponding links should be added to the reference list. Final versions of abstracts might be distributed to participants in hardcopy and/or in electronic form. Dates * Submission deadline: April 3, 2017 * Notification of authors: May 1, 2017 * Final version: May 29, 2017 Conference Web Page http://cca-net.de/cca2017/ A co-located "Workshop on Real Verification" will take place on Friday, July 28, jointly organized by: * Gyesik Lee (Hankyong National University, Republic of Korea) * Martin Ziegler (KAIST, Republic of Korea) https://complexity.kaist.edu/CCA2017/workshop.html

1 0

DICE-FOPARA 2017 - Second Call for Papers
by Nao Hirokawa 09 Feb '17

09 Feb '17

皆様 ETAPS に併設されます DICE-FOPARA 2017 の論文募集案内をお送り致します。投稿締切は2月19日です。ぜひご投稿をご検討下さい。廣川 (JAIST) ------------------------------------------------------------------------------------------- 8th Workshop on Developments in Implicit Computational complExity and 5th Workshop on Foundational and Practical Aspects of Resource Analysis (DICE-FOPARA 2017) Affiliated with ETAPS 2017 April 22 - 23, 2017, Uppsala, Sweden http://cbr.uibk.ac.at/events/dice-fopara ------------------------------------------------------------------------------------------- OBJECTIVES The first joint international workshop on Developments in Implicit Computational complExity and FOundational and Practical Aspects of Resource Analysis (DICE-FOPARA) will be held in Uppsala, Sweden, from April 22-23, 2017 as part of ETAPS. DICE-FOPARA serves as a forum for presenting results relevant to the implicit computational complexity theory *and* to the analysis of resource consumption by computer programs (e.g. time, space, energy). The workshop aims to bring together the researchers that work on foundational issues with the researchers that focus more on practical results. INVITED SPEAKERS Elvira Albert (Complutense University of Madrid) Kerstin I. Eder (University of Bristol) Lars Kristiansen (University of Oslo) Jan Reinecke (Universität Saarland) SUBMISSIONS We ask for submission of *regular papers* describing original work (10-15 pages) or *extended abstracts* (2--6 pages) presenting already published work or work in progress. Regular papers must be prepared using the LaTeX EPTCS class (see http://eptcs.org/). Accepted regular papers will appear in an EPTCS volume. Papers should be submitted electronically via the submission page: https://easychair.org/conferences/?conf=dicefopara2017 IMPORTANT DATES Paper submission February 19, 2017 Notification March 19, 2017 Final versions due March 26, 2017 Workshop date April 22-23, 2017 CONFERENCE VENUE The workshop will be held as a satellite workshop of European Joint Conferences on Theory and Practice of Software 2017 (ETAPS 2017) which takes place in Uppsala, Sweden. PROGRAM COMMITTEE Beniamino Accattoli (Paris) Guillaume Bonfante (Nancy, co-chair) Marko van Eekelen (Nijmegen) Marco Gaboardi (Buffalo) Dan Ghica (Birmingham) Clemens Grelck (Amsterdam) Charles Grellois (Bologna) Nao Hirokawa (JAIST) Jan Hoffmann (CMU) Thomas Jensen (Rennes) Björn Lisper (Mälardalen) Hans-Wolfgang Loidl (Edinburgh) Georg Moser (Innsbruck, co-chair) Kazushige Terui (Kyoto) Simon Wegener (Saarbrücken) Florian Zuleger (Vienna)

1 0

Summer School in Dynamic Epistemic Logic, Sapporo (Japan), 14-25 Aug 2017
by Katsuhiko Sano 07 Feb '17

07 Feb '17

The Department of Philosophy at Hokkaido University (Sapporo, Japan) will hold a two-week summer school in dynamic epistemic logic and its applications, jointly with three guest lecturers from ILLC (University of Amsterdam) from August 14 to August 25 as part of Hokkaido Summer Institute (HSI) 2017. The following two intensive courses are scheduled to be offered during the summer school. Course 1 (August 14 to August 18): Introduction to Logic (For details, see http://hokkaidosummerinstitute.oia.hokudai.ac.jp/courses/CourseDetail=G070) Course 2 (August 21 to August 25): Dynamic Epistemic Logic and its Applications (For details, see http://hokkaidosummerinstitute.oia.hokudai.ac.jp/courses/CourseDetail=G074 ) The main lecturer of Course 1 is Katsuhiko Sano (Department of Philosophy, Hokkaido University). The main lectures of Course 2 are Alexandru Baltag and Sonja Smets (ILLC, University of Amsterdam). There will be a special live on-line lecture by Johan van Benthem (University of Amsterdam, Stanford University, and Tsinghua University) during Course 2. Tomoyuki Yamada and Yasushi Nomura (Hokkaido University) will also join the classes to help students follow the lectures, and communicate with the lecturers. The courses are intended for graduate students. Course 1 is meant for students without prior knowledge of logic and will prepare them for Course 2. Each course is designed to be independent from the other course. Those students who have some familiarity with basics of propositional logic, first order logic, and modal logic can skip Course 1, and those who wish to take only Course 1 can learn basics of logic. Application period for students from universities other than Hokkaido University is from February 1 to February 28 2017. For more details about applications, please check the HSI official website: https://hokkaidosummerinstitute.oia.hokudai.ac.jp/applications/ As the summer in Sapporo is beautiful and pleasant, it's a good idea to learn logic this summer in Sapporo. Tomoyuki Yamada Department of Philosophy Hokkaido University

1 0

早稲田大学江田勝哉先生最終講義
by Toshimichi Usuba 06 Feb '17

06 Feb '17

（このお知らせを重複して受け取られた方はご容赦ください）皆様、早稲田大学の薄葉です。本年3月をもちまして、早稲田大学基幹理工学部数学科江田勝哉先生がご退職されますことに伴い、 3月11日（土）に最終講義が行われることをお知らせいたします。日時：3月11日（土）13時〜14時30分題目：Speckerの定理（双対定理）をめぐって場所：早稲田大学西早稲田キャンパス52号館101教室最終講義に関する問い合わせは薄葉 <usuba(a)waseda.jp> までお願いいたします。皆様のご参加をお待ちしております。 -- Toshimichi USUBA School of Fundamental Science and Engineering, Waseda University

1 0

Fwd: categories: CALCO 2017: Second Call for Papers
by Ichiro Hasuo 04 Feb '17

04 Feb '17

========================================================= CALL FOR PAPERS: CALCO 2017 7th International Conference on Algebra and Coalgebra in Computer Science June 13 - 16, 2017 Ljubljana, Slovenia http://coalg.org/mfps-calco2017/ ========================================================== Abstract submission: April 3, 2017 Paper submission: April 7, 2017 Author notification: May 15, 2017 Final version due: May 31, 2017 ========================================================== -- SCOPE -- CALCO aims to bring together researchers and practitioners with interests in foundational aspects, and both traditional and emerging uses of algebra and coalgebra in computer science. It is a high-level, bi-annual conference formed by joining the forces and reputations of CMCS (the International Workshop on Coalgebraic Methods in Computer Science), and WADT (the Workshop on Algebraic Development Techniques). Previous CALCO editions took place in Swansea (Wales, 2005), Bergen (Norway, 2007), Udine (Italy, 2009), Winchester (UK, 2011), Warsaw (Poland, 2013) and Nijmegen (the Netherlands, 2015). The seventh edition will be held in Ljubljana, Slovenia, colocated with MFPS XXXIII. -- INVITED SPEAKERS -- Nicoletta Sabadini - University of Insubria, IT Alex Simpson - University of Ljubljana, SL *Joint Session with MFPS on Metrics, Privacy and Learning:* James Worrell - University of Oxford, UK (Tutorial) *Further Invited Speakers:* Catuscia Palamidessi - Ecole polytechnique, FR Vincent Danos - Ecole normale superieure, FR Marco Gaboardi - University at Buffalo, USA -- TOPICS OF INTEREST -- We invite submissions of technical papers that report results of theoretical work on the mathematics of algebras and coalgebras, the way these results can support methods and techniques for software development, as well as experience with the transfer of the resulting technologies into industrial practice. We encourage submissions in topics included or related to those listed below. * Abstract models and logics - Automata and languages - Categorical semantics - Modal logics - Relational systems - Graph transformation - Term rewriting * Specialised models and calculi - Hybrid, probabilistic, and timed systems - Calculi and models of concurrent, distributed, mobile, and context-aware computing - General systems theory and computational models (chemical, biological, etc.) * Algebraic and coalgebraic semantics - Abstract data types - Inductive and coinductive methods - Re-engineering techniques (program transformation) - Semantics of conceptual modelling methods and techniques - Semantics of programming languages * System specification and verification - Algebraic and coalgebraic specification - Formal testing and quality assurance - Validation and verification - Generative programming and model-driven development - Models, correctness and (re)configuration of hardware/middleware/architectures, - Process algebra * Corecursion in Programming Languages - Corecursion in logic / constraint / functional / answer set programming - Corecursive type inference - Coinductive methods for proving program properties - Implementing corecursion - Applications * Algebra and Coalgebra in quantum computing - Categorical semantics for quantum computing - Quantum calculi and programming languages - Foundational structures for quantum computing - Applications of quantum algebra * String Diagrams and Network Theory - Combinatorial approaches - Theory of PROPs and operads - Rewriting problems and higher-dimensional approaches - Automated reasoning with string diagrams - Applications of string diagrams - Connections with Control Theory, Engineering and Concurrency -- SUBMISSION GUIDELINES -- Prospective authors are invited to submit full papers in English presenting original research. Submitted papers must be unpublished and not submitted for publication elsewhere. Experience papers are welcome, but they must clearly present general lessons learned that would be of interest and benefit to a broad audience of both researchers and practitioners. Proceedings will be published in the Dagstuhl LIPIcs???Leibniz International Proceedings in Informatics series. Final papers should be no more than 15 pages long in the format specified by LIPIcs (http://www.dagstuhl.de/publikationen/lipics/anleitung-fuer-autoren/). It is recommended that submissions adhere to that format and length. Submissions that are clearly too long may be rejected immediately. Proofs omitted due to space limitations may be included in a clearly marked appendix. Both an abstract and the full paper must be submitted by their respective submission deadlines. A special issue of the open access journal Logical Methods in Computer Science (http://www.lmcs-online.org), containing extended versions of selected papers, is also being planned. Submissions will be handled via EasyChair https://www.easychair.org/conferences/?conf=calco2017 -- BEST PAPER AND BEST PRESENTATION AWARDS -- This edition of CALCO will feature two awards: a Best Paper Award whose recipients will be selected by the PC before the conference and a Best Presentation Award, elected by the participants. -- IMPORTANT DATES -- Abstract submission: April 3, 2017 Paper submission: April 7, 2017 Author notification: May 15, 2017 Final version due: May 31, 2017 -- PROGRAMME COMMITTEE -- Andrej Bauer (University of Ljubljana, Slovenia) Filippo Bonchi (ENS Lyon, France, co-chair) Marcello Bonsangue (University of Leiden, Netherlands) Corina Cirstea (University of Southampton, UK) Robin Cockett (University of Calgary, Canada) Andrea Corradini (University of Pisa, Italy) Sergey Goncharov (Universitaet Erlangen-Nuernberg, Germany) Helle Hvid Hansen (Delft University of Technology, Netherlands) Ichiro Hasuo (University of Tokyo, Japan) Tobias Heindel (University of Copenhagen, Denmark) Tom Hirschowitz (Savoie Mont Blanc University, France) Bart Jacobs (University of Nijmegen, Netherlands) Bartek Klin (Warsaw University, Poland) Barbara Koenig (University of Duisburg-Essen, Germany, co-chair) Alexander Kurz (University of Leicester, UK) Paul Levy (University of Birmingham, UK) Radu Mardare (Aalborg University, Denmark) Stefan Milius (Universitaet Erlangen-Nuernberg, Germany) Samuel Mimram (Ecole Polytechnique, France) Till Mossakowski (Universitaet Magdeburg, Germany) Larry Moss (Indiana University, US) Daniela Petrisan (Universite Paris-Diderot, France) John Power (University of Bath, UK) Grigore Rosu (University of Illinois, US) Jan Rutten (CWI, University of Nijmegen, Netherlands) Peter Selinger (Dalhousie University, Canada) Alexandra Silva (University College London, UK) Pawel Sobocinski (University of Southampton, UK) Ana Sokolova (University of Salzburg, Austria) -- ORGANISING COMMITTEE -- Andrej Bauer (University of Ljubljana, Slovenia) Matija Pretnar (University of Ljubljana, Slovenia) -- PUBLICITY CHAIR -- Fabio Zanasi (University College London, UK) -- SATELLITE WORKSHOPS: CALCO EARLY IDEAS AND CALCO TOOLS -- The CALCO Early Ideas Workshop is intended to enable presentation of work in progress and original research proposals. PhD students and young researchers are particularly encouraged to contribute. The CALCO Tools Workshop is dedicated to tools based on algebraic and/or coalgebraic principles. CALCO 2017 will run together with the CALCO Early Ideas Workshop, with dedicated sessions at the end of each conference day. CALCO Tools will take place on June 13. [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

第28回松山TGSAセミナーのお知らせ
by Hiroshi Fujita 03 Feb '17

03 Feb '17

皆さま、第28回松山TGSAセミナーにおいて、下記のとおり、池上大祐さん（東京電機大学）の講演を予定していますのでお知らせします。皆さまのご参加をお待ちしております。　　（記）【日時】2017年2月22日(水) 16:30〜17:30 【場所】愛媛大学理学部2号館2階・大演習室(201号室) 【講演題目】 omega_1 の超コンパクト性【講演概要】集合論は無限について研究する数学の一分野である。現代数学では通常選択公理を仮定して議論を進めるが、集合論で重要な数学的対象である巨大基数の研究を進めるうえで、 "ZF+決定性公理" を初めとする選択公理の否定を導く集合論の公理系について考察するのが重要であることがここ三十年ほどで明らかになってきた。この講演では、集合論や巨大基数について紹介した後、選択公理の否定を導く巨大基数の性質について考察する。特に、omega_1（可算でない最小の無限基数）が超コンパクト基数という巨大基数になっているとき、実数直線にどのような影響があるかについて議論する。この研究は Nam Trang 氏との共同研究である。　　（以上です） -- 追記：松山TGSAセミナーは、「一般トポロジー・幾何学・集合論およびその応用」を広く扱うセミナーで、原則として月に１回、愛媛大学において開催されています。これまでの講演の記録はWeb http://www.math.sci.ehime-u.ac.jp/MGTSA.ja.html でご覧になれます。 -- 愛媛大学理学部藤田博司 <fujita.hiroshi.mh(a)ehime-u.ac.jp>

1 0

Talk by Marc Bagnol (9 Feb 11:00-)
by Tetsuya Sato 30 Jan '17

30 Jan '17

京都大学数理解析研究所の佐藤です。 2月9日11:00から、東京大学のMarc Bagnol氏に以下の講演をしていただくことになりましたので、ご連絡いたします。どうぞお気軽にお越しください。 ========== Time: 11:00-12:00, 9 Feb, 2017 Place: Rm 478, Research Building 2, Main Campus, Kyoto University 京都大学本部構内総合研究2号館 4階478号室 http://www.kyoto-u.ac.jp/en/access/yoshida/main.html (Building 34) http://www.kyoto-u.ac.jp/ja/access/campus/map6r_y.htm (34番の建物) Speaker: Marc Bagnol (JSPS Postdoctoral Fellow, University of Tokyo) Title: Multiplicative-Additive Proof Equivalence is Logspace-complete Abstract: Given a logic presented in a sequent calculus, a natural question is that of equivalence of proofs: to determine whether two given proofs are equated by any denotational semantics, i.e. any categorical interpretation of the logic compatible with its cut-elimination procedure. This notion can usually be captured syntactically by a set of rule permutations. Very generally, proofnets can be defined as combinatorial objects which provide canonical representatives of equivalence classes of proofs. In particular, the existence of proof nets for a logic provides a solution to the equivalence problem of this logic. In certain fragments of linear logic, it is possible to give a notion of proofnet with good computational properties, making it a suitable representation of proofs for studying the cut-elimination procedure, among other things. It has recently been proved that there cannot be such a notion of proofnets for the multiplicative (with units) fragment of linear logic, due to the equivalence problem for this logic being Pspace-complete. We will investigate the multiplicative-additive (without unit) fragment of linear logic and see it is closely related to binary decision trees: we can build a representation of proofs based on binary decision trees, reducing proof equivalence to decision tree equivalence. We will see as a consequence that the proof equivalence problem multiplicative-additive linear logic is Logspace-complete.

1 0

Kusatsu_Seminar_2017
by Naosuke MATSUDA 29 Jan '17

29 Jan '17

みなさま神奈川大学の松田と申します．毎年草津セミナーハウスで開催されている，ラムダ計算と論理の早春セミナーを，今年も開催することになりましたので連絡させていただきます．日程：2017年3月16日-3月20日場所：国立大学草津セミナーハウス詳細等は， http://www.geocities.jp/naosuke_not_good/event/lls_spring_2017.html にあります．研究打ち合わせ・学生の発表練習の場など，様々な用途でお使いいただければと思います．質問等ございましたら，松田（神奈川大学）までお気軽にお問い合わせください． -- Naosuke Matsuda, Dept. of Information Sciences Kanagawa University 2946, Tsuchiya, Hiratsuka-shi, Kanagawa, 259-1293, JAPAN matsuda.naosuke(a)gmail.com -- ------------------------------ Naosuke Matsuda, Dept. of Information Sciences Kanagawa University Tsuchiya 2946, Hiratsuka-shi, Kanagawa 259-1293, Japan

1 0

TABLEAUX 2017, Brasilia (Brazil), 25-28 Sep 2017
by Katsuhiko Sano 24 Jan '17

24 Jan '17

Apologies for multiple postings. ------------------------------------------------------------------------------------------- SECOND CALL FOR PAPERS TABLEAUX 2017 26th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods University of Brasilia, Brazil September 25-28, 2017 Submission Deadline: 25 Apr 2017 http://tableaux2017.cic.unb.br/ GENERAL INFORMATION TABLEAUX is the main international conference at which research on all aspects, theoretical foundations, implementation techniques, systems development and applications, of the mechanization of tableau-based reasoning and related methods is presented. As the first TABLEAUX workshop was held in Lautenbach in 1992, this year's conference will include special events celebrating 25 years of TABLEAUX. The conference will be held in Brasilia from 25-28 September 2017. It will be co-located with both the 11th International Symposium on Frontiers of Combining Systems (FroCoS 2017) and the 8th International Conference on Interactive Theorem Proving (ITP 2017). TOPICS Tableau methods offer a convenient and flexible set of tools for automated reasoning in classical logic, extensions of classical logic, and a large number of non-classical logics. For large groups of logics, tableau methods can be generated automatically. Areas of application include verification of software and computer systems, deductive databases, knowledge representation and its required inference engines, teaching, and system diagnosis. Topics of interest include but are not limited to: * tableau methods for classical and non-classical logics (including first-order, higher-order, modal, temporal, description, hybrid, intuitionistic, substructural, relevance, non-monotonic logics) and their proof-theoretic foundations; * related methods (SMT, model elimination, model checking, connection methods, resolution, BDDs, translation approaches); * sequent calculi and natural deduction calculi for classical and non-classical logics, as tools for proof search and proof representation; * flexible, easily extendable, light weight methods for theorem proving; * novel types of calculi for theorem proving and verification in classical and non-classical logics; * systems, tools, implementations, empirical evaluations and applications (provers, logical frameworks, model checkers, ...); * implementation techniques (data structures, efficient algorithms, performance measurement, extensibility, ...); * extensions of tableau procedures with conflict-driven learning, generation of proofs; compact (or humanly readable) representation of proofs; * decision procedures, theoretically optimal procedures; * applications of automated deduction to mathematics, software development, verification, deductive and temporal databases, knowledge representation, ontologies, fault diagnosis or teaching. We also welcome papers describing applications of tableau procedures to real world examples. Such papers should be tailored to the tableau community and should focus on the role of reasoning, and logical aspects of the solution. CELEBRATING 25 YEARS To celebrate 25 years TABLEAUX the conference will include a special session of invited talks by: Reiner Haehnle Technische Universitaet Darmstadt, Germany Wolfgang Bibel Technische Universitaet Darmstadt, Germany INVITED SPEAKERS: Carlos Areces FaMAF - Universidad Nacional de Cordoba, Argentina Katalin Bimbo University of Alberta, Canada (joint with FroCoS and ITP) Jasmin Blanchette Inria and LORIA, Nancy, France (joint with FroCoS and ITP) Cesary Kaliszyk Universitaet Innsbruck, Austria (joint with FroCoS and ITP) WORKSHOPS AND TUTORIALS There will be a three-day programme of four workshops and four tutorials from 23-25 September. Workshops: 12th Logical and Semantic Frameworks with Applications (LSFA 2017) Sandra Alves, Renata Wassermann, Flavio L. C. de Moura 23 and 24 September 2017 Proof eXchange for Theorem Proving (PxTP) Catherine Dubois, Bruno Woltzenlogel Paleo 23 and 24 September 2017 EPS - Encyclopedia of Proof Systems Giselle Reis, Bruno Woltzenlogel Paleo 24 and 25 September 2017 DaLi - Dynamic Logic: new trends and applications Mario Benevides, Alexandre Madeira 24 September 2017 Tutorials: General methods in proof theory for modal and substructural logics Bjoern Lellmann, Revantha Ramanayake 23 September 2017 From proof systems to complexity bounds Anupam Das 24 September 2017 Proof Compressions and the conjecture NP =3D PSPACE Lew Gordeev, Edward Hermann Haeusler 25 September 2017 PVS for Computer Scientists Cesar Munoz, Mauricio Ayala-Rincon, Mariano Moscato 25 September 2017 Details will be published in separate calls and on the conference website. PUBLICATION DETAILS The conference proceedings will be published in the Springer LNAI/LNCS series, as in previous editions. SUBMISSIONS Submissions are invited in two categories: A Research papers, which describe original theoretical research, original algorithms, or applications, with length up to 15 pages. B System descriptions, with length up to 9 pages. Submissions will be reviewed by the PC, possibly with the help of external reviewers, taking into account readability, relevance and originality. For category A, theoretical results and algorithms must be original, and not submitted for publication elsewhere. Submissions will be reviewed taking into account correctness, theoretical elegance, and possible implementability. For category B submissions, a working implementation must be accessible via the internet, which includes sources. The aim of a system description is to make the system available in such a way that users can use it, understand it, and build on it. Accepted papers in both categories will be published in the conference proceedings. Papers must be edited in LaTeX using the llncs style and must be submitted electronically as PDF files via the EasyChair system: https://easychair.org/conferences/?conf=3Dtableaux2017. For all accepted papers at least one author is required to attend the conference and present the paper. A paper title and a short abstract of about 100 words must be submitted before the paper submission deadline. Further information about paper submissions will be made available at the conference website. Be aware that neither plagiarism, nor self-plagiarism, nor duplicate publication is acceptable. Formatting instructions and the LNCS style files can be obtained via http://www.springer.com/br/computer-science/lncs/conference-proceedings-gui= delines BEST PAPER AWARD The TABLEAUX 2017 Best Paper Award will be presented to the best submission nominated and chosen by the Program Committee among the accepted papers. The eligibility criteria will place emphasis on the originality and significance of the contribution, but readability and the overall technical quality, including correctness and completeness of results, will also be considered. The TABLEAUX Best Paper Award was established in 2015 and is a permanent initiative of TABLEAUX. IMPORTANT DATES 18 Apr 2017 Abstract submission 25 Apr 2017 Paper submission 8 Jun 2017 Notification of paper decisions 3 Jul 2017 Camera-ready papers due 23-25 Sep 2017 Workshops & Tutorials 25-28 Sep 2017 TABLEAUX Conference PROGRAM COMMITTEE Peter Baumgartner National ICT Australia, Canberra Maria Paola Bonacina Universita degli Studi di Verona Laura Bozzelli Universidad Politecnica de Madrid Torben Brauener Roskilde University Serenella Cerrito Ibisc, Universite d'Evry Val d'Essonne Agata Ciabattoni Technische Universitaet Wien Clare Dixon University of Liverpool Pascal Fontaine LORIA, INRIA, Universite de Lorraine Didier Galmiche LORIA, Universite de Lorraine Martin Giese Universitetet i Oslo Laura Giordano DISIT, Universita del Piemonte Orientale Rajeev Gore The Australian National University Volker Haarslev Concordia University George Metcalfe Universitaet Bern Angelo Montanari Universita degli Studi di Udine Barbara Morawska Technische Universitaet Dresden Boris Motik University of Oxford Leonardo de Moura Microsoft Research Neil Murray SUNY at Albany Claudia Nalon Universidade de Brasilia Linh Anh Nguyen Uniwersytet Warszawski Hans de Nivelle Uniwersytet Wroclawski Nicola Olivetti LSIS, Aix-Marseille Universite Jens Otten Universitetet i Oslo Valeria de Paiva Nuance Communications Nicolas Peltier Centre National de la Recherche Scientifique, Laboratoire d'Informatique de Grenoble Elaine Pimentel Universidade Federal do Rio Grande do Norte Giselle Reis Carnegie Mellon University-Qatar Philipp Ruemmer Uppsala Universitet Katsuhiko Sano Hokkaido University Renate Schmidt The University of Manchester Cesare Tinelli The University of Iowa Alwen Tiu Nanyang Technological University David Toman University of Waterloo Josef Urban Ceske vysoke uceni technicke v Praze LOCAL CONFERENCE ORGANIZATION COMMITTEE Claudia Nalon, Universidade de Brasilia, Brazil Daniele Nantes Sobrinho, Universidade de Brasilia, Brazil Elaine Pimentel, Universidade Federal do Rio Grande do Norte, Brazil Joao Marcos, Universidade Federal do Rio Grande do Norte, Brazil CONFERENCE CHAIR Claudia Nalon, University of Brasilia, Brazil PC CHAIRS Claudia Nalon, University of Brasilia, Brazil Renate Schmidt, The University of Manchester, UK

1 0

第19回プログラミングおよびプログラミング言語ワークショップ（PPL2017）参加募集
by Isao Sasano 24 Jan '17

24 Jan '17

皆様芝浦工業大学の篠埜です。第19回プログラミングおよびプログラミング言語ワークショップ（PPL2017）のご案内です。以下のweb pageで参加登録を開始いたしました。参加登録の締切は 2月21日（火）です。 https://ppl2017.ipl-e.ai.kyutech.ac.jp/registration/ カテゴリ2（国外既発表論文）およびカテゴリ4（サーベイ・チュートリアル発表）の発表申込締切も近づいております。カテゴリ2 発表申込締切: 2017年1月25日(水) 17:00 (JST) カテゴリ4 発表申込締切: 2017年1月25日(水) 17:00 (JST) 是非、発表申込、参加登録をお願いいたします。篠埜　功 -- Isao Sasano <sasano(a)sic.shibaura-it.ac.jp>

1 0

ITP 2017 - 2nd Call for Papers
by Nao Hirokawa 24 Jan '17

24 Jan '17

皆様９月にブラジリアで開催されます、対話的定理証明に関する国際会議 ITP 2017 の論文募集案内をお送り致します。ぜひ投稿をご検討下さい。廣川 (JAIST) -------------------------------------------------------------------- SECOND CALL FOR PAPERS ITP 2017 8th International Conference on Interactive Theorem Proving Brasilia, Brazil September 26-29, 2017 http://itp2017.cic.unb.br SUBMISSION DEADLINES * April 3, 2017 (abstracts) * April 10, 2017 (full papers) GENERAL INFORMATION The ITP conference series is concerned with all topics related to interactive theorem proving, ranging from theoretical foundations to implementation aspects and applications in program verification, security, and formalization of mathematics. ITP is the evolution of the TPHOLs conference series to the broad field of interactive theorem proving. TPHOLs meetings took place every year from 1988 until 2009. The eighth ITP conference, ITP 2017, will be held at Universidade de Brasilia, September 26-29, 2017. SCOPE OF CONFERENCE ITP welcomes submissions describing original research on all aspects of interactive theorem proving and its applications. Suggested topics include but are not limited to the following: * formal aspects of hardware and software * formalizations of mathematics * improvements in theorem prover technology * user interfaces for interactive theorem provers * formalizations of computational models * verification of security algorithms * use of theorem provers in education * industrial applications of interactive theorem provers * concise and elegant worked examples of formalizations (proof pearls) PUBLICATION DETAILS The proceedings of the symposium will be published in the Springer's LNCS series. PAPER SUBMISSIONS All submissions must be original, unpublished, and not submitted concurrently for publication elsewhere. Furthermore, when appropriate, submissions are expected to be accompanied by verifiable evidence of a suitable implementation, such as the source files of a formalization for the proof assistant used. Submissions should be no more than 16 pages in length and are to be submitted in PDF via EasyChair at the following address: https://easychair.org/conferences/?conf=itp2017 Submissions must conform to the LNCS style in LaTeX. Authors of accepted papers are expected to present their paper at the conference and will be required to a sign copyright release form. In addition to regular papers, described above, there will be a rough diamond section. Rough diamond submissions are limited to 6 pages and may consist of an extended abstract. They will be refereed and be expected to present innovative and promising ideas, possibly in an early form and without supporting evidence. Accepted diamonds will be published in the main proceedings and will be presented as short talks. After the conference the authors of selected papers will be invited to submit revised papers for a special issue of the Journal of Automated Reasoning. IMPORTANT DATES Abstract submission deadline: April 3, 2017 Full paper submission deadline: April 10, 2017 Author notification: June 2, 2017 Camera-ready papers: June 30, 2017 Workshops & Tutorials: September 23-25, 2017 Conference: September 26-29, 2017 INVITED SPEAKERS Moa Johansson, Chalmers University of Technology, Sweden Leonardo de Moura, Microsoft Research Katalin Bimbo, University of Alberta, Canada (joint with TABLEAUX and FroCos) Jasmin Blanchette Inria and LORIA, Nancy, France (joint with TABLEAUX and FroCos) Cesary Kaliszyk Universitaet Innsbruck, Austria (joint with TABLEAUX and FroCos) WORKSHOPS AND TUTORIALS There will be a three-day programme of four workshops and four tutorials from 23-25 September. Workshops: 12th Logical and Semantic Frameworks with Applications (LSFA 2017) Sandra Alves, Renata Wassermann, Flavio L. C. de Moura 23 and 24 September 2017 Proof eXchange for Theorem Proving (PxTP) Catherine Dubois, Bruno Woltzenlogel Paleo 23 and 24 September 2017 EPS - Encyclopedia of Proof Systems Giselle Reis, Bruno Woltzenlogel Paleo 24 and 25 September 2017 DaLi - Dynamic Logic: new trends and applications Mario Benevides, Alexandre Madeira 24 September 2017 Tutorials: General methods in proof theory for modal and substructural logics Bjoern Lellmann, Revantha Ramanayake 23 September 2017 From proof systems to complexity bounds Anupam Das 24 September 2017 Proof Compressions and the conjecture NP =3D PSPACE Lew Gordeev, Edward Hermann Haeusler 25 September 2017 PVS for Computer Scientists Cesar Munoz, Mauricio Ayala-Rincon, Mariano Moscato 25 September 2017 Details will be published in separate calls and on the conference website. PROGRAM COMMITTEE CHAIRS Mauricio Ayala-Rincon, U. Brasilia Cesar Munoz, NASA PROGRAM COMMITTEE CHAIRS Maria Alpuente, T.U. Valencia Vander Alves, U. Brasilia June Andronick, Data61, CSIRO, UNSW Jeremy Avigad, Carnegie Mellon U. Sylvie Boldo, INRIA LRI Ana Bove, Chalmers & Gothenburg U. Adam Chlipala, MIT Gilles Dowek, INRIA, ENS Cachan Aaron Dutle, NASA Amy Felty, U. Ottawa Marcelo Frias, I.T. Buenos Aires Ruben Gamboa, U. Wyoming Herman Geuvers, Radboud U. Elsa Gunter, U. Illinois U.C. John Harrison, Intel Corporation Nao Hirokawa, JAIST Matt Kaufmann, U. Texas Austin Mark Lawford, McMaster U. Andreas Lochbihler, ETH Zurich Assia Mahboubi, INRIA Panagiotis Manolios, Northeastern U. Gopalan Nadathur, U. Minnesota Keiko Nakata, SAP Potsdam Adam Naumowicz, U. Bialystok Tobias Nipkow, T.U. Munich Scott Owens, U. Kent Sam Owre, SRI Lawrence Paulson, U. Cambridge Leila Ribeiro, U.F. Rio Grande do Sul Claudio Sacerdoti Coen, U. Bologna Augusto Sampaio, U.F. Pernambuco Monika Seisenberger, Swansea U. Christian Sternagel, U. Innsbruck Sofiene Tahar, Concordia U. Christian Urban, King's College London Josef Urban, Czech T.U. Prague CONTACT INFORMATION Cesar Munoz Mauricio Ayala-Rincon itp2017(a)easychair.org http://itp2017.cic.unb.br

1 0

セミナー案内
by KASHIMA Ryo 21 Jan '17

21 Jan '17

数理論理学セミナーのお知らせ日時：1月20日(金) 17:00から場所：東京工業大学大岡山西８号館Ｗ棟10階 W1008 話者：竹内泉（産総研）題目：数学と変数概要：　これは数学の言語哲学の研究である。変数の使用は数学の言語に特有であるので変数の使用を分析することによって数学の本質に迫ることを目標とする。数学の変数の使用には幾つもの種類がある。本発表では、以下のような分類に沿って説明する。 (1)恒等式の文字 (2)方程式の未知数 (3)多項式論の変数と命題変数 (4)座標変数と確率変数 (5)独立変数と従属変数 ------ 本セミナーは定期的に東工大で開催しているものです。初めて参加を希望される方はご一報ください。 ----- 鹿島亮東京工業大学情報理工学院数理・計算科学系 kashima(a)is.titech.ac.jp

1 1

DICE-FOPARA 2017: Call for Papers
by Nao Hirokawa 18 Jan '17

18 Jan '17

皆様 ETAPS 2017 に併設されます、暗黙計算量 (ICC) とリソース解析に関する合同ワークショップ DICE-FOPARA 2017 の論文募集の案内をお送り致します。ぜひ投稿をご検討下さい。廣川 (JAIST) ------------------------------------------------------------------------------------------- 8th Workshop on Developments in Implicit Computational complExity and 5th Workshop on Foundational and Practical Aspects of Resource Analysis (DICE-FOPARA 2017) Affiliated with ETAPS 2017 April 22 - 23, 2017, Uppsala, Sweden http://cbr.uibk.ac.at/events/dice-fopara ------------------------------------------------------------------------------------------- OBJECTIVES The first joint international workshop on Developments in Implicit Computational complExity (DICE) and FOundational and Practical Aspects of Resource Analysis (FOPARA) will be held in Uppsala, Sweden, from April 22-23, 2017 as part of ETAPS. The DICE workshop explores the area of Implicit Computational Complexity (ICC), which grew out from several proposals to use logic and formal methods to provide languages for complexity-bounded computation (e.g. Ptime, Logspace computation). It aims at studying the computational complexity of programs without referring to external measuring conditions or a particular machine model, but only by considering language restrictions or logical/computational principles entailing complexity properties. The FOPARA workshop serves as a forum for presenting original research results that are relevant to the analysis of resource (e.g. time, space, energy) consumption by computer programs. The workshop aims to bring together the researchers that work on foundational issues with the researchers that focus more on practical results. Therefore, both theoretical and practical contributions are encouraged. We also encourage papers that combine theory and practice. Given the complementarity and the synergy between these two communities, and following the successful experience of co-location of DICE-FOPARA 2015 in London at ETAPS 2015, we will hold the 8th Workshop on DICE and the 5th Workshop on FOPARA together at ETAPS 2017. TOPICS he joint international DICE-FOPARA workshop serves as a forum for presenting original and established research results that are relevant to the implicit computational complexity theory and to the analysis of resource (e.g. time, space, energy) consumption by computer programs. The workshop aims to bring together the researchers that work on foundational issues with the researchers that focus more on practical results. Therefore, both theoretical and practical contributions are encouraged, as well as papers that combine theory and practice. Areas of interest to the workshop include, but are not limited to, the following: * type systems for controlling/inferring/checking complexity * logical and machine-independent characterisations of complexity classes * logics closely related to complexity classes * linear logic * semantics of complexity-bounded computation * rewriting and termination orderings * interpretation-based methods for implicit complexity * programming languages for complexity-bounded computation * theoretical foundations of program complexity analysis * application of implicit complexity to security * resource static analysis for embedded or/and critical systems; * semantic methods to analyse resources, including quasi-interpretations; * practical applications of resource analysis; * resource analysis by term and graph rewriting. SUBMISSIONS We ask for submission of *regular papers* describing original work (10-15 pages) or *extended abstracts* (2-6 pages) presenting already published work or work in progress. With respect to regular papers, submissions will be in particular verified for originality and novelty and the manuscript must not have been published, nor is presently submitted, elsewhere. With respect of submissions of extended abstracts already published manuscripts are acceptable, but have to be within the scope of the workshop and potentially give rise to lively discussions during the meeting. After the workshop we plan to edit a special issue of DICE-FOPARA 2017 in a renown journal in conjunction with the 7th Workshop on Developments in Implicit Computational complExity (DICE 2016). Regular papers must be prepared using the LaTeX EPTCS class (see http://eptcs.org/). Accepted regular papers will appear in an EPTCS volume (application pending). Papers should be submitted electronically via the submission page: https://easychair.org/conferences/?conf=dicefopara2017 IMPORTANT DATES Paper submission February 19, 2017 Notification March 19, 2017 Final versions due March 26, 2017 Workshop date April 22-23, 2017 CONFERENCE VENUE The workshop will be held as a satellite workshop of European Joint Conferences on Theory and Practice of Software 2017 (ETAPS 2017) which takes place in Uppsala, Sweden. PROGRAM COMMITTEE Beniamino Accattoli (Paris) Guillaume Bonfante (Nancy, co-chair) Marko van Eekelen (Nijmegen) Marco Gaboardi (Buffalo) Dan Ghica (Birmingham) Clemens Grelck (Amsterdam) Charles Grellois (Bologna) Nao Hirokawa (JAIST) Jan Hoffmann (CMU) Thomas Jensen (Rennes) Björn Lisper (Mälardalen) Hans-Wolfgang Loidl (Edinburgh) Georg Moser (Innsbruck, co-chair) Kazushige Terui (Kyoto) Simon Wegener (Saarbrücken) Florian Zuleger (Vienna)

1 0

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

17 Jan '17

皆様芝浦工業大学の篠埜です。第19回プログラミングおよびプログラミング言語ワークショップ（PPL2017）のご案内です。カテゴリ2（国外既発表論文）およびカテゴリ4（サーベイ・チュートリアル発表）の発表申込締切が近づいてまいりました。カテゴリ2 発表申込締切: 2017年1月25日(水) 17:00 (JST) カテゴリ4 発表申込締切: 2017年1月25日(水) 17:00 (JST) 是非、発表申込をお願いいたします。 ====================================================================== 第19回プログラミングおよびプログラミング言語ワークショップ (PPL2017) https://ppl2017.ipl-e.ai.kyutech.ac.jp/ 論文募集/発表募集主催: 日本ソフトウェア科学会プログラミング論研究会日程: 2017年3月8日(水)～3月10日(金) 会場: 山梨県笛吹市石和温泉「華やぎの章慶山」 PPL2017は，プログラミングとプログラミング言語に関連する幅広い分野の研究者・技術者・学生が一堂に会し，最新の研究成果の発表や，新たな研究課題の提案・討論・アイディア交換を行うことを目的とした，合宿形式の研究集会です．プログラミング方法論，プログラミング言語の理論・設計・実装などに関する研究発表を，カテゴリ別に幅広く募集します．カテゴリ1: 国内外で未発表の論文の発表カテゴリ2: 国際会議・学術雑誌等で既発表であるが，国内では未発表の研究の紹介カテゴリ3: ポスター・デモ発表(既発表・未発表の別を問いません) カテゴリ4: サーベイ・チュートリアル発表(既発表・未発表の別を問いません) カテゴリ1の採択論文の中から，特に独創的なアイディアや顕著な成果を含むものに対して論文賞を授与する予定です．また全論文発表と全ポスター・デモのなかから，聴衆の投票によりそれぞれ，最も優秀な論文プレゼンテーションには発表賞(一般の部，学生の部，既受賞者は除く)，最も優秀なポスター・デモにはポスター賞を授与する予定です．カテゴリ1 (国内外未発表論文) ---------------------------- 完成した理論やシステムの研究発表のみならず，萌芽的なアイディアや問題点の提示等も歓迎します．発展途上の研究内容も積極的に採録する方針です(ただし，PPLでの発表として相応しくないと判断される場合は，この限りではありません)．また，カテゴリ1で発表された研究については，会場での討議や査読コメントをもとにその完成度を高め，将来の学術雑誌・国際会議等での業績に結び付けることを奨励しています．そのため，予稿集の配布は参加者のみへの限定的なものとします．カテゴリ1で発表された研究のうち，PPL2017プログラム委員会により優れていると認められたものは， PPL2017終了後(2017年4月下旬予定)，「コンピュータソフトウェア」誌のPPL2017推薦論文としての投稿が可能です．推薦論文は，PPLプログラム委員が引き続き査読を行うことによる，迅速な査読プロセスを特長としています．カテゴリ2 (国外既発表論文) -------------------------- 査読付の国際会議または学術雑誌等で既発表であるが国内では未発表である研究を紹介する場です．採録決定済みの研究も含みます．PPLへの関連をもとに採否を判定いたしますが，申し込み多数の場合はプログラム委員会で選考致します．カテゴリ3 (ポスター・デモ発表) ------------------------------ 2時間程度のセッション内でのポスター発表またはデモ発表です．既発表・未発表の別を問いません．PPLへの関連をもとに採否を判定いたしますが，申し込み多数の場合はプログラム委員会で選考致します．会場の状況により，ポスターの常設展示を可能とします．ショートプレゼンテーションは行いません．カテゴリ4 (サーベイ・チュートリアル発表) ---------------------------------------- 研究動向の紹介(発表者の研究も含む) や分野間の相互理解と参加者の知識の底上げとなる発表を募集します．既発表・未発表の別を問いません．発表後，発表スライドをPPL2017ウェブページ上にて公開して頂く予定です．PPLへの関連，著者の研究発表実績，トピックや切り口の興味深さをもとに，プログラム委員会で選考致します．招待講演 -------- 神谷年洋（島根大学教授）原田康徳（合同会社デジタルポケット代表）以上お二方の招待講演を予定しております．なお，PPL2017の終了は昼頃〜夕刻を予定しています． ====================================================================== 投稿・発表申込要領すべてのカテゴリの投稿・発表について，次のURLから申し込んでください． https://easychair.org/conferences/?conf=ppl2017 申込にあたってはEasyChairのアカウントが必要です．4つのカテゴリそれぞれに対する申込要領の詳細は以下の通りです．申し込み時にEasychairで入力する氏名，所属の情報はプログラム作成に用いますので，参加者の便宜を考慮し，日本語が良いと考えられる場合には日本語での入力をお願い致します．最新の情報は上記ウェブページでご確認ください．カテゴリ1 (国内外未発表論文) --------------------------- 投稿手続きは2段階です．発表申込を行った上で論文提出を行ってください．発表申込締切: 2016年12月21日(水) 17:00 (JST) 著者名，所属，論文タイトル，論文概要(日本語300〜400字程度もしくは英語200 words 程度)，キーワード(3つ以上)を提出してください．論文提出締切: 2017年1月11日(水) 17:00 (JST) 10ページ程度(最大15ページ，参考文献を含む)の論文(日本語もしくは英語，PDF形式．PPL2017ウェブページにて指定のスタイルファイルを利用のこと)を提出してください．最大ページ数を超える付録は投稿版に入れて構いませんが，最終原稿においては削除してもらいます．著者のweb page等においてソースコードや実験データなどを載せて引用しても構いません．最大ページ数を超える付録やweb page等の情報については査読において考慮されない場合もあります．採否通知：2017年2月3日(金) 最終原稿締切: 2017年2月16日(木) 採録された論文の最終原稿の提出方法は，採否通知にてお知らせいたします． (注) 採録された論文等著作物は，日本ソフトウェア科学会著作権規定にもとづいて利用されますので，予めご確認ください． (注) 投稿論文と類似の論文を，他の会議(予稿集を出版するもの)・論文誌などに同時投稿する場合は，査読の有無に関わらず，その旨を発表申込および論文提出の際に明記してください．PPLでは同時投稿の事実のみをもって論文を不採録とすることはありませんが，採否の決定に利用する場合があります(他の会議との重複を避けるため，発表内容についての条件付採録とすることもあります)．カテゴリ2 (国外既発表論文) ------------------------- 発表申込時に採録が決定している国際会議および国際学術雑誌等の発表論文が対象です．理論系だけではなく実装系の論文の投稿も歓迎いたします．発表申込締切: 2017年1月25日(水) 17:00 (JST) 原論文(ページ数不問，PDF形式)と論文概要(テキスト形式)を，著者名，所属，論文タイトル，キーワード(3つ以上)と併せて提出してください．論文概要にて，原論文の出典(発表会議名，掲載済／予定の別等を含む)についても明記してください．採否通知：2017年2月6日(月) カテゴリ3 (ポスター・デモ発表) ----------------------------- ポスター発表またはデモ発表(あるいは両方)を募集いたします．発表申込締切: 2017年2月8日(水) 17:00 (JST) 希望する発表形態を明記して著者名，所属，発表タイトル，発表概要 (200〜300字程度)，キーワード(3つ以上)を提出してください．発表形態については発表タイトル(Title欄)の最後の部分に括弧（）に入れて，「ポスター」「デモ」「ポスター・デモ」のいずれかを記載してください．採否通知：2017年2月15日(水) カテゴリ4 (サーベイ・チュートリアル発表) --------------------------------------- 発表申込締切: 2017年1月25日(水) 17:00 (JST) 著者名，所属，発表タイトル，キーワード(3つ以上)，発表概要(3ページ以内，PDF形式．目的，カバーする話題，想定する聴衆，必要な知識の記述を含むもの)を提出してください．採否通知：2017年2月6日(月) ====================================================================== 問い合わせ先 ppl2017-oc(a)ipl-e.ai.kyutech.ac.xn--jp()-753c9gpa1b92cqcsg7jrh5d1ix122cxi0h ppl2017-pc-chairs(a)ipl-e.ai.kyutech.ac.xn--jp(/)-m53d8hra6b05cmntd6e6b1719ok76b ====================================================================== プログラム委員会青谷知幸 (東京工業大学) 浅田和之 (東京大学) Reynald Affeldt (産業技術総合研究所) 稲葉一浩 (Google) 上野雄大 (東北大学) 菊池健太郎 (東北大学) 小宮常康 (電気通信大学) 篠埜功 (芝浦工業大学) 佐藤亮介 (東京大学) 首藤一幸 (東京工業大学) 末永幸平 (京都大学) 宋剛秀 (神戸大学) 千葉滋 (東京大学) 土屋達弘 (大阪大学) 中野圭介 (電気通信大学) 鍋島英知 (山梨大学) 番原睦則 (神戸大学) 前田敦司 (筑波大学) 松田一孝 (東北大学) 森畑明昌 (東京大学) 八杉昌宏 (九州工業大学) 組織委員会江本健斗 (九州工業大学) [組織委員長] 平石拓 (京都大学) 佐藤重幸 (高知工科大学) 海野広志 (筑波大学) 対馬かなえ (国立情報学研究所) 塚田武志 (東京大学) 篠埜功 (芝浦工業大学) [プログラム共同委員長] 番原睦則 (神戸大学) [プログラム共同委員長] ====================================================================== 篠埜　功 -- Isao Sasano <sasano(a)sic.shibaura-it.ac.jp>

1 0

FSCD 2017: CFP
by Takahito Aoto 10 Jan '17

10 Jan '17

皆様，国際会議FSCD 2017の論文募集をご案内致します． RTAとTLCAを融合・発展させた国際会議(2回目)です．ぜひ投稿をご検討いただければ幸いです． --- 青戸等人(新潟大学) ============================================================== CALL FOR PAPERS Second International Conference on Formal Structures for Computation and Deduction (FSCD'17) 3 -- 6 September 2017, Oxford, UK (co-located with ICFP 2017) http://www.cs.ox.ac.uk/conferences/fscd2017/ FSCD (http://fscdconference.org/) covers all aspects of formal structures for computation and deduction from theoretical foundations to applications. Building on two communities, RTA (Rewriting Techniques and Applications) and TLCA (Typed Lambda Calculi and Applications), FSCD embraces their core topics and broadens their scope to closely related areas in logics, proof theory and new emerging models of computation such as quantum computing or homotopy type theory. ========================================================================== IMPORTANT DATES All deadlines are midnight anywhere-on-earth (AoE) and are firm; late submissions will not be considered. Abstract Deadline: 7 April 2017 Submission Deadline: 14 April 2017 Rebuttal: 29--31 May 2017 Notification: 14 June 2017 Camera-Ready: 7 July 2017 ========================================================================== Suggested, but not exclusive, list of topics for submission are: 1. Calculi: Lambda calculus * Concurrent calculi * Logics * Rewriting systems * Proof theory * Type theory and logical frameworks 2. Methods in Computation and Deduction: Type systems * Induction and coinduction * Matching, unification, completion, and orderings * Strategies * Tree automata * Model checking * Proof search and theorem proving * Constraint solving and decision procedures 3. Semantics: Operational semantics * Abstract machines * Game Semantics * Domain theory and categorical models * Quantitative models 4. Algorithmic Analysis and Transformations of Formal Systems: Type Inference and type checking * Abstract Interpretation * Complexity analysis and implicit computational complexity * Checking termination, confluence, derivational complexity and related properties * Symbolic computation 5. Tools and Applications: Programming and proof environments * Verification tools * Libraries for proof assistants and interactive theorem provers * Case studies in proof assistants and interactive theorem provers * Certification PUBLICATION The proceedings will be published as an electronic volume in the Leibniz International Proceedings in Informatics (LIPIcs) of Schloss Dagstuhl. All LIPIcs proceedings are open access. SUBMISSION GUIDELINES Submissions can be made in two categories. Regular research papers are limited to 15 pages and must present original research which is unpublished and not submitted elsewhere. System descriptions are limited to 10 pages and must describe a working system which has not been published or submitted elsewhere. Submissions must be formatted using the LIPIcs style files and submitted via EasyChair. Complete instructions on submitting a paper can be found on the conference web site. SPECIAL ISSUES Full versions of several accepted papers, to be selected by the program committee, will be invited for submission to a special issue of Logical Methods in Computer Science. BEST PAPER AWARD BY JUNIOR RESEARCHERS The program committee will consider declaring this award to a paper in which all authors are junior researchers: a junior researcher is a person who is either a student or whose PhD award date is less than three years from the first day of the meeting. PROGRAM COMMITTEE CHAIR Dale Miller, Inria Saclay & LIX <fscd17(a)easychair.org> PROGRAM COMMITTEE Andreas Abel, Gothenburg Univ. Elvira Albert, Complutense Madrid Maria Alpuente, TU Valencia Takahito Aoto, Niigata Univ. Zena Ariola, Univ. Oregon Federico Aschieri, TU Wien Stefano Berardi, Univ. Turin Lars Birkedal, Aarhus Univ. Filippo Bonchi, CNRS, ENS Lyon Pierre Clairambault, CNRS, ENS Lyon Ugo Dal Lago, Univ. Bologna Herman Geuvers, Radboud Univ. Silvia Ghilezan, Univ. Novi Sad Juergen Giesl, RWTH Aachen Hugo Herbelin, Inria Paris Jan Hoffmann, Carnegie Mellon Deepak Kapur, Univ. New Mexico Paul Blain Levy, Univ. Birmingham Paulo Oliva, QMUL, London Vincent van Oostrom, Univ. Innsbruck Daniela Petrisan, LIAFA, Paris Femke van Raamsdonk, VU Univ. Amsterdam Grigore Rosu, Univ. Illinois Albert Rubio, UPC-BarcelonaTech Paula Severi, Univ. Leicester Bas Spitters, Aarhus Univ. Aaron Stump, Univ. Iowa Kazushige Terui, Kyoto Univ. Rene Thiemann, Univ. Innsbruck Sophie Tison, Lille Univ. CONFERENCE CHAIR Sam Staton, Univ. of Oxford WORKSHOP CHAIR Jamie Vicary, Univ. of Oxford PUBLICITY CHAIR Sandra Alves, Univ. of Porto FSCD STEERING COMMITTEE T. Altenkirch (Univ. Nottingham), S. Alves (Univ. Porto), G. Dowek, (Inria), S. Escobar (Univ. Politecnica de Valencia), M. Fernandez (King's College London), H. Herbelin (Inria), D. Kesner (Univ. Paris), N. Kobayashi (Univ. Tokyo), L. Ong (Chair, Univ. Oxford), B. Pientka (McGill Univ.), R. Thiemann (Univ. Innsbruck).

1 0

第４回山陰基礎論・解析学研究集会の御案内
by horihata 04 Jan '17

04 Jan '17

Logic-ml 各位米子高専の堀畑です。今週末、８日（日）と９日（月）に米子で件名の研究会を開催いたします。参加自由ですので、お気軽に御参加頂ければ幸いです。懇親会もありますので、研究会に参加頂ける方は堀畑までご連絡ください。詳細はホームページをご参照ください： https://sites.google.com/site/yonagonctmath/home/slas2017 参加者２６名。発表者は以下１２名（敬称略）。阿部敏一　（茨城大学）池上大祐　（東京電機大）石原哉　　（ＪＡＩＳＴ）薄葉季路　（早稲田大学）沖坂祥平　（東北大学）熊本真一郎（神戸大学）鈴木信行　（静岡大学）冨樫瑠美　（長岡高専）根元多佳子（ＪＡＩＳＴ）藤原誠　（早稲田大学）三浦毅　（新潟大学）横山啓太　（ＪＡＩＳＴ）以上です。よろしくお願いします。堀畑佳宏 -- 米子工業高等専門学校教養教育科・数学 E-mail: horihata(a)yonago-k.ac.jp

1 0

Announcement 「論理と数学の哲学―論証の哲学に向けて」Workshop “Philosophy of logic and Mathematics
by Mitsuhiro Okada 19 Dec '16

19 Dec '16

次の共同ワークショップを企画しておりますので、ご案内させて頂きます。　　　　　　　　　　　　　　　　　　　　　　　　　慶応義塾大学岡田光弘 ************************************************************************** 「論理と数学の哲学―論証の哲学に向けて」日仏ワークショップ Workshop “Philosophy of logic and Mathematics – Towards Philosophy of Proofs (本会合情報　https://abelard.flet.keio.ac.jp/seminar/frjp17jan.html) *************************************************************************** 日時：2017年1月12日(木)-13日(金)、参加自由、事前登録なし。 Date: Jan 12th Thursday-13th Friday, 2017 場所：慶應義塾大学三田キャンパス南館地下4階ディスタンスラーニングルーム Place: Distance Learning Room (B4F), South Building, Mita Campus of Keio University (キャンパスマップ https://www.keio.ac.jp/en/maps/mita.html 13番の建物です。/ Building #13 on this map.) 論理と数学の哲学についての日仏ワークショップを案内させて頂きます。特に、証明(論証)の哲学に向けたテーマを議論する予定です。フランス側招待講演者：ピエール・ワーグナー Pierre Wagner (パリ第１大学哲学科兼パリ科学史・科学哲学研究所) マルコ・パンツァ Marco Panza (パリ第１大学哲学科兼パリ科学史・科学哲学研究所) アンドリュー・アラナ Andrew Arana (パリ第１大学哲学科兼パリ科学史・科学哲学研究所) アルベルト・ナイボ Alberto Naibo (パリ第１大学哲学科兼パリ科学史・科学哲学研究所) 日本側招待講演者：岡本賢吾 Kengo Okamoto (首都大学東京哲学分野) 喜田浩平 Kohei Kida (慶應義塾大学文学部仏文学専攻) 峯島宏次 Koji Mineshima (お茶の水女子大学シミュレーション科学教育研究センター) 藤原誠 Makoto Fujiwara (早稲田大学高等研究所) 他の講演者：秋吉亮太 Ryota Akiyoshi (早稲田大学高等研究所) 高橋優太 Yuta Takahashi (名古屋大学・日本学術振興会) 西牟田祐樹 Yuki Nishimuta (慶應義塾大学後期博士課程) 岡田光弘 Mitsuhiro Okada (慶應義塾大学文学部哲学専攻) その他。　）暫定版プログラム： (プログラムの最新情報は https://abelard.flet.keio.ac.jp/seminar/frjp17jan.html をご覧ください。 1月12日(木) 9:45 受付開始 10:00 開会挨拶岡田光弘秋吉亮太 Mitsuhiro Okada and Ryota Akiyoshi 10:05 Introduction：ワークショップ趣旨説明岡田光弘ピエール・ワーグナー Mitsuhiro Okada and Pierre Wagner 10:20 ピエール・ワーグナー Pierre Wagner　“The normative character of logic” 11:20 峯島宏次 Koji Mineshima “Diagrams, proofs, and natural reasoning with “most"” 12:00 昼食休憩 13:30 喜田浩平 Kohei Kida “Une approche argumentative du sens (An argumentative approach to meaning)” 14:30 マルコ・パンツァ Marco Panza “The logicality of Frege’s definition of real numbers” 15:30 小休憩 15:50 岡本賢吾 Kengo Okamoto “Mathematical Necessity and Possibility from Kant to Frege and Wittgenstein” 16:50 アンドリュー・アラナ Andrew Arana “ “Purity and content” - the purity constraint, in the case of arithmetical proofs” 17:50 小休憩 18:10-18:40 ディスカッション (Discussion with French Speakers) 1月13日(金) 9:45 受付開始 10:00 アルベルト・ナイボ Alberto Naibo “Harmony, Stability and Identity: An intensional account in proof-theoretic semantics” 11:00 藤原誠 Makoto Fujiwara “Reverse mathematics and uniform provability” 11:40 昼食休憩 13:10 秋吉亮太 Ryota Akiyoshi “On Brouwer’s argument of bar induction” 13:40 高橋優太 Yuta Takahashi “Phase Semantic Framework for Proof-Terms as Proof-Theoretic Semantics” 14:10 小休憩 14:30 西牟田祐樹岡田光弘 Yuki Nishimuta and Mitsuhiro Okada On introduction rules of generalized connectives with proof-nets and substructural logics 岡田光弘 Mitsuhiro Okada “Normativity, normality and normalizability of proofs” 15:30 小休息 15:40-16:20 Discussion with Invited Speakers. 共同オーガナイザー：秋吉亮太 (早稲田大学高等研究所) 岡田光弘 (慶應義塾大学文学部哲学専攻) 高橋優太 (名古屋大学・日本学術振興会) , , 共催：慶應義塾論理と感性のグロル研究センター,次世代研究推進プロジェクト, CNRS-フランス国立科学研究センター連絡先：東京都港区三田２－１５－４５、慶應義塾大学文学部岡田光弘研究室メール：logic(a)abelard.flet.keio.ac.jp ----------------------------------------------

1 0

Fwd: 松山 TGSA セミナーのお知らせ（１２月２６日）
by Hiroshi Fujita 19 Dec '16

19 Dec '16

Logic-MLの皆さま、今月26日開催の松山TGSAセミナーのお知らせを転送いたします。藤田博司（愛媛大学大学院理工学研究科） -------- Forwarded Message -------- Subject: 松山 TGSA セミナーのお知らせ（１２月２６日） Date: Sat, 17 Dec 2016 18:29:24 +0000 From: Dmitri SHAKHMATOV <dmitri.shakhmatov(a)dmitri.math.sci.ehime-u.ac.jp> To: fujita.hiroshi.mh(a)ehime-u.ac.jp CC: dmitri.shakhmatov(a)dmitri.math.sci.ehime-u.ac.jp 皆様、「Matsuyama Seminar on Topology, Geometry, Set Theory and their Applications」（松山TGSAセミナー）のお知らせです。 ***** 第27回のセミナー日時: 2016年12月26日（月） 16:45〜17:45 場所: 愛媛大学理学部2号館2階，大演習室 (201号室) 講演者: Franklin D. Tall (University of Toronto, Canada) 題目: Definable versions of Menger's conjecture 概要： A topological space is Menger if, given a countable sequence of open covers, there is a finite selection from each of them, so that the union of the selections is a cover. The Menger property lies strictly between sigma-compactness and Lindelofness. In 1925 Hurewicz conjectured that Menger was equivalent to sigma-compact in metrizable spaces. This was refuted by Chaber and Pol in 2002. However, for spaces which are in some sense ``definable", the situation is less clear. Our principal result (joint with S. Todorcevic and S. Tokgoz) is that Hurewicz' Conjecture for projective sets of reals is equiconsistent with an inaccessible cardinal. In general topological spaces, the situation is more complicated, but we have a variety of similar results for co-analytic spaces, i.e. spaces having Cech-Stone remainders which are continuous images of the space of irrationals. 講演終了後に交流会を予定しています。交流会にご参加いただける方はシャクマトフ<dmitri.shakhmatov(a)ehime-u.ac.jp>までご一報お願い致します。以上、よろしくお願い申し上げます。世話人（五十音順）井上友喜尾國新一シャクマトフディミトリ野倉嗣紀平出耕一平田浩一藤田博司山内貴光 --- ウェブページ： http://www.math.sci.ehime-u.ac.jp/MTGSA.ja.html

1 0

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

17 Dec '16

皆様芝浦工業大学の篠埜です。第19回プログラミングおよびプログラミング言語ワークショップ（PPL2017）のご案内です。カテゴリー1の発表申込締切が近づいてまいりました。発表申込締切: 2016年12月21日(水) 17:00 (JST) 論文提出締切: 2017年1月11日(水) 17:00 (JST) 是非論文のご投稿をお願いいたします。 ====================================================================== 第19回プログラミングおよびプログラミング言語ワークショップ (PPL2017) https://ppl2017.ipl-e.ai.kyutech.ac.jp/ 論文募集/発表募集主催: 日本ソフトウェア科学会プログラミング論研究会日程: 2017年3月8日(水)～3月10日(金) 会場: 山梨県笛吹市石和温泉「華やぎの章慶山」 PPL2017は，プログラミングとプログラミング言語に関連する幅広い分野の研究者・技術者・学生が一堂に会し，最新の研究成果の発表や，新たな研究課題の提案・討論・アイディア交換を行うことを目的とした，合宿形式の研究集会です．プログラミング方法論，プログラミング言語の理論・設計・実装などに関する研究発表を，カテゴリ別に幅広く募集します．カテゴリ1: 国内外で未発表の論文の発表カテゴリ2: 国際会議・学術雑誌等で既発表であるが，国内では未発表の研究の紹介カテゴリ3: ポスター・デモ発表(既発表・未発表の別を問いません) カテゴリ4: サーベイ・チュートリアル発表(既発表・未発表の別を問いません) カテゴリ1の採択論文の中から，特に独創的なアイディアや顕著な成果を含むものに対して論文賞を授与する予定です．また全論文発表と全ポスター・デモのなかから，聴衆の投票によりそれぞれ，最も優秀な論文プレゼンテーションには発表賞(一般の部，学生の部，既受賞者は除く)，最も優秀なポスター・デモにはポスター賞を授与する予定です．カテゴリ1 (国内外未発表論文) ---------------------------- 完成した理論やシステムの研究発表のみならず，萌芽的なアイディアや問題点の提示等も歓迎します．発展途上の研究内容も積極的に採録する方針です(ただし，PPLでの発表として相応しくないと判断される場合は，この限りではありません)．また，カテゴリ1で発表された研究については，会場での討議や査読コメントをもとにその完成度を高め，将来の学術雑誌・国際会議等での業績に結び付けることを奨励しています．そのため，予稿集の配布は参加者のみへの限定的なものとします．カテゴリ1で発表された研究のうち，PPL2017プログラム委員会により優れていると認められたものは， PPL2017終了後(2017年4月下旬予定)，「コンピュータソフトウェア」誌のPPL2017推薦論文としての投稿が可能です．推薦論文は，PPLプログラム委員が引き続き査読を行うことによる，迅速な査読プロセスを特長としています．カテゴリ2 (国外既発表論文) -------------------------- 査読付の国際会議または学術雑誌等で既発表であるが国内では未発表である研究を紹介する場です．採録決定済みの研究も含みます．PPLへの関連をもとに採否を判定いたしますが，申し込み多数の場合はプログラム委員会で選考致します．カテゴリ3 (ポスター・デモ発表) ------------------------------ 2時間程度のセッション内でのポスター発表またはデモ発表です．既発表・未発表の別を問いません．PPLへの関連をもとに採否を判定いたしますが，申し込み多数の場合はプログラム委員会で選考致します．会場の状況により，ポスターの常設展示を可能とします．ショートプレゼンテーションは行いません．カテゴリ4 (サーベイ・チュートリアル発表) ---------------------------------------- 研究動向の紹介(発表者の研究も含む) や分野間の相互理解と参加者の知識の底上げとなる発表を募集します．既発表・未発表の別を問いません．発表後，発表スライドをPPL2017ウェブページ上にて公開して頂く予定です．PPLへの関連，著者の研究発表実績，トピックや切り口の興味深さをもとに，プログラム委員会で選考致します．招待講演 -------- 神谷年洋（島根大学教授）原田康徳（合同会社デジタルポケット代表）以上お二方の招待講演を予定しております．なお，PPL2017の終了は昼頃〜夕刻を予定しています． ====================================================================== 投稿・発表申込要領すべてのカテゴリの投稿・発表について，次のURLから申し込んでください． https://easychair.org/conferences/?conf=ppl2017 申込にあたってはEasyChairのアカウントが必要です．4つのカテゴリそれぞれに対する申込要領の詳細は以下の通りです．申し込み時にEasychairで入力する氏名，所属の情報はプログラム作成に用いますので，参加者の便宜を考慮し，日本語が良いと考えられる場合には日本語での入力をお願い致します．最新の情報は上記ウェブページでご確認ください．カテゴリ1 (国内外未発表論文) --------------------------- 投稿手続きは2段階です．発表申込を行った上で論文提出を行ってください．発表申込締切: 2016年12月21日(水) 17:00 (JST) 著者名，所属，論文タイトル，論文概要(日本語300〜400字程度もしくは英語200 words 程度)，キーワード(3つ以上)を提出してください．論文提出締切: 2017年1月11日(水) 17:00 (JST) 10ページ程度(最大15ページ，参考文献を含む)の論文(日本語もしくは英語，PDF形式．PPL2017ウェブページにて指定のスタイルファイルを利用のこと)を提出してください．最大ページ数を超える付録は投稿版に入れて構いませんが，最終原稿においては削除してもらいます．著者のweb page等においてソースコードや実験データなどを載せて引用しても構いません．最大ページ数を超える付録やweb page等の情報については査読において考慮されない場合もあります．採否通知：2017年2月3日(金) 最終原稿締切: 2017年2月16日(木) 採録された論文の最終原稿の提出方法は，採否通知にてお知らせいたします． (注) 採録された論文等著作物は，日本ソフトウェア科学会著作権規定にもとづいて利用されますので，予めご確認ください． (注) 投稿論文と類似の論文を，他の会議(予稿集を出版するもの)・論文誌などに同時投稿する場合は，査読の有無に関わらず，その旨を発表申込および論文提出の際に明記してください．PPLでは同時投稿の事実のみをもって論文を不採録とすることはありませんが，採否の決定に利用する場合があります(他の会議との重複を避けるため，発表内容についての条件付採録とすることもあります)．カテゴリ2 (国外既発表論文) ------------------------- 発表申込時に採録が決定している国際会議および国際学術雑誌等の発表論文が対象です．理論系だけではなく実装系の論文の投稿も歓迎いたします．発表申込締切: 2017年1月25日(水) 17:00 (JST) 原論文(ページ数不問，PDF形式)と論文概要(テキスト形式)を，著者名，所属，論文タイトル，キーワード(3つ以上)と併せて提出してください．論文概要にて，原論文の出典(発表会議名，掲載済／予定の別等を含む)についても明記してください．採否通知：2017年2月6日(月) カテゴリ3 (ポスター・デモ発表) ----------------------------- ポスター発表またはデモ発表(あるいは両方)を募集いたします．発表申込締切: 2017年2月8日(水) 17:00 (JST) 希望する発表形態を明記して著者名，所属，発表タイトル，発表概要 (200〜300字程度)，キーワード(3つ以上)を提出してください．発表形態については発表タイトル(Title欄)の最後の部分に括弧（）に入れて，「ポスター」「デモ」「ポスター・デモ」のいずれかを記載してください．採否通知：2017年2月15日(水) カテゴリ4 (サーベイ・チュートリアル発表) --------------------------------------- 発表申込締切: 2017年1月25日(水) 17:00 (JST) 著者名，所属，発表タイトル，キーワード(3つ以上)，発表概要(3ページ以内，PDF形式．目的，カバーする話題，想定する聴衆，必要な知識の記述を含むもの)を提出してください．採否通知：2017年2月6日(月) ====================================================================== 問い合わせ先 ppl2017-oc(a)ipl-e.ai.kyutech.ac.xn--jp()-753c9gpa1b92cqcsg7jrh5d1ix122cxi0h ppl2017-pc-chairs(a)ipl-e.ai.kyutech.ac.xn--jp(/)-m53d8hra6b05cmntd6e6b1719ok76b ====================================================================== プログラム委員会青谷知幸 (東京工業大学) 浅田和之 (東京大学) Reynald Affeldt (産業技術総合研究所) 稲葉一浩 (Google) 上野雄大 (東北大学) 菊池健太郎 (東北大学) 小宮常康 (電気通信大学) 篠埜功 (芝浦工業大学) 佐藤亮介 (東京大学) 首藤一幸 (東京工業大学) 末永幸平 (京都大学) 宋剛秀 (神戸大学) 千葉滋 (東京大学) 土屋達弘 (大阪大学) 中野圭介 (電気通信大学) 鍋島英知 (山梨大学) 番原睦則 (神戸大学) 前田敦司 (筑波大学) 松田一孝 (東北大学) 森畑明昌 (東京大学) 八杉昌宏 (九州工業大学) 組織委員会江本健斗 (九州工業大学) [組織委員長] 平石拓 (京都大学) 佐藤重幸 (高知工科大学) 海野広志 (筑波大学) 対馬かなえ (国立情報学研究所) 塚田武志 (東京大学) 篠埜功 (芝浦工業大学) [プログラム共同委員長] 番原睦則 (神戸大学) [プログラム共同委員長] ====================================================================== 篠埜　功 -- Isao Sasano <sasano(a)sic.shibaura-it.ac.jp>

1 0

PhDs in Logic IX, Bochum (Germany), 2-4 May 2017
by Hitoshi Omori 16 Dec '16

16 Dec '16

(Apologies for multiple copies) Call for submissions: PhDs in Logic IX, Bochum, 2nd - 4th May 2017 PhDs in Logic is an annual graduate conference organised by local graduate students. This interdisciplinary conference welcomes contributions to various topics in mathematical logic, philosophical logic, and logic in computer science. It involves tutorials by established researchers as well as short (20 minutes) presentations by PhD students, master students and first-year postdocs on their research. We are happy to announce that the ninth edition of PhDs in Logic will take place at the Ruhr University Bochum, Germany, during 2nd - 4th May 2017. Confirmed tutorial speakers are : Petr Cintula (Czech Academy of Sciences) María Manzano (University of Salamanca) João Marcos (University of Natal) Gabriella Pigozzi (Paris Dauphine University) Christian Straßer (Ruhr-University Bochum) Heinrich Wansing (Ruhr-University Bochum) Abstract submission: PhD students, master students and first-year postdocs in logic from disciplines, that include but are not limited to philosophy, mathematics and computer science are invited to submit an extended abstract on their research. Submitted abstracts should be between 2 and 3 pages, including the relevant references. Each abstract will be anonymously reviewed by the scientific committee. Accepted abstracts will be presented by their authors in a 20-minute presentation during the conference. The deadline for abstract submission is 2nd February 2017. Please submit your blinded abstract via: https://easychair.org/conferences/?conf=phdsinlogic9 For more information please see: http://www.ruhr-uni-bochum.de/phdsinlogicix Local organisers: Christopher Badura, AnneMarie Borg, Jesse Heyninck and Daniel Skurt

1 0

Talk by Nao Hirokawa (22 Dec 11:00-)
by Tetsuya Sato 15 Dec '16

15 Dec '16

京都大学数理解析研究所の佐藤です。 12月22日11:00から、北陸先端科学技術大学院大学‎の廣川直先生に以下の講演をしていただくことになりましたので、ご連絡いたします。どうぞお気軽にお越しください。 ========== Time: 11:00-12:00, 22 Dec, 2016 Place: Rm 478, Research Building 2, Main Campus, Kyoto University 京都大学本部構内総合研究2号館 4階478号室 http://www.kyoto-u.ac.jp/en/access/yoshida/main.html (Building 34) http://www.kyoto-u.ac.jp/ja/access/campus/map6r_y.htm (34番の建物) Speaker: Nao Hirokawa (Japan Advanced Institute of Science and Technology) Title: Basic Normalization Abstract: The Normalization Theorem (O'Donnell 1977) states that for every left-normal orthogonal rewrite system, the leftmost outermost strategy reduces any term to the normal form if it exists. Although the theorem ensures the normalization property of important systems such as Combinatory Logic, the left-normality condition rules out most of functional programs. We revisit the problem to seek a solution for normalization of the leftmost outermost strategy. This work is based on joint work with Aart Middeldorp and Georg Moser.

1 0

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

15 Dec '16

みなさま：吉信＠名古屋大学情報科学です。重複して受け取られた方はご容赦ください。下記の要領で名古屋集合論セミナーを開催します。奮ってご参加下さい。日時：12月22日(木)15:30-17:00 場所：名古屋大学大学院情報科学研究科棟322号室講演者：Franklin D. Tall (トロント大学) 題目：Definable versions of Hurewicz’ conjecture アブストラクト： A topological space is Menger if, given a countable sequence of open covers, there is a finite selection from each of them, so that the union of the selections is a cover. The Menger property lies strictly between \sigma-compactness and Lindelofness. In 1925 Hurewicz conjectured that Menger was equivalent to \sigma-compact in metrizable spaces. This was refuted by Chaber and Pol in 2002. However, for spaces which are in some sense "definable", the situation is less clear. Our principal result (joint with S. Todorcevic and S. Tokgoz) is that Hurewicz' Conjecture for projective sets of reals is equiconsistent with an inaccessible cardinal. In general topological spaces, the situation is more complicated, but we have a variety of similar results for co-analytic spaces, i.e. spaces having Cech-Stone remainders which are continuous images of the space of irrationals.

1 0

GaLoP 2017: Call for Papers
by Ichiro Hasuo 02 Dec '16

02 Dec '16

(Apologies for multiple copies) 12th Workshop on Games for Logic and Programming Languages (GaLoP 2017) Uppsala, Sweden, 22-23 April http://www.gamesemantics.org GaLoP is an annual international workshop on game-semantic models for logics and programming languages and their applications. This is an informal workshop that welcomes work in progress, overviews of more extensive work, programmatic or position papers and tutorials. GaLoP XII will be held in Uppsala, Sweden, on 22-23 April 2017 as a satellite workshop of ETAPS (http://www.etaps.org/). Areas of interest include: * Games and other interaction-based denotational and operational models; * Game-based program analysis and verification; * Logics for games and games for logics; * Algorithmic aspects of game semantics; * Categorical aspects of game semantics; * Programming languages and full abstraction; * Higher-order automata and Petri nets; * Geometry of interaction; * Ludics; * Epistemic game theory; * Logics of dependence and independence; * Computational linguistics; * Games and multi-valued logics. There will be no formal proceedings but the possibility of a special issue in a journal will be considered. (The 2005, 2008, 2011 and 2014 workshops led to special issues in Annals of Pure and Applied Logic.) // Submission Instructions // Please submit an abstract (up to one page, excluding bibliography) of your proposed talk on the EasyChair submission page below. Supplementary material may be submitted, and will be considered at the discretion of the PC. https://easychair.org/conferences/?conf=galop2017 // Important Dates // Submission: 30 January 2017 Notification: 20 February 2017 Workshop: 22-23 April 2017 // Tutorial // Lauri Hella // Invited talks // Andreas Blass Dan Ghica Erich Grädel Martin Hyland (TBC) // Programme Committee // Dietmar Berwanger Esfandiar Haghverdi Juha Kontinen (Co-Chair) Jim Laird Marina Lenisa (Co-Chair) Pierre Lescanne Luke Ong Jouko Väänänen

1 0

Talk by Bakh Khoussainov and Toru Takisaka (1 Dec 11:00-)
by Tetsuya Sato 24 Nov '16

24 Nov '16

京都大学数理解析研究所の佐藤です。 12月1日11:00から、オークランド大学のBakh Khoussainov先生と京都大学数理解析研究所の滝坂透氏の両名に以下のjoint talkをしていただくことになりましたので、ご連絡いたします。どうぞお気軽にお越しください。 ========== Time: 11:00-12:00, 1 Dec, 2016 Place: Rm 478, Research Building 2, Main Campus, Kyoto University 京都大学本部構内総合研究2号館 4階478号室 http://www.kyoto-u.ac.jp/en/access/yoshida/main.html (Building 34) http://www.kyoto-u.ac.jp/ja/access/campus/map6r_y.htm (34番の建物) Speakers: Bakh Khoussainov (University of Auckland) and Toru Takisaka (RIMS, Kyoto university) Title: On large scale geometries of infinite strings Abstract: Motivated by notions in geometric group theory, we introduce the concept of large scale geometry on infinite strings. Informally, two infinite strings have the same large scale geometry if there is a bi-Lipschitz map between both strings with a finite uniform distortion. We call these maps quasi-isometric maps. Introduction of large scale geometries poses several questions. The first question is related to understanding the partial order induced by quasi-isometric maps on large scale geometries of strings. We prove that there is the greatest large scale geometry and infinitely many minimal large scale geometries. The second is related to understanding the quasi-isometric maps on various classes of strings. The third question address the issue of building quasi-isometric maps between computable infinite strings. We show that the problem is Sigma_3-complete. The fourth question is about understanding sets of large scale geometries given some tools (e.g. Buchi automata) that describe sets of strings. We provide an efficient algorithm that gives a full description of large scale geometries of strings accepted by such automata. Finally, the fifth question asks if it is possible to associate with every large scale geometry an algebraic structure that describes the geometry uniquely. Here we use tools of geometric group theory by invoking the notion of asymptotic cone.

1 0

JAIST Logic Seminar Series
by Hajime Ishihara 22 Nov '16

22 Nov '16

皆様ウィーン工科大学のMatthias Baaz先生の講演のお知らせです。どうぞふるってご参加ください。問合せ先：石原　哉北陸先端科学技術大学院大学情報科学系 e-mail: ishihara(a)jaist.ac.jp ----------------------------------------------- * JAIST Logic Seminar Series * Date: Tuesday 6 December, 2016, 15:20-17:00 Place: JAIST, Collaboration room 6 (I-57g) (Access: http://www.jaist.ac.jp/english/location/access.html) Speaker: Matthias Baaz (Vienna University of Technology) (joint work with Juan.P.Aguilera) Title: Unsound inferences make proofs shorter Abstract: We give examples of calculi that extend Gentzen's sequent calculus LK in such a way that (i) derivations lead only to true sequents (ii) cut free proofs may be non-elementary shorter than cut free LK proofs.

1 0

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

18 Nov '16

皆様第19回プログラミングおよびプログラミング言語ワークショップ（PPL2017）のご案内です。投稿・発表申込の詳細について記載しています。是非論文のご投稿をお願いいたします。 ====================================================================== 第19回プログラミングおよびプログラミング言語ワークショップ (PPL2017) https://ppl2017.ipl-e.ai.kyutech.ac.jp/ 論文募集/発表募集主催: 日本ソフトウェア科学会プログラミング論研究会日程: 2017年3月8日(水)～3月10日(金) 会場: 山梨県笛吹市石和温泉「華やぎの章慶山」 PPL2017は，プログラミングとプログラミング言語に関連する幅広い分野の研究者・技術者・学生が一堂に会し，最新の研究成果の発表や，新たな研究課題の提案・討論・アイディア交換を行うことを目的とした，合宿形式の研究集会です．プログラミング方法論，プログラミング言語の理論・設計・実装などに関する研究発表を，カテゴリ別に幅広く募集します．カテゴリ1: 国内外で未発表の論文の発表カテゴリ2: 国際会議・学術雑誌等で既発表であるが，国内では未発表の研究の紹介カテゴリ3: ポスター・デモ発表(既発表・未発表の別を問いません) カテゴリ4: サーベイ・チュートリアル発表(既発表・未発表の別を問いません) カテゴリ1の採択論文の中から，特に独創的なアイディアや顕著な成果を含むものに対して論文賞を授与する予定です．また全論文発表と全ポスター・デモのなかから，聴衆の投票によりそれぞれ，最も優秀な論文プレゼンテーションには発表賞(一般の部，学生の部，既受賞者は除く)，最も優秀なポスター・デモにはポスター賞を授与する予定です．カテゴリ1 (国内外未発表論文) ---------------------------- 完成した理論やシステムの研究発表のみならず，萌芽的なアイディアや問題点の提示等も歓迎します．発展途上の研究内容も積極的に採録する方針です(ただし，PPLでの発表として相応しくないと判断される場合は，この限りではありません)．また，カテゴリ1で発表された研究については，会場での討議や査読コメントをもとにその完成度を高め，将来の学術雑誌・国際会議等での業績に結び付けることを奨励しています．そのため，予稿集の配布は参加者のみへの限定的なものとします．カテゴリ1で発表された研究のうち，PPL2017プログラム委員会により優れていると認められたものは， PPL2017終了後(2017年4月下旬予定)，「コンピュータソフトウェア」誌のPPL2017推薦論文としての投稿が可能です．推薦論文は，PPLプログラム委員が引き続き査読を行うことによる，迅速な査読プロセスを特長としています．カテゴリ2 (国外既発表論文) -------------------------- 査読付の国際会議または学術雑誌等で既発表であるが国内では未発表である研究を紹介する場です．採録決定済みの研究も含みます．PPLへの関連をもとに採否を判定いたしますが，申し込み多数の場合はプログラム委員会で選考致します．カテゴリ3 (ポスター・デモ発表) ------------------------------ 2時間程度のセッション内でのポスター発表またはデモ発表です．既発表・未発表の別を問いません．PPLへの関連をもとに採否を判定いたしますが，申し込み多数の場合はプログラム委員会で選考致します．会場の状況により，ポスターの常設展示を可能とします．ショートプレゼンテーションは行いません．カテゴリ4 (サーベイ・チュートリアル発表) ---------------------------------------- 研究動向の紹介(発表者の研究も含む) や分野間の相互理解と参加者の知識の底上げとなる発表を募集します．既発表・未発表の別を問いません．発表後，発表スライドをPPL2017ウェブページ上にて公開して頂く予定です．PPLへの関連，著者の研究発表実績，トピックや切り口の興味深さをもとに，プログラム委員会で選考致します．招待講演 -------- 神谷年洋（島根大学教授）原田康徳（合同会社デジタルポケット代表）以上お二方の招待講演を予定しております．なお，PPL2017の終了は昼頃〜夕刻を予定しています． ====================================================================== 投稿・発表申込要領すべてのカテゴリの投稿・発表について，次のURLから申し込んでください． https://easychair.org/conferences/?conf=ppl2017 申込にあたってはEasyChairのアカウントが必要です．4つのカテゴリそれぞれに対する申込要領の詳細は以下の通りです．申し込み時にEasychairで入力する氏名，所属の情報はプログラム作成に用いますので，参加者の便宜を考慮し，日本語が良いと考えられる場合には日本語での入力をお願い致します．最新の情報は上記ウェブページでご確認ください．カテゴリ1 (国内外未発表論文) --------------------------- 投稿手続きは2段階です．発表申込を行った上で論文提出を行ってください．発表申込締切: 2016年12月21日(水) 17:00 (JST) 著者名，所属，論文タイトル，論文概要(日本語300〜400字程度もしくは英語200 words 程度)，キーワード(3つ以上)を提出してください．論文提出締切: 2017年1月11日(水) 17:00 (JST) 10ページ程度(最大15ページ，参考文献を含む)の論文(日本語もしくは英語，PDF形式．PPL2017ウェブページにて指定のスタイルファイルを利用のこと)を提出してください．最大ページ数を超える付録は投稿版に入れて構いませんが，最終原稿においては削除してもらいます．著者のweb page等においてソースコードや実験データなどを載せて引用しても構いません．最大ページ数を超える付録やweb page等の情報については査読において考慮されない場合もあります．採否通知：2017年2月3日(金) 最終原稿締切: 2017年2月16日(木) 採録された論文の最終原稿の提出方法は，採否通知にてお知らせいたします． (注) 採録された論文等著作物は，日本ソフトウェア科学会著作権規定にもとづいて利用されますので，予めご確認ください． (注) 投稿論文と類似の論文を，他の会議(予稿集を出版するもの)・論文誌などに同時投稿する場合は，査読の有無に関わらず，その旨を発表申込および論文提出の際に明記してください．PPLでは同時投稿の事実のみをもって論文を不採録とすることはありませんが，採否の決定に利用する場合があります(他の会議との重複を避けるため，発表内容についての条件付採録とすることもあります)．カテゴリ2 (国外既発表論文) ------------------------- 発表申込時に採録が決定している国際会議および国際学術雑誌等の発表論文が対象です．理論系だけではなく実装系の論文の投稿も歓迎いたします．発表申込締切: 2017年1月25日(水) 17:00 (JST) 原論文(ページ数不問，PDF形式)と論文概要(テキスト形式)を，著者名，所属，論文タイトル，キーワード(3つ以上)と併せて提出してください．論文概要にて，原論文の出典(発表会議名，掲載済／予定の別等を含む)についても明記してください．採否通知：2017年2月6日(月) カテゴリ3 (ポスター・デモ発表) ----------------------------- ポスター発表またはデモ発表(あるいは両方)を募集いたします．発表申込締切: 2017年2月8日(水) 17:00 (JST) 希望する発表形態を明記して著者名，所属，発表タイトル，発表概要 (200〜300字程度)，キーワード(3つ以上)を提出してください．発表形態については発表タイトル(Title欄)の最後の部分に括弧（）に入れて，「ポスター」「デモ」「ポスター・デモ」のいずれかを記載してください．採否通知：2017年2月15日(水) カテゴリ4 (サーベイ・チュートリアル発表) --------------------------------------- 発表申込締切: 2017年1月25日(水) 17:00 (JST) 著者名，所属，発表タイトル，キーワード(3つ以上)，発表概要(3ページ以内，PDF形式．目的，カバーする話題，想定する聴衆，必要な知識の記述を含むもの)を提出してください．採否通知：2017年2月6日(月) ====================================================================== 問い合わせ先 ppl2017-oc(a)ipl-e.ai.kyutech.ac.xn--jp()-753c9gpa1b92cqcsg7jrh5d1ix122cxi0h ppl2017-pc-chairs(a)ipl-e.ai.kyutech.ac.xn--jp(/)-m53d8hra6b05cmntd6e6b1719ok76b ====================================================================== プログラム委員会青谷知幸 (東京工業大学) 浅田和之 (東京大学) Reynald Affeldt (産業技術総合研究所) 稲葉一浩 (Google) 上野雄大 (東北大学) 菊池健太郎 (東北大学) 小宮常康 (電気通信大学) 篠埜功 (芝浦工業大学) 佐藤亮介 (東京大学) 首藤一幸 (東京工業大学) 末永幸平 (京都大学) 宋剛秀 (神戸大学) 千葉滋 (東京大学) 土屋達弘 (大阪大学) 中野圭介 (電気通信大学) 鍋島英知 (山梨大学) 番原睦則 (神戸大学) 前田敦司 (筑波大学) 松田一孝 (東北大学) 森畑明昌 (東京大学) 八杉昌宏 (九州工業大学) 組織委員会江本健斗 (九州工業大学) [組織委員長] 平石拓 (京都大学) 佐藤重幸 (高知工科大学) 海野広志 (筑波大学) 対馬かなえ (国立情報学研究所) 塚田武志 (東京大学) 篠埜功 (芝浦工業大学) [プログラム共同委員長] 番原睦則 (神戸大学) [プログラム共同委員長] ====================================================================== 篠埜　功 -- Isao Sasano <sasano(a)sic.shibaura-it.ac.jp>

1 0

1st Call for Papers of The Sixth International Conference on Logic, Rationality and Interaction (LORI-VI): September 11-14, 2017, Hokkaido University, Sapporo, Japan
by Katsuhiko Sano 16 Nov '16

16 Nov '16

皆様、北海道大学の佐野勝彦と申します。来年度9月1日から14日に北海道、札幌で開催される会議 LORI-VI についてご案内いたします。ぜひ奮ってご投稿ください。佐野勝彦 --------------------------------------------------------------------------------------- 1st Call for Papers The Sixth International Conference on Logic, Rationality and Interaction (LORI-VI) September 11-14, 2017, Hokkaido University, Sapporo, Japan Submission deadline: March 31, 2017 The International Conference on Logic, Rationality and Interaction (LORI) conference series aims at bringing together researchers working on a wide variety of logic-related topics that concern the understanding of rationality and interaction. The series aims at fostering a view of Logic as an interdisciplinary endeavour, and supports the creation of an East-Asian community of interdisciplinary researchers. We invite submission of contributed papers on any of the broad themes of LORI series; specific topics of interest include, but are not limited to, formal approaches to - agency - argumentation and agreement - belief representation - cooperation - belief revision and belief merging - strategic reasoning - games - decision making and planning - knowledge and action - epistemology - dynamics of informational attitudes - speech acts - knowledge representation - interaction - norms and normative systems - natural language - rationality - philosophy and philosophical logic - preference and utility - social choice - probability and uncertainty - social interaction - intentions, plans, and goals Submitted papers should be at most 12 pages long, with one additional page for references, in PDF format following the Springer LNCS style. Please submit your paper by Friday March 31, 2017, via EasyChair ( http://easychair.org/conferences/?conf=lori6 ). Accepted papers will be collected as a volume in the FoLLI Series on Logic, Language and Information, and authors may be later invited to submit extended versions of their papers in a special issue of a prestigious journal. For detailed conference information and registration, please visit the website at http://golori.org/lori2017/ . Invited Speakers: Mike Dunn (Indiana University, U.S.A.) Alan Hájek (Australian National University) Nina Gierasimczuk (Technical University of Denmark) Willemien Kets (Northwestern University, U.S.A) Sara Negri (University of Helsinki, Finland) Hiroakira Ono (JAIST, Japan) PC Chairs: Alexandru Baltag (University of Amsterdam, The Netherlands) Jeremy Seligman (University of Auckland, New Zealand) Conference Organiser: Tomoyuki Yamada (Hokkaido University, Japan) Sponsors: LORI, Hokkaido University Contacts: Programme: The PC Chairs mailto:lori6@easychair.org Conference: Tomoyuki Yamada mailto:tomoyuki.s.yamada@gmail.com

1 1

Banquet of RIMS Set Theory Workshop 2016
by Teruyuki YORIOKA 10 Nov '16

10 Nov '16

みなさま静岡大学の依岡です。 RIMS Set Theory Workshop 2016 の懇親会のご案内です。 11月30日（水）18時30分から黄桜じろく亭京都府京都市中京区木屋町通三条下ル一筋目東南角　黄桜木屋町ビル4階 5,000円参加をご希望の方は11月25日（金）までに依岡にメールでお知らせください。皆様のご参加をお待ちしております。なお、11月30日（水）の午後は遠足を予定しています。計画が決まりましたらウェブサイトで公開します。こちらも合わせてご参加ください。 RIMS Set Theory Workshop 2016 http://www.ipc.shizuoka.ac.jp/~styorio/rims16/

1 0

CAPEレクチャーのご案内 (Zach Weber, Nov 14, 2016)
by Hitoshi Omori 02 Nov '16

02 Nov '16

CAPEレクチャーのご案内 (重複してお受け取りの際はご容赦ください。) 以下の通り講演会が開催されます。皆さまのお越しをお待ちしております。 ------------------- 日時：2016年11月14日(月) 16:30--18:00 場所：京都大学文学部校舎１階会議室話者：Prof. Zach Weber (University of Otago) 言語：英語題目： Paraconsistent set theory and inconsistent mathematics 概要： Paraconsistent set theory takes as axiomatic the `naive' comprehension principle that every collection forms a set. The infamous paradoxes are then just theorems. The background logic that makes this coherently possible is substantially weaker than classical logic; but the expressive power of the theory is substantially stronger than classical set theory. With these competing forces in the background, we will look at two interrelated goals: Recapture -- reassurance that nothing too important mathematically is lost Expansion -- where new insights and results are gained, studying novel mathematical objects not visible with any other theory I will survey the development of paraconsistent set theory, showing how the basic properties of ordinal and cardinal numbers can be established, along with new perspectives on `proper classes', the axiom of choice, and the continuum hypothesis. With this foundation, I will mention some further work in inconsistent mathematics: from computability theory, arithmetic, analysis, and topology. Throughout I will call attention to the challenges that this research program faces. ------------------- 大森仁

1 0

homotopy type theory
by logic＠math.tsukuba.ac.jp 29 Oct '16

29 Oct '16

> 圏論に関して質問があります。 > 種々の圏の存在はどのようにして主張されますか？ > > 例えば、公理的集合論では、論理式f(x),集合Xに関して、Xの元xでf(x)を満たすもの > から成る集合{x \in X|f(x)}が存在することが分出公理によって言えますが、圏論に > おいても、圏の存在を主張する公理群が定められていますか？ > 上記のような質問をいただいていますが、これはこの質問者以外の広い範囲の方に関心があることと思われますので、ここにお答えします。質問者の名前等は削除してあります。まず質問を Homotopy type theoryはZFCにかわる数学の基礎づけになるという話であるが、集合論はたとえばComprehensionのような豊かな構成原理をもっているが、HTTはどうなのか？と変形させていただきます。まずHTTのなかではn-typeというHierarchyが定義されます。ｎは−２以上の整数です。これはHomotopy theoryから借用された概念で、n-typeというのはｎを越える次元ではhomotopicalにはtrivialであることを意味します。Homotopy theoryの言葉づかいで言うならば、ｎを越える次元のhomotopy groupsはすべてtrivialであることを意味します。０-typeがいわゆるsetで、ここに話を限定するならば comprehensionをはじめとする集合論的構成はだいたいそのまま行えます。一般にはdependent function typeやdependent pair typeという構成原理を最初から内臓していますが、これだけではもちろん足りません。HTTがもつ強力な構成原理はinductionで、特に higher inductionが重要な役割を演じます。計算機言語のCOQや AGDAは通常にinductionを組み込んでいますが、higher inductive typesはまだ持っておりません。少しslogan的な言い方を許していただければ、 inductive typesはfree monadsに、higher inductive typesはmonadsの表現に対応します。 Inductiveな構成のいい例はCauchy realsの構成です。自然数から有理数を作るのは、古典的な話とあまりかわりません。それで有理数から実数を作るには、Dedekindのやり方とCauchyのやり方がありますが、後者の構成をinductiveにやるとどうなるかが、 https://homotopytypetheory.org/book/ の１１．３節に縷説されています。あるいはcirclesやspheresやsuspensionsはどのようにinductiveに構成されるか、第６章に縷説されています。是非ご覧になってください。にしむら筑波大学数学追伸：オマケです。手持無沙汰な折にどうぞ。 https://www.youtube.com/watch?v=VY01dVHvlFE

2 2

Re: [logic-ml] [jssst-ppl] 上級研究員・研究員・RA・インターン募集のお知らせ
by koba＠kb.is.s.u-tokyo.ac.jp 28 Oct '16

28 Oct '16

皆様、東京大学の小林です。下記のアナウンスに便乗して宣伝させていただきます。科研費基盤S「高階モデル検査の深化と発展」でも特任研究員を募集しておりますので http://www-kb.is.s.u-tokyo.ac.jp/~koba/hmc/call-for-postdoc.txt ご検討ください。（こちらではRAは公募しておりません。博士課程に入っていただければ似た待遇でのRAの雇用は可能かと思います）小林直樹東京大学大学院情報理工学系研究科コンピュータ科学専攻〒113-0033 東京都文京区本郷7-3-1 Phone: 03-5841-4124 Fax: 03-5841-4124 email: koba(a)is.s.u-tokyo.ac.jp From: Ichiro Hasuo <i.hasuo(a)acm.org> Subject: [jssst-ppl] 上級研究員・研究員・RA・インターン募集のお知らせ Date: Fri, 28 Oct 2016 14:28:18 +0900 > みなさま（重複投稿ご容赦ください）， > > 今年の10月から開始した ERATO プロジェクトで，上級研究員・研究員・RA > およびインターンを募集しております．プロジェクトの研究内容，職務内容，および応募・問い合わせについては > http://www-mmm.is.s.u-tokyo.ac.jp/~ichiro/ERATO_MMSD_JobDescr.html > をご覧ください．どうかよろしくお願いいたします． > > 蓮尾一郎 > http://www-mmm.is.s.u-tokyo.ac.jp/~ichiro/ > _______________________________________________ > jssst-ppl mailing list > jssst-ppl(a)fos.kuis.kyoto-u.ac.jp > http://www.fos.kuis.kyoto-u.ac.jp/cgi-bin/mailman/listinfo/jssst-ppl

1 0

24th WoLLIC 2017 - Call for Papers
by 小野寛晰 24 Oct '16

24 Oct '16

WoLLIC 2017 24th Workshop on Logic, Language, Information and Computation July 18-21, 2017 University College London (UCL), London, UK 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) ACM Special Interest Group on Logic and Computation (ACM-SIGLOG) (TBC) Sociedade Brasileira de Computação (SBC) Sociedade Brasileira de Lógica (SBL) ORGANISATION Department of Computer Science, University College London, London, UK School of Electronic Engineering and Computer Science, Queen Mary College, London, UK Centro de Informática, Universidade Federal de Pernambuco, Brazil HOSTED BY Department of Computer Science, University College London, London, UK 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-fourth WoLLIC will be held at the School of Electronic Engineering and Computer Science, Queen Mary College, London, UK, from July 18th to 21st, 2017. 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; philosophy 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. Articles should be written in the LaTeX format of LNCS by Springer (see authors instructions at http://www.springer.com/computer/lncs?SGWID=0-164-6-793341-0 <http://www.springer.com/computer/lncs?SGWID=0-164-6-793341-0>). They must not exceed 12 pages, 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 2017 EasyChair website. (Please go to http://wollic.org/wollic2017/instructions.html <http://wollic.org/wollic2017/instructions.html> for instructions.) A title and single-paragraph abstract should be submitted by Mar 14, 2017, and the full paper by Mar 21, 2017 (firm date). Notifications are expected by Apr 22, 2017, and final papers for the proceedings will be due by May 6, 2017 (firm date). PROCEEDINGS The proceedings of WoLLIC 2017, 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 2017 issue of a scientific journal (to be confirmed). INVITED SPEAKERS Hazel Brickhurst (Bristol) (TBC) Ofra Magidor <http://users.ox.ac.uk/~ball1646/> (Oxford University, UK) Peter O'Hearn (UCL) (TBC) Nicole Schweikardt (Humboldt) (TBC) Fan Yang <https://sites.google.com/site/fanyanghp/> (Delft University, The Netherlands) Boris Zilber <https://people.maths.ox.ac.uk/zilber/> (Oxford University, UK) STUDENT GRANTS ASL sponsorship of WoLLIC 2017 will permit ASL student members to apply for a modest travel grant (deadline: May 1st, 2017). See http://www.aslonline.org/studenttravelawards.html <http://www.aslonline.org/studenttravelawards.html> for details. IMPORTANT DATES Mar 14, 2017: Paper title and abstract deadline Mar 21, 2017: Full paper deadline Apr 22, 2017: Author notification May 6, 2017: Final version deadline (firm) PROGRAMME COMMITTEE Matthias Baaz <http://www.logic.tuwien.ac.at/staff/baaz/home.html> (University of Technology, Vienna, Austria) John Baldwin <http://homepages.math.uic.edu/~jbaldwin/> (University of Illinois at Chicago, USA) Dana Bartozová <http://www.math.toronto.edu/bartosov/> (Universidade de São Paulo, Brazil) Agata Ciabattoni <https://www.logic.at/staff/agata/> (University of Technology, Vienna, Austria) Walter Dean <http://www2.warwick.ac.uk/fac/soc/philosophy/people/dean/> (University of Warwick, UK) Erich Grädel <https://logic.rwth-aachen.de/~graedel/> (RWTH Aachen, Germany) Volker Halbach <http://users.ox.ac.uk/~sfop0114/> (University of Oxford, UK) Juliette Kennedy <http://www.math.helsinki.fi/logic/people/juliette.kennedy/> (Helsinki University, Finland) (Chair) Dexter Kozen <http://www.cs.cornell.edu/~kozen/> (Cornell University, USA) Janos Makowsky <http://www.cs.technion.ac.il/~janos/> (Technion - Israel Institute of Technology, Israel) Larry Moss <http://www.indiana.edu/~iulg/moss/> (indiana University, USA) Alessandra Palmigiano <http://www.appliedlogictudelft.nl/alessandra-palmigiano/> (Delft University, The Netherlands) Mehrnoosh Sadrzadeh <http://www.eecs.qmul.ac.uk/people/view/33472/dr-mehrnoosh-sadrzadeh> (Queen Mary, UK) Sonja Smets <http://sonja.tiddlyspot.com/#HOME> (Amsterdam University, The Netherlands) Asger Törnquist <http://www.math.ku.dk/~asgert/> (Københavns Universitet, Denmark) Rineke Verbrugge <http://www.rinekeverbrugge.nl/> (University of Groningen, The Netherlands) Andrés Villaveces <https://avillavecesn.net/> (Universidad Nacional, Colombia) Philip Welch <http://www.maths.bris.ac.uk/~mapdw/> (University of Bristol, UK) 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, Valeria de Paiva, Ruy de Queiroz, Jouko Väänänen. ORGANISING COMMITTEE Alexandra Silva <http://www.alexandrasilva.org/#/main.html> (Univ College London, UK) (Local co-chair) Mehrnoosh Sadrzadeh <http://www.eecs.qmul.ac.uk/people/view/33472/dr-mehrnoosh-sadrzadeh> (Queen Mary, UK) (Local co-chair) Paulo Oliva <http://www.eecs.qmul.ac.uk/~pbo/> (Queen Mary, UK) James Brotherston <http://www0.cs.ucl.ac.uk/staff/J.Brotherston/> (Univ College London, UK) Anjolina G. de Oliveira <http://www.cin.ufpe.br/~ago> (U Fed Pernambuco) Ruy de Queiroz <http://www.cin.ufpe.br/~ruy> (U Fed Pernambuco) (co-chair) FURTHER INFORMATION Contact one of the Co-Chairs of the Organising Committee. WEB PAGE http://wollic.org/wollic2017/ <http://wollic.org/wollic2017/>

1 0

RIMS研究集会「無限組合せ論と強制法理論」
by Teruyuki YORIOKA 24 Oct '16

24 Oct '16

みなさま静岡大学の依岡です。 11月28日（月）から12月1日（木）まで京都大学数理解析研究所で開催されます RIMS研究集会「無限組合せ論と強制法理論」のプログラムを下記のウェブサイトで公開しています。 http://www.ipc.shizuoka.ac.jp/~styorio/rims16/ 11月30日（水）に懇親会などを予定しています。懇親会などの予定はウェブサイトで公開します。みなさまぜひご参加ください。

1 0

第51回MLG数理論理学研究集会（10/27-30箱根）
by Kazushige TERUI 21 Oct '16

21 Oct '16

みなさま第51回MLG数理論理学研究集会のプログラムが確定しましたのでご案内申し上げます。宿泊を伴わない参加は無料ですので、お気軽にお越しください。 Web Page: http://www.kurims.kyoto-u.ac.jp/~terui/mlg2016.html Program: http://www.kurims.kyoto-u.ac.jp/~terui/mlg2016.pdf 照井一成 ------------------------------------------ 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

PEPM 2017: Call for Posters
by Ryosuke SATO 21 Oct '16

21 Oct '16

皆様、（複数受け取られた場合はご容赦ください。）東京大学の佐藤亮介です。 PEPM 2017 のポスター募集のお知らせです．投稿の締め切りは11月8日（火）です．是非，投稿をご検討ください． -- 東京大学大学院情報理工学系研究科佐藤亮介 ryosuke(a)kb.is.s.u-tokyo.ac.jp ------------------------------------------------------------------- CALL FOR POSTERS Workshop on PARTIAL EVALUATION AND PROGRAM MANIPULATION (PEPM 2017) PEPM 2017 information: http://conf.researchr.org/home/PEPM-2017 Submissions: https://pepm17.hotcrp.com/ Paris, France, January 16th - 17th, 2017 (co-located with POPL 2017) PEPM is the premier forum for discussion of semantics-based program manipulation. The first ACM SIGPLAN PEPM symposium took place in 1991, and meetings have been held in affiliation with POPL every year since 2006. PEPM 2017 will be based on a broad interpretation of semantics-based program manipulation, reflecting the expanded scope of PEPM in recent years beyond the traditionally covered areas of partial evaluation and specialization. Posters ------- In order to maintain the dynamic and interactive nature of PEPM, we solicit submission of posters. Poster submissions are 2-page articles in ACM Proceedings style that present preliminary work (see "Submission guidelines" below for more details). If accepted, the work will be presented as part of an interactive poster session at PEPM. Scope ----- Topics of interest for PEPM 2017 include, but are not limited to: * Program and model manipulation techniques such as: supercompilation, partial evaluation, fusion, on-the-fly program adaptation, active libraries, program inversion, slicing, symbolic execution, refactoring, decompilation, and obfuscation. * Program analysis techniques that are used to drive program/model manipulation such as: abstract interpretation, termination checking, binding-time analysis, constraint solving, type systems, automated testing and test case generation. * Techniques that treat programs/models as data objects including metaprogramming, generative programming, embedded domain-specific languages, program synthesis by sketching and inductive programming, staged computation, and model-driven program generation and transformation. * Application of the above techniques including case studies of program manipulation in real-world (industrial, open-source) projects and software development processes, descriptions of robust tools capable of effectively handling realistic applications, benchmarking. Examples of application domains include legacy program understanding and transformation, DSL implementations, visual languages and end-user programming, scientific computing, middleware frameworks and infrastructure needed for distributed and web-based applications, embedded and resource-limited computation, and security. This list of categories is not exhaustive, and we encourage submissions describing applications of semantics-based program manipulation techniques in new domains. If you have a question as to whether a potential submission is within the scope of the workshop, please contact the programme chairs. Submission guidelines --------------------- * Posters should describe work relevant to the PEPM community, and must not exceed 2 pages in ACM Proceedings style. We invite poster submissions that present early work not yet ready for submission to a conference or journal, identify new research problems, showcase tools and technologies developed by the author(s), or describe student research projects. If accepted, the work will be presented as part of an interactive poster session at PEPM. At least one author of each accepted contribution must attend the workshop and present the work. Student participants with accepted poster papers can apply for a SIGPLAN PAC grant to help cover travel expenses and other support. PAC also offers other support, such as for child-care expenses during the meeting or for travel costs for companions of SIGPLAN members with physical disabilities, as well as for travel from locations outside of North America and Europe. For details on the PAC programme, see its web page. Publication ----------- Posters will appear along with accepted papers in formal proceedings published by ACM Press and in the ACM Digital Library. Keynote ------- Neil Jones (DIKU) will give the PEPM keynote talk, titled Compiling Untyped Lambda Calculus to Lower-level Code by Game Semantics and Partial Evaluation Submission ---------- Posters should be submitted electronically via HotCRP. https://pepm17.hotcrp.com/ Authors using LaTeX to prepare their submissions should use the new improved SIGPLAN proceedings style, and specifically the sigplanconf.cls 9pt template. Important Dates --------------- * Poster submission : Tuesday 8th November 2016 * Author notification : Friday 18th November 2016 * Camera ready : Monday 28th November 2016 * Workshop : Monday 16th - Tuesday 17th January 2017 The proceedings will be published 2 weeks pre-conference. AUTHORS TAKE NOTE: The official publication date is the date the proceedings are made available in the ACM Digital Library. This date may be up to two weeks prior to the first day of your conference. The official publication date affects the deadline for any patent filings related to published work. (For those rare conferences whose proceedings are published in the ACM Digital Library after the conference is over, the official publication date remains the first day of the conference.). PEPM'17 Programme Committee --------------------------- Elvira Albert (Complutense University of Madrid, Spain) Don Batory (University of Texas at Austin, USA) Martin Berger (University of Sussex, UK) Sebastian Erdweg (TU Delft, Netherlands) Andrew Farmer (Facebook, USA) Matthew Flatt (University of Utah, USA) John Gallagher (Roskilde University, Denmark) Robert Glück (DIKU, Denmark) Jurriaan Hage (Utrecht University, Netherlands) Zhenjiang Hu (National Institute of Informatics, Japan) Yukiyoshi Kameyama (University of Tsukuba, Japan) Ilya Klyuchnikov (Facebook, UK) Huiqing Li (EE, UK) Annie Liu (Stony Brook University, USA) Markus Püschel (ETH Zurich, Switzerland) Ryosuke SATO (University of Tokyo, Japan) Sven-Bodo Scholz (Heriot-Watt University, UK) Ulrik Schultz (co-chair) (University of Southern Denmark) Ilya Sergey (University College London, UK) Chung-chieh Shan (Indiana University, USA) Tijs van der Storm (Centrum Wiskunde & Informatica, Netherlands) Jeremy Yallop (co-chair) (University of Cambridge, UK)

1 0

Kobe Colloquium on Logic, Statistics and Informatics, October 13, 2016
by Hirotaka Kikyo 06 Oct '16

06 Oct '16

Kobe Colloquium on Logic, Statistics and Informatics 以下の要領でコロキウムを開催します。 (2重に受け取られた方はご容赦願います) 日時: 2016/10/13 (木) 3:00pm - 4:30pm 場所: 神戸大学六甲台第2キャンパス自然科学総合研究棟3号館421室講演者： Kaisa Kangas （神戸大・システム情報/Helsinki U.）題目： Group Configuration for Quasiminimal Classes 交通：阪急六甲駅またはJR六甲道駅から神戸市バス36系統「鶴甲団地」行きに乗車，「神大本部工学部前」停留所下車，徒歩すぐ． http://www.kobe-u.ac.jp/guid/access/rokko/rokkodai-dai2.html 連絡先：桔梗宏孝 kikyo(a)kobe-u.ac.jp

1 0

Talk by Adam Prenosil (13 Oct 11:00-)
by Tetsuya Sato 04 Oct '16

04 Oct '16

京都大学数理解析研究所の佐藤です。 10月13日11:00から、チェコ科学アカデミーのAdam Prenosil氏に以下の講演をしていただくことになりましたので、ご連絡いたします。どうぞお気軽にお越しください。 ========== Time: 11:00-12:00, 13 Oct, 2016 Place: Rm 478, Research Building 2, Main Campus, Kyoto University 京都大学本部構内総合研究2号館 4階478号室 http://www.kyoto-u.ac.jp/en/access/yoshida/main.html (Building 34) http://www.kyoto-u.ac.jp/ja/access/campus/map6r_y.htm (34番の建物) Speaker: Adam Prenosil (Czech Academy of Sciences) Title: Classical proof theory, non-classically Abstract: We present an approach to cut elimination in classical logic which appeals to elimination rules.rather than to induction on cut rank and which works equally well for proofs from a non-empty set of sequential premises. As an illustration of the benefits of accepting elimination rules as an integral part of the sequent calculus for classical logic, we use the calculus with elimination rules to provide a particularly simple syntactic proof of a recent non-classical refinement of Craig's interpolation theorem due to Milne. This approach, while non-standard, is in fact natural when we view classical logic as part of the family of super-Belnap logics, that is, extensions of the four-valued Belnap-Dunn logic. We shall therefore start by introducing this family proof-theoretically as the logics which retain the structural and logical rules of classical logic, but relax Identity and Cut (as opposed to substructural logics, which retain Identity and Cut but relax the structural rules of classical logic).

1 0

ワークショップ「2階論理の意味論」
by Makoto Kikuchi 30 Sep '16

30 Sep '16

皆様，以下の要領でワークショップを開催しますのでお知らせします．神戸大学菊池誠日時：2016年11月5日（土）15:45〜17:45 場所：東京大学駒場キャンパス1号館1階108室題目：ワークショップ「 2階論理の意味論」　　科学基礎論学会2016年度秋の研究例会（非会員は参加費1,000円が必要です）　　科学基礎論学会 Web Page：http://phsc.jp オーガナイザ：菊池誠（神戸大学）提題者：　佐藤智哉　2階論理的妥当性の新しい意味論的特徴づけ　池上大祐（東京電機大学）2階論理とブール値2階論理　新井敏康（千葉大学）竹内の基本予想の意味論的証明ワークショップ趣旨：「すべて」や「存在」という量化の対象が「個物」に限定される形式的論理が 1階論理，「個物と概念」であるのが2階論理，そして「個物，概念，概念上の概念，…」のすべてであるのが高階論理である．1階論理が形式的論理の現在の事実上の標準理論である．ただし，BoolosやShapiro，Vaananenの哲学的な議論やFriedmanの逆数学の研究プログラムにも見られるように，今でも2階論理それ自身や2階論理の上で展開される公理系に関心が持たれている． 2階論理の意味論を考える際に問題になるのが「概念」を対象とする2階量化子の解釈である．2階量化子の解釈は「個物全体の集合」の部分集合族を与えることで定められる．最も自然な2階論理の意味論は2階量化子の解釈を与える部分集合族を「個物全体の集合」の冪集合とすることで定められるが，この意味論では通常の公理と推論規則で2階論理の完全性定理は成り立たない． Henkinは2階量化子の解釈を与える部分集合族を「個物全体の集合」の任意に選ばれた部分集合族とすれば，通常の公理と推論規則で2階論理の完全性定理が成り立つことを示した． Henkin流の意味論が2階論理の現在の事実上の標準的な意味論である．しかし，このHenkin流の意味論に基づく2階論理とは実質的には1階論理の特別な場合であり，他の意味論の可能性や必要性がない訳ではない．本ワークショップではHenkin流の意味論以外の2階論理の意味論について，佐藤智哉が哲学の立場から，池上大祐が集合論の立場から最近の研究を紹介し，新井敏康が証明論の立場から古典的な議論を紹介する．提題要旨：提題1：2階論理的妥当性の新しい意味論的特徴づけ　佐藤智哉二階述語論理の標準意味論に関する一つの問題は、標準意味論においては特定の集合の特定の性質に依存するような論証が妥当となることである。そのような集合論の結果に基づく論証は「集合論的妥当」とでも呼ばれるべきで、「論理的妥当」な論証とは区別されなければならない。標準意味論の中で妥当となる論証のうち、どの論証が真の意味での論理的妥当であり、どの論証が集合論的妥当なのか。二階述語言語の論理的妥当性を特徴づけるためには、標準意味論とは別の新しい意味論システムが必要である。本発表の主目的は、そのような標準意味論に代わる新しい意味論システムの紹介である。新しい意味論システムのための一つのアイデアは、論理定項とは何かという哲学的議論が、論理的妥当性と集合論的妥当性の区別に応用できるということである。Tarskiに始まる近年の論理定項研究を紹介した後で、それを使ってどのように二階論理的妥当性が参考文献 D. Bonnay, Logicality and invariance, The Bulletin of Symbolic Logic, 14, 29–68, 2008. S. Feferman, Logic, logics, and logicism, Notre Dame Journal of Formal Logic, 40, 31–54, 1999 G. Sher, The Bounds of Logic: A Generalized View Point, Cambridge, MA: MIT Press, (1991). T. Sato, A new semantic characterization of second-order logical validity (unpublished). A Tarski, What are logical notions? J. Corcoran (Ed.), History and Philosophy of Logic, 7, 143–154, 1986. 提題2：2階論理とブール値2階論理　池上大祐（東京電機大学）二階述語論理の代表的な意味論としてタルスキ意味論（完全意味論）とヘンキン意味論の二つがある。タルスキ意味論を用いると、一階述語論理で表現できない様々な性質を記述できるが、一階述語論理において成り立つ定理（完全性定理、コンパクト性定理など）がことごとく成り立たず、二階述語論理は非常に複雑になる。一方、ヘンキン意味論を用いると、一階述語論理において成り立つ多くの定理が成り立つが、論理の表現力は一階述語論理と全く同じで、一階述語論理と比べて二階述語論理に新しい現象は見られない。本講演では、二階述語論理の意味論としてブール値意味論を導入し、 1) V = L の下ではブール値意味論はタルスキ意味論と同じ複雑さを持つこと 2) 巨大基数とウディンのΩ論理についての適切な仮定をすると、ブール値意味論は、　タルスキ意味論より単純でヘンキン意味論より複雑な意味論になることの二点について論じる。本講演で述べる多くの研究成果は Jouko Vaananen 氏との共同研究によるものである。参考文献 D. Ikegami and J. Vaananen, Boolean-Valued Second-Order Logic, Notre Dame Journal of Formal Logic, 56 (1), 167–190, 2015. 提題3：基本予想の意味論的証明　新井敏康（千葉大学）竹内外史は1953に高階論理GLCを定め，GLCについてCut除去定理が成り立つという基本予想を提示した．GLCの部分体系である2階論理がG1LCであり，竹内外史はG1LCの部分体系で基本予想が成り立つことを構文論的に示した．意味論的には，まずCutを持たない体系の3値モデルに対する完全性がSchutteによって示され，その後，3値モデルを2値モデルに完備化する方法で，G1LCについてはTaitによって，GLCについては高橋元男とPrawitzによって独立に，竹内の基本予想が成り立つことが証明された．その意味論的な議論を紹介する．参考文献新井敏康「竹内の基本予想とは何か，何であるべきか」数理解析研究所講究録, 1442, 1-7, 2005.

1 0

Talk by Yoriyuki Yamagata (6 Oct 11:00-)
by Tetsuya Sato 29 Sep '16

29 Sep '16

京都大学数理解析研究所の佐藤です。 10月6日11:00から、産業技術総合研究所の山形頼之氏に以下の講演をしていただくことになりましたので、ご連絡いたします。どうぞお気軽にお越しください。 ========== Time: 11:00-12:00, 6 Oct, 2016 Place: Rm 478, Research Building 2, Main Campus, Kyoto University 京都大学本部構内総合研究2号館 4階478号室 http://www.kyoto-u.ac.jp/en/access/yoshida/main.html (Building 34) http://www.kyoto-u.ac.jp/ja/access/campus/map6r_y.htm (34番の建物) Speaker: Yoriyuki Yamagata (National Institute of Advanced Industrial Science and Technology) (Website: http://staff.aist.go.jp/yoriyuki.yamagata/en/) Title: Consistency proof of an arithmetic with substitution inside a bounded arithmetic Abstract: Bounded arithmetics are systems of arithmetic in which induction is restricted to bounded formulas. Bounded formulas are formulas in which all quantifiers are bounded by some terms. Among many such systems, Buss's hierarchy of bounded arithmetics have particular interest, because their provably total functions exactly correspond polynomial-time hierarchy. A major open problem on bounded arithmetics is whether Buss's hierarchy collapses or not. If it collapses, for example, it implies P=NP. One strategy to differentiate the hierarchy is to use Gödel sentence of some theories. In this talk, we consider a theory PV by Cook and Urquhart and its restrictions. PV is an equational system, which has roughly the same strength to Buss's S12. Beckmann proved that when induction and substitution are removed from PV, the consistency of the system can be proved by S12. On the other hand, Buss and Ignjatović proved that S12 cannot prove the consistency of the system which obtained by removing just induction, but adding propositional logic and BASIC axioms, from PV. In this talk, we improve the Beckmann by proving that S22 can prove the consistency of the system which obtained by removing just induction from PV. By delineating bounded arithmetics which can prove consistency of various restrictions of PV, we hope to prove non-collapse of Buss's hierarchy, and relatedly, polynomial-time hierarchy.

1 0

締切延長：第51回MLG数理論理学研究集会（10/27-30箱根）
by Kazushige TERUI 26 Sep '16

26 Sep '16

みなさま先日来ご案内しているMLG研究集会についてですが、宿泊・講演ともまだ余裕がありますので、締切を９月２９日（木）まで延長したいと思います。なお今回はチェコ科学アカデミーから以下の方々が参加されます。 Petr Cintula（数理ファジィ論理・抽象代数論理など） Zuzana Hanikova（ファジィ集合論など） Rostislav Horcik（部分構造論理など） Carles Noguera（数理ファジィ論理・抽象代数論理など） Tommaso Moraschini, Adam Prenosil, Igor Sedlar, Amanda Vidal うち数名の方には入門的な講演をお願いする予定です。３泊４日ですが、部分参加も歓迎します。どうぞよろしくお願いします。照井 --------------------------------------------------- 第51回MLG数理論理学研究集会締切延長 MLG数理論理学研究集会は，1971年開始された，この分野の多くの研究者が参加している40年以上続く研究集会です。成果を発表し合ったり，アイデアを交換したりと，ザックバランな雰囲気で行われています。数学の他分野や，広く数理科学，情報科学，哲学の方々や，外国からの研究者を迎えるなど，オープンに運営されています。（昨年度の様子：http://www.kurims.kyoto-u.ac.jp/~terui/mlg2015.html ）日時：2016年10月27日（木）午後 − 30日（日）午前場所：四季の湯強羅静雲荘（ http://gora-seiunsou.jp/ ）参加費用：全参加の場合30,000円（3食つき、懇親会費は別途）参加・講演申し込み： 9月29日（木）までウェブページ：http://www.kurims.kyoto-u.ac.jp/~terui/mlg2016.html 詳細は上記Web Pageをご覧ください。みなさまの参加をお待ちしております。京都大学数理解析研究所照井　一成 ------------------------------------------ Kazushige TERUI Research Institute for Mathematical Sciences, Kyoto University. Kitashirakawa Oiwakecho, Sakyo-ku, Kyoto 606-8502, JAPAN. Phone: +81-75-753-7235 Fax: +81-75-753-7276 terui(a)kurims.kyoto-u.ac.jp http://www.kurims.kyoto-u.ac.jp/~terui/

1 0

correction again
by 吉信康夫 21 Sep '16

21 Sep '16

皆様：吉信＠名古屋大学大学院情報科学研究科です。すでに何人の方からご指摘いただきましたように、セミナーご案内の日時も誤っておりました。重ねてお詫びいたしますとともに、訂正したものを改めて投稿させていただきます。名古屋数学基礎論セミナーのご案内日時：9月23日(金) 15:30- 場所：名古屋大学大学院情報科学研究科棟 2F 206号室講演者：木原貴行 (University of California, Berkeley) タイトル：　多対一次数の一様Martin予想とWadge次数アブストラクト：　多対一次数は，決定問題の計算論的複雑性を測る指標の一つであり，Wadge次数は，ベール空間の部分集合の位相的複雑性を測る指標の一つである．両者の定義は酷似している一方，多対一次数構造は混沌として掴み所がなく，Wadge次数構造は美しく整然としており単純明快である．したがって，それらの酷似した定義とは対照的に，それらの構造は如何なる意味でも同型ではない．それにも関わらず，「自然」な多対一次数の構造と Wadge次数構造が同型であることを示す．　より正確には，Woodinによって提案された決定性公理の拡張であるAD+の下で，任意の better-quasi-order Q に対して，一様次数不変な Q 値多対一次数の構造と Q 値Wadge次数構造が同型であることを示す．

1 0

correction
by 吉信康夫 20 Sep '16

20 Sep '16

皆様：吉信康夫＠名古屋大学大学院情報科学研究科です。先ほどお送りしたセミナーのご案内で、講演者のお名前の字が誤っておりました。お詫びいたしますとともに、訂正したものを改めてお送りいたします。名古屋数学基礎論セミナーのご案内日時：9月13日(金) 15:30- 場所：名古屋大学大学院情報科学研究科棟 2F 206号室講演者：木原貴行 (University of California, Berkeley) タイトル：　多対一次数の一様Martin予想とWadge次数アブストラクト：　多対一次数は，決定問題の計算論的複雑性を測る指標の一つであり，Wadge次数は，ベール空間の部分集合の位相的複雑性を測る指標の一つである．両者の定義は酷似している一方，多対一次数構造は混沌として掴み所がなく，Wadge次数構造は美しく整然としており単純明快である．したがって，それらの酷似した定義とは対照的に，それらの構造は如何なる意味でも同型ではない．それにも関わらず，「自然」な多対一次数の構造と Wadge次数構造が同型であることを示す．　より正確には，Woodinによって提案された決定性公理の拡張であるAD+の下で，任意の better-quasi-order Q に対して，一様次数不変な Q 値多対一次数の構造と Q 値Wadge次数構造が同型であることを示す．

1 0

nagoya logic seminar
by 吉信康夫 20 Sep '16

20 Sep '16

皆様：吉信康夫＠名古屋大学大学院情報科学研究科です。以下の要領で名古屋数学基礎論セミナーを開催します。奮って御参加下さい。日時：9月13日(金) 15:30- 場所：名古屋大学大学院情報科学研究科棟 2F 206号室講演者：木原貴之 (University of California, Berkeley) タイトル：　多対一次数の一様Martin予想とWadge次数アブストラクト：　多対一次数は，決定問題の計算論的複雑性を測る指標の一つであり，Wadge次数は，ベール空間の部分集合の位相的複雑性を測る指標の一つである．両者の定義は酷似している一方，多対一次数構造は混沌として掴み所がなく，Wadge次数構造は美しく整然としており単純明快である．したがって，それらの酷似した定義とは対照的に，それらの構造は如何なる意味でも同型ではない．それにも関わらず，「自然」な多対一次数の構造と Wadge次数構造が同型であることを示す．　より正確には，Woodinによって提案された決定性公理の拡張であるAD+の下で，任意の better-quasi-order Q に対して，一様次数不変な Q 値多対一次数の構造と Q 値Wadge次数構造が同型であることを示す．

1 0

公募
by 泉英明 19 Sep '16

19 Sep '16

皆様千葉工業大学教育センター数学教室の泉です。現在、当数学教室では助教１名の公募を行っております。締切は 2016年10月20日(必着)となっております。詳細については http://www.it-chiba.ac.jp/institute/adoption/ をご覧ください

1 0

(no subject)
by 泉英明 19 Sep '16

19 Sep '16

皆様千葉工業大学教育センター数学教室の泉です。現在、当数学教室では助教１名の公募を行っております。締切は 2016年10月20日(必着)となっております。詳細については http://www.it-chiba.ac.jp/institute/adoption/ をご覧ください。

1 0

数学基礎論とその応用
by Makoto Kikuchi 16 Sep '16

16 Sep '16

皆様，以前にもご案内しましたが，2016年9月26日（月）から29日（木）まで， RIMS 研究集会「数学基礎論とその応用」を開催しますのでお知らせします． http://www2.kobe-u.ac.jp/~mkikuchi/mla2016.html 事前登録なしで参加できます．また，以下の要領で懇親会を開きます．日時：2016年9月28日（水）午後6時から会場：マーブルルーム https://www.hotpepper.jp/strJ000040535/ 場所：京都府京都市中京区先斗町通三条下ル橋下町135先斗町ビル4F 交通：京阪三条駅から徒歩5分，阪急河原町駅から徒歩10分内容：立食（飲み放題）会費：3,000円（当日会場で支払い） 8月に研究集会への参加申し込みをお送り下さった方で，懇親会への出欠の変更のない方はご連絡くださる必要はありません．出欠を変更される方，未定とお答えになられた方，また，参加申し込みをなさっていない方で懇親会への出席をご希望の方は，2016年9月24日（土）までに，研究代表者（菊池）宛に件名「mla2016」として e-mail でご連絡ください．なお，本研究集会は研究交流を目的とするものですが，学部学生を含む学生の方の研究集会および懇親会への参加を歓迎します．午前中の講演は全て日本語です．ご興味をお持ちの方はご遠慮なくご参加ください．菊池誠記 RIMS研究集会　数学基礎論とその応用日時：2016年9月26日(月)11:00 ~ 9月29日(木)15:00 場所：京都大学数理解析研究所111室研究代表者：菊池誠(神戸大)mkikuchi(a)kobe-u.ac.jp プログラム： 9月26日(月) 11:00-11:50 宮元忠敏(南山大) 集合論で試される構造と構成のいくつか 13:30-14:20 Joel David Hamkins(CUNY) The Modal Logic of Set-Theoretic Potentialism 14:30-15:20 樋口幸治郎(日大工) Computably Represented Structures 15:30-16:20 竹内耕太(筑波大) Properties Characterized by Generalized Indiscernible 9月27日(火) 10:00-10:50 新井敏康(千葉大) 角田先生, 証明論を分かって下さい 11:00-11:50 板井昌典(東海大) 1980年代半ば,米国中西部のモデル理論,そして未来-モデル理論賛歌 13:30-14:20 Frank Wager (Lion 大) Recent Interactions between Model Theory and Combinatorics 14:30-15:20 横山啓太(JAIST) On the Proof-Theoretic Strength of Ramsey's Theorem for Pairs 15:30-16:20 丸山善宏(京大) Dynamics of Duality: How Duality Emerges, Changes, and Breaks 9月28日(水) 10:00-10:50 向井国昭(慶応大) Barwiseのモデル論的意味論の周辺と抽象設計学 11:00-11:50 金井康雄(大和大) 公理的集合論の一角を彷徨って 13:30-14:20 Bakh Khoussainov(Auckland 大/京都大) Computably Enumerable Structures: Domain Dependence 14:30-15:20 星野直彦(京都大) Geometry of Interaction and Higher Order Functions 15:30-16:20 Diego Mejia(静岡大) Several Values in Cichon's Diagram 9月29日(木) 10:00-10:50 佐藤洋祐(東理大) 限量子記号消去アルゴリズムとその計算の現状について 11:00-11:50 隈部正博(放送大) Generic Sets の Turing Degrees について 13:30-14:20 Philip Welch(Bristol 大) Generalised Squares and Higher Stationarity

1 0

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

16 Sep '16

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

1 0

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

16 Sep '16

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

1 0

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

15 Sep '16

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

1 0

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

14 Sep '16

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

1 0

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

13 Sep '16

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

1 0

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

09 Sep '16

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

1 0

JAIST Logic Seminar Series
by Hajime Ishihara 09 Sep '16

09 Sep '16

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

1 0

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

07 Sep '16

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

1 0

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Logic-ml