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

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

06 Sep '16

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

1 0

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

06 Sep '16

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

1 0

PEPM 2017: Deadline extension
by Ryosuke SATO 05 Sep '16

05 Sep '16

皆様、（複数受け取られた場合はご容赦ください。）東京大学の佐藤亮介です。 PEPM 2017 の締め切りが 9/30 まで延長されました。新しい日程は次の通りです。 For Regular Research Papers and Short Papers: * Abstract submission : Tuesday 27th September 2016 * Paper submission : Friday 30th September 2016 * Author notification : Friday 4th November 2016 * Camera ready : Monday 28th November 2016 For Posters: * Poster submission : Tuesday 8th November 2016 * Author notification : Friday 18th November 2016 * Camera ready : Monday 28th November 2016 論文の締め切りまでまだ1ヶ月近くありますので、是非、投稿をご検討ください。 -- 東京大学大学院情報理工学系研究科佐藤亮介 ryosuke(a)kb.is.s.u-tokyo.ac.jp ------------------------------------------------------------------- FINAL CALL FOR PAPERS Workshop on PARTIAL EVALUATION AND PROGRAM MANIPULATION (PEPM 2017) NEWS: Deadline extension to 30th September (see below) NEWS: Keynote talk by Neil Jones, DIKU (see below). http://conf.researchr.org/home/PEPM-2017 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. Specifically, PEPM 2017 will include practical applications of program transformations such as refactoring tools, and practical implementation techniques such as rule-based transformation systems. In addition, the scope of PEPM covers manipulation and transformations of program and system representations such as structural and semantic models that occur in the context of model-driven development. In order to maintain the dynamic and interactive nature of PEPM and to encourage participation by practitioners, we also solicit submissions of short papers, including tool demonstrations, and of posters. 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 categories and guidelines ------------------------------------ Three kinds of submissions will be accepted: Regular Research Papers, Short Papers and Posters. * Regular Research Papers should describe new results, and will be judged on originality, correctness, significance and clarity. Regular research papers must not exceed 12 pages in ACM Proceedings style (including appendix). * Short Papers may include tool demonstrations and presentations of exciting if not fully polished research, and of interesting academic, industrial and open-source applications that are new or unfamiliar. Short papers must not exceed 6 pages in ACM Proceedings style (including appendix). * 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. At least one author of each accepted contribution must attend the workshop and present the work. In the case of tool demonstration papers, a live demonstration of the described tool is expected. Suggested topics, evaluation criteria, and writing guidelines for both research tool demonstration papers will be made available on the PEPM 2017 web site. Student participants with accepted 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 and special issue ----------------------------- All accepted papers, short papers and posters included, will appear in formal proceedings published by ACM Press. Accepted papers will be included in the ACM Digital Library. Authors of selected papers from PEPM 2016 and PEPM 2017 will also be invited to expand their papers for publication in a special issue of the journal Computer Languages, Systems and Structures (COMLAN, Elsevier). 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 Best paper award ---------------- PEPM 2017 continues the tradition of a Best Paper award. The winner will be announced at the workshop. Submission ---------- Papers 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 --------------- UPDATE: following feedback from potential authors, we have extended the PEPM submission dates by two weeks to avoid clashes with other events. The new deadlines are consequently strict, and there will be no further extensions. For Regular Research Papers and Short Papers: * Abstract submission : Tuesday 27th September 2016 * Paper submission : Friday 30th September 2016 * Author notification : Friday 4th November 2016 * Camera ready : Monday 28th November 2016 For Posters: * Poster submission : Tuesday 8th November 2016 * Author notification : Friday 18th November 2016 * Camera ready : Monday 28th November 2016 PEPM workshop: * 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

CfP: FTSCS 2016 deadline extension
by Takashi Kitamura 01 Sep '16

01 Sep '16

--------------------------------------------------------------------- Call for Papers FTSCS 2016 5th International Workshop on Formal Techniques for Safety-Critical Systems Tokyo, November 14/15, 2016 (satellite workshop of ICFEM 2016) http://www.ftscs.org --------------------------------------------------------------------- *** Deadline extension: Final submission deadline September 11 *** *** Science of Computer Programming special issue *** *** Springer CCIS proceedings *** Aims and Scope: There is an increasing demand for using formal methods to validate and verify safety-critical systems in fields such as power generation and distribution, avionics, automotive systems, and medical systems. In particular, newer standards, such as DO-178C (avionics), ISO 26262 (automotive systems), IEC 62304 (medical devices), and CENELEC EN 50128 (railway systems), emphasize the need for formal methods and model-based development, thereby speeding up the adaptation of such methods in industry. The aim of this workshop is to bring together researchers and engineers who are interested in the application of formal and semi-formal methods to improve the quality of safety-critical computer systems. FTSCS strives to promote research and development of formal methods and tools for industrial applications, and is particularly interested in industrial applications of formal methods. Specific topics include, but are not limited to: * case studies and experience reports on the use of formal methods for analyzing safety-critical systems, including avionics, automotive, medical, railway, and other kinds of safety-critical and QoS-critical systems * methods, techniques and tools to support automated analysis, certification, debugging, etc., of complex safety/QoS-critical systems * analysis methods that address the limitations of formal methods in industry (usability, scalability, etc.) * formal analysis support for modeling languages used in industry, such as AADL, Ptolemy, SysML, SCADE, Modelica, etc. * code generation from validated models. The workshop will provide a platform for discussions and the exchange of innovative ideas, so submissions on work in progress are encouraged. Submission: We solicit submissions reporting on: A- original research contributions (15 pages max, LNCS format); B- applications and experiences (15 pages max, LNCS format); C- surveys, comparisons, and state-of-the-art reports (15 pages max, LNCS); D- tool papers (5 pages max, LNCS format); E- position papers and work in progress (5 pages max, LNCS format) related to the topics mentioned above. All submissions must be original, unpublished, and not submitted concurrently for publication elsewhere. Paper submission is done via EasyChair at https://easychair.org/conferences/?conf=ftscs2016. The final version of the paper must be prepared in LaTeX, adhering to the LNCS format available at http://www.springer.com/computer/lncs?SGWID=0-164-6-793341-0. Publication: All accepted papers will appear in the pre-proceedings of FTSCS 2016. Accepted papers in the categories A-D above will appear in the workshop proceedings that will be published as a volume in Springer's CCIS series. The authors of a selected subset of accepted papers will be invited to submit extended versions of their papers to appear in a special issue of the Science of Computer Programming journal. Important dates: Submission deadline: September 4, 2016; extended to September 11, 2016 Notification of acceptance: October 7, 2016 Workshop: November 14/15, 2016 Venue: Tokyo, Japan Program chairs: Cyrille Artho AIST, Japan and KTH, Sweden Peter Olveczky University of Oslo, Norway Program committee: Etienne Andre University Paris 13, France Toshiaki Aoki JAIST, Japan Cyrille Artho AIST, Japan and KTH, Sweden Kyungmin Bae Pohang University of Science and Technology, Korea Eun-Hye Choi AIST, Japan Alessandro Fantechi University of Florence and ISTI-CNR, Pisa, Italy Bernd Fischer Stellenbosch University, South Africa Osman Hasan National University of Sciences & Technology, Pakistan Klaus Havelund NASA JPL, USA Jerome Hugues Institute for Space and Aeronautics Engineering, France Marieke Huisman University of Twente, The Netherlands Ralf Huuck Synopsys, Australia Fuyuki Ishikawa National Institute of Informatics, Japan Takashi Kitamura AIST, Japan Alexander Knapp Augsburg University, Germany Thierry Lecomte ClearSy System Engineering, France Yang Liu Nanyang Technological University, Singapore Robi Malik University of Waikato, New Zealand Frederic Mallet INRIA Sophia Antipolis, France Roberto Nardone University of Napoli "Federico II", Italy Vivek Nigam Federal University of ParaÃba, Brazil Thomas Noll RWTH Aachen University, Germany Kazuhiro Ogata JAIST, Japan Peter Olveczky University of Oslo, Norway Charles Pecheur Universite catholique de Louvain, Belgium Markus Roggenbach Swansea University, UK Ralf Sasse ETH Zurich, Switzerland Martina Seidl Johannes Kepler University, Austria Oleg Sokolsky University of Pennsylvania, USA Sofiene Tahar Concordia University, Canada Carolyn Talcott SRI International, USA Tatsuhiro Tsuchiya Osaka University, Japan Andras Voros Budapest University of Technology and Economics, Hungary Chen-Wei Wang State University of New York (SUNY), Korea Alan Wassyng McMaster University, Canada Michael Whalen University of Minnesota, USA Huibiao Zhu East China Normal University, China -- Takashi KITAMURA t.kitamura(a)aist.go.jp http://staff.aist.go.jp/t.kitamura/ Tel: +81-72-751-9633, AIST internal: *33-272-79633

1 0

Fwd: [hscc] 2017 Hybrid Systems: Computation and Control (HSCC) -- Call for Papers
by Ichiro Hasuo 31 Aug '16

31 Aug '16

みなさま，東京大学の蓮尾です．物理情報システム分野の一大イベント CPS Week （来年はアメリカ開催です）のメイン会議の一つ， HSCC の論文募集をお送りします．コミュニティとしては，主にプログラム検証・システム検証の人たちと，制御理論の人たちが，協力して研究を行っている印象です．よろしければぜひ，論文投稿や参加をご検討ください．どうかよろしくお願いいたします．蓮尾一郎 http://www-mmm.is.s.u-tokyo.ac.jp/~ichiro/ ======= 20th International Conference on Hybrid Systems: Computation and Control (HSCC) April 18-21, 2017, Pittsburgh, Pennsylvania, USA URL: http://hscc2017.ece.illinois.edu/ Important dates Paper Submission deadline: October 13, 2016 (firm, 11:59 pm UTC-12) Notifications: December 20, 2016 Demo/poster submission: TBA Camera-ready: February 17, 2017 Conference dates: April 18-21, 2017 Conference Scope HSCC 2017 is the 20th in a series of conferences on all aspects of hybrid systems. It is dedicated to advancing design and analysis techniques that bridge control theory and computer science, and is expanding to new domains in security and privacy and in systems biology. The conference covers the range from theoretical results to practical applications and experiences in cyber-physical systems (CPS), mixed signal circuits, robotics, infrastructure networks, and biological models. Topics of interest include, but are not limited to, the following subjects: * Mathematical foundations, computability and complexity * Modeling paradigms and techniques * Design, synthesis, planning, and control * Analysis, verification, validation, and testing * Programming and specification languages * Network science and control over networks * Security and privacy in cyberphysical systems * Software tools * Applications and case studies HSCC 2017 will be part of the ninth Cyber Physical Systems Week (CPS Week), and co- located with the International Conference on Cyber-Physical Systems (ICCPS), Information Processing in Sensor Networks (IPSN), the Real-Time and Embedded Technology and Applications Symposium (RTAS), Conference on Internet-of-Things Design and Implementation (IOTDI), and related workshops. Regular papers: Submissions should present unpublished original research, not under review elsewhere. Maximum 10 pages in 10pt, two-column ACM format. This year we will enforce a light double-blind reviewing process; the conference webpage will have more details. Paper submissions should be preceded by an abstract (date TBA). Authors of distinguished papers may be invited to submit an extended version of their work for possible publication in a Special issue of a leading journal. A Best Student Paper Award will be presented to the author of the best paper written solely or primarily by a student. Tool and case study papers: Tool Papers should describe an implemented tool and its novelty. Maximum 6 pages in the 10pt, two-column ACM format. Demo/posters: Demo/poster descriptions are used for selecting contributions for demo/poster session, and will not be published in the proceedings. Maximum 2 pages, ACM format. Title should begin with “Demo (Poster):”. Descriptions should be submitted to the “Demonstrations and Posters” track at the submission website. Submission website for papers: https://easychair.org/conferences/?conf=hscc17 Repeatability evaluation: Authors of accepted papers will be invited to participate in an optional repeatability evaluation process after the camera-ready submission. Papers that pass will receive the “artifact evaluated” badge and there will be a Best RE Award. The official publication date may be up to two weeks before the conference. Committees for HSCC 2017 Program Committee Chairs Goran Frehse, Univ. Grenoble Alpes-Verimag Sayan Mitra, Univ. of Illinois at Urbana-Champaign Publicity Chair Necmiye Ozay, Univ. of Michigan Program Committee Alessandro Abate, University of Oxford Erika Abraham, RWTH Aachen Matthias Althoff, TU München Saurabh Amin, MIT Murat Arcak, UC Berkeley Shun-Ichi Azuma, Kyoto Univ. Christel Baier, TU Dresden Hamsa Balakrishnan, MIT Ezio Bartocci, TU Wien Calin Belta, Boston Univ. Sergiy Bogomolov, IST Austria Alessandro Cimatti, Fondazione Bruno Kessler Alessandro D'Innocenzo, Univ. of L'Aquila Thao Dang, VERIMAG, France Anupam Datta, CMU Jyotirmoy Deshmukh, Toyota Arvind Easwaran, Nanyang Tech. Univ. Georgios Fainekos, Arizona State Univ. Lu Feng, Univ. of Virginia Martin Fränzle, Carl von Ossietzky Univ. Oldenburg Sicun Gao, MIT Antoine Girard, Laboratoire des Signaux et Sys. CNRS Ichiro Hasuo, Univ. of Tokyo Franjo Ivancic, Google Taylor T Johnson, Vanderbilt Univ. James Kapinski, Toyota Hadas Kress-Gazit, Cornell University Marta Kwiatkowska, University of Oxford Mircea Lazar, Eindhoven Univ. of Technology Jun Liu, Univ. of Waterloo Daniele Magazzeni, King's College London Manuel Mazo Jr., TU Delft Ian Mitchell, Univ. of British Columbia Meeko Oishi, Univ. of New Mexico Necmiye Ozay, Univ. of Michigan André Platzer, CMU Vinayak Prabhu, MPI-SWS Maria Prandini, Politecnico di Milano Akshay Rajhans, MathWorks S Ramesh, General Motors Grigore Rosu, Univ. of Illinois at Urbana-Champaign Indranil Saha, IIT Kanpur Ricardo Sanfelice, Univ. of Arizona Scott Smolka, Stony Brook Univ. Oleg Sokolsky, Univ. of Pennsylvania Herbert Tanner, Univ. of Delaware Ashish Tiwari, SRI Ufuk Topcu, Univ. of Texas at Austin Jana Tumova, Royal Institute of Technology Ram Vasudevan, Univ. of Michigan Steering Committee Rajeev Alur, University of Pennsylvania Werner Damm, OFFIS John Lygeros, ETH Zurich Oded Maler, Verimag Paulo Tabuada, UCLA Claire Tomlin, UC Berkeley

1 0

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

29 Aug '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/

1 0

数学基礎論サマースクールの案内２
by Hirotaka Kikyo 24 Aug '16

24 Aug '16

各位神戸大学の桔梗です。数学基礎論サマースクールを次の要領で開催いたします。今年のテーマはモデル理論です。大勢のご参加をお待ちしております。期間：2016年9月5日（月）から2016年9月7日（水）場所：早稲田大学西早稲田キャンパス５２号館１０１教室〒169-0072 東京都新宿区大久保３丁目４−１スケジュールをほぼ確定いたしました。次のリンクをご覧ください。 https://sites.google.com/site/logicsummerschool2016/ 現在の内容は次の通りです。数学基礎論サマースクール2016 日本数学会数学基礎論および歴史分科会の運営委員会でテーマを決めて開催されている研究集会です。2016年はモデル理論がテーマです。今回は主要と思われるトピックスから４種類を選んで紹介いたします。最初にモデル理論の入門にあたる話題を話してもらいます。初日は午前中から、最終日も午後まで行う予定です。なお、一般講演の募集は行いません。 *期間：2016年9月5日（月）から2016年9月7日（水）場所：早稲田大学西早稲田キャンパス５２号館１０１教室* *〒169-0072 東京都新宿区大久保３丁目４−１世話人：* 桔梗宏孝（神戸大学） *問い合わせ先： kikyo(a)kobe-u.ac.jp <kikyo(a)kobe-u.ac.jp> (桔梗宏孝)* 江田勝哉(早稲田大学) 薄葉季路(早稲田大学) * テーマ：* *モデル理論入門担当：坪井明人（筑波大学）* *順序極小理論と数論担当：板井昌典（東海大学）* *付値体のモデル理論の系譜担当：桔梗宏孝（神戸大学）フルショフスキの融合法担当：池田宏一郎（法政大学）* *スケジュール（案）* *9月5日月曜日* 10:00-10:10 注意事項 10:10-11:00 モデル理論入門（坪井明人） 11:10-12:00 モデル理論入門（坪井明人）（昼休み） 14:00-14:50 モデル理論入門（坪井明人） 15:00-15:50 順序極小理論と数論（板井昌典） 16:00-16:50 順序極小理論と数論（板井昌典） *9月6日火曜日*09:00-09:50 付値体のモデル理論の系譜（桔梗宏孝） 10:00-10:50 付値体のモデル理論の系譜（桔梗宏孝） 11:00-11:50 フルショフスキの融合法（池田宏一郎）（昼休み） 14:00-14:50 フルショフスキの融合法（池田宏一郎） 15:00-15:50 順序極小理論と数論（板井昌典） 16:00-16:50 順序極小理論と数論（板井昌典） *9月7日水曜日* 09:00-09:50 フルショフスキの融合法（池田宏一郎） 10:00-10:50 フルショフスキの融合法（池田宏一郎） 11:00-11:50 付値体のモデル理論の系譜（桔梗宏孝） 12:00-12:50 付値体のモデル理論の系譜（桔梗宏孝）（終了） *概要(案)モデル理論入門（坪井明人）* 1. 言語，構造，モデル 2. コンパクト性定理 3. 大きなモデルと小さなモデルの構成 4. 不安定な理論 *順序極小理論と数論（板井昌典）* 1. 順序極小構造と順序極小理論, RCF について 2. Monotonicity Theorem, Cell Decomposition 3. Wilkie の結果(R_exp に関するもの） 4. Pilla-Wilkie Counting Theorem *付値体のモデル理論の系譜（桔梗宏孝）* 1. Ax-Kochen-Ersovの定理 (p進閉体と有限素体係数のローラン級数体の類似性) 2. MacintireのQE, Cell-Decomposition, ポアンカレ級数の有理性 3. Denef-PasのQEと Igusa Zeta関数の有理性 4. Motivic Integration

1 0

Kyoto Workshop on Dialetheism and Paraconsistencyのご案内
by Hitoshi Omori 22 Aug '16

22 Aug '16

Kyoto Workshop on Dialetheism and Paraconsistencyのご案内 (重複してお受け取りの際はご容赦ください。) 京都大学の大森仁です。以下の通り矛盾許容型論理とその哲学的動機として知られている真矛盾主義に関するワークショップを開催いたします。題目・概要・プログラムなどの詳細は9月中旬までにウェブサイトにて更新の予定です。 ------------------------------------- Kyoto Workshop on Dialetheism and Paraconsistency 【日時】2016年10月9日、10日【場所】京都大学吉田泉殿【ウェブサイト】https://sites.google.com/site/hitoshiomori/home/workshops/kwdp2016 【話者】(アルファベット順) Franz Berto (Amsterdam) Colin Caret (Seoul) Filippo Casati (St. Andrews) Yasuo Deguchi (Kyoto) Naoya Fujikawa (Tokyo) Ryosuke Igarashi (Kyoto) Takuro Onishi (Kyoto) Adam Prenosil (Prague) Daniel Skurt (Bochum) Zach Weber (Otago) Timo Weiss (Bonn) Maiko Yamamori (Kyoto) 【世話人】出口康夫・大森仁 ------------------------------------- 会場及び軽食の準備の都合上、参加を希望される場合は hitoshiomori[at]gmail[dot]com までご一報いただければ幸いです。どうぞよろしくお願いいたします。大森仁

1 0

JAIST Logic Seminar Series
by Hajime Ishihara 22 Aug '16

22 Aug '16

皆様ルートヴィヒ・マクシミリアン大学ミュンヘンのJosef Berger先生、およびスワンジー大学のAnton Setzer先生・Bashar Igriedさんの講演のお知らせです。どうぞふるってご参加ください。問合せ先：石原　哉北陸先端科学技術大学院大学情報科学系 e-mail: ishihara(a)jaist.ac.jp ----------------------------------------------- * JAIST Logic Seminar Series * * The lectures below are 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: Tuesday 6 September, 2016, 13:30-17:00 Place: JAIST, Lecture room I2 (Access: http://www.jaist.ac.jp/english/location/access.html) *LECTURE 1* Speaker: Josef Berger (Ludwig-Maximilians-Universität München) Title: The fan theorem and convexity (joint work with Gregor Svindland) Abstract: The fan theorem is the following statement: (FAN) Let B be a decidable set of finite binary sequences. Assume that every infinite binary sequence has an initial part that belongs to B. Then there exist an N such that every infinite binary sequence has an initial part of length smaller than N that belongs to B. This axiom plays an important role in Intuitionism, a philosophy of mathematics that was introduced by the Dutch mathematician L.E.J. Brouwer. We work in constructive mathematics in the tradition of Errett Bishop. Here, the fan theorem is neither provable nor falsifiable. Many theorems of analysis are equivalent to the fan theorem. One example for such a theorem is: (POS) Every positive-valued uniformly continuous function on the unit interval has positive infimum. In our paper 'Convexity and constructive infamy’ we have shown that, under the additional condition of convexity of the function, POS is constructively valid. In this talk, we discuss to which extent this gives rise to a notion of 'convex bars' and a corresponding constructively valid 'convex fan theorem'. *LECTURE 2* Speaker: Anton Setzer and Bashar Igried (Swansea University) Title: Coinductive Reasoning in Dependent Type Theory - Copatterns, Objects, Processes (part on Processes joint work with Bashar Igried) Abstract: When working in logic in computer science, one is very often confronted with bisimulation. The reason for its importance is that in computer science, one often reasons about interactive or concurrent programs. Such programs can have infinite execution paths, and therefore correspond to coinductive data types. The natural equality on coinductive data types is bisimulation. Proofs of bisimulation form one of the main principles for reasoning about coinductive data types. However, bisimulation is often very difficult to understand and to teach. This is in contrast to the principle of induction, where there exists a well established tradition of carrying out proofs by induction. One goal of this talk is to demonstrate that one can reason about coinductive data types in a similar way as one can reason inductively about inductive data types. Reasoning about inductive data types can be done by pattern matching. For instance for reasoning about natural numbers one makes a case distinction on whether the argument is 0 or a successor. For coinductive data types the dual is copattern matching, which is essentially a case distinction on the observations one can make for a coinductively defined set. For instance, streams have observations head and tail, and one can introduce a stream by determining its head and its tail. We then look at examples of the use of coinductive data types. One is the notion of an object, as it occurs in object-oriented program. Objects are defined by their method calls, which are observations, so they are defined coinductively. The final example will be the representation of processes in dependent type theory, where we will refer to the process algebra CSP.

1 0

SLACS2016のご案内
by sasaki 22 Aug '16

22 Aug '16

みなさま　「記号論理と情報科学研究集会（SLACS）」のプログラム(暫定版)を http://www.seto.nanzan-u.ac.jp/~sasaki/SLACS2016.html におきました．若干の余裕がありますので，　　　　　　8月21日まで講演申込を受け付けます．詳細は，上記URLをご確認ください．　プログラム等について，ご指摘・ご意見がある場合は，世話人(sasaki(a)nanzan-u.ac.xn--jp)-u63b4b3ai1gqet146cnwrdnb3b. 世話人　南山大学　佐々木克巳 sasaki <sasaki(a)nanzan-u.ac.jp>

1 1

International Symposium on Computability and Complexityのご案内
by Kenshi Miyabe 20 Aug '16

20 Aug '16

皆様 (複数受け取られた場合はご容赦下さい) シンポジウムとサマースクールの案内を転送いたします．宮部 ---------- Forwarded message ---------- International Symposium on Computability and Complexity (in honour of Rod Downey's 60th birthday), and Summer School in Mathematical Logic In early 2017, Victoria University of Wellington will be hosting a Computability and Complexity Symposium. These areas have seen significant development in recent years. The purpose of this symposium is to bring together a wide cross-section of researchers in the area, from leading researchers to graduate students, to discuss these developments and future directions. The symposium will take place between the 5th and 8th of January 2017 at the town of Raumati, a short drive from Wellington. For details and updates please see http://sms.victoria.ac.nz/Events/CCS2017/WebHome After the symposium, a summer school in mathematical logic will take place in Napier, between the Monday 9th and Saturday 14th of January 2017. The topic is mathematical logic and computability. We plan to have five tutorial series, the level aimed at graduate students. The speakers will be: • Denis Hirschfeldt (Chicago) • Jack Lutz (Iowa State) • Maryanthe Malliaris (Chicago) • Antonio Montalban (UC Berkeley) • Hugh Woodin (Harvard) Details can be found at http://sms.victoria.ac.nz/Events/NZMRI2017/WebHome We anticipate receiving NSF funding in early October to help cover the travel cost of US-based researchers and students. To apply for this funding please email Peter Cholak, at cholak(a)nd.edu, by October 15. We are particularly interested having women, minorities, students and postdocs apply. We are working on getting ASL sponsorship. Students also can apply to the ASL for travel support. Please share with your colleagues and students and postdocs. Sorry if you received multiple copies of this. -- Kenshi Miyabe email (research) : research(a)kenshi.miyabe.name email (other) : miyabe(a)meiji.ac.jp Senior Assistant Professor Department of Mathematics School of Science and Technology Meiji University Tel: +81-44-934-7460

1 0

CTFM2016のご案内
by Makoto Fujiwara 19 Aug '16

19 Aug '16

皆様 (複数受け取られた場合はご容赦下さい) 早稲田大学の藤原誠です。以下の要領で研究集会 Computability Theory and Foundations of Mathematics 2016 (2016年9月20日(火)～9月21日(水)、早稲田大学国際会議場) を開催いたします。講演を希望される方は8月31日までに以下に沿って講演要旨をお送り下さい。 (締切日が迫ってからの連絡となってしまい申し訳ありません。) http://www.sendailogic.com/CTFM2016/submission.html 本研究集会への参加は自由ですが、20日夜の懇親会に参加される方は9月12日までに以下より参加登録をお願いいたします。準備の都合上、懇親会に参加されない方も事前に参加登録をしていただけると助かります。 http://www.sendailogic.com/CTFM2016/registration.html 詳しくは下記ホームページをご覧ください。 http://www.sendailogic.com/CTFM2016/ 本研究集会に関するお問い合わせは以下へお願いいたします。 ctfm2016[at]fastmail.com どうぞよろしくお願いいたします。 ============================================================== Computability Theory and Foundations of Mathematics 2016 Waseda University, Tokyo, Japan, September 20 - 21, 2016 http://www.sendailogic.com/CTFM2016/ ============================================================== Computability Theory and Foundations of Mathematics (CTFM) aims to develop computability theory and logical foundations of Mathematics. The scope involves the topics Computability Theory, Reverse Mathematics, Nonstandard Analysis, Proof Theory, Set Theory, Philosophy of Mathematics, Constructive Mathematics, Theory of Randomness and Computational Complexity Theory. This is the sixth conference of the CTFM conference series: http://www.jaist.ac.jp/CTFM/CTFM_SERIES/ This conference is supported by the Waseda Insitute for Advanced Study and JSPS KAKENHI Grant Numbers JP26540001 and JP15H03634. ------------------------------------------------------------------------------------------------------------------------- Invited speakers: • David Belanger (National University of Singapore) • Chi Tat Chong (National University of Singapore) • Daisuke Ikegami (Tokyo Denki University) • Wei Li (National University of Singapore) • Kenshi Miyabe (Meiji University) • Paul Shafer (Ghent University) • Frank Stephan (National University of Singapore) • Philip Welch (University of Bristol) • Guohua Wu (Nanyang Technological University) • Takeshi Yamazaki (Tohoku University) • Yang Yue (National University of Singapore) ------------------------------------------------------------------------------------------------------------------------- Submission deadline for presentations: August 31, 2016 ------------------------------------------------------------------------------------------------------------------------- Registration deadline: September 12, 2016. (It will still be possible to register for the conference after the deadline, but in that case the participant cannot attend the banquet. The banquet will be held on September 20 (18:30-20:30), at the same place as the conference venue.) ------------------------------------------------------------------------------------------------------------------------- Organising Committee: Makoto Fujiwara (Waseda University, co-chair) Florian Pelupessy (Tohoku University) Kazuyuki Tanaka (Tohoku University, co-chair) Toshimichi Usuba (Waseda University) Keita Yokoyama (JAIST) ============================================ 藤原誠 (Makoto Fujiwara) 早稲田大学高等研究所 (Waseda Institute for Advanced Study, Waseda University) E-mail: makoto_fujiwara(a)aoni.waseda.jp ============================================ ============================================ Makoto Fujiwara, Waseda Institute for Advanced Study, Waseda University E-mail: makoto_fujiwara(a)aoni.waseda.jp ============================================

1 0

CTFM2016のご案内
by Makoto Fujiwara 19 Aug '16

19 Aug '16

皆様早稲田大学の藤原誠です。以下の要領で研究集会 Computability Theory and Foundations of Mathematics 2016 (2016年9月20日(火)～9月21日(水)、早稲田大学国際会議場) を開催いたします。講演を希望される方は8月31日までに以下に沿って講演要旨をお送り下さい。 (締切日が迫ってからの連絡となってしまい申し訳ありません。) http://www.sendailogic.com/CTFM2016/submission.html 本研究集会への参加は自由ですが、20日夜の懇親会に参加される方は9月12日までに以下より参加登録をお願いいたします。準備の都合上、懇親会に参加されない方も事前に参加登録をしていただけると助かります。 http://www.sendailogic.com/CTFM2016/registration.html 詳しくは下記ホームページをご覧ください。 http://www.sendailogic.com/CTFM2016/ 本研究集会に関するお問い合わせは以下へお願いいたします。 ctfm2016[at]fastmail.com どうぞよろしくお願いいたします。 ============================================================== Computability Theory and Foundations of Mathematics 2016 Waseda University, Tokyo, Japan, September 20 - 21, 2016 http://www.sendailogic.com/CTFM2016/ ============================================================== Computability Theory and Foundations of Mathematics (CTFM) aims to develop computability theory and logical foundations of Mathematics. The scope involves the topics Computability Theory, Reverse Mathematics, Nonstandard Analysis, Proof Theory, Set Theory, Philosophy of Mathematics, Constructive Mathematics, Theory of Randomness and Computational Complexity Theory. This is the sixth conference of the CTFM conference series: http://www.jaist.ac.jp/CTFM/CTFM_SERIES/ This conference is supported by the Waseda Insitute for Advanced Study and JSPS KAKENHI Grant Numbers JP26540001 and JP15H03634. ------------------------------------------------------------------------------------------------------------------------- Invited speakers: • David Belanger (National University of Singapore) • Chi Tat Chong (National University of Singapore) • Daisuke Ikegami (Tokyo Denki University) • Wei Li (National University of Singapore) • Kenshi Miyabe (Meiji University) • Paul Shafer (Ghent University) • Frank Stephan (National University of Singapore) • Philip Welch (University of Bristol) • Guohua Wu (Nanyang Technological University) • Takeshi Yamazaki (Tohoku University) • Yang Yue (National University of Singapore) ------------------------------------------------------------------------------------------------------------------------- Submission deadline for presentations: August 31, 2016 ------------------------------------------------------------------------------------------------------------------------- Registration deadline: September 12, 2016. (It will still be possible to register for the conference after the deadline, but in that case the participant cannot attend the banquet. The banquet will be held on September 20 (18:30-20:30), at the same place as the conference venue.) ------------------------------------------------------------------------------------------------------------------------- Organising Committee: Makoto Fujiwara (Waseda University, co-chair) Florian Pelupessy (Tohoku University) Kazuyuki Tanaka (Tohoku University, co-chair) Toshimichi Usuba (Waseda University) Keita Yokoyama (JAIST) ============================================ 藤原誠 (Makoto Fujiwara) 早稲田大学高等研究所 (Waseda Institute for Advanced Study, Waseda University) E-mail: makoto_fujiwara(a)aoni.waseda.jp ============================================

1 0

Call for Participation: Automated Technology for Verification and Analysis (ATVA) 2016
by Takashi Kitamura 18 Aug '16

18 Aug '16

---------------------------------------------------------------------- CALL FOR PARTICIPATION: ATVA 2016 14th International Symposium on Automated Technology for Verification and Analysis (ATVA) 2016 Chiba, Japan, October 17-20th, 2016 http://atva2016.gforge.inria.fr/ ---------------------------------------------------------------------- The purpose of ATVA is to promote research on theoretical and practical aspects of automated analysis, verification and synthesis by providing a forum for interaction between the regional and the international research communities and industry in the field. The previous events were held in Taiwan - 2003-5, Beijing - 2006, Tokyo - 2007, Seoul - 2008, Macao - 2009, Singapore - 2010, Taiwan - 2011, Thiruvananthapuram - 2012, Hanoi - 2013, Sydney - 2014, and Shanghai - 2015. Venue Chiba, Japan Main conference: Mitsui Garden Hotel Tutorials: Chiba University, Nishi-Chiba campus (one station away from hotel) Scope * Formalisms for modeling hardware, software and embedded systems * Specification and verification of finite-state, infinite-state and parameterized systems * Program analysis and software verification * Analysis and verification of hardware circuits, systems-on-chip and embedded systems * Analysis of real-time, hybrid, priced/weighted and probabilistic systems * Deductive, algorithmic, compositional, and abstraction/refinement techniques for analysis and verification * Analytical techniques for safety, security, and dependability * Testing and runtime analysis based on verification technology * Analysis and verification of parallel and concurrent hardware/software systems * Verification in industrial practice * Applications and case studies Keynotes (Oct. 17-19) Masahiro Fujita: Unification of Synthesis and Verification in Topologically Constrained Logic Design Javier Esparza: From LTL to Limit-Deterministic Automata Tevfik Bultan: Side Channel Analysis Using a Model Counting Constraint Solver and Symbolic Execution Tutorials (Oct. 20) Masahiro Fujita: Synthesizing and completely testing hardware based on templates through small numbers of test patterns Javier Esparza: Verification of population protocols Tevfik Bultan: String Analysis for Vulnerability Detection and Repair Important Dates: Early registration: August 31 (Japan Standard Time) Conference: October 17-20 Programme Committee Co-Chairs Cyrille Artho (AIST, Japan and KTH, Sweden) Axel Legay (INRIA, France) Doron Peled (Bar Ilan University, Israel) Publicity Chair Takashi Kitamura (AIST, Japan) Local Chairs Mitsuharu Yamamoto (Chiba University, Japan) Yoshinori Tanabe (Tsurumi University, Japan) -- Takashi KITAMURA t.kitamura(a)aist.go.jp http://staff.aist.go.jp/t.kitamura/ Tel: +81-72-751-9633, AIST internal: *33-272-79633 -- Takashi KITAMURA t.kitamura(a)aist.go.jp http://staff.aist.go.jp/t.kitamura/ Tel: +81-72-751-9633, AIST internal: *33-272-79633

1 0

PEPM 2017: Second Call for Papers
by Ryosuke SATO 17 Aug '16

17 Aug '16

皆様、（複数受け取られた場合はご容赦ください。）東京大学の佐藤亮介です。来年1月に POPL 併設で開催される PEPM 2017 の 2nd CFP をお送りいたします。日程は次の通りです。 For Regular Research Papers and Short Papers: * Abstract submission : Tuesday 13th September 2016 * Paper submission : Friday 16th September 2016 * Author notification : Monday 24th October 2016 * Camera ready : Monday 28th November 2016 For Posters: * Poster submission : Sunday 30th October 2016 * Author notification : Friday 10th November 2016 * Camera ready : Monday 28th November 2016 Keynote talk は、Neil Jones 氏（DIKU）に決まりました。是非，投稿をご検討ください。 -- 東京大学大学院情報理工学系研究科佐藤亮介 ryosuke(a)kb.is.s.u-tokyo.ac.jp ------------------------------------------------------------------- SECOND CALL FOR PAPERS Workshop on PARTIAL EVALUATION AND PROGRAM MANIPULATION (PEPM 2017) NEWS: Keynote talk by Neil Jones, DIKU (see below). http://conf.researchr.org/home/PEPM-2017 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. Specifically, PEPM 2017 will include practical applications of program transformations such as refactoring tools, and practical implementation techniques such as rule-based transformation systems. In addition, the scope of PEPM covers manipulation and transformations of program and system representations such as structural and semantic models that occur in the context of model-driven development. In order to maintain the dynamic and interactive nature of PEPM and to encourage participation by practitioners, we also solicit submissions of short papers, including tool demonstrations, and of posters. 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 categories and guidelines ------------------------------------ Three kinds of submissions will be accepted: Regular Research Papers, Short Papers and Posters. * Regular Research Papers should describe new results, and will be judged on originality, correctness, significance and clarity. Regular research papers must not exceed 12 pages in ACM Proceedings style (including appendix). * Short Papers may include tool demonstrations and presentations of exciting if not fully polished research, and of interesting academic, industrial and open-source applications that are new or unfamiliar. Short papers must not exceed 6 pages in ACM Proceedings style (including appendix). * 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. At least one author of each accepted contribution must attend the workshop and present the work. In the case of tool demonstration papers, a live demonstration of the described tool is expected. Suggested topics, evaluation criteria, and writing guidelines for both research tool demonstration papers will be made available on the PEPM 2017 web site. Student participants with accepted 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 and special issue ----------------------------- All accepted papers, short papers and posters included, will appear in formal proceedings published by ACM Press. Accepted papers will be included in the ACM Digital Library. Authors of selected papers from PEPM 2016 and PEPM 2017 will also be invited to expand their papers for publication in a special issue of the journal Computer Languages, Systems and Structures (COMLAN, Elsevier). 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 Best paper award ---------------- PEPM 2017 continues the tradition of a Best Paper award. The winner will be announced at the workshop. Submission ---------- Papers 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 --------------- For Regular Research Papers and Short Papers: * Abstract submission : Tuesday 13th September 2016 * Paper submission : Friday 16th September 2016 * Author notification : Monday 24th October 2016 * Camera ready : Monday 28th November 2016 For Posters: * Poster submission : Sunday 30th October 2016 * Author notification : Friday 10th November 2016 * Camera ready : Monday 28th November 2016 PEPM workshop: * 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

数学基礎論若手の会2016の参加講演募集
by Kenshi Miyabe 13 Aug '16

13 Aug '16

（重複して受け取られた場合はご容赦ください）皆様，明治大学の宮部賢志です．数学基礎論若手の会2016の参加講演の募集の案内です． ===== 数学基礎論若手の会2016 日時：2016年10月21日(金)午後〜23日(日)午前場所：明治大学清里セミナーハウス住所：〒407-0301 山梨県北杜市高根町清里3545-1 参加費学生: 8,000円一般: 10,000円締め切り交通費宿泊費の援助希望者の参加締め切り: 9月9日(金) 参加一次締め切り: 9月30日(金) 参加最終締め切り: 10月11日(火) 講演タイトル，アブストラクト締め切り: 10月14日(金) 参加費の内訳および申込の書式等の詳細は，以下のウェブサイトをごらんください． http://kenshi.miyabe.name/wakate2016/ ===== 宮部 -- Kenshi Miyabe email (research) : research(a)kenshi.miyabe.name email (other) : miyabe(a)meiji.ac.jp Senior Assistant Professor Department of Mathematics School of Science and Technology Meiji University Tel: +81-44-934-7460

1 0

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

10 Aug '16

Workshop 参加者募集のお知らせ 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 頃まで講演がある予定です。 16 日の夜には、近くで懇親会を予定しております。場所はまだ決まっておりませんが、 4000 〜 5000 円程度で考えております。当日参加も可能ですが、本事業参加研究者以外で参加を予定されている方は、下記フォームにて、できるだけ事前にご連絡を頂けますようにお願い申し上げます。特に、懇親会に参加希望される方は、8 月 31 日までにご連絡ください。ご質問等がございましたら、core2core2016(a)jaist.ac.jp までお寄せください。多くの方のご参加をお待ちしております。オルガナイザー：石原哉立木秀樹照井一成 Matthew de Brecht 根元多佳子 --------------------------------------- 「数理論理学とその応用に関するワークショップ」に参加します。所属：名前：懇親会に参加 / 不参加

1 0

[2nd CfP] FTSCS 2016 @ November 14-15, Tokyo
by Takashi Kitamura 10 Aug '16

10 Aug '16

--------------------------------------------------------------------- Call for Papers FTSCS 2016 5th International Workshop on Formal Techniques for Safety-Critical Systems Tokyo, November 14/15, 2016 (satellite workshop of ICFEM 2016) http://www.ftscs.org --------------------------------------------------------------------- *** Science of Computer Programming special issue *** *** Springer CCIS proceedings *** Aims and Scope: There is an increasing demand for using formal methods to validate and verify safety-critical systems in fields such as power generation and distribution, avionics, automotive systems, and medical systems. In particular, newer standards, such as DO-178C (avionics), ISO 26262 (automotive systems), IEC 62304 (medical devices), and CENELEC EN 50128 (railway systems), emphasize the need for formal methods and model-based development, thereby speeding up the adaptation of such methods in industry. The aim of this workshop is to bring together researchers and engineers who are interested in the application of formal and semi-formal methods to improve the quality of safety-critical computer systems. FTSCS strives to promote research and development of formal methods and tools for industrial applications, and is particularly interested in industrial applications of formal methods. Specific topics include, but are not limited to: * case studies and experience reports on the use of formal methods for analyzing safety-critical systems, including avionics, automotive, medical, railway, and other kinds of safety-critical and QoS-critical systems * methods, techniques and tools to support automated analysis, certification, debugging, etc., of complex safety/QoS-critical systems * analysis methods that address the limitations of formal methods in industry (usability, scalability, etc.) * formal analysis support for modeling languages used in industry, such as AADL, Ptolemy, SysML, SCADE, Modelica, etc. * code generation from validated models. The workshop will provide a platform for discussions and the exchange of innovative ideas, so submissions on work in progress are encouraged. Submission: We solicit submissions reporting on: A- original research contributions (15 pages max, LNCS format); B- applications and experiences (15 pages max, LNCS format); C- surveys, comparisons, and state-of-the-art reports (15 pages max, LNCS); D- tool papers (5 pages max, LNCS format); E- position papers and work in progress (5 pages max, LNCS format) related to the topics mentioned above. All submissions must be original, unpublished, and not submitted concurrently for publication elsewhere. Paper submission is done via EasyChair at https://easychair.org/conferences/?conf=ftscs2016. The final version of the paper must be prepared in LaTeX, adhering to the LNCS format available at http://www.springer.com/computer/lncs?SGWID=0-164-6-793341-0. Publication: All accepted papers will appear in the pre-proceedings of FTSCS 2016. Accepted papers in the categories A-D above will appear in the workshop proceedings that will be published as a volume in Springer's CCIS series. The authors of a selected subset of accepted papers will be invited to submit extended versions of their papers to appear in a special issue of the Science of Computer Programming journal. Important dates: Submission deadline: September 4, 2016 Notification of acceptance: October 7, 2016 Workshop: November 14/15, 2016 Venue: Tokyo, Japan Program chairs: Cyrille Artho AIST, Japan Peter Olveczky University of Oslo, Norway Program committee: Etienne Andre University Paris 13, France Toshiaki Aoki JAIST, Japan Cyrille Artho AIST, Japan Kyungmin Bae Pohang University of Science and Technology, Korea Eun-Hye Choi AIST, Japan Alessandro Fantechi University of Florence and ISTI-CNR, Pisa, Italy Bernd Fischer Stellenbosch University, South Africa Osman Hasan National University of Sciences & Technology, Pakistan Klaus Havelund NASA JPL, USA Jerome Hugues Institute for Space and Aeronautics Engineering, France Marieke Huisman University of Twente, The Netherlands Ralf Huuck Synopsys, Australia Fuyuki Ishikawa National Institute of Informatics, Japan Takashi Kitamura AIST, Japan Alexander Knapp Augsburg University, Germany Thierry Lecomte ClearSy System Engineering, France Yang Liu Nanyang Technological University, Singapore Robi Malik University of Waikato, New Zealand Frederic Mallet INRIA Sophia Antipolis, France Roberto Nardone University of Napoli "Federico II", Italy Vivek Nigam Federal University of Paraíba, Brazil Thomas Noll RWTH Aachen University, Germany Kazuhiro Ogata JAIST, Japan Peter Olveczky University of Oslo, Norway Charles Pecheur Universite catholique de Louvain, Belgium Markus Roggenbach Swansea University, UK Ralf Sasse ETH Zurich, Switzerland Martina Seidl Johannes Kepler University, Austria Oleg Sokolsky University of Pennsylvania, USA Sofiene Tahar Concordia University, Canada Carolyn Talcott SRI International, USA Tatsuhiro Tsuchiya Osaka University, Japan Andras Voros Budapest University of Technology and Economics, Hungary Chen-Wei Wang State University of New York (SUNY), Korea Alan Wassyng McMaster University, Canada Michael Whalen University of Minnesota, USA Huibiao Zhu East China Normal University, China Contact: (web) http://www.ftscs.org (email) peterol(a)ifi.uio.no and c.artho(a)aist.go.jp -- Takashi KITAMURA t.kitamura(a)aist.go.jp http://staff.aist.go.jp/t.kitamura/ Tel: +81-72-751-9633, AIST internal: *33-272-79633

1 0

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

05 Aug '16

皆様，下記の要領で研究集会「数学基礎論とその応用」を開催します．この研究集会は，1980年頃より数年毎に数理解析研究所で開催されていたが，2006年を最後に途絶えている，数学基礎論の様々な分野の研究者の交流を目的とする研究集会を継承するものです．今回の集会では，この研究集会のシリーズの創始者の一人であり，我が国の数学基礎論の発展にご尽力され，昨年亡くなられた角田譲先生を追悼し，午前中は角田先生と縁の深い研究者を中心に，かつての数学基礎論の状況や最近の発展の紹介，様々な思い出を含むご講演をお願いしています．午後は海外からの招聘研究者の講演と，若手研究者による最先端の研究成果を紹介する英語による講演からなります．いずれの講演も数学基礎論の専門外の研究者や大学院生が聴講することを前提としており，講演者には背景や目的の説明に十分な時間を取るようにお願いしています．期間が短く大変に申し訳ございませんが，参加者の概数を把握する必要があるために，参加ご希望の方，参加される可能性のある方は，【2016年8月16日】までに件名を「mla2016」として email で，以下の情報を菊池（mkikuchi(a)kobe-u.ac.xn--jp)-u63b3a0e8fwh6d0645a8vxi. ただし，今回お送りいただく情報は最終的なものである必要はなく，送付後の集会への出欠，懇親会への出欠の変更は可能です．宿泊の手配はいたしません．各自でご予約下さるようお願いします．昨今の京都は宿泊の手配が難しくなっています．参加される方にはお早目のご予約をお勧めいたします．今回は，原則として大学院修士課程修了以上の方を対象として，参加者に旅費を援助できる可能性があります．旅費の援助を希望される場合は〆切厳守で，出欠の情報と共に，その旨，菊池までご連絡下さい．なお，ご希望には添えない場合があること，旅費を援助する場合には申し込み後の出欠の変更は原則として控えていただく必要があることをご了承下さい．また，学生の方が旅費の補助を希望する場合は，書式自由で指導教員による簡単な推薦文を参加申し込みに合わせてお送り下さい．皆様のお越しをお待ちしています．菊池誠ーー参加申込ーー氏名：所属大学・部局・職名または身分：旅費援助の希望：有・無　　「有」の場合の出張期間：　月　日〜　月　日懇親会（会費5000円程度，詳細未定）：出席・欠席ーーーーーーーー　　　　　　　　　　記研究集会「数学基礎論とその応用」日時：2016年9月26日（月）〜 9月29日（木）場所：京都大学数理解析研究所111室 Web page：http://www2.kobe-u.ac.jp/~mkikuchi/mla2016.html 問い合わせ先：菊池誠（神戸大）mkikuchi(a)kobe-u.ac.jp プログラム： 9月26日（月） 11:00-11:50 宮元忠敏（南山大）集合論で試される構造と構成のいくつか 13:30-14:20 Joel Hamkins（CUNY） TBA (set theory) 14:30-15:20 樋口幸治郎（日大工） Computably Represented Structures 15:30-16:20 竹内耕太（筑波大） Properties Characterized by Generalized Indiscernible 9月27日（火） 10:00-10:50 新井敏康（千葉大） TBA (proof theory) 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/Kyoto） 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） Higher Type Recursion and Sigma^0_3-Determinacy

1 0

SLACS2016のご案内
by sasaki 05 Aug '16

05 Aug '16

みなさま　期日が近づきましたので、「記号論理と情報科学研究集会（SLACS）」を再度案内させてください．　現在、講演の申込件数が、非常に少ない状態ですので、是非とも、ご参加・ご講演をお願いいたします。　　　　　　8月16日が締め切りになっています。以下、前回案内の内容です。 ================================================================================= みなさま 2016年度の「記号論理と情報科学研究集会（SLACS）」を案内させてください．完成された話題はもちろん，未完成の話題やこれから考えてみたい話題なども歓迎します．是非とも，参加・講演をご検討ください．　日程：2016年8月25日(木),26日(金) 　場所：名古屋大学VBL(ベンチャービジネスラボラトリー)3階ベンチャーホール　招待講演：新屋良磨さんに，形式言語理論に関する，全然知らない人向けの話をお願いしています．　懇親会：25日に予算3500円程度で行う予定です．講演を希望される方・懇親会参加を希望される方は，　　氏名　　所属　　e-mail アドレス　　懇親会参加の有無　　(講演を希望される場合)題目・希望講演時間(30〜50分) 　　その他の要望（講演日など）の情報を，　　　　　　8月16日までに，世話人(sasaki(a)nanzan-u.ac.xn--jp)-u63b4b3ai1gqet146cnwrdnb3b. 詳細は， http://www.seto.nanzan-u.ac.jp/~sasaki/SLACS2016.html にあります．世話人　南山大学　佐々木克巳 ======================================================================= 南山大学　佐々木克巳 -- sasaki <sasaki(a)nanzan-u.ac.jp>

1 0

2016年数学基礎論サマースクールのご案内
by Hirotaka Kikyo 03 Aug '16

03 Aug '16

皆様数学基礎論サマースクールを2016年９月５日（月）から９月７日（水）まで、早稲田大学西早稲田キャンパスで開催する予定です。初日は午前中から、最終日も午後まで行う予定です。今年のテーマはモデル理論です。初日の最初の方にモデル理論の基本事項を解説するつもりです。詳しくは次のサイトでお知らせします。 https://sites.google.com/site/logicsummerschool2016/ どうぞ、よろしくお願い致します。世話人桔梗宏孝

1 0

Kobe Colloquium: Aug 8, 2016, Jun Otsuka
by Makoto Kikuchi 02 Aug '16

02 Aug '16

Kobe Colloquium on Logic, Statistics and Informatics 以下の要領でコロキウムを開催します。日時: 2016/8/8 (月) 11.00am - 正午場所: 神戸大学六甲台第2キャンパス自然科学総合研究棟3号館421室講演者：大塚淳（神戸大・文）題目：因果・統計・機械学習の哲学に向けてアブストラクト：限られたデータから推論を行う帰納推論の手法は、 19世紀末からの古典統計学および近年の機械学習理論の発展にともない、大きな進展を見せてきた。しかしそれらは決して一枚岩ではなく、異なった哲学・目的に支えられているといっていいだろう。本発表では、推測統計、因果推論、機械学習など、現代の帰納推論にまつわる様々な数理的手法の背景にある哲学的前提について探ってみたい。特にJudea Pearlらによって開発された、グラフ表現を用いた統計的因果推論を紹介し、それを従来の伝統的統計学および近年の機械学習的手法と比較することで、それぞれの思想的背景を浮き上がらせることが、本発表の目的である。交通：阪急六甲駅またはJR六甲道駅から神戸市バス36系統「鶴甲団地」行きに乗車，「神大本部工学部前」停留所下車，徒歩すぐ． http://www.kobe-u.ac.jp/guid/access/rokko/rokkodai-dai2.html 連絡先：菊池誠　mkikuchi(a)kobe-u.ac.jp

1 0

第二十七回 ALGI（代数，論理，幾何と情報科学研究集会）の暫定プログラムと懇親会参加について
by 西澤弘毅 01 Aug '16

01 Aug '16

logic-ml メーリングリストの皆様，神奈川大学の西澤弘毅と申します。第二十七回 ALGI（代数，論理，幾何と情報科学研究集会）の暫定プログラムのアナウンスをさせていただきます。 < 重複してお受け取りの節はご容赦願います。> ご参加をお待ちしております。 --------------------------------------------------------------------- **************************************************************** * 第二十七回 ALGI（代数，論理，幾何と情報科学研究集会） * * * * 2016年8月27日（土）13:45～8月28日（日）12:45 * * 信州大学松本キャンパス人文学部・経法学部新棟1階第1講義室 * * * * 暫定プログラムのお知らせと講演募集 * **************************************************************** ALGI (Algebra, Logic, Geometry and Informatics) は、代数学や論理学、幾何学の情報科学への応用について、および情報科学の代数学や論理学、幾何学への応用についての研究集会で、年一回の頻度で開催されています。 ALGIの趣旨や過去の集会の情報がウェブページ http://sakura.imi.kyushu-u.ac.jp/algi/ にありますので、参考までに御覧ください。このたび、第二十七回ALGIを開催することになりました。会場の手配などは信州大学の田中康平先生にお願いしています。開催場所は下記のとおりです。信州大学松本キャンパス人文学部・経法学部新棟1階第1講義室 http://www.shinshu-u.ac.jp/guidance/maps/map05.html http://www.shinshu-u.ac.jp/general/extension-courses/pdf/map01-02.pdf 講演枠が１つ空いております。講演を希望される方は、・題目・講演者名・e-mail address ・所属・梗概・希望時間・講演に必要な道具などの情報を nishizawa(a)kanagawa-u.ac.jp までお寄せください。 ALGIは申し込み不要で自由にご参加いただけます。ただし、一日目の18:30から松本駅周辺で懇親会を予定しておりますので、懇親会への参加を希望される方は、8/20（土）までに西澤 (nishizawa AT kanagawa-u.ac.jp) にメールでお知らせください。また、今回のALGIの前後には次のような集会も予定されています。併せて参加をご検討下さい。 2016年度 SLACS(記号論理と情報科学研究集会) 日時：2016年8月25日(木),26日(金) 会場：名古屋大学VBL(ベンチャービジネスラボラトリー)3階ベンチャーホール詳細：http://www.seto.nanzan-u.ac.jp/~sasaki/SLACS2016.html 「空間の代数的・幾何的モデルとその周辺」日時：2016年8月29日（月）14:00～8月31日（水）12:15 会場：信州大学理学部講義棟第一講義室詳細：http://marine.shinshu-u.ac.jp/~kuri/ALG_TOP2016/AGM2016.html できるだけ多くの皆さんのご講演・ご参加をお待ちしております。西澤弘毅（神奈川大学工学部）古澤仁（鹿児島大学大学院理工学研究科） -- 西澤弘毅神奈川大学工学部情報システム創成学科〒221-8686 神奈川県横浜市神奈川区六角橋3-27-1 nishizawa(a)kanagawa-u.ac.jp TEL（代表）045-481-5661 （内線：3378）

1 0

Call for Participation: ICFP 2016
by Jacques Garrigue 26 Jul '16

26 Jul '16

みなさま、9月に奈良で開催される ICFP 2016 の案内を転送します。早期参加申し込みの〆切は8月17日になっております。 5年ぶりの日本開催で、ご参加をお待ちしています。 ===================================================================== Call for Participation ICFP 2016 21st ACM SIGPLAN International Conference on Functional Programming and affiliated events September 18 - September 24, 2016 Nara, Japan http://conf.researchr.org/home/icfp-2016 ===================================================================== ICFP provides a forum for researchers and developers to hear about the latest work on the design, implementations, principles, and uses of functional programming. The conference covers the entire spectrum of work, from practice to theory, including its peripheries. A full week dedicated to functional programming: 1 conference, 1 symposium, 10 workshops, tutorials, programming contest results, student research competition, and mentoring workshop * Overview and affiliated events: http://conf.researchr.org/home/icfp-2016 * Program: http://conf.researchr.org/program/icfp-2016/program-icfp-2016 * Accepted Papers: http://conf.researchr.org/track/icfp-2016/icfp-2016-papers#event-overview * Registration is available via: https://regmaster4.com/2016conf/ICFP16/register.php Early registration is due 17 August, 2016. * Programming contest, 5-8 August, 2016: http://2016.icfpcontest.org/ * Student Research Competition (deadline: 3 August, 2016): http://conf.researchr.org/info/icfp-2016/student-research-competition * Follow @icfp_conference on twitter for the latest news: http://twitter.com/icfp_conference There are several events affiliated with ICFP: Sunday, September 18 Workshop on Higher-order Programming with Effects Workshop on Type-Driven Development Scheme and Functional Programming Workshop Programming Languages Mentoring Workshop Monday, September 19 – Wednesday, September 21 ICFP Thursday, September 22 Haskell Symposium – Day 1 ML Family Workshop Workshop on Functional High-Performance Computing Commercial Users of Functional Programming – Day 1 Friday, September 23 Haskell Symposium – Day 2 OCaml Workshop Erlang Workshop Commercial Users of Functional Programming – Day 2 Saturday, September 5 Commercial Users of Functional Programming – Day 3 Haskell Implementors Workshop Functional Art, Music, Modeling and Design Conference Organizers General Co-Chairs: Jacques Garrigue, Nagoya University Gabriele Keller, University of New South Wales Program Chair: Eijiro Sumii, Tohoku University Local Arrangements Co-Chairs: Shinya Katsumata, Kyoto University Susumu Nishimura, Kyoto University Industrial Relations Chair: Rian Trinkle, Obsidian Systems LLC Workshop Co-Chairs: Nicolas Wu, University of Bristol Andres Loeh, Well-Typed LLP Programming Contest Chair: Keisuke Nakano, The University of Electro-Communications Student Research Competition Chair: David Van Horn, University of Maryland, College Park Mentoring Workshop Co-Chairs: Amal Ahmed, Northeastern University Robby Findler, Northwestern University Atsushi Igarashi, Kyoto Universty Publicity Chair: Lindsey Kuper, Intel Labs Video Chair: Iavor Diatchki, Galois Jose Calderon, Galois Student Volunteer Co-Chairs: Yosuke Fukuda, Kyoto University Yuki Nishida, Kyoto University Gabriel Scherer, INRIA Industrial partners: Platinum partners Jane Street Capital Ahrefs Gold partners Mozilla Research Silver partners Ambiata Tsuru Capital Bronze partners Awake Networks Microsoft Research =====================================================================

1 0

Glynn Winskel "Formal Semantics of Programming Languages" の翻訳をお手伝いいただける方を探しています
by Kohei SUENAGA 22 Jul '16

22 Jul '16

皆様，京都大学の末永です．メーリングリストをお借りして，教科書の翻訳をお手伝いいただける方を募集させていただければと思います．重複して受け取られた場合はご容赦ください． Glynn Winskel "Formal Semantics of Programming Languages " の翻訳出版の話が来ていて，お手伝いいただける方を探しています． https://www.amazon.com/dp/0262731037 プログラム意味論の世界で一番有名な教科書の一つです．トピックはプログラムの意味を数学を使って厳密に与える様々な方法や，与えた意味論を使ってプログラミング言語の性質を証明する方法です．興味のある方は末永 ksuenaga(a)kuis.kyoto-u.ac.jp までメールをいただければと思います．書誌情報に訳者として名前を載せられるのは数人らしいのですが，お手伝いいただいた方には謝辞などでお名前を出させていただきます．また，些少ながら原稿料も出るようです．どうぞよろしくお願い致します．末永幸平 -- Kohei Suenaga (末永幸平), Ph.D Associate professor (准教授) Graduate School of Informatics, Kyoto University (京都大学情報学研究科) ksuenaga(a)gmail.com http://www.fos.kuis.kyoto-u.ac.jp/~ksuenaga/

1 0

JAIST Logic Seminar Series
by Hajime Ishihara 20 Jul '16

20 Jul '16

皆様ルートヴィヒ・マクシミリアン大学ミュンヘンのHelmut Schwichtenberg先生の講演のお知らせです。どうぞふるってご参加ください。問合せ先：石原　哉北陸先端科学技術大学院大学情報科学系 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: Thursday 25 August, 2016, 13:30-15:10 Place: JAIST, Lecture room I2 (Access: http://www.jaist.ac.jp/english/location/access.html) Speaker: Helmut Schwichtenberg (Ludwig-Maximilians-Universität München) Title: Invariance axioms for realizability Abstract: Kolmogorov (1932) proposed to consider mathematical formulas as problems asking for solutions. Following this idea it seems reasonable to extend arithmetical theories by adding invariance axioms, which state that every formula is equivalent to the (internal) formula stating that it has a realizer. We sketch such a theory, which in addition allows to fine-tune the computational content of proofs by decorations of the logical connectives. A soundness theorem holds.

1 0

Kobe Colloquium: July 26, 2016, Bakhadyr Khoussainov
by Makoto Kikuchi 20 Jul '16

20 Jul '16

Kobe Colloquium on Logic, Statistics and Informatics 以下の要領でコロキウムを開催します。 Date: 2016/7/26 (Tue) 3.00pm - 4.30pm Place: Room 421 Speaker: Bakhadyr Khoussainov (Auckland/Kyoto) Title: Algorithmically random infinite structures Abstract: Over the last two decades a significant progress has been made in the study of algorithmic random infinite strings. The main concepts of algorithmic randomness on infinite strings are based on the natural measure on the Cantor space. In spite of much work, research on algorithmic randomness has excluded the investigation of randomness for infinite structures such as graph, trees, algebras. The reason is that it was unclear how one introduces a meaningful measures into these classes of structures that would be pivotal in defining algorithmic randomness. We provide a solution to this problem. We present an axiomatic approach that introduces measure, and hence algorithmic randomness into various classes of structures. We prove the existence of algorithmically random structures with various computability-theoretic properties. We show that any nontrivial variety of algebras has an effective measure 0. This, for instance, implies that no finitely presented algebra in a variety is algorithmically random. We also prove a counter-intuitive result that there are algorithmically random yet computable structures. This establishes a connection between algorithmic randomness and computable model theory. 交通：阪急六甲駅またはJR六甲道駅から神戸市バス36系統「鶴甲団地」行きに乗車，「神大本部工学部前」停留所下車，徒歩すぐ． http://www.kobe-u.ac.jp/guid/access/rokko/rokkodai-dai2.html 連絡先：菊池誠　mkikuchi(a)kobe-u.ac.jp

1 0

JAIST Logic Seminar Series
by Hajime Ishihara 19 Jul '16

19 Jul '16

皆様インスブリア大学のMarco Benini先生の講演のお知らせです。どうぞふるってご参加ください。問合せ先：石原　哉北陸先端科学技術大学院大学情報科学系 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: Monday 8 August, 2016, 13:30-15:10 Place: JAIST, Collaboration room 7 (I-56) (Access: http://www.jaist.ac.jp/english/location/access.html) Speaker: Marco Benini (University of Insubria) Title: Variations on the Higman's Lemma Abstract: The Higman's Lemma says that if A is a well-quasi-order, so is the set of finite sequences over A with the order induced by embedding. By considering the structure of the categories of well-founded quasi-orders and well-quasi-orders, another proof of the Lemma will be derived, along with a number of variants, which may be of some interest.

1 0

Talk by Liang-ting Chen, 19 Tue Jul
by Takumi Akazaki 16 Jul '16

16 Jul '16

Dear colleagues, Dr. Liang-Ting Chen, postdoc. in University of Hawaii at Manoa will visit us next Tuesday. He is working mainly on categorical-algebraic automata theory, and the topic of the talk is Schutzenberger Products. His talk is scheduled on 19 Jul (Tuesday). You're all invited. Thanks, and see you, Takumi Akazaki http://www-mmm.is.s.u-tokyo.ac.jp/seminars.html ----------- Tue 19 July 2016, 13:00–15:00 理学部7号館102 Room 102, School of Science Bldg. No. 7 Liang-Ting Chen <https://de.linkedin.com/in/liang-ting-chen-b5a74988> (Dept. of Info. and Comp. Sci., University of Hawaii), Schutzenberger Products in a Category The Sch\"utzenberger product of monoids is a key tool for the algebraic treatment of language concatenation. In this paper we generalize the Sch\"utzenberger product to the level of monoids in an algebraic category 𝒟, leading to a uniform view of the corresponding constructions for monoids (Sch\"utzenberger), ordered monoids (Pin), idempotent semirings (Kl\'ima and Pol\'ak) and algebras over a field (Reutenauer). In addition, assuming that 𝒟 is part of a Stone-type duality, we derive a characterization of the languages recognized by Sch\"utzenberger products. -- /_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/ Dept. of Computer Science Graduate School of Information Science and Technology The University of Tokyo Akazaki Takumi mail :<ultraredrays(a)gmail.com> mobile : <090-5379-4901> /_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/

1 0

Nagoya Set Theory Seminar
by 吉信康夫 11 Jul '16

11 Jul '16

名古屋集合論セミナーのご案内：日時：2016年7月15日(金) 午後3時30分より場所：名古屋大学大学院情報科学研究科2階206号室講演者：渕野昌(神戸大学) 題目：Pre-Hilbert spaces without orthonormal bases 概要：Halmos proved in 1970's that there are pre-Hilbert spaces without orthonormal bases. His example of such pre-Hilbert space was so that its dimension (size of maximal orthonormal system in the space) is strictly less than the density of the space. We show that there are also pre-Hilbert spaces X without orthonormal bases such that dim(X)=d(X). We also show that Shelah Singular Compactness Theorem holds for non-existence of orthonormal bases holds and a natural reflection statement of non-existence of orthonormal bases is equivalent to the Fodor-type Reflection Principle. 多数のご参加をお待ちしております。名古屋大学大学院情報科学研究科吉信康夫

1 0

JAIST Logic Seminar Series (Thursday, 7th July 2016, 15:30-17:00, Ren-June Wang)
by Katsuhiko Sano 05 Jul '16

05 Jul '16

皆様台湾 National Chung Cheng University のRen-June Wangさんの講演会のお知らせです。どうぞふるってご参加ください。問合せ先：佐野勝彦北陸先端科学技術大学院大学情報科学系 e-mail: v-sano(a)jaist.ac.jp ----------------------------------------------------------------- * JAIST Logic Seminar Series * Date: Thursday, 7th July 2016, 15:30-17:00 Place: JAIST, IS school collaboration room 7, 5F (Access: http://www.jaist.ac.jp/english/top/access/index.html) Speaker: Ren-June Wang (Department of Philosophy, National Chung Cheng University) Title: Logical Omniscience and Deductive Rationality Abstract: Epistemic logic as an important tool for reasoning about an intellectual agent’s epistemic states has long suffered from the so-called logical omniscience problem since the beginning of its introduction. The problem indicates an idealized assumption on the part of the agent presented by a formalism of such kind. Although alternative epistemic formalisms have been proposed for dealing with the problem, there is no sight of that the problem is settled. Thus in this talk I will try my hand firstly to give an analysis of the problem, hopefully to pin down the source of the problem, and accordingly provide an advice as to what is the right direction of solving the problem. At the end of the talk I will suggest that what we need is not a formalism with a machinery that can limit what is known by the agent, but one with more powerful expressivity such that the resource that an agent will consume in the course of his/her reasoning, such as the temporal duration, can be explicitly stated. -- Katsuhiko Sano School of Information Science Japan Advanced Institute of Science and Technology IS building No.1 7F, 1-1 Asahidai, Nomi, Ishikawa, 923-1292, Japan

2 1

[TACL 2017] First announcement
by 小野寛晰 04 Jul '16

04 Jul '16

[Apologies for multiple copies] ======================================================= TOPOLOGY, ALGEBRA AND CATEGORIES IN LOGIC (TACL 2017) ======================================================= Conference: June 26 -- 30, 2017 (Prague) School: June 20 -- 24, 2017 (Olomouc) http://www.cs.cas.cz/tacl2017 <http://www.cs.cas.cz/tacl2017> The Eighth International Conference on Topology, Algebra and Categories in Logic organized by Institute of Computer Science, Czech Academy of Sciences Faculty of Arts, Charles University in Prague & & & & & & & & & & & & & & & & & & & & & & & The Third Summer School organized by Faculty of Science, Palacký University Olomouc Studying logics via semantics is a well-established and very active branch of mathematical logic, with many applications, in computer science and elsewhere. The area is characterized by results, tools and techniques stemming from various fields, including universal algebra, topology, category theory, order, and model theory. The programme of the conference TACL 2017 will focus on three interconnecting mathematical themes central to the semantical study of logics and their applications: algebraic, categorical, and topological methods. This is the eighth conference in the series Topology, Algebra and Categories in Logic (TACL, formerly TANCL). Earlier instalments of this conference have been organized in Tbilisi (2003), Barcelona (2005), Oxford (2007), Amsterdam (2009), Marseille (2011), Nashville (2013) and Ischia (2015). Starting from 2013, the conference is preceded by a summer school. Featured topics ------------------ Contributed talks can be on with any topic involving the use of algebraic, categorical or topological methods in either logic or computer science. This includes, but is not limited to, the following areas: * Algebraic structures in CS * Algebraic logic * Coalgebra * Categorical methods in logic * Domain theory * Lattice theory * Lattices with operators * Many-valued and fuzzy logics * Modal logics * Non-classical logics * Ordered topological spaces * Ordered algebraic structures * Pointfree topology * Proofs and Types * Residuated structures * Semantics * Stone-type dualities * Substructural logics * Topological semantics of modal logic Venues ------ The conference will be held at the campus of the Faculty of Arts, Charles University in Prague. The school will be held at the campus of the Faculty of Science, Palacký University Olomouc. (The two cities are two hours train trip apart.) Important dates ----------------- June 20 - June 24, 2017: School (Olomouc) June 26 - June 30, 2017: Conference (Prague) Programme Committee Chairs -------------------------- John Harding, New Mexico State University Rosalie Iemhoff, Utrecht University Steering Committee -------------------- Guram Bezhanishvili, New Mexico State University Mai Gehrke, University of Paris Diderot Rob Goldblatt, Victoria University, Wellington Ramón Jansana, University of Barcelona Achim Jung, University of Birmingham Hiroakira Ono, Japan Advanced Institute of Science and Technology Yde Venema, University of Amsterdam Michael Zakharyaschev, University of London Organizing Committees --------------------- Conference: Marta Bílková (chair), Faculty of Arts, Charles University in Prague Petr Cintula (chair), Institute of Computer Science, CAS Zuzana Haniková Rostislav Horčík Tomáš Lávička Ondrej Majer Tommaso Moraschini Carles Noguera Adam Přenosil Igor Sedlár Amanda Vidal Wandelmer School: Radomír Halaš (chair), Faculty of Science, Palacký University Olomouc Martin Broušek Jan Kuhr More Information ---------------- TACL 2017 web site: http://www.cs.cas.cz/tacl2017 <http://www.cs.cas.cz/tacl2017> Conference email: tacl2017(a)cs.cas.cz <mailto:tacl2017@cs.cas.cz> School email: school2017(a)upol.cz <mailto:school2017@upol.cz>

1 0

CFP: 日本ソフトウェア科学会第33回大会
by KIKUCHI Kentaro 01 Jul '16

01 Jul '16

(重複して受け取られた場合は御容赦ください) 東北大学の菊池健太郎です。 9月に東北大学片平キャンパスで開催されます日本ソフトウェア科学会第33回大会の発表申込締切が一週間後となりましたので、開催案内・参加募集を再度お送りさせていただきます。予稿の締切はさらに一ヶ月ほど先となっております。是非発表申込をご検討いただければ幸いです。どうぞよろしくお願いいたします。 --- 東北大学電気通信研究所菊池健太郎 (kentaro(a)nue.riec.tohoku.ac.jp) ------------------------------------------------------------------------ 日本ソフトウェア科学会第33回大会開催案内・参加募集 https://jssst2016.wordpress.com/ 日時：2016年9月6日(火)〜9日(金) (6日(火)はプレイベント) 会場：東北大学片平キャンパス (〒980-8577 仙台市青葉区片平2-1-1) 共催：東北大学電気通信研究所登壇発表申込締切：2016年7月8日(金) 予稿原稿締切：2016年8月5日(金) デモ・ポスター発表申込締切：2016年8月23日(火) 今年も一般セッション，研究会セッション，ソフトウェア論文セッションにおける登壇発表，ならびにデモ・ポスター発表の場が用意されています．予稿の共著者に会員が含まれていれば非会員でも登壇発表できますので，是非，発表をご検討ください．未来のソフトウェアとそれを支えるソフトウェア科学に関する活発な議論を期待しております． ■開設セッション 1. 一般セッション：ソフトウェア科学全般についての発表の場です． 2. 研究会セッション：研究会と連携した企画による発表の場です．・プログラミング論研究会 (PPL) コーディネータ：森畑明昌 (東京大学) ・ソフトウェア工学の基礎研究会 (FOSE) コーディネータ：杉山安洋 (日本大学)，門田暁人 (岡山大学) ・実践的IT教育研究会 (rePiT) コーディネータ：吉田則裕 (名古屋大学)，鵜林尚靖 (九州大学) ・マルチ・エージェントと協調計算研究会 (MACC) [チュートリアル] コーディネータ：清雄一 (電気通信大学) 3. ソフトウェア論文セッション：先進的なアイデアを実現したソフトウェアの成果発表の場です．ソフトウェア論文特集号への投稿を前提としたメンタリングを受けることができます．コーディネータ：小宮常康 (電気通信大学) 4. デモ・ポスターセッション：研究アイデアやそれを実現したソフトウェアの紹介と議論の場です．予稿なしで発表することができます．コーディネータ：青谷知幸 (東京工業大学) 上記以外にも，招待講演，特別講演(トップコンファレンス採択論文の著者による講演)，FTD (Future Technology Design)などを予定しています． ■発表申込要領予稿の共著者(デモ・ポスターセッションの場合は発表者)に少なくとも1名の正会員，学生会員または名誉会員が含まれている必要があります．ただし，発表申込時に入会手続中の場合も含みます．発表申込はEasyChairと申し込みフォームを併用して行います．予稿はPDFファイルで作成し，EasyChairから提出してください．詳しい予稿作成要領は大会ホームページをご覧ください． ■学会誌への同時投稿登壇発表の予稿は通常論文またはレター論文として学会誌に同時投稿できます．大会発表で得られたコメントを反映した上での大会後投稿も可能です．詳細は，大会ホームページの大会同時投稿要領をご覧ください． ■大会組織大会委員長：大堀淳 (東北大学) 運営委員長：上野雄大 (東北大学) プログラム委員長：光来健一 (九州工業大学) プログラム副委員長：松崎公紀 (高知工科大学) 広報委員長：山田浩史 (東京農工大学) デモ・ポスター委員長：青谷知幸 (東京工業大学)

1 0

JAIST Logic Seminar Series
by Hajime Ishihara 28 Jun '16

28 Jun '16

皆様ジェノヴァ大学のEugenio Moggi先生の特別集中講演のお知らせです。どうぞふるってご参加ください。問合せ先：石原　哉北陸先端科学技術大学院大学情報科学系 e-mail: ishihara(a)jaist.ac.jp ----------------------------------------------- * JAIST Logic Seminar Series * * This series of lectures 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/) Dates: Tuesday 2 August, 2016, 13:30-15:10 Thursday 4 August, 2016, 13:30-15:10 Friday 5 August, 2016, 10:50-12:30 Place: JAIST, Collaboration room 7 (I-56) (Access: http://www.jaist.ac.jp/english/location/access.html) Speaker: Eugenio Moggi (University of Genova) *Tuesday 2 August, 2016, 13:30-15:10* LECTURE 1: Categories of Classes for Collection Types ABSTRACT. Collection types have been proposed by Buneman and others (in the '90) as a way to capture database query languages in a typed setting. In 1998 Manes introduced the notion of collection monad on the category S of sets as a suitable semantics for collection types. The canonical example of collection monad is the finite powerset monad Pf. In order to account for the algorithmic aspects of database languages, the category S is unsuitable, and should be replaced with other categories, whose arrows are maps computable by "low complexity" algorithms. We propose "realizability for DSL" (Domain Specific Languages), where the starting point is a monoid C of endomaps on a set D, instead of a combinatory algebra on D, as a way to get such categories by constructions like the category A[C] of "assemblies". To get Pf in a systematic way we borrow ideas from AST (Algebraic Set Theory, started by Joyal and Moerdijk in the '90), where they fix a notion of "small" map in a category of "classes", and read "small" as "finite". *Thursday 4 August, 2016, 13:30-15:10* LECTURE 2: Hybrid System Trajectories as Partial Continuous Maps ABSTRACT. Hybrid systems (HS) are dynamic systems that exhibit both continuous and discrete dynamic behavior: they can flow (according to a differential equation) and jump (according to a transition relation). HS can be used for modeling rigid body dynamics with impacts, and more generally Cyber-Physical Systems. HS can exhibit Zeno behaviors, that arise naturally in rigid body dynamics with impacts, but are absent from purely discrete or purely continuous systems. Dealing properly with these behaviors is a prerequisite to give sound definitions of concepts such as reachability. We propose the use of partial continuous maps (PCM) as trajectories that describe how a HS evolves over time. PCMs enable a notion of trajectory that can go beyond Zeno points. *Friday 5 August, 2016, 10:50-12:30* LECTURE 3: Models, Over-approximations and Robustness ABSTRACT. Hybrid systems, and related formalisms, have been successfully used to model Cyber- Physical Systems. The usual definition of "reachability", in terms of the reflexive and transitive closure of a transition relation, is unsound for Zeno systems. We propose "safe reachability", which gives an over-approximation of the set of states that are "reachable in finite time" from a set of initial states. Moreover, mathematical models are always a simplification of the system they are meant to describe, and one must be aware of this mismatch, when using these models for system analyses. In safety analysis it is acceptable to use over-approximations of the system behavior, indeed they are the bread and butter of counterexample guided abstraction refinement (CEGAR). We propose a notion of safe (time-bounded) reachability, which is also robust wrt arbitrary small overapproximations, and argue that it is particularly appropriate for safety analysis.

1 0

CFP: PEPM 2017
by Ryosuke SATO 27 Jun '16

27 Jun '16

皆様、（複数受け取られた場合はご容赦ください。）東京大学の佐藤亮介です。来年1月に POPL 併設で開催される PEPM 2017 の CFP をお送りいたします。日程は次の通りです。 * Abstract submission: Tue, 13 Sep, 2016 * Paper submission: Fri, 16 Sep, 2016 * Author notification: Mon, 24 Oct, 2016 * Camera ready: Mon, 28 Nov, 2016 レギュラー論文の他に、ショート論文、ポスターも受け付けております。是非，投稿をご検討ください。 -- 東京大学大学院情報理工学系研究科佐藤亮介 ryosuke(a)kb.is.s.u-tokyo.ac.jp ------------------------------------------------------------------- CALL FOR PAPERS Workshop on Partial Evaluation and Program Manipulation (PEPM 2017) Paris, France, January 16th – 17th, 2017 http://conf.researchr.org/home/PEPM-2017 PEPM 2017 in Paris, co-located with POPL 2017. The PEPM Symposium/Workshop series aims at bringing together researchers and practitioners working in the areas of program manipulation, partial evaluation, and program generation. PEPM focuses on techniques, theory, tools, and applications of analysis and manipulation of programs. 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. Specifically, PEPM 2017 will include practical applications of program transformations such as refactoring tools, and practical implementation techniques such as rule-based transformation systems. In addition, the scope of PEPM covers manipulation and transformations of program and system representations such as structural and semantic models that occur in the context of model-driven development. In order to maintain the dynamic and interactive nature of PEPM and to encourage participation by practitioners, we also solicit submissions of short papers, including tool demonstrations, and of posters. 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 CATEGORIES AND GUIDELINES Three kinds of submissions will be accepted: Regular Research Papers, Short Papers and Posters. * Regular Research Papers should describe new results, and will be judged on originality, correctness, significance and clarity. Regular research papers must not exceed 12 pages in ACM Proceedings style (including appendix). * Short Papers may include tool demonstrations and presentations of exciting if not fully polished research, and of interesting academic, industrial and open-source applications that are new or unfamiliar. Short papers must not exceed 6 pages in ACM Proceedings style (including appendix). * 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. At least one author of each accepted contribution must attend the workshop and present the work. In the case of tool demonstration papers, a live demonstration of the described tool is expected. Suggested topics, evaluation criteria, and writing guidelines for both research tool demonstration papers will be made available on the PEPM 2017 web site. Student participants with accepted 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 AND SPECIAL ISSUE All accepted papers, short papers and posters included, will appear in formal proceedings published by ACM Press. Accepted papers will be included in the ACM Digital Library. Authors of selected papers from PEPM 2016 and PEPM 2017 will also be invited to expand their papers for publication in a special issue of the journal Computer Languages, Systems and Structures (COMLAN, Elsevier). BEST PAPER AWARD PEPM 2017 continues the tradition of a Best Paper award. The winner will be announced at the workshop. IMPORTANT DATES Abstract submission: Tue, 13 Sep, 2016 Paper submission: Fri, 16 Sep, 2016 Author notification: Mon, 24 Oct, 2016 Camera ready: Mon, 28 Nov, 2016 INVITED SPEAKERS to be announced PROGRAM CHAIRS Jeremy Yallop (University of Cambridge) Ulrik Pagh Schultz (Unversity of Southern Denmark) PROGRAM COMMITTEE to be announced

1 0

第二十七回 ALGI（代数，論理，幾何と情報科学研究集会）の講演募集の再アナウンス
by 西澤弘毅 23 Jun '16

23 Jun '16

logic-mlメーリングリストの皆様，神奈川大学の西澤弘毅と申します。第二十七回 ALGI（代数，論理，幾何と情報科学研究集会）の開催と講演募集の再アナウンスをさせていただきます。 < 重複してお受け取りの節はご容赦願います。> 下記にも記しましたが、二日目には、代数トポロジーに関する１時間程度の特別講演を信州大学理学部の玉木大先生にお願いしております。ご参加をお待ちしております。 --------------------------------------------------------------------- **************************************************************** * 第二十七回 ALGI（代数，論理，幾何と情報科学研究集会） * * * * 2016年8月27日（土）午後～8月28日（日） * * 信州大学松本キャンパス人文学部・経法学部新棟1階第1講義室 * * * * 開催のお知らせと講演の募集 * **************************************************************** ALGI (Algebra, Logic, Geometry and Informatics) は、代数学や論理学、幾何学の情報科学への応用について、および情報科学の代数学や論理学、幾何学への応用についての研究集会で、年一回の頻度で開催されています。 ALGIの趣旨や過去の集会の情報がウェブページ http://sakura.imi.kyushu-u.ac.jp/algi/ にありますので、参考までに御覧ください。このたび、第二十七回ALGIを開催することになりました。会場の手配などは信州大学の田中康平先生にお願いしています。開催場所は下記のとおりです。信州大学松本キャンパス人文学部・経法学部新棟1階第1講義室 http://www.shinshu-u.ac.jp/guidance/maps/map05.html http://www.shinshu-u.ac.jp/general/extension-courses/pdf/map01-02.pdf 講演を希望される方は、・題目・講演者名・e-mail address ・所属・梗概・希望時間・講演に必要な道具などの情報を nishizawa(a)kanagawa-u.ac.jp までお寄せください。「講演したいと思っている」程度の不完全情報でも結構です。時間の空きがある限り、開催直前まで講演申込を受け付けるつもりですが、申込順に発表時間を割り当てていきますので、講演をお考えの方は、なるべくお早めにお知らせいただけますようにお願い致します。初日は午後から開催いたします。夕方には松本駅周辺で懇親会を計画しています。二日目には、代数トポロジーに関する１時間程度の特別講演を信州大学理学部の玉木大先生にお願いしております。また、今回のALGIの前後には次のような集会も予定されています。併せて参加をご検討下さい。 2016年度 SLACS(記号論理と情報科学研究集会) 日時：2016年8月25日(木),26日(金) 会場：名古屋大学VBL(ベンチャービジネスラボラトリー)3階ベンチャーホール詳細：http://www.seto.nanzan-u.ac.jp/~sasaki/SLACS2016.html 「空間の代数的・幾何的モデルとその周辺」日時：2016年8月29日（月）午後 ? 8月31日（水）午前会場：信州大学理学部講義棟第一講義室詳細：決まり次第アナウンス予定 ALGIは申し込み不要で自由にご参加いただけます。ただし懇親会については事前に詳細を告知し参加申し込みを受け付けます。できるだけ多くの皆さんのご講演・ご参加をお待ちしております。西澤弘毅（神奈川大学工学部）古澤仁（鹿児島大学大学院理工学研究科） ----------------------------------------------------------- -- 西澤弘毅神奈川大学工学部情報システム創成学科〒221-8686 神奈川県横浜市神奈川区六角橋3-27-1 nishizawa(a)kanagawa-u.ac.jp TEL（代表）045-481-5661 （内線：3378）

1 0

IWC 2016 - 2nd Call for Papers
by Nao Hirokawa 14 Jun '16

14 Jun '16

皆様 9月にオーストリアで開催されます「合流性に関するワークショップ IWC 2016」の二回目の論文募集をご案内致します。 - 開催日が 9月8日〜9日に決定致しました。 - 招待講演者は Florent Jacquemard 氏 (INRIA) と Paul-Andre Mellies 氏です。ぜひ投稿・参加をご検討下さい。廣川 (JAIST) ============================================================== Second Call for Papers IWC 2016 5th International Workshop on Confluence Sep 8-9, 2016, Obergurgl, Austria, Part of Computational Logic in the Alps CLA 2016 http://www.csl.sri.com/~tiwari/iwc2016/ ============================================================== 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 had 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 2016 is part of the Computational Logic in the Alpsevent to be held in Obergurgl, Austria, during the week Sep 4-10, 2016. Previous editions of the workshop were held in Nagoya (2012), Eindhoven (2013), Vienna (2014), and Berlin (2015). During the workshop, the 5th Confluence Competition (CoCo 2016) takes place. IMPORTANT DATES: * submission June 22, 2016 * notification July 12, 2016 * final version Aug 03, 2016 * workshop Sep 4-10, 2016 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: * Florent Jacquemard (INRIA) * Paul-Andre Mellies (CNRS & Paris Diderot University) PROGRAM COMMITTEE: * Beniamino Accattoli (INRIA) * Bertram Felgenhauer (University of Innsbruck) * Yves Guiraud (INRIA & Paris Diderot University) * Nao Hirokawa (JAIST) * Koji Nakazawa (Nagoya) * Ashish Tiwari (Menlo Park) 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=iwc2016

1 0

JAIST Logic Seminar Series
by Hajime Ishihara 08 Jun '16

08 Jun '16

皆様オークランド大学のBakhadyr Khoussainov先生の講演のお知らせです。どうぞふるってご参加ください。問合せ先：石原　哉北陸先端科学技術大学院大学情報科学系 e-mail: ishihara(a)jaist.ac.jp ----------------------------------------------- * JAIST Logic Seminar Series * Date: Monday 20 June, 2016, 15:20-17:00 Place:JAIST, Collaboration room 7 (I-56) (Access: http://www.jaist.ac.jp/english/location/access.html) Speaker: Bakhadyr Khoussainov (University of Auckland) Title: Computably Enumerable Structures: Domain dependency Abstract: Computably enumerable structures arise naturally in algebra and computer science. In algebra examples include finitely presented universal algebras such as finitely presented groups. In computer science, these are abstract data types defined by equational or quasi-equational specifications. The domains of these algebraic structures are quotient sets of the form $\omega/E$, where $\omega$ is the set of natural numbers and $E$ is a computably enumerable (c.e.) equivalence relations. We consider c.e. structures whose domains are of the form $\omega/E$ and study various properties of these structures and their dependence on the domain $\omega/E$

1 0

Talk by Sato Tetsuya, 14 Tue Jun
by Takumi Akazaki 08 Jun '16

08 Jun '16

皆様、(重複して受け取られた方はご容赦ください) 東京大学蓮尾研の赤崎と申します。以下の要領で、来週の火曜日に、京大数理研の佐藤哲也さんをお招きして講演をしていただきます。ぜひご参加くださいませ。日時: 6月14日 13:00-15:00 場所: 東京大学理学部7号館102教室 --------- Tue 14 June 2016, 13:00–15:00 理学部7号館102 Room 102, School of Science Bldg. No. 7 Tetsuya Sato <http://www.kurims.kyoto-u.ac.jp/~satoutet/> (RIMS, Kyoto University), 差分プライバシーの圏論的特徴づけと、その検証差分プライバシー[Dwork, ICALP 2006]は、確率的プログラムで与えられたデータベース・クエリーに関するプライバシー保護の定義／基準で、背景知識攻撃に対する安全性を数学的に保証するという特長を持ち、近年でも盛んに研究されている。 Bartheによる Approximate Relational Hoare Logic (apRHL) [Barthe et al., POPL 2012]は、クエリーの差分プライバシーを形式的に検証するための枠組みで、差分プライバシーの概念を、圏Set上の確率分布モナドのパラメトリックな二項関係持ち上げによって与えるというアイデアに基づいて構成されている。本講演で紹介する Continuous apRHL はapRHLの測度論的拡張と呼ぶべきもので、連続分布型の確率的プログラムであるクエリーの差分プライバシーの検証を可能とする。構成はまず、クエリーの差分プライバシーを、Giryモナドのgradedな二項関係持ち上げによって特徴づけ、それらでjudgementの解釈を与え直すことでapRHLを拡張するという流れである。[Sato, MFPS 2016] 可能であれば、これからの発展などについてもお話ししたい。 -- /_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/ Dept. of Computer Science Graduate School of Information Science and Technology The University of Tokyo Akazaki Takumi mail :<ultraredrays(a)gmail.com> mobile : <090-5379-4901> /_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/

1 0

Talk by Bakhadyr Khoussainov (* 7 Jun 11:00- *)
by Tetsuya Sato 02 Jun '16

02 Jun '16

京都大学数理解析研究所の佐藤です。来週の *火曜日*、6月7日11:00から、オークランド大学のBakhadyr Khoussainov先生に以下の講演をしていただくことになりましたので、ご連絡いたします。どうぞお気軽にお越しください。 ========== Time: 11:00-12:00, 7 Jun, 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: Bakhadyr Khoussainov (University of Auckland) Title: Open questions in the theory of automatic structures. Abstract: In this talk, we introduce the notion of automatic structure (defined by the speaker and Nerode). Informally, these are infinite algebraic structures (such as graphs, trees, groups, linear orders) that can be presented by automata. We present many examples, several basic results, formulate and discuss some open questions in the area.

1 0

高等研究所セミナー「可換環論における逆数学」
by 秋吉亮太 28 May '16

28 May '16

早稲田大学高等研究所の秋吉と申します．以下の要領で，高等研究所セミナー「可換環論における逆数学」を開催いたします．ご都合よろしければぜひご参加ください。 ———————————————————————————————————————————————————————————— 次のようなセミナーを予定しております．参加自由です． ------------------------------------------------------------------------------ 高等研究所主催セミナー講演者：佐藤隆（東北大学理学研究科）日時：6月7日（火）16:00—18:00 場所：早稲田大学早稲田キャンパス9号館5階　第2会議室 (URL: http://www.waseda.jp/wias/) タイトル：可換環論における逆数学アブストラクト：　本研究は「逆数学」の手法を用いて，数学史の観点も加味しながら，可換環論をメタ分析する，というものです．可換環論の歴史を大雑把に辿れば，十九世紀中盤の代数的整数論が動機となり，イデアル論を経て，二十世紀前半の抽象代数学の勃興という道筋が見えてきます．この抽象化にあたって，D. Hilbert, Van der Waerden, E. Noetherらの貢献が指摘できます．その一連の抽象化の中で，本質的に必要とされる公理はどのように変わっていったのでしょうか？これまでに得られた結果から，可算な一般の可換環のクラスについて，その理論を展開するには，算術的集合存在公理（体系ACA）が必要かつ十分であることが示唆されます．一方，より狭いアルティン環のクラスの理論については，より弱い公理である弱ケーニッヒの補題（体系WKL）が必要かつ十分であることがC. Conidisにより示されています．それでは，整数環の素イデアル分解，ネータ環の準素イデアル分解，PIDの単因子論など，各クラスの理論を特徴付ける公理はどのようなものになるのでしょうか？本講演では，以上の結果を紹介するとともに，これからの研究を進めるにあたっての困難な点や，解決のアイディアについてお話しします．問い合わせ先：早稲田大学高等研究所　秋吉亮太 (georg.logic(a)aoni.waseda.jp)

1 0

[CFP] Workshop on Termination - part of Alps Workshops
by Yukiyoshi Kameyama 27 May '16

27 May '16

皆様 > ９月にオーストリアで開催される「合流性に関するワークショップ IWC 2016」の > 論文募集をご案内致します。今回は TRS Meeting, WST, LC&A との合同開催と > なっております。関連する話題をお持ちの方は、ぜひ投稿をご検討下さい。 > 廣川 (JAIST) WST というワークショップの Call for Papers をお送りします。 WST の方は、termination / normalization に関するワークショップです。これらのワークショップは、Innsbruck大学の Aart Middeldorp さんらが全体を企画している Computational Logic in the Alps (CLA2016) http://cl-informatik.uibk.ac.at/events/cla-2016/ というワークショップ集合体の1つとして、 9月上旬の気候の良い頃に、ヨーロッパアルプスのオーストリア側の山あいの施設で開催されます。奮って御投稿ください。 -- 亀山幸義 (筑波大学) http://logic.cs.tsukuba.ac.jp/~kam ========================================================================== WST 2016 - 1st Call for Papers 15th International Workshop on Termination September 5-7, 2016, Obergurgl, Austria http://cl-informatik.uibk.ac.at/events/wst-2016/ ========================================================================== The Workshop on Termination (WST) traditionally brings together, in an informal setting, researchers interested in all aspects of termination, whether this interest be practical or theoretical, primary or derived. The workshop also provides a ground for cross-fertilization of ideas from term rewriting and from the different programming language communities. The friendly atmosphere enables fruitful exchanges leading to joint research and subsequent publications. The event is held as part of CLA 2016 http://cl-informatik.uibk.ac.at/events/cla-2016/ IMPORTANT DATES: * submission June 22, 2016 * notification July 12, 2016 * final version August 3, 2016 * workshop September 5-7, 2016 TOPICS: The 15th International Workshop on Termination welcomes contributions on all aspects of termination and termination analysis. Contributions from the imperative, constraint, functional, and logic programming communities, and papers investigating applications of complexity or termination (for example in program transformation or theorem proving) are particularly welcome. Topics of interest include all aspects of termination. This includes (but is not limited to): * certification of termination and complexity proofs * challenging termination problems * comparison and classification of termination methods * complexity analysis in any domain * implementation of termination and complexity methods * implicit computational complexity * infinitary normalization * non-termination analysis and loop detection * normalization in lambda calculi * operational termination of conditional rewrite systems * ordinal notation and subrecursive hierarchies * SAT, SMT, and constraint solving for (non-)termination analysis * scalability and modularity of termination methods * termination analysis in any domain * well-founded relations and well-quasi-orders COMPETITION: There will be a live complexity and termination competition during the workshop, including time to present both the results and the tools of the participants. More details will be provided in a dedicated announcement on the competition. PROGRAM COMMITTEE: * Ugo Dal Lago Bologna University * J旦rg Endrullis VU University Amsterdam * Yukiyoshi Kameyama University of Tsukuba * Salvador Lucas Universidad Polit辿cnica de Valencia * Aart Middeldorp University of Innsbruck, co-chair * Andrey Rybalchenko Microsoft Research * Thomas Str旦der RWTH Aachen * Ren辿 Thiemann University of Innsbruck, co-chair * Andreas Weiermann Ghent University INVITED SPEAKERS: * Rainer H辰hnle TU Darmstadt SUBMISSION: Submissions are short papers/extended abstract which should not exceed 5 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 provides additional feedback for each submission. The accepted papers will be made available electronically before the workshop. Papers should be submitted electronically via the submission page: http://www.easychair.org/conferences/?conf=wst2016 Final versions should be created using LaTeX and the LIPIcs style file http://drops.dagstuhl.de/styles/lipics/lipics-authors.tgz

1 0

CFP: ESSS 2016
by Yoriyuki Yamagata 18 May '16

18 May '16

皆様、産総研の山形と申します。下記の通り、FM2016併催のワークショップESSS2016の発表を募集いたします。どうぞ宜しくお願い致します。 > 転送されたメッセージ： > > ================================================== > 5th International Workshop on > Engineering Safety and Security Systems > November 7th or 8th, 2015, Limassol, Cyprus > Co-located with FM 2016 in Limassol, Cyprus, November 7-11, 2016 > > More information: > http://pat.scse.ntu.edu.sg/esss16/index.html > =================================================== > > Important dates > ----------------- > * August 12th, 2016: Submission deadline > * September 23rd, 2016: Notification of acceptance/rejection > * November 7th or 8th, 2016: Workshop date > > > Introduction of the Workshop > ----------------- > The International Workshop on Engineering Safety and Security Systems > (ESSS) aims at contributing to the challenge of constructing reliable > and secure systems. The workshop covers areas such as formal > specification, (extended) type checking, model checking, program > analysis/transformation, model-based testing and model-driven software > construction. The workshop will bring together researchers and > industry R&D expertise together to exchange their knowledge, discuss > their research findings, and explore potential collaborations. > > > Theme of the Workshop > ----------------- > The main theme of the workshop is methods and techniques for > constructing large reliable and secure systems. The goal of the > workshop is to establish a platform for the exchange of ideas, > discussion, cross-fertilization, inspiration, co-operation, and > dissemination. The topics of the workshop include, but are not > limited to: > > -- methods, techniques and tools for system safety and security > -- methods, techniques and tools for analysis, certification, and > debugging of complex safety and security systems > -- model-based and verification-based testing > -- emerging application domains such as cloud computing and > cyber-physical systems > -- case studies and experience reports on the use of formal methods > for analyzing safety and security systems > > > Submissions guidelines > ----------------- > Paper submissions must be original, unpublished work. Submissions > should be in made via the Easychair site: > https://www.easychair.org/conferences/?conf=esss2016. > > We invite two types of submissions: > > --Regular papers (up to 15 pages) describing original and unpublished > work within the scope of the workshop. > --Short papers (up to 6 pages) describing work in progress or less > mature results. > > Case studies and tool papers are welcome as well. All submissions must > be prepared in LATEX using the EPTCS macro package. > > The final versions of accepted regular and short papers will be > published as a volume of Electronic Proceedings in Theoretical > Computer Science (EPTCS). Furthermore, authors of a selection of the > accepted papers will be invited to submit an extended version of their > articles to a special issue of a high-quality journal, after the > workshop. Publication of accepted articles requires the commitment of > one of the authors to register for the workshop and present the paper. > > > Workshop chairs > ----------------- > Yang Liu, Nanyang Technological University, Singapore > Sjouke Mauw, University of Luxembourg, Luxembourg > Jun Pang, University of Luxembourg, Luxembourg > > > Program committee > ----------------- > Etienne Andre, Universite Paris 13, France > Guandong Bai, National University of Singapore, Singapore > Weiqiang Kong, Dalian University of Technology, China > Keqin Li, Huawei European Research Center, Germany > Wojciech Mostowski, Halmstad University, Sweden > Volker Stolz, University of Oslo, Norway > Cong Tian, Xidian University, China > Anton Wijs, Eindhoven University of Technology > Yoriyuki Yamagata, AIST, Japan > Tian Zhang, Nanjing University, China — 山形賴之国立研究開発法人産業技術総合研究所主任研究員 http:://staff.aist.go.jp/yoriyuki.yamagata/

1 0

FSCD 2016: Call for participation (early registration: May 22)
by Nao Hirokawa 18 May '16

18 May '16

皆様 6月にポルトガル・ポルトで行われます FSCD の参加者募集の案内をお送り致します。早期登録の締切は5月22日になっております。廣川　(JAIST) ================================================================== CALL FOR PARTICIPATION 1st International Conference on Formal Structures for Computation and Deduction FSCD 2016 22-26 June 2016 Porto, Portugal http://fscd2016.dcc.fc.up.pt/ <http://fscd2016.dcc.fc.up.pt/> 　　 "It is our thesis that formal elegance is 　　 a prerequisite to efficient implementation." -- Gérard Huet FSCD is a new conference covering 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 and homotopy type theory. INVITED SPEAKERS Amal Ahmed (Northeastern University, USA) Ichiro Hasuo (University of Tokyo, Japan) Gérard Huet (INRIA Paris Center, France) Tobias Nipkow (Technical University Munich, Germany) SATELLITE EVENTS - 6th Workshop on Classical Logic and Computation (CL&C) - Concurrent, Resourceful and Effectful COmputation, by Geometry of Interaction: Project Meeting (CRECOGI) - 2nd Workshop on Higher-Dimensional Rewriting and Applications (HDRA) - 8th Workshop on Higher-Order Rewriting (HOR) - IFIP Working Group on Term Rewriting (IFIP-WG 1.6) - 2nd Workshop on Homototy Theory/Univalent Foundations (HOTT/UF) - 8th Workshop on Intersection Types and Related Systems (ITRS) - 4th Workshop on Linearity (LINEARITY) - 18th Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP) - 11th Logical and Semantic Frameworks with Applications (LSFA) - 30th Workshop on Unification (UNIF) - 3rd Workshop on Rewriting Techniques for Program Transformation and Evaluation (WPTE) - 12th Workshop on Automated Specification of Web Systems (WWV) ACCEPTED PAPERS * Dmitriy Traytel. Formal Languages, Formally and Coinductively * Olivier Laurent. Focusing in Orthologic * Stefan Kahrs and Connor Smith. Non-omega-overlapping TRSs are UN * Tomer Libal and Dale Miller. Functions-as-constructors Higher-order Unification * Franziska Rapp and Aart Middeldorp. Automating the First-Order Theory of Rewriting for Left-Linear Right-Ground TRSs * Martin Avanzini and Georg Moser. Complexity of Term Graph Rewriting * Ofer Arieli and Arnon Avron. Minimal Paradefinite Logics for Reasoning with Incompleteness and Inconsistency * Thorsten Altenkirch and Ambrus Kaposi. Normalisation by Evaluation for Dependent Types * Ryota Akiyoshi and Kazushige Terui. Strong normalization for the parameter-free polymorphic lambda calculus based on the Omega-rule * Takahito Aoto and Yoshihito Toyama. Ground Confluence Prover based on Rewriting Induction * Thierry Coquand and Bassel Mannaa. The Independence of Markov’s Principle in Type Theory * Andrej Dudenhefner, Jakob Rehof and Moritz Martens. The Intersection Type Unification Problem * Cynthia Kop and Jakob Grue Simonsen. Complexity Hierarchies and Higher-Order Cons-Free Rewriting * Marcin Benke, Aleksy Schubert and Daria Walukiewicz-Chrząszcz. Synthesis of Functional Programs with Help of First-order Intuitionistic Logic * Kaustuv Chaudhuri, Sonia Marin and Lutz Strassburger. Modular Focused Proof Systems for Intuitionistic Modal Logics * Andrés Aristizábal, Dariusz Biernacki, Sergueï Lenglet and Piotr Polesiuk. Environmental bisimulations for delimited-control operators with dynamic prompt generation * Flavien Breuvart, Giulio Manzonetto, Andrew Polonsky and Domenico Ruoppolo. New Results on Morris's Observational Theory: the benefits of separating the inseparable * Fer-Jan de Vries. On Undefined and Meaningless in Lambda Definability * Stéphane Gimenez and David Obwaller. Interaction Automata and the ia2d Interpreter * Giulio Guerrieri, Luc Pellissier and Lorenzo Tortora De Falco. Computing connected proof(-structure)s from their Taylor expansion * Vincent van Oostrom and Yoshihito Toyama. Normalisation by Random Descent * Naoki Nishida, Adrian Palacios and German Vidal. Reversible Term Rewriting * Amin Timany and Bart Jacobs. Category Theory in Coq 8.5 * Philippe Malbos and Samuel Mimram. Homological Computations for Term Rewriting Systems * Jon Hael Brenas, Rachid Echahed and Martin Strecker. Proving Correctness of Graph Rewriting Systems using C2PDL * Christian Sternagel and Thomas Sternagel. Certifying Confluence of Almost Orthogonal CTRSs via Exact Tree Automata Completion * Valentin Blot. Classical extraction in continuation models * James Laird. Weighted Relational Models for Mobile Names * Krzysztof Bar, Aleks Kissinger and Jamie Vicary. Globular: a proof assistant for higher rewriting * Daniele Nantes-Sobrinho, Mauricio Ayala-Rincon and Maribel Fernandez. Nominal Narrowing * Makoto Hamana. Strongly Normalising Cyclic Data Computation by Iteration Categories of Second-Order Algebraic Theory * Ryuta Arisaka. Structural Interactions and Absorption of Structural Rules in BI Sequent Calculus REGISTRATION The registration page and the hotel reservation page are already open. The early registration deadline is May 15 (local time). For more details please visit our conference webpage: http://fscd2016.dcc.fc.up.pt/registration/ <http://fscd2016.dcc.fc.up.pt/registration/> VENUE The conference will be held at the Department of Computer Science, from the Faculty of Science of the University of Porto. The beautiful city of Porto is the second largest city in Portugal, dating back to the IV century, and classified as world heritage patrimony by UNESCO. The city gives its name to the worldwide renowned Port Wine. PROGRAM CHAIRS Delia Kesner (Univ. Paris-Diderot) Brigitte Pientka (McGill University) PROGRAM COMMITTEE Andreas Abel (Gothenburg Univ.) Zena Ariola (Univ. Oregon) Patrick Baillot (CNRS & ENS Lyon) Andrej Bauer (Univ. Ljubljana) Eduardo Bonelli (Univ. Quilmes) Patricia Bouyer (ENS Cachan) Ugo Dal Lago (Univ. Bologna) Nachum Dershowitz (Univ. Tel Aviv) Mariangiola Dezani-Ciancaglini (Univ. Torino) Derek Dreyer (MPI-SWS) Santiago Figueira (Univ. Buenos Aires) Marcelo Fiore (Univ. Cambridge) Juergen Giesl (Univ. Aachen) Nao Hirokawa (JAIST) Martin Hofmann (LMU Munchen) Delia Kesner (Univ. Paris-Diderot) Naoki Kobayashi (Univ. Tokyo) Dan Licata (Wesleyan Univ.) Chris Lynch (Clarkson Univ.) Narciso Marti-Oliet (Univ. Complutense) Aart Middeldorp (Univ. Innsbruck) Dale Miller (INRIA Saclay) Cesar Munoz (NASA) Vivek Nigam (Univ. Paraiba) Brigitte Pientka (McGill Univ.) Jakob Rehof (Univ. Dortmund) Xavier Rival (ENS Paris) Peter Selinger (Dalhousie Univ.) Paula Severi (Univ. Leicester) Jakob Grue Simonsen (Univ. Copenhagen) Matthieu Sozeau (INRIA Rocquencourt) Sophie Tison (Univ. Lille) Femke van Raamsdonk (VU Univ. Amsterdam) Nobuko Yoshida (Imperial College) CONFERENCE CHAIR Sandra Alves (University of Porto) WORKSHOPS CHAIR Sabine Broda (University of Porto) CONTACT: fscd2016(a)dcc.fc.up.pt <mailto:fscd2016@dcc.fc.up.pt> Looking forward to seeing you in Porto! ==================================================================

1 0

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

16 May '16

みなさま静岡大学の依岡です。以下の研究集会の講演を募集しております。 RIMS研究集会「無限組合せ論と強制法理論」 2016年11月28日から12月1日 http://www.ipc.shizuoka.ac.jp/~styorio/rims16/ 募集締め切りはまだ決まっていません。決まり次第 website でお知らせします。多数の方々にご講演いただきたいと考えております。講演をご希望の方はぜひお気軽に依岡にお知らせください。依岡輝幸静岡大学 styorio(a)ipc.shizuoka.ac.jp

1 0

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

16 May '16

みなさま、愛媛の藤田です。第21回松山TGSAセミナーのお知らせを転送いたします。藤田博司 <fujita.hiroshi.mh(a)ehime-u.ac.jp> -------- Forwarded Message -------- Subject: 松山 TGSAセミナーのお知らせ（６月２日） Date: Sat, 14 May 2016 09:02:35 +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セミナー）のお知らせです。 ***** 第21回のセミナー日時: 2016年6月2日（木） 16:30〜17:30 場所: 愛媛大学理学部2号館2階，大演習室 (201号室) 講演者: 江田勝哉 (早稲田大学) 題目: Infinite sheeted covering map on solenoids Abstract: http://www.math.sci.ehime-u.ac.jp/TGSAsem21-eda-abstract.pdf ***** 講演終了後に交流会（wine party）を以下の要領で行います。日時：2016年6月2日（木）18:30〜場所：Amitie アミティエ住所：愛媛県松山市南堀端町 6-23 TEL：089-998-2811 予算：4,500円〜5,000円程度交流会にご参加いただける方は5月31日（火）までにシャクマトフ <dmitri.shakhmatov(a)ehime-u.ac.jp>まで電子メイルでご連絡下さい。以上、よろしくお願い申し上げます。世話人（五十音順）井上友喜尾國新一シャクマトフディミトリ野倉嗣紀平出耕一平田浩一藤田博司山内貴光 --- ウェブページ： http://www.math.sci.ehime-u.ac.jp/MTGSA.ja.html

1 0

IWC 2016 - Call for Papers
by Nao Hirokawa 14 May '16

14 May '16

皆様９月にオーストリアで開催される「合流性に関するワークショップ IWC 2016」の論文募集をご案内致します。今回は TRS Meeting, WST, LC&A との合同開催となっております。関連する話題をお持ちの方は、ぜひ投稿をご検討下さい。廣川 (JAIST) ===================================================================== Call for Papers IWC 2016 5th International Workshop on Confluence Sep 8-9, 2016, Obergurgl, Austria, Part of Computational Logic in the Alps, CLA 2016 http://www.csl.sri.com/~tiwari/iwc2016/ ===================================================================== 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 had 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 2016 is part of the Computational Logic in the Alps event to be held in Obergurgl, Austria, during the week Sep 4-10, 2016. Previous editions of the workshop were held in Nagoya (2012), Eindhoven (2013), Vienna (2014), and Berlin (2015). During the workshop, the 5th Confluence Competition (CoCo 2016) takes place. IMPORTANT DATES: * submission June 22, 2016 * notification July 12, 2016 * final version Aug 03, 2016 * workshop Sep 8-9, 2016 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: * TBD PROGRAM COMMITTEE: * Beniamino Accattoli (INRIA) * Bertram Felgenhauer (University of Innsbruck) * Yves Guiraud (University of Paris 7) * Nao Hirokawa (JAIST) * Koji Nakazawa (Nagoya) * Ashish Tiwari (Menlo Park) 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=iwc2016

2 3

AiML-2016: CALL FOR SHORT PRESENTATIONS
by 小野寛晰 09 May '16

09 May '16

(sorry for multiple copies) AiML-2016: CALL FOR SHORT PRESENTATIONS Short presentations submission deadline: 20 May 2016 Short presentations acceptance notification: 3 June 2016 11TH INTERNATIONAL CONFERENCE ON ADVANCES IN MODAL LOGIC BUDAPEST, 30 AUGUST -- 2 SEPTEMBER 2016 http://phil.elte.hu/aiml2016/ <http://phil.elte.hu/aiml2016/> Advances in Modal Logic is an initiative aimed at presenting the state of the art in modal logic and its various applications. The initiative consists of a conference series together with volumes based on the conferences. Information about the AiML series can be obtained at http://www.aiml.net <http://www.aiml.net/>. AiML-2016 is the 11th conference in the series. TOPICS We invite submission on all aspects of modal logic, including: - history of modal logic - philosophy of modal logic - applications of modal logic - computational aspects of modal logic (complexity and decidability of modal and temporal logics, modal and temporal logic programming, model checking, model generation, theorem proving for modal logics) - theoretical aspects of modal logic (algebraic/categorical perspectives on modal logic, coalgebraic modal logic, completeness and canonicity, correspondence and duality theory, many-dimensional modal logics, modal fixed point logics, model theory of modal logic, proof theory of modal logic) - specific instances and variations of modal logic (description logics, modal logics over non-boolean bases, dynamic logics and other process logics, epistemic and deontic logics, modal logics for agent-based systems, modal logic and game theory, modal logic and grammar formalisms, provability and interpretability logics, spatial and temporal logics, hybrid logic, intuitionistic logic, substructural logics, computationally light fragments of all such logics) Papers on related subjects will also be considered. PAPER SUBMISSIONS There will be two types of submissions to AiML-2016: (1) Full papers for publication in the proceedings and presentation at the conference. (2) Short presentations intended for presentation at the conference but not for the published proceedings. Both types of papers should be submitted electronically using the EasyChair submission page at https://easychair.org/conferences/?conf=aiml16 <https://easychair.org/conferences/?conf=aiml16> At least one author of each accepted paper or short presentation must register for and attend the conference. (2) SHORT PRESENTATIONS. These should be at most 5 pages. They may describe preliminary results, work in progress etc., and will be subject to light reviewing. The accepted submissions will be made available at the conference, and the authors will have the opportunity to give short presentations (of up to 15 minutes) on them. INVITED SPEAKERS INCLUDE: Sonja Smets (ILLC, Universiteit van Amsterdam) Yde Venema (ILLC, Universiteit van Amsterdam) Guram Bezhanishvili (New Mexico State University) LOCAL ORGANIZING COMMITTEE Tamas Bitai (Eotvos University, Budapest, Hungary) Reka Markovich (Eotvos University, Budapest, Hungary) Andras Mate (Eotvos University, Budapest, Hungary) Péter Mekis (Eotvos University, Budapest, Hungary) Attila Molnar (Eotvos University, Budapest, Hungary) Gergely Szekely (Alfred Rényi Institute of Mathematics, Hungarian Academy of Sciences) PROGRAMME COMMITTEE Natasha Alechina (University of Nottingham) Carlos Areces (FaMAF, Universidad Nacional de Córdoba) Philippe Balbiani (IRIT, Toulouse, France) Alexandru Baltag (FNWI ILLC) Lev Beklemishev (Steklov Mathematical Institute of Russian Academy of Sciences in Moscow) Thomas Bolander (Technical University of Denmark) Torben Brauner (Roskilde University, Denmark) Serenella Cerrito (Laboratoire IBISC, Evry France) Stéphane Demri (LSV, CNRS, ENS Cachan) Valeria de Paiva (Nuance, USA) David Fernandez-Duque (Instituto Tecnológico Autónomo de México) Melvin Fitting (Lehman College, CUNY, USA) David Gabelaia (The Free University of Tbilisi, Tbilisi, Georgia) Silvio Ghilardi (Università degli Studi di Milano, Italy) Valentin Goranko (Stockholm University) Rajeev Gore (The Australian National University) Andreas Herzig (IRIT, Toulouse, France) Rosalie Iemhoff (Utrecht University) Agi Kurucz (King's College London) Roman Kuznets (TU Wien) Martin Lange (University of Kassel, Germany) Carsten Lutz (Universität Bremen) Andras Mate (Eotvos University, Budapest, Hungary) Angelo Montanari (University of Udine) Larry Moss (Indiana University, USA) Sara Negri (University of Helsinki) Sergei Odintsov (Novosibirsk State University) Hiroakira Ono (Japan Advanced Insitute of Science and Technology) Mark Reynolds (The University of Western Australia) Ilya Shapirovsky (Institute for the Information Transmission Problems) Renate Schmidt (University of Manchester) Valentin Shehtman (Institute for the Information Transmission Problems) Viorica Sofronie-Stokkermans (Universitat Koblenz-Landau) Thomas Studer (Universität Bern) Rineke Verbrugge (Groningen, NL) Heinrich Wansing (Ruhr University Bochum) Michael Zakharyaschev (Birkbeck College London, UK) PROGRAMME COMMITTEE CO-CHAIRS Lev Beklemishev (Steklov Mathematical Institute of Russian Academy of Sciences in Moscow) Stephane Demri (LSV, CNRS, ENS Cachan) IMPORTANT DATES Full papers acceptance notification: 18 May 2016 Short presentations submission deadline: 20 May 2016 Short presentations acceptance notification: 3 June 2016 Final version of full papers and short presentations due: 12 June 2016 Conference: 30 August -- 2 September 2016 FURTHER INFORMATION. Please see http://phil.elte.hu/aiml2016/?page=call_for_papers <http://phil.elte.hu/aiml2016/?page=call_for_papers> ENQUIRIES. E-mail enquiries should be directed to the PC co-chairs, sent to aiml16(a)easychair.org <mailto:aiml16@easychair.org>

1 0

(Reminder) Talk by Cho Kenta (Nijmegen), Tue 10 May
by Takumi Akazaki 09 May '16

09 May '16

みなさま、東京大学蓮尾研の赤崎と申します。先日お伝えした通リ、明日13:00より、Nijmegenの長健太さんをお招きして講演をしていただきます。ぜひご参加ください。日時: 5月10日(火) 13:00-15:00 場所: 東京大学理学部７号館214教室 ----------- Tue 10 May 2016, 13:00–15:00 理学部7号館214 Room 214, School of Science Bldg. No. 7 Kenta Cho <https://www.google.com/url?q=http://www.cs.ru.nl/K.Cho/&sa=D&ust=1461640002…> (Inst. of Comp. & Info. Sci., Radboud University), Von Neumann algebras from a logical / categorical perspective Many researches at the Nijmegen group involve von Neumann algebras, which are now important not only in quantum physics but also in the context of quantum computation and information. I plan to talk about: 1) basics of von Neumann algebras and quantum theory; 2) von Neumann algebras in effectus theory (a categorical approach to quantum computation and logic); 3) von Neumann algebras as a (categorical, denotational) model of the quantum lambda calculus. -- /_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/ Dept. of Computer Science Graduate School of Information Science and Technology The University of Tokyo Akazaki Takumi mail :<ultraredrays(a)gmail.com> mobile : <090-5379-4901> /_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/

1 0

4th AJSW = 45th TRS Meeting
by Nao Hirokawa 03 May '16

03 May '16

皆様今年９月に開催される「第45回 TRS Meeting」参加者募集をご案内致します。通常、国内で開催しておりますが、今回は項書換えに関する日墺のサマーワークショップとして、オーストリアのオーバーグルグルで開催されます。皆様、ぜひ参加をご検討下さい。廣川直 (JAIST) ====================================================================== 4th Austria-Japan Summer Workshop on Term Rewriting 45th TRS Meeting Obergurgl http://cl-informatik.uibk.ac.at/events/ajsw-2016/ AJSW is an informal workshop for researchers in Austria and Japan and aims to facilitate and share new developments and ideas in term rewriting. Not only presentations about published results but also work-in-progress talks are welcome. The event is held as part of CLA 2016 http://cl-informatik.uibk.ac.at/events/cla-2016/ and synonymous with the 45th TRS Meeting. The Term Rewriting Meeting (TRS Meeting) is a biannual informal workshop that aims at promoting the research on rewriting and related areas. Participants are expected to give a talk of approximately 15 to 60 minutes in English on their research activities. The subject of the talk is not required to be one's original result; for example, explaining an interesting paper is perfectly acceptable. (For information on TRS meetings in general, see: http://www.jaist.ac.jp/~hirokawa/trs-meeting/) Date: September 7 (Wed) -- 9 (Fr), 2013 Venue: Obergurgl University Center http://www.uz-obergurgl.at/english/ Gaisbergweg 5, 6456 Obergurgl, Austria Program September 7 (Wed) CLA excursion September 8 (Thu) first day of workshop September 9 (Fri) second day of workshop Preliminary Registration Please indicate whether you would like to join by sending the registration form below to Christian Sternagel (christian.sternagel(a)uibk.ac.at) as soon as possible. This is just in order to get a rough estimate of the number of participants. The official registration and arrangements for accommodation will be handled through the main CLA 2016 event. ---------------------------------------------------------------------- Registration Form of the 45th TRS Meeting name: affiliation: number of accompanying persons: attendance: CLA / AJSW + excursion / AJSW only ---------------------------------------------------------------------- * number of accompanying persons: in case you want to bring family and/or significant others (which is encouraged), please indicate the number of additional persons here * CLA: full week, arrival on September 4 (Sun) and departure on September 10 (Sat); this is the preferred option * AJSW + excursion: arrival on September 6 (Tue) and departure on September 10 (Sat) * AJSW only: arrival on September 7 (Wed) and departure on September 10 (Sat)

1 0

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Logic-ml