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

International Conference on Topology and Geometry 2013 （９月２日〜６日）
by Joerg Brendle 04 Jun '13

04 Jun '13

みなさま、神戸大学のブレンドレです。９月２日〜６日まで島根大学で国際会議 International Conference on Topology and Geometry 2013 が開催されます。７つのスペシャル・セッションの一つとして集合論のスペシャル・セッションを開くこととなっています。詳細については下記のホームページをご覧下さい。 http://www.math.shimane-u.ac.jp/~topgeo2013/ レジストレーションやアブストラクトの投稿の締切は *６月１６日* です。トポロジーや幾何学などと関係のある基礎論の分野のみなさまの参加をお待ちしています。よろしくお願いします。 joerg brendle

1 0

CfP: 2nd International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS2013)
by Takashi KITAMURA 04 Jun '13

04 Jun '13

皆様、産業技術総合研究所の北村です。今年10月にニュージーランドで開催される FTSCS2013 の論文募集の案内をお送りいたします。是非論文投稿をご検討下さい。 --------------------------------------------------------------------- Call for Papers FTSCS 2013 2nd International Workshop on Formal Techniques for Safety-Critical Systems Queenstown, New Zealand, October 29, 2013 (satellite workshop of ICFEM 2013) http://www.ftscs.org --------------------------------------------------------------------- *** Science of Computer Programming special issue *** *** Springer CCIS proceedings *** Aims and Scope: There is an increasing demand in industry to use formal methods to achieve software-independent verification and validation of safety-critical systems, e.g., in fields such as avionics, automotive, medical, and other cyber-physical systems. Newer standards, such as DO-178C (avionics) and ISO 26262 (automotive), emphasize the need for formal methods and model-based development, 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. In particular, FTSCS strives 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, 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. Invited speaker: TBA 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 format); 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 will be done electronically via EasyChair at http://www.easychair.org/conferences/?conf=ftscs2013. 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 2013. 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 1, 2013 Notification of acceptance: September 28, 2013 Workshop: October 29, 2013 Venue: Queenstown, New Zealand Program chairs: Cyrille Artho AIST, Japan Peter Olveczky University of Oslo, Norway Program committee: Erika Abraham RWTH Aachen University, Germany Musab AlTurki King Fahd University of Petroleum and Minerals, Saudi Arabia Farhad Arbab Leiden University and CWI, The Netherlands Cyrille Artho AIST, Japan Saddek Bensalem Verimag, France Armin Biere Johannes Kepler University, Austria Santiago Escobar Universidad Politecnica de Valencia, Spain Ansgar Fehnker University of the South Pacific, Fiji Mamoun Filali IRIT, France Bernd Fischer Stellenbosch University, South Africa and University of Southampton, UK Kokichi Futatsugi JAIST, Japan Klaus Havelund NASA JPL, USA Marieke Huisman University of Twente, The Netherlands Ralf Huuck NICTA/UNSW, Sydney, Australia Fuyuki Ishikawa National Institute of Informatics, Tokyo, Japan Takashi Kitamura AIST, Japan Alexander Knapp Augsburg University, Germany Paddy Krishnan Oracle Labs Brisbane, Australia Yang Liu Nanyang Technological University, Singapore Robi Malik University of Waikato, New Zealand Cesar Munoz NASA Langley, USA Tang Nguyen UST Hanoi, Vietnam Thomas Noll RWTH Aachen University, Germany Peter Olveczky University of Oslo, Norway Paul Pettersson Malardalen University, Sweden Camilo Rocha Escuela Colombiana de Ingenieria, Colombia Grigore Rosu University of Illinois at Urbana-Champaign, USA Neha Rungta NASA Ames, USA Ralf Sasse ETH Zurich, Switzerland Oleg Sokolsky University of Pennsylvania, USA Sofiene Tahar Concordia University, Canada Carolyn Talcott SRI International, USA Tatsuhiro Tsuchiya Osaka University, Japan Michael Whalen University of Minnesota, USA Peng Wu Chinese Academy of Sciences, China Contact: (web) http://www.ftscs.org (email) peterol(a)ifi.uio.no and c.artho(a)aist.go.jp -- Takashi KITAMURA Ph.D. t.kitamura(a)aist.go.jp http://staff.aist.go.jp/t.kitamura/ Research Institute for Secure Systems (RISEC) National Institute of Advanced Industrial Science and Technology (AIST) Nakoji 3-11-46, Amagasaki, Hyogo 661-0974, Japan Tel: +81-6-6494-8054 Fax: +81-6-6494-8073 Internal Tel: *33-274-71902

1 0

数学基礎論サマースクール（８月５日−７日）
by Kazushige TERUI 04 Jun '13

04 Jun '13

みなさま今年度の数学基礎論サマースクールのご案内をさせていただきます。今年のテーマは「証明と構成」です。基礎論のみならず、計算機科学や数学の哲学など幅広い分野のみなさまの参加をお待ちしております。詳細については下記ホームページをご参照ください。なお、サマースクールに引き続き8月8日−9日には証明論研究集会を開催する予定です。こちらについては追ってご案内させていただきます。身近に学生さんや興味を持たれそうな方がいらっしゃいましたらご転送いただければ幸いです。どうぞよろしくお願いします。照井一成 -------------------------------------------------- 数学基礎論サマースクール 2013 ホームページ： http://www.kurims.kyoto-u.ac.jp/~terui/school2013.html ・テーマ：証明と構成・日時： 2013年8月5日（月）午後 -- 8月7日（水）午後・会場：慶応義塾大学　三田キャンパス・参加費：無料・申し込み：懇親会（8月6日）の参加・不参加のみお知らせください。・講師　新井敏康（千葉大学）　勝股審也（京都大学）　照井一成（京都大学）　根元多佳子（JAIST） ------------------------------------------ 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

APLAS 2013 second call for papers
by Chung-chieh Shan 03 Jun '13

03 Jun '13

APLASの締め切りが6月14日に迫って来ました。重複をご容赦下さい。 =============================================================== APLAS 2013 11th Asian Symposium on Programming Languages and Systems 9-11 December 2013 Melbourne, Australia (colocated with CPP 2013) CALL FOR PAPERS =============================================================== ========== BACKGROUND ========== APLAS aims to stimulate programming language research by providing a forum for the presentation of latest results and the exchange of ideas in programming languages and systems. APLAS is based in Asia, but is an international forum that serves the worldwide programming language community. APLAS is sponsored by the Asian Association for Foundation of Software (AAFS) founded by Asian researchers in cooperation with many researchers from Europe and the USA. Past APLAS symposiums were successfully held in Kyoto ('12), Kenting ('11), Shanghai ('10), Seoul ('09), Bangalore ('08), Singapore ('07), Sydney ('06), Tsukuba ('05), Taipei ('04) and Beijing ('03) after three informal workshops. Proceedings of the past symposiums were published in Springer's LNCS. ====== TOPICS ====== The symposium is devoted to foundational and practical issues in programming languages and systems. Papers are solicited on topics such as * semantics, logics, foundational theory; * design of languages, type systems and foundational calculi; * domain-specific languages; * compilers, interpreters, abstract machines; * program derivation, synthesis and transformation; * program analysis, verification, model-checking; * logic, constraint, probabilistic and quantum programming; * software security; * concurrency and parallelism; * tools and environments for programming and implementation. Topics are not limited to those discussed in previous symposiums. Papers identifying future directions of programming and those addressing the rapid changes of the underlying computing platforms are especially welcome. Demonstration of systems and tools in the scope of APLAS are welcome to the System and Tool presentations category. Authors concerned about the appropriateness of a topic are welcome to consult with program chair prior to submission. ========== SUBMISSION ========== We solicit submissions in two categories: *Regular research papers* describing original scientific research results, including tool development and case studies. Regular research papers should not exceed 16 pages in the Springer LNCS format, including bibliography and figures. They should clearly identify what has been accomplished and why it is significant. Submissions will be judged on the basis of significance, relevance, correctness, originality, and clarity. In case of lack of space, proofs, experimental results, or any information supporting the technical results of the paper could be provided as an appendix or a link to a web page, but reviewers are not obliged to read them. *System and Tool presentations* describing systems or tools that support theory, program construction, reasoning, or program execution in the scope of APLAS. System and Tool presentations are expected to be centered around a demonstration. The paper and the demonstration should identify the novelties of the tools and use motivating examples. System and Tool papers should not exceed 8 pages in the Springer LNCS format, including bibliography and figures. Submissions will be judged based on both the papers and the described systems or tools. It is highly desirable that the tools are available on the web. Papers should be submitted electronically via the submission web page: https://www.easychair.org/conferences/?conf=aplas2013 Acceptable formats are PostScript or PDF. Submitted papers must be unpublished and not submitted for publication elsewhere. Papers must be written in English. The proceedings will be published as a volume in Springer's LNCS series. Accepted papers must be presented at the conference. (While the general chair and the program chair cannot submit papers, other members of the program committee can.) ===== DATES ===== Abstract due: 10 June 2013 (Monday), 23:59 UTC Submission due: 14 June 2013 (Friday), 23:59 UTC Notification: 26 August 2013 (Monday) Final paper due: 19 September 2013 (Thursday) Conference: 9-11 December 2013 (Monday-Wednesday) ========== ORGANIZERS ========== General chair: Peter Schachte (University of Melbourne) Program chair: Chung-chieh Shan (Indiana University) Program committee: Filippo Bonchi (CNRS, ENS-Lyon, France) Yu-Fang Chen (Academia Sinica, Taiwan) Shigeru Chiba (The University of Tokyo, Japan) Jacques Garrigue (Nagoya University, Japan) Robert Glück (University of Copenhagen, Denmark) R. Govindarajan (Indian Institute of Science, India) Kazuhiro Inaba (Google, Inc., Japan) Jie-Hong Roland Jiang (National Taiwan University, Taiwan) Shin-ya Katsumata (Kyoto University, Japan) Gabriele Keller (University of New South Wales, Australia) Ana Milanova (Rensselaer Polytechnic Institute, USA) Keisuke Nakano (The University of Electro-Communications, Japan) Hakjoo Oh (Seoul National University, Korea) Bruno C. d. S. Oliveira (National University of Singapore, Singapore) Kaushik Rajan (Microsoft Research, India) Max Schäfer (Nanyang Technological University, Singapore) Ulrich Schöpp (Ludwig-Maximilians-Universität München, Germany) Paula Severi (University of Leicester, UK) Gang Tan (Lehigh University, USA) Hiroshi Unno (University of Tsukuba, Japan) Meng Wang (Chalmers University of Technology, Sweden) Jingling Xue (University of New South Wales, Australia) Mingsheng Ying (University of Technology, Sydney, Australia) Kenny Q. Zhu (Shanghai Jiao Tong University, China) ======= CONTACT ======= http://aplas2013.soic.indiana.edu/ aplas2013(a)easychair.org

1 0

KEOD special session
by 小野寛晰 31 May '13

31 May '13

皆様以下のメールを代理投稿します。　小野寛晰 ---------------------------------------- Dear Madam/Sir, I would like to announce the KEOD’s Special Session (this year in Vilamoura, Portugal) devoted to formal and non-formal aspects of nonmonotonicity. Strict applying of the definition of nonmonotonic inference shows that many examples for nonmonotonicity of human thinking as well as constructions, traditionally understood as nonmonotonic have nothing common with the negation of well known Tarski’s condition for monotonic operation. A rejection from nonmonotonic interpretation of those examples and constructions opens new perspectives in researches on human thinking. http://www.keod.ic3k.org/non-nonmonotonicity.aspx With kind regards, Piotr Lukowski - Chair of KEOD’s Special Session: “Non-nonmonotonicity” Department of Cognitive Science Institute of Psychology University of Lodz, Poland

1 0

Fwd: GALOP 2013 - 2nd Call for Papers
by Ichiro Hasuo 28 May '13

28 May '13

みなさま，こんにちは！東京大学の蓮尾です． SCメンバーとして，ゲーム意味論についてのワークショップ GaLoP のご案内を再度お送りします．投稿締切は 5/31 ですが，アブストラクトのみの投稿で，論文投稿は optional です．ぜひご検討ください．どうかよろしくお願いいたします．それでは！蓮尾一郎 http://www-mmm.is.s.u-tokyo.ac.jp/~ichiro/ ---------- Forwarded message ---------- 8th Workshop on Games for Logic and Programming Languages (GaLoP 2013) // Queen Mary, University of London // London, UK // 18-19 July // [http://www.gamesemantics.org] ----------------------------------------------------------------------- Please note the deadline of *** MAY 31 *** for submission of abstracts. ----------------------------------------------------------------------- GaLoP is an annual international workshop on game-semantic models for logics and programming languages and their applications. This is an informal workshop that welcomes work in progress, overviews of more extensive work, programmatic or position papers and tutorials as well as contributed papers and invited talks. GaLoP VIII will be held in London, UK, on 18-19 July 2013. It will be a stand-alone workshop hosted at the Mile End campus of Queen Mary, University of London. Contributions are invited on all pertinent subjects, with particular interest in game-semantic and interaction models for logics and programming languages, and applications to program analysis. Typical but not exclusive areas of interest are: * Game theory and interaction models in semantics; * Games-based program analysis and verification; * Logics for games and games for logics; * Algorithmic aspects of games; * Categorical aspects; * Programming languages and full abstraction; * Higher-order automata and Petri nets; * Geometry of interaction; * Ludics; * Epistemic game theory; * Logics of dependence and independence; * Computational linguistics. There will be no formal proceedings but the possibility of a special issue in a journal will be considered (the 2005, 2008 and 2011 workshops led to special issues in Annals of Pure and Applied Logic). // Submission Instructions // Please submit an abstract of your proposed talk on the easychair submission page below. You may also submit an accompanying paper for the talk. https://www.easychair.org/conferences/?conf=galop2013 // Important Dates // Submission: May 31 Notification: June 7 Workshop: July 18-19 // Invited speakers // * Ichiro Hasuo, Tokyo * Colin Stirling, Edinburgh * Viktor Winschel, Mannheim * Nobuko Yoshida, Imperial // Program Committee // * Ugo Dal Lago, Bologna * Dan Ghica, Birmingham * Juha Kontinen, Helsinki * Guy McCusker, Bath (co-chair) * Andrzej Murawski, Warwick * Nikos Tzevelekos, QMUL (co-chair) * Glynn Winskel, Cambridge

1 0

Kobe Colloquium on Logic, Statistics and Informatics, May 28 (Daisuke Ikegami)
by Joerg Brendle 23 May '13

23 May '13

Kobe Colloquium on Logic, Statistics and Informatics 以下の要領でコロキウムを開催します。日時：2013年5月28日（火）13:20-14:50 講演者：Daisuke Ikegami (University of California, Berkeley) 場所：神戸大学自然科学総合研究棟3号館4階421室（プレゼンテーション室） ============================================================ 題目： Inner models from logics アブストラクト： The goal of this research is to construct a model of set theory which is "close to" HOD but easier to analyze. The motivation comes from Woodin's HOD Conjecture, which states that HOD is very "close to" V under the presence of a very strong large cardinal (extendible cardinal). HOD Conjecture is closely related to the problem of constructing a canonical extender model with a supercompact cardinal and it has striking applications to the theory of large cardinals without the Axiom of Choice. To solve HOD Conjecture, one would expect a fine analysis of HOD. The difficulty of the analysis of HOD lies in the fact that HOD is very "non-absolute", e.g., one could force V = HOD with a proper class partial order. Given that HOD is obtained using full second order logic in the same way as Gödel's constructible universe L via first order logic, in this talk, we use Boolean valued higher order logics to construct inner models of set theory which are more "absolute" than HOD and investigate the properties of the models. ============================================================ 交通：阪急六甲駅またはJR六甲道駅から神戸市バス36系統「鶴甲団地」行きに乗車，「神大本部工学部前」停留所下車，徒歩すぐ． http://www.kobe-u.ac.jp/info/access/rokko/rokkodai-dai2.htm 連絡先：ブレンドレヨーグ brendle(a)kurt.scitec.kobe-u.ac.jp

1 0

Talk by Irek Ulidowski (U. Leicester), Tue 21 May
by Ichiro Hasuo 21 May '13

21 May '13

みなさま，東京大学の蓮尾です．来週火曜日の研究室セミナーでは， Leicester 大学の Irek Ulidowski さんをお迎えしてプロセス計算と event structure に関するご研究をお話いただきます．ぜひご参加ください．蓮尾一郎 http://www-mmm.is.s.u-tokyo.ac.jp/ ________________________________ Tue 21 May 2013, 15:30-17:30 Irek Ulidowski (University of Leicester) Modelling of bonding with processes ad events 理学部7号館1階 102教室 Room 102, School of Science Bldg. No. 7 アクセス： https://www-mmm.is.s.u-tokyo.ac.jp/indexj.html （一番下） Access: http://www-mmm.is.s.u-tokyo.ac.jp/ (see bottom) We introduce two forms of modelling of systems that consist of objects that are combined together by the means of bonds. In reaction systems for bonding we define how bonds are created and dissolved via reduction-style semantics. The usefulness of reaction systems is illustrated with examples taken from software engineering and biochemistry. We also introduce reversible event structures and define the notion of configuration. We then discuss how to give semantics of reaction systems for bonding in terms of reversible event structures.

1 1

Seminar (Bakhadyr Khoussainov), Mon May 20, Tamachi
by Akitoshi Kawamura 18 May '13

18 May '13

皆様東大の河村ですお世話になっております直前の御連絡ですみませんが 20日（月）の講演会の御案内ですどうぞお越し下さい -- 河村彰星東京大学大学院情報理工学系研究科コンピュータ科学専攻助教（今井研究室） 03-5841-4097 http://www-imai.is.s.u-tokyo.ac.jp/~kawamura/index_j.html ELC Seminar http://www.al.ics.saitama-u.ac.jp/elc/event/list.cgi?regid=20130520-0000-20… Monday 1 pm, May 20, 2013 Seminar room, ELC Centre, 5th floor of Tokyo Institute of Technology Tamachi office (東京工業大学キャンパスイノベーションセンター) http://www.al.ics.saitama-u.ac.jp/elc/en/?celc Algorithmically random infinite structures Bakhadyr Khoussainov (University of Auckland) The last two decades have witnessed significant advances in the investigation of algorithmic randomness of infinite strings. Monographs by Downey and Hirschfeldt, and by Nies account for the recent research activities in the area. In spite of much work, research on randomness of infinite strings has excluded the investigation of algorithmic randomness for infinite algebraic structures such graphs, trees, groups or more generally universal algebras. In this talk, we provide a framework for reasoning about algorithmic randomness for various classes of infinite structures.

1 0

Nagoya Set Theory Seminar
by 吉信康夫 17 May '13

17 May '13

皆様：以下の要領で名古屋集合論セミナーを開催します。奮って御参加下さい。日時：5月24日(金) 15:30- 場所：名古屋大学全学教育棟3階 SIS5 教室 (http://www.nagoya-u.ac.jp/2012website/global-info/images/access-map/map2.pdf の地図でB4(1)の建物です。建物内配置図は http://www.ilas.nagoya-u.ac.jp/student/lectureroom/ でご覧になれます。 SIS5 教室は3階の中央より少し北, C36の北隣にあります。) 講演者：池上大祐 (学振海外特別研究員, カリフォルニア大学バークレー校) 題： Inner models from logics アブストラクト： The goal of this research is to construct a model of set theory which is "close to" HOD but easier to analyze. The motivation comes from Woodin's HOD Conjecture, which states that HOD is very "close to" V under the presence of a very strong large cardinal (extendible cardinal). HOD Conjecture is closely related to the problem of constructing a canonical extender model with a supercompact cardinal and it has striking applications to the theory of large cardinals without the Axiom of Choice. To solve HOD Conjecture, one would expect a fine analysis of HOD. The difficulty of the analysis of HOD lies in the fact that HOD is very "non-absolute", e.g., one could force V = HOD with a proper class partial order. Given that HOD is obtained using full second order logic in the same way as Gödel's constructible universe L via first order logic, in this talk, we use Boolean valued higher order logics to construct inner models of set theory which are more "absolute" than HOD and investigate the properties of the models.

1 0

NUE seminar (33)
by Yoshihito Toyama 16 May '13

16 May '13

第 33 回 NUEセミナーのお知らせ東北大学・電気通信研究所・外山研究室ではNUEセミナーを開催しています。テーマはプログラム理論や定理自動証明を中心に、情報科学の理論的なさまざまな話題をとりあげています。興味をおもちの方はどなたでもフラリと気楽におたちより下さい。 ********************************************* 日時：　５月２３日（木）１４：００ -- １５：３０場所：東北大学・電気通信研究所・２号館・４階中会議室 (W401) ********************************************* 講演話題提供者： Irek Ulidowski (University of Leicester) 題目： Modelling of bonding with processes ad events 概要： We introduce two forms of modelling of systems that consist of objects that are combined together by the means of bonds. In reaction systems for bonding we define how bonds are created and dissolved via reduction-style semantics. The usefulness of reaction systems is illustrated with examples taken from software engineering and biochemistry. We also introduce reversible event structures and define the notion of configuration. We then discuss how to give semantics of reaction systems for bonding in terms of reversible event structures. ============================================== NUEセミナーに関する問い合わせは以下にどうぞ。外山芳人〒980-8577 仙台市青葉区片平 2-1-1 東北大学電気通信研究所 TEL 022 217 5449 FAX 022 217 5452 MAIL toyama(a)nue.riec.tohoku.ac.jp

1 0

教員公募 (東北大学)
by Yoshihito Toyama 15 May '13

15 May '13

LOGIC MLの皆様メーリングリストをお借りして、の教員公募教授１名の案内を送付いたします。(重複して受信された場合はご容赦ください) 応募締切は 7月26日（金）必着です。外山芳人@東北大学 ----------------------------------------------------------------------- 教員公募情報東北大学大学院情報科学研究科情報基礎科学専攻では、教授職の教員を下記により公募いたします。募集人員：教授１名所　　属：情報基礎科学専攻ソフトウェア基礎科学分野専門分野：　本分野では、ソフトウェアが実現すべき機能の複雑化と高機能化に対する要請に応えるために、ソフトウェアの厳密な論理構造の追究と、それに基づく信頼性や生産性を支える新たな学術的基盤の確立を目的としています。具体的には、プログラムや仕様記述などの形式化に基づいた開発手法や検証手法の構築を通して高信頼性・高生産性を有するソフトウェア開発に貢献するための研究と教育を行います。着任時期：平成26年4月頃、またはそれ以降のなるべく早い時期応募資格：博士号取得者。年齢については特に制限はありません。応募期限：平成25年7月26日（金）必着なお、提出書類や書類送付先などの詳細につきましては以下をご覧ください。 http://www.is.tohoku.ac.jp/publicadv/kobo130425.html -----------------------------------------------------------------------

1 0

Fwd: PhD positions in operational semantics at Univ. of Warsaw
by Ichiro Hasuo 14 May '13

14 May '13

みなさま，東京大学の蓮尾です．ワルシャワ大学の Bartek Klin さんからの博士課程学生募集のメッセージを転送します．プロジェクトの内容は bialgebra と operational semantics で，給料はとても良くはありませんが，ワルシャワの物価を考えると十分な額だと思います．ごはんもおいしくて楽しい街です．また，同じプロジェクトでポスドクの募集もそのうちにあるそうです．蓮尾一郎 www-mmm.is.s.u-tokyo.ac.jp/~ichiro/ ----------------------------------------------------------------------------------------------------------- Two PhD student positions will soon be available to work under the direction of Bartek Klin in the Institute of Informatics, University of Warsaw. The positions are in the field of semantics of programming languages and process algebras, in connection to the project "Modular operational semantics: a bialgebraic approach", funded by the Polish National Science Center. The applicants should have solid background in Mathematics and Computer Science, and be interested in topics such as semantics of programming languages, process algebra, formal methods, and/or category theory. The positions will be available from October 2013. Interested candidates should apply for a PhD fellowship at the Warsaw Center of Mathematics and Computer Science (http://www.wcmcs.edu.pl/node/38), with the deadline of *** June 7th, 2013 ***. A successful candidate will earn 5000PLN(~1200EUR)/month (3500PLN tax-free from the WCMCS fellowship + 1500PLN pre-tax funded by the research project), subject to yearly evaluation of progress. The positions are associated with teaching duties of up to 60 hours/year. Any queries about the positions should be addressed to Bartek Klin, klin(a)mimuw.edu.pl . -----------------------------------------------------------------------------------------------------------

1 0

DCM 2013 - Call for Papers
by Nao Hirokawa 10 May '13

10 May '13

皆様 CONCUR 2013 に併設されます、計算モデルに関するワークショップ DCM 2013 の論文募集の案内をお送り致します。ご投稿・ご参加を検討して頂ければ幸いです。廣川　直（JAIST） ====================================================================== Call for Papers DCM 2013 Developments in Computational Models http://www.dcm-workshop.org.uk/2013 Buenos Aires, Argentina Monday August 26 2013 A satellite event of CONCUR 2013 ====================================================================== Several new models of computation have emerged in the last years, and many developments of traditional computational models have been proposed with the aim of taking into account the new demands of computer systems users and the new capabilities of computation engines. A new computational model, or a new feature in a traditional one, usually is reflected in a new family of programming languages, and new paradigms of software development. The aim of this workshop is to bring together researchers who are currently developing new computational models or new features for traditional computational models, in order to foster their interaction, to provide a forum for presenting new ideas and work in progress, and to enable newcomers to learn about current activities in this area. DCM 2013 will be a one-day satellite event of CONCUR 2013. Topics of interest include all abstract models of computation and their applications to the development of programming languages and systems: - quantum computation, including implementations and formal methods in quantum protocols; - probabilistic computation and verification in modelling situations; - chemical, biological and bio-inspired computation, including spatial models, self-assembly, growth models; - general concurrent models including the treatment of mobility; - infinitary models of computation; - trust, and security; information-theoretic ideas in computing. SUBMISSION ---------- Submit your paper in PDF format via the conference EasyChair submission page: http://www.easychair.org/conferences/?conf=dcm2013 Submissions should be an abstract of at most 5 pages, written in English. Simultaneous submission to journals, conferences or other workshops is not permitted. Please use the EPTCS macro package and follow the instructions of EPTCS: http://eptcs.org/ http://style.eptcs.org/ A submission may contain an appendix, but reading the appendix should not be necessary to assess its merits. PUBLICATION ----------- Accepted contributions will appear in EPTCS (Electronic Proceedings in Theoretical Computer Science). After the workshop, full versions of selected papers will be invited for a special issue in an internationally leading journal. IMPORTANT DATES --------------- - Submission Deadline for Abstracts: 1 June 2013 - Notification: 1 July 2013 - Pre-proceedings version due: 1 August 2013 - Workshop: 26 August 2013 INVITED SPEAKER: Veronica Becher (Universidad de Buenos Aires, Argentina) PROGRAMME COMMITTEE: Pablo Arrighi (France) Mauricio Ayala Rincon (Brazil) co-chair Pablo Barcelo (Chile) Mario Benevides (Brazil) Eduardo Bonelli (Argentina) co-chair Paola Bonizzoni (Italy) Nachum Dershowitz (Israel) Ruben Gamboa (USA) Rajeev Gore (Australia) Holger Hermanns (Germany) Nao Hirokawa (Japan) Jean Krivine (France) Luis Lamb (Brazil) Ian Mackie (France) co-chair Cesar Munoz (USA) Carlos Olarte (Colombia) Femke van Raamsdonk (Netherlands) Camilo Rocha (Colombia) Nora Szasz (Uruguay) Rene Thiemann (Austria)

1 0

Kobe Colloquium on Logic, Statistics and Informatics, May 10 (Andre Nies)
by Joerg Brendle 26 Apr '13

26 Apr '13

Kobe Colloquium on Logic, Statistics and Informatics 以下の要領でコロキウムを開催します。日時：2013年5月10日（金）10:40-12:10 講演者：Andre Nies (University of Auckland, New Zealand) 場所：神戸大学自然科学総合研究棟3号館4階421室（プレゼンテーション室） ======================================================================== 題目：The complexity of similarity relations among Polish metric spaces アブストラクト：We calibrate the complexity of similarity relations between Polish metric spaces. First we discuss the classical case, based on concepts of Gromov. Thereafter we consider computable Polish metric spaces. For instance, Melnikov and I give the exact complexity of isometry between compact computable spaces, and show that isometric spaces of this kind have a Delta 3 isometry. ======================================================================== 交通：阪急六甲駅またはJR六甲道駅から神戸市バス36系統「鶴甲団地」行きに乗車，「神大本部工学部前」停留所下車，徒歩すぐ． http://www.kobe-u.ac.jp/info/access/rokko/rokkodai-dai2.htm 連絡先：ブレンドレヨーグ brendle(a)kurt.scitec.kobe-u.ac.jp

1 0

浦本武雄さん（京大数学）によるご講演（来週火曜，4/30）
by Ichiro Hasuo 26 Apr '13

26 Apr '13

みなさま，東京大学の蓮尾です．来週は研究室のセミナーに浦本武雄さん（京都大学数学教室D3）をお招きして，形式言語理論と圏論的双対性の関連についての結果をお話いただきます．どうかご自由にご参加ください．どうかよろしくお願いいたします．それでは！蓮尾一郎研究室ウェブページ： https://www-mmm.is.s.u-tokyo.ac.jp/indexj.html ============ Tue 30 April 2013, 15:30-17:30 Takeo Uramoto (Dept. Mathematics, Kyoto University) Tannaka-style reconstruction theorem for profinite monoids with an application to Eilenberg-Reiterman's variety theory 理学部7号館1階 102教室 Room 102, School of Science Bldg. No. 7 アクセス： https://www-mmm.is.s.u-tokyo.ac.jp/indexj.html （一番下） Access: http://www-mmm.is.s.u-tokyo.ac.jp/ (see bottom) Eilenberg-Reiterman's variety theory is one of the central theories in algebraic studies of finite automata and regular languages. In its recent development, Rhodes and Steinberg pointed out that the Boolean algebra of regular languages admits a bialgebra structure and revealed its important role in the duality-theoretic formulation of the variety theory. In this talk, we study the structure of the bialgebra of regular languages using a traditional idea from the linear representation theory of groups. In particular, we aim at clarifying a close connection between algebraic structures on the bialgebra of regular languages and geometric structures of finite automata. Our main result claims that there exists a bijective correspondence between bilinear multiplications of regular languages that are compatible with respect to word decompositions and binary products on finite automata that are stable with respect to simulations. This is proved as a corollary of the Tannaka-style reconstruction theorem for profinite monoids, which is an analogue of the classical Tannaka duality theorem for compact groups and indicates a categorical universality of the Boolean algebra of regular languages with respect to finite automata and simulations.

1 0

ランダムネスの研究集会のご案内と参加募集
by Kenshi Miyabe 26 Apr '13

26 Apr '13

4月から東大に移りました宮部です．お世話になっております．ランダムネスに関する研究集会を次のように開催します．集会名：ELC Workshop on Randomness and Probability Through Computability (RPTC2013) 日時：2013年5月14日(火)15日(水) 場所: 東京大学本郷工学部6号館セミナー室A,D http://kenshi.miyabe.name/rptc2013/ 直前の2013年5月13日(月)14日(火)には，近い場所でランダムネスのセミナーも行う予定です． ELC Seminar on Algorithmic Randomness http://kenshi.miyabe.name/rptc2013/seminar.html 招待講演者: Rod Downey André Nies Bakhadyr Khoussainov Shuji Kijima Prof. Downeyにはランダムネスの導入的な話もお願いしてあります．プログラムおよびアブストラクトを以下で見ることができます． http://kenshi.miyabe.name/rptc2013/programme.html セミナーの方のプログラムも近々詳細をアップロード予定です． http://kenshi.miyabe.name/rptc2013/seminar.html 皆様のご参加お待ちしております。なお，本集会は文部科学省科学研究費補助金新学術領域研究「多面的アプローチの統合による計算限界の解明」 http://www.al.ics.saitama-u.ac.jp/elc/ および FIRST 合原最先端数理モデルプロジェクト http://www.sat.t.u-tokyo.ac.jp/first/ の支援を受けております．東京大学情報理工学系研究科河村彰星 kawamura(a)is.s.u-tokyo.ac.jp 東京大学情報理工学系研究科宮部賢志 kmiyabe(a)kurims.kyoto-u.ac.jp -- Kenshi Miyabe email: research(a)kenshi.miyabe.name JSPS Research Fellow Graduate school of Information Science and Technology, The University of Tokyo Tel: +81-3-5841-6943

1 0

APLAS 2013 call for papers
by Jacques Garrigue 24 Apr '13

24 Apr '13

Logic-MLの皆様、 12月にオーストラリアのメルボルンで開催されるAPLASの論文募集案内をお送りします。投稿締め切りは6月14日ですので、ご検討をよろしくお願いいたします。 Jacques Garrigue =============================================================== APLAS 2013 11th Asian Symposium on Programming Languages and Systems 9-11 December 2013 Melbourne, Australia (colocated with CPP 2013) CALL FOR PAPERS =============================================================== ========== BACKGROUND ========== APLAS aims to stimulate programming language research by providing a forum for the presentation of latest results and the exchange of ideas in programming languages and systems. APLAS is based in Asia, but is an international forum that serves the worldwide programming language community. APLAS is sponsored by the Asian Association for Foundation of Software (AAFS) founded by Asian researchers in cooperation with many researchers from Europe and the USA. Past APLAS symposiums were successfully held in Kyoto ('12), Kenting ('11), Shanghai ('10), Seoul ('09), Bangalore ('08), Singapore ('07), Sydney ('06), Tsukuba ('05), Taipei ('04) and Beijing ('03) after three informal workshops. Proceedings of the past symposiums were published in Springer's LNCS. ====== TOPICS ====== The symposium is devoted to foundational and practical issues in programming languages and systems. Papers are solicited on topics such as * semantics, logics, foundational theory; * design of languages, type systems and foundational calculi; * domain-specific languages; * compilers, interpreters, abstract machines; * program derivation, synthesis and transformation; * program analysis, verification, model-checking; * logic, constraint, probabilistic and quantum programming; * software security; * concurrency and parallelism; * tools and environments for programming and implementation. Topics are not limited to those discussed in previous symposiums. Papers identifying future directions of programming and those addressing the rapid changes of the underlying computing platforms are especially welcome. Demonstration of systems and tools in the scope of APLAS are welcome to the System and Tool presentations category. Authors concerned about the appropriateness of a topic are welcome to consult with program chair prior to submission. ========== SUBMISSION ========== We solicit submissions in two categories: *Regular research papers* describing original scientific research results, including tool development and case studies. Regular research papers should not exceed 16 pages in the Springer LNCS format, including bibliography and figures. They should clearly identify what has been accomplished and why it is significant. Submissions will be judged on the basis of significance, relevance, correctness, originality, and clarity. In case of lack of space, proofs, experimental results, or any information supporting the technical results of the paper could be provided as an appendix or a link to a web page, but reviewers are not obliged to read them. *System and Tool presentations* describing systems or tools that support theory, program construction, reasoning, or program execution in the scope of APLAS. System and Tool presentations are expected to be centered around a demonstration. The paper and the demonstration should identify the novelties of the tools and use motivating examples. System and Tool papers should not exceed 8 pages in the Springer LNCS format, including bibliography and figures. Submissions will be judged based on both the papers and the described systems or tools. It is highly desirable that the tools are available on the web. Papers should be submitted electronically via the submission web page: https://www.easychair.org/conferences/?conf=aplas2013 Acceptable formats are PostScript or PDF. Submitted papers must be unpublished and not submitted for publication elsewhere. Papers must be written in English. The proceedings will be published as a volume in Springer's LNCS series. Accepted papers must be presented at the conference. (While the general chair and the program chair cannot submit papers, other members of the program committee can.) ===== DATES ===== Abstract due: 10 June 2013 (Monday), 23:59 UTC Submission due: 14 June 2013 (Friday), 23:59 UTC Notification: 26 August 2013 (Monday) Final paper due: 19 September 2013 (Thursday) Conference: 9-11 December 2013 (Monday-Wednesday) ========== ORGANIZERS ========== General chair: Peter Schachte (University of Melbourne) Program chair: Chung-chieh Shan (Indiana University) Program committee: Filippo Bonchi (CNRS, ENS-Lyon, France) Yu-Fang Chen (Academia Sinica, Taiwan) Shigeru Chiba (The University of Tokyo, Japan) Jacques Garrigue (Nagoya University, Japan) Robert Glück (University of Copenhagen, Denmark) R. Govindarajan (Indian Institute of Science, India) Kazuhiro Inaba (Google, Inc., Japan) Jie-Hong Roland Jiang (National Taiwan University, Taiwan) Shin-ya Katsumata (Kyoto University, Japan) Gabriele Keller (University of New South Wales, Australia) Ana Milanova (Rensselaer Polytechnic Institute, USA) Keisuke Nakano (The University of Electro-Communications, Japan) Hakjoo Oh (Seoul National University, Korea) Bruno C. d. S. Oliveira (National University of Singapore, Singapore) Kaushik Rajan (Microsoft Research, India) Max Schäfer (Nanyang Technological University, Singapore) Ulrich Schöpp (Ludwig-Maximilians-Universität München, Germany) Paula Severi (University of Leicester, UK) Gang Tan (Lehigh University, USA) Hiroshi Unno (University of Tsukuba, Japan) Meng Wang (Chalmers University of Technology, Sweden) Jingling Xue (University of New South Wales, Australia) Mingsheng Ying (University of Technology, Sydney, Australia) Kenny Q. Zhu (Shanghai Jiao Tong University, China) ======= CONTACT ======= http://aplas2013.soic.indiana.edu/ aplas2013(a)easychair.org

1 0

Kobe Colloquium on Logic, Statistics and Informatics, May 1 (Rod Downey)
by Joerg Brendle 23 Apr '13

23 Apr '13

Kobe Colloquium on Logic, Statistics and Informatics 以下の要領でコロキウムを開催します。日時：2013年5月1日（水）15:00-16:30 場所：神戸大学自然科学総合研究棟3号館4階421室（プレゼンテーション室）講演者：Rod Downey (Victoria University of Wellington, New Zealand) ======================================================================== 題目：Effectively in Abelian Group Theory アブストラクト：The effectiveness of the theory of abelian groups has been long studied beginning with the work of Mal'cev in the 60's. Nevertheless many problems remain. In this lecture I will discuss ongoing work on questions of effectiveness of categoricity and presentability for computable torsion-free abelian groups and for p-groups. For example, for categoricity, general problem is impossible; for example Downey and Montalban showed that the isomorphism problem for torsion-free abelian groups is Sigma_1^1-complete. The principle difficulty lies in the lack of invariants. However, where there are some invariants there we can salvage some effectiveness. The groups we look at are the completely decomposable ones, which have decompositions of the form oplus_{i in omega} G_i with G_i a subgroup of the additive group of the rationals. Such groups are called homogeneous if G_i=H for all i. Alexander Melnikov and the author have shown that homogeneous computable completely decomposable groups are always Delta_3^0 categorical, this bound is sharp, and have classified when the groups are Delta_2^0 categorical in terms of what are called semilow sets. In more recent work, we have shown that every computable completely decomposable group is Delta_5^0 categorical and that this bound is sharp. Additionally we can show that the index set of such groups is Sigma_7^0. I will also describe ongoing work on Ulm's Theorem. ======================================================================== 交通：阪急六甲駅またはJR六甲道駅から神戸市バス36系統「鶴甲団地」行きに乗車，「神大本部工学部前」停留所下車，徒歩すぐ． http://www.kobe-u.ac.jp/info/access/rokko/rokkodai-dai2.htm 連絡先：ブレンドレヨーグ brendle(a)kurt.scitec.kobe-u.ac.jp

1 0

Fwd: GALOP 2013 - Call for Papers
by Ichiro Hasuo 23 Apr '13

23 Apr '13

みなさま，こんにちは！東京大学の蓮尾です． SCメンバーとして，ゲーム意味論についてのワークショップ GaLoP のご案内を転送します．トピック限定＆コミュニティ指向型の，深い議論のできるワークショップです．どうか投稿・参加をご検討ください．どうかよろしくお願いいたします．それでは！蓮尾一郎\ http://www-mmm.is.s.u-tokyo.ac.jp/~ichiro/ ---------- Forwarded message ---------- 8th Workshop on Games for Logic and Programming Languages (GaLoP 2013) // Queen Mary, University of London // London, UK // 18-19 July // http://www.gamesemantics.org [apologies for possible cross-postings] GaLoP is an annual international workshop on game-semantic models for logics and programming languages and their applications. This is an informal workshop that welcomes work in progress, overviews of more extensive work, programmatic or position papers and tutorials as well as contributed papers and invited talks. GaLoP VIII will be held in London, UK, on 18-19 July 2013. It will be a stand-alone workshop hosted at the Mile End campus of Queen Mary, University of London. Contributions are invited on all pertinent subjects, with particular interest in game-semantic and interaction models for logics and programming languages, and applications to program analysis. Typical but not exclusive areas of interest are: * Game theory and interaction models in semantics; * Games-based program analysis and verification; * Logics for games and games for logics; * Algorithmic aspects of games; * Categorical aspects; * Programming languages and full abstraction; * Higher-order automata and Petri nets; * Geometry of interaction; * Ludics; * Epistemic game theory; * Logics of dependence and independence; * Computational linguistics. There will be no formal proceedings but the possibility of a special issue in a journal will be considered (the 2005, 2008 and 2011 workshops led to special issues in Annals of Pure and Applied Logic). // Submission Instructions // Please submit an abstract of your proposed talk on the easychair submission page below. You may also submit an accompanying paper for the talk. https://www.easychair.org/conferences/?conf=galop2013 // Important Dates // Submission: May 31 Notification: June 7 Workshop: July 18-19 // Invited speakers // * Ichiro Hasuo, Tokyo * Colin Stirling, Edinburgh * Viktor Winschel, Mannheim * Nobuko Yoshida, Imperial // Program Committee // * Ugo Dal Lago, Bologna * Dan Ghica, Birmingham * Juha Kontinen, Helsinki * Guy McCusker, Bath (co-chair) * Andrzej Murawski, Warwick * Nikos Tzevelekos, QMUL (co-chair) * Glynn Winskel, Cambridge

1 0

Set Theory Seminar Kobe
by Joerg Brendle 18 Apr '13

18 Apr '13

Kobe Set Theory Seminar This semester the Kobe Set Theory Seminar will take place Tuesdays 1:20 to 2:50 pm in room 421 of Science and Technology Research Building 3, Kobe University. http://www.kobe-u.ac.jp/en/access/rokko/campus.htm Members and guests of the set theory groups will present their research. All talks are given in English. There is no program. For information about speakers and topics please contact Jörg Brendle. brendle(a)kurt.scitec.kobe-u.ac.jp See also the following webpage for current activities. http://kurt.scitec.kobe-u.ac.jp/~brendle/events.html ============================================================ 集合論のセミナー時限：前期・火曜日・３時限（１：２０〜２：５０）場所：神戸大学自然科学総合研究棟3号館4階421室（プレゼンテーション室）交通：阪急六甲駅またはJR六甲道駅から神戸市バス36系統「鶴甲団地」行きに乗車，「神大本部工学部前」停留所下車，徒歩すぐ． http://www.kobe-u.ac.jp/info/access/rokko/rokkodai-dai2.htm 連絡先：ブレンドレヨーグ brendle(a)kurt.scitec.kobe-u.ac.jp http://kurt.scitec.kobe-u.ac.jp/~brendle/events.html

1 0

CFP: LENLS10 (Logic and Engineering of Natural Language Semantics 10)
by BEKKI Daisuke 17 Apr '13

17 Apr '13

（重複して受け取られた場合はご容赦ください）今年の１０月に東京で開催される LENLS 10 国際ワークショップのプログラムをお送り致します。皆様のご参加をお待ちしております。戸次大介（お茶の水女子大学／国立情報学研究所） [Apologies for multiple copies] ================================================================= FIRST CALL FOR PAPERS Logic and Engineering of Natural Language Semantics 10 (LENLS 10) Workshop Site : "Raiousha Building, Keio University" Kanagawa, Japan. http://www.keio.ac.jp/en/maps/hiyoshi.html Dates : October 27-28, 2013 Contact Person: Shunsuke Yatabe (West Japan Railway Company) Contact Email : lenls10[[at]]easychair.org Website : http://www.is.ocha.ac.jp/‾bekki/lenls/ ================================================================= Chair: Shunsuke Yatabe (West Japan Railway Company) Co-chair: Daisuke Bekki (Ochanomizu University /National Institute of Informatics) Eric McCready (Aoyama Gakuin University) LENLS is an annual international workshop on formal syntax, semantics and pragmatics. It will be held as one of the workshops of the fifth JSAI International Symposia on AI (isAI2013) (http://www.ai-gakkai.or.jp/jsai-isai/2013/) sponsored by the Japan Society for Artificial Intelligence (JSAI) (http://www.ai-gakkai.or.jp/jsai/english.html). Aims and Topics: ================ We invite submissions to this year's workshop on topics in formal semantics and pragmatics, and related fields, including but in no way limited to the following: - Dynamic syntax/semantics/pragmatics of natural language - Categorical/topological/coalgebraic approaches for natural language syntax/semantics/pragmatics - Logic and its relation to natural language and linguistic reasoning (especially dynamic logics) - Type-theoretic approaches to natural language - Formal Philosophy of language - Formal pragmatics (especially game-theoretic and utility-theoretic approaches) - Substructural expansion of Lambek Lambda Calculi - Many-valued/Fuzzy and other non-classical logics and natural language Submissions: ============ Abstracts (up to 4 pages, including figures and references) must be submitted electronically in PDF format at: https://www.easychair.org/conferences/?conf=lenls10 When his/her abstract is accepted, the author is expected to submit a full paper (10-14 pages) before the workshop. The proceedings of the workshop will be available at the conference site for registered persons. Important dates: ================ Abstract submission deadline: July 31, 2013 Notification of acceptance: August 26, 2013 Deadline for camera-ready copy: September, 2013 LENLS10: October 27-28, 2013 Tutorial Lecture: October 29, 2013 Workshop Organizers/Program Committee: ====================================== - Shunsuke Yatabe (West Japan Railway Company) - Daisuke Bekki (Ochanomizu University/National Institute of Informatics) - Alastair Butler (PRESTO JST/Tohoku University) - Eric McCready (Aoyama Gakuin University) - Koji Mineshima (Keio University) - Yoshiki Mori (University of Tokyo) - Yasuo Nakayama (Osaka University) - Katsuhiko Sano (Japan Advanced Institute of Science and Technology) - Katsuhiko Yabushita (Naruto University of Education) - Tomoyuki Yamada (Hokkaido University) - Kei Yoshimoto (Tohoku University)

1 0

4/16, Talk by Keisuke Nakano (Univ. Electro-Communications)
by Tetsuri Moriya 16 Apr '13

16 Apr '13

みなさま、東京大学の蓮尾研究室M2の森谷です。蓮尾研究室では4月16日に電気通信大学の中野圭介さんをお迎えしてご講演いただきます。詳細は以下で、事前の登録等は一切不要です。ご興味のある方はぜひお越しください！ ============================================================= Tue 16 April 2013, 15:30-17:30 Keisuke Nakano (Univ. Electro-Communications), 2 Talks 理学部7号館1階 102教室 Room 102, School of Science Bldg. No. 7 Talk 1: Juggling meets coinduction In this talk, I will present an application of coinduction, juggling. Buhler et al. presented a mathematical theory of toss juggling by regarding a toss pattern as an arithmetic function, where the function must satisfy a condition for the pattern to be valid. In this talk, I will formalize their theory in terms of coinduction, reflecting the fact that the validity of toss juggling is related to a property of infinite phenomena. A tactic is implemented for proving the validity of toss patterns in Coq. Additionally, the completeness and soundness of a well-known algorithm for checking the validity is certified. The result exposes a practical aspect of coinductive proofs. Most part of this talk has been presented in CPP 2012. Some open problems also will be introduced. Talk 2: Metamorphism in jigsaw In this talk, I will present a new computation model for metamorphism. A metamorphism is an unfold after a fold, consuming an input by the fold then generating an output by the unfold. It is typically useful for converting data representations, e.g., radix conversion of numbers. Bird and Gibbons have shown that metamorphisms can be incrementally processed in streaming style when a certain condition holds because part of the output can be determined before the whole input is given. However, whereas radix conversion of fractions is amenable to streaming, radix conversion of natural numbers cannot satisfy the condition because it is impossible to determine part of the output before the whole input is completed. In this talk, I present a jigsaw model in which metamorphisms can be partially processed for outputs even when the streaming condition does not hold. The jigsaw model allows us to process metamorphisms in a flexible way that includes parallel computation. We also apply our model to other examples of metamorphisms. Most part of this talk is recently published in Journal of Functional Programming. Additionally, I will present some further work on this work.

2 1

JAIST Logic Seminar Series
by Takayuki Kihara 15 Apr '13

15 Apr '13

皆様北陸先端科学技術大学院大学の木原貴行です． JAIST Logic Seminar Seriesのお知らせです．問合せ先：木原貴行北陸先端科学技術大学院大学情報科学研究科 e-mail: kihara(a)jaist.ac.jp -------------------------------------------------- * JAIST Logic Seminar Series * Date: Friday 26 April, 2013, 15:00-17:00 Place: JAIST, Collaboration room 7 (I-56) (Access: http://www.jaist.ac.jp/english/location/access.html) Speaker: Dr. Arno Pauly (University of Cambridge) Title: Synthetic Descriptive Set Theory Abstract: Typically, (effective) descriptive set theory is viewed as a study of classes of discontinuous / uncomputable functions. Inside the theory of represented spaces though, we can consider the same concepts as special cases of continuity/computability. Using category-theoretic language, an abstract and unifying framework is achieved that allows very simple formulations and proofs corresponding closely to various fundamental results in descriptive set theory. * The seminar is held as a part of the EU FP7 Marie Curie Actions IRSES project COMPUTAL (http://computal.uni-trier.de/).

1 0

Computability and Complexity in Analysis 2013
by Akitoshi Kawamura 12 Apr '13

12 Apr '13

皆様東京大の河村と申しますお世話になっておりますメーリングリストをお借りして七月に仏ナンシーにて開催されます解析学に於る計算可能性と計算量に関する国際会議（CCA 2013）の御案内をさせて頂きます（投稿締切4月1日）御投稿・参加を検討頂ければ幸いです -- 河村彰星東京大学大学院情報理工学系研究科コンピュータ科学専攻助教（今井研究室） 03-5841-4097 http://www-imai.is.s.u-tokyo.ac.jp/~kawamura/index_j.html First Call for Papers http://cca-net.de/cca2013/ The Tenth International Conference on Computability and Complexity in Analysis (CCA 2013) will take place in Nancy, France, July 8-11, 2013. The CCA 2013 Program Committee cordially invites researchers in the area of computability and complexity theory to submit papers for presentation at the conference. Topics: * Computable analysis * Complexity on real numbers * Constructive analysis * Domain theory and analysis * Theory of representations * Computable numbers, subsets and functions * Randomness and computable measure theory * Models of computability on real numbers * Realizability theory and analysis * Reverse analysis * Real number algorithms * Implementation of exact real number arithmetic Submissions: Authors are invited to submit a PDF version of an extended abstract (typically 10 pages) on the following web page: https://www.easychair.org/conferences/?conf=cca2013 Dates: Submission deadline: April 1, 2013 Notification of authors: May 6, 2013 Registration deadline: May 20, 2013 Final version: May 27, 2013 Invited Speakers: * Ulrich Berger (Swansea, UK) * Takayuki Kihara (JAIST, Japan) * Cristobal Rojas (Toronto, Canada) * Daniel Roy (Cambridge, UK) * Martin Ziegler (Darmstadt, Germany) Program Committee: * Andrej Bauer (Ljubljana, Slovenia) * Arno Pauly (Cambridge, UK) * Hannes Diener (Siegen, Germany) * Cameron Freer (MIT, USA) * Laurent Bienvenu (Paris, France) * Akitoshi Kawamura (Tokyo, Japan) * Ker-I Ko (Stony Brook, USA) * Matthias Schröder (Vienna, Austria) * Robert Rettinger (Hagen, Germany) * Ning Zhong (Cincinnati, USA), chair Local Organizers * Anne-Lise Charbonnier * Hugo Férée * Emmanuel Hainry * Mathieu Hoyrup (chair) * Emmanuel Jeandel * Romain Péchoux

1 1

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Logic-ml