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

PPL2013のご案内（参加登録:2/18まで）
by Shinya Katsumata 16 Feb '13

16 Feb '13

京都大学の勝股です。先週ご案内したばかりですが、PPL2013の参加登録の締め切り (来週月曜 2/18)が近くなったため、リマインダを兼ねて最終のご案内を御送りいたします。重複して受け取られていた場合はご容赦ください。 ---------- 東北大学の上野です． 3月に福島県会津若松市東山温泉で開催される第15回プログラミングおよびプログラミング言語ワークショップ (PPL2013) につきまして，参加登録を開始いたしましたのでお知らせします．参加登録要領 http://www.pllab.riec.tohoku.ac.jp/ppl2013/registration.html をご参照の上，日本旅行の参加登録受付ページからご登録ください．皆様のご参加をお待ちしております．最新情報は引き続き下記webページにてお知らせします． -------------------------------------------------------------------------- 第15回プログラミングおよびプログラミング言語ワークショップ（PPL2013） http://www.pllab.riec.tohoku.ac.jp/ppl2013/ 主催: 日本ソフトウェア科学会プログラミング論研究会日程: 2013年3月4日(月)〜3月6日(水) 会場: 福島県会津若松東山温泉「御宿東鳳」 http://www.onyado-toho.co.jp/ ====================================================================== 参加申し込み締切： 2013年2月18日（月）参加登録要領 http://www.pllab.riec.tohoku.ac.jp/ppl2013/registration.html をご参照の上，日本旅行の参加登録受付ページからご登録ください．皆様のご参加をお待ちしております． ====================================================================== PPL2013は，プログラミングおよびプログラミング言語に関する研究者が一堂に会し，最新の研究成果の発表，および新たな研究課題についての討論やアイディア交換等を行うことを目的とした，合宿形式のワークショップです．プログラミングおよびプログラミング言語の理論・設計・実装・処理系などに関する研究発表を，カテゴリ別に幅広く募集しています．カテゴリ１: 国内外で未発表の論文の発表カテゴリ２: 国際会議・学術雑誌等で既発表であるが，国内では未発表の研究の紹介カテゴリ３: ポスター・デモ発表（既発表・未発表の別を問いません） ※ショートプレゼンテーションは行いませんカテゴリ１の採択論文の中から，特に独創的なアイディアや顕著な成果を含むものに対して論文賞を授与する予定です．また，ポスター・デモを含む全発表のなかから，聴衆の投票により，最も優秀なプレゼンテーションに発表賞（一般の部，学生の部）を授与する予定です．詳細および最新情報は下記webページをご覧下さい． http://www.pllab.riec.tohoku.ac.jp/ppl2013/ ワークショップ全般に関する問い合わせ先：oc-ppl2013(a)kurims.kyoto-u.ac.jp ====================================================================== 招待講演 ====================================================================== 鍋島英知 (山梨大学) 村主崇行 (京都大学) 以上お二方の招待講演を予定しております． ====================================================================== 運営組織 ====================================================================== プログラム委員会青木利晃 (北陸先端科学技術大学院大学) 青谷知幸 (北陸先端科学技術大学院大学) 天野俊一 (IBM東京基礎研究所) 磯部祥尚 (産業技術総合研究所) 岩見宗弘 (島根大学) 角谷良彦 (東京大学) 勝股審也 (京都大学) [プログラム共同委員長] 小宮常康 (電気通信大学) 権藤克彦 (東京工業大学) [プログラム共同委員長] 田浦健次朗 (東京大学) 高田喜朗 (高知工科大学) 田辺良則 (国立情報学研究所) 中田景子 (Institute of Cybernetics at Tallinn University of Technology) 中野圭介 (電気通信大学) 長谷部浩二 (筑波大学) 番原睦則 (神戸大学) 松崎公紀 (高知工科大学) 実行委員会上野雄大 (東北大学) [実行委員長] 鵜川始陽 (電気通信大学) [実行副委員長] 勝股審也 (京都大学) [プログラム共同委員長] 権藤克彦 (東京工業大学) [プログラム共同委員長] --------------------------------------------------------------------------

1 0

Kobe Colloquium (Feb. 18, 2013)
by fuchino＠diamond.kobe-u.ac.jp 14 Feb '13

14 Feb '13

以下の要領でコロキウムを開催します．日時：2013年2月18日（月）15:10-16:40 場所：神戸大学自然科学総合研究棟3号館4階421室（プレゼンテーション室）講演者：Philip Welch (Univ. of Bristol) タイトル： Determinacy within Second Order Arithmetic Abstract: It was proven by H. Friedman in 1971 that the determinacy of two person perfect information games played on integers at the 5th level of the arithmetic hierarchy (so Sigma^0_5) would require the use of set theoretical axioms such as the Power Set Axiom. (This was improved by Martin to the 4th level.) Strategies for Sigma^0_k games for k =3D 1,2 were located in the Goedel L-hierachy by a folklore result (k=3D1) and Solovay (for k=3D2). We give a theorem on this kind for the last case left in the arithmetical hierarchy provable in analysis, thus for k=3D3. More recently Montalban and Shore have calculated the exact strength of determinacy provable in Second Order Number theory. We give some conjectures and a report on recent work that seeks to lift Montalban-Shore to the corresponding theory that includes a single measurable cardinal. -- best regards Saka\'e Fuchino (渕野昌) ------------------------------------------------------------------------- Kobe University Graduate School of System Informatics Rokko-dai 1-1, Nada, Kobe 657-8501 Japan e-mail: fuchino(a)diamond.kobe-u.ac.jp web page: http://kurt.scitec.kobe-u.ac.jp/~fuchino/ -------------------------------------------------------------------------

1 0

ICE 2013 Call for Papers
by Ichiro Hasuo 13 Feb '13

13 Feb '13

みなさま，国際ワークショップ ICE 2013 のお知らせです． - トピックは concurrency や coordination を軸に，verification, specification など多岐に渡ります．プログラミング言語理論や形式意味論などもスコープに入るはずです．（下をご覧ください） - フィレンツェの DisCoTec 併設です． - review の後，採否決定まで wiki による議論が行われます（レビュアー，著者，PC member 入り乱れて）．どうか投稿をご検討ください．それでは！蓮尾一郎東京大学コンピュータ科学専攻 http://www-mmm.is.s.u-tokyo.ac.jp/~ichiro/ ---------------------------------------------------------------------- [- Apologies for multiple copies -] ICE 2013 6th Interaction and Concurrency Experience June 6, 2013, Florence, Italy http://www.discotec.org/workshops/ice2013/ Satellite workshop of DisCoTec 2013 http://www.discotec.org === Highlights === - Invited talks: Davide Sangiorgi & Damien Pous - Innovative selection procedure - Special issue of Science of Computer Programming (http://www.journals.elsevier.com/science-of-computer-programming/) === Important Dates === 20 March 2013...................Full paper submission 21 March - 21 April 2013........Reviews, rebuttal, and PC discussion 24 April 2013...................Notification to authors 6 June 2013.....................ICE in Florence 15 Sept 2013....................Camera-ready for post-proceedings === Scope === Interaction and Concurrency Experiences (ICEs) is a series of international scientific meetings oriented to theoretical computer science researchers with special interest in models, verification, tools and programming primitives for complex interactions. The general scope of the venue includes theoretical and applied aspects of interactions and the synchronization mechanisms used among components of concurrent/distributed systems, related to several areas of computer science in the broad spectrum ranging from formal specification and analysis to studies inspired by emerging computational models. Topics of interest include, but are not limited to: - Process algebra and coordination: transformation, analysis and implementation - Models for distributed coordination and semantics - Techniques and tools for specification, analysis, verification of resilient interactions - Coinductive techniques for reactive systems - Languages, protocols and mechanisms for sound distributed coordination - Logics and types for interactions - Comparison among different coordination and/or execution models - Expressive power of coordination languages and execution models - Formal semantics of coordination languages - Formal verification of distributed coordinated architectures - Relations between different semantic models for coordination languages === Selection Procedure === Since its 1st edition in 2008, the distinguishing feature of ICE has been an innovative paper selection mechanism based on an interactive discussion amongst authors and PC members. During the review phase, each submitted paper is published on a Wiki and associated with a discussion forum. The discussion forum can be accessed by the authors of the paper and by all the PC members not in conflict with the paper. The forum is used by reviewers to ask questions and clarifications to the authors, allowing them to better explain all the aspects of their paper. The evaluation of the paper will keep into account not only the reviews, but also the outcome of the discussion. As witnessed by the past five editions of ICE, this procedure considerably improves the accuracy of the feedback from reviews, the fairness of the selection, the quality of camera-ready papers, and the discussion during the workshop. === The Public Wiki === After the notification, the accepted papers are published on a public forum, in order to initiate public discussions that will trigger and stimulate the scientific debate at the workshop. We believe that this will drive the workshop discussions and let prospective participants interact with each other much earlier than in more traditional events. === Submission Guidelines === We invite for three types of submissions: (1) Full Papers, (2) Short Papers, and (3) Brief Announcements of already Published Papers. Full and short papers to appear in the post-proceedings must report previously unpublished work and not be simultaneously submitted to other conferences/workshops with refereed proceedings. The ICE 2013 post-proceedings will be published in Electronic Proceedings in Theoretical Computer Science (http://eptcs.org/). In addition, we invite for brief announcements of already published results, should the authors feel like advertising their work and giving a talk. Brief announcements will not be part of the post-proceedings. Submissions must be made electronically in PDF format via EasyChair (http://www.easychair.org/conferences/?conf=ice2013). Full papers should not exceed 15 pages while short papers and brief announcements should not exceed 5 pages with the EPTCS style (http://style.eptcs.org/). Accepted (full and short) papers and brief announcements must be presented at the workshop by one of the authors. === Special Issue === Extended versions of the best full papers selected by the PC will be invited to appear in a special issue of the journal of Science of Computer Programming (http://www.journals.elsevier.com/science-of-computer-programming/ ). Such contributions will be regularly peer-reviewed according to the standard journal policy, but they will be handled in a shorter time than regular submissions. === Program Committee === Luca Aceto (Reykjavik University, Iceland) Simon Bliudze (EPFL, Switzerland) Laura Bocchi (University of Leicester, UK) Filippo Bonchi (CNRS, France) Roberto Bruni (University of Pisa, Italy) Marcello Bonsangue (Leiden University, The Netherlands) Ornela Dardha (University of Bologna/INRIA, Italy) Ichiro Hasuo (University of Tokyo, Japan) Tobias Heindel (CEA Saclay, France) Ludovic Henrio (CNRS, France) Clemens Kupke (University of Oxford, UK) Julien Lange (University of Leicester, UK) Antonia Lopes (University of Lisbon, Portugal) Giuliano Losa (EPFL, Switzerland) Claudio A. Mezzina (FBK Trento, Italy) Matteo Mio (University of Edinburgh, UK) Valentina Monreale (University of Pisa, Italy) Luca Mottola (Politecnico di Milano, Italy) Daniela Petrisan (University of Leicester, UK) Paola Spoletini (University of Insubria, Italy) Emilio Tuosto (University of Leicester, UK) Valerio Senni (IMT Lucca, Italy) Alexandra Silva (Radboud University Nijmegen, The Netherlands) Josef Widder (TU Vienna, Austria) Roberto Zunino (Università degli Studi di Trento and COSBI, Italy) === ICEcreamers === - Marco Carbone (IT University of Copenhagen, Denmark; co-chair) - Ivan Lanese (University of Bologna/INRIA, Italy) - Alberto Lluch Lafuente (IMT Lucca, Italy) - Ana Sokolova (University of Salzburg, Austria; co-chair) === Contact === ice2013(a)easychair.org === Previous editions === The previous five editions of ICE have been held on * July 6th, 2008 in Reykjavik, Iceland, co-located with ICALP'08. The post-proceedings were published in ENTCS (vol.229-3). * August 31st, 2009 in Bologna, Italy, co-located with CONCUR'09. The post-proceedings were published in EPTCS (vol.12) and selected papers appeared in a joint special issue of MSCS (with EXPRESS’09 and SOS’09, Vol. 22, Number 2). * June 10th, 2010 in Amsterdam, The Netherlands, co-located with DisCoTec'10. The post-proceedings were published in EPTCS (vol.38) and selected papers appeared in a joint special issue of SACS (with CAMPUS'10 and CS2BIO'10, Vol. XXI). * June 9th, 2011 in Reykjavik, Iceland, co-located with DisCoTec'11. The post-proceedings were published in EPTCS (vol.59) and selected papers appeared in a special issue of SACS (Vol. XXII). * June 16th, 2012 in Stockholm, Sweden, co-located with DisCoTec'12. The post-proceedings were published in EPTCS (vol.104) and a special issue of SCP is now in preparation.

1 0

Call for papers, 2nd Conf History & Philosophy of Computing, ENS Paris, oct 2013
by Kazushige TERUI 12 Feb '13

12 Feb '13

CALL FOR PAPERS, 2nd International CONFERENCE on the HISTORY AND PHILOSOPHY OF COMPUTING (HaPoC 2013) 28th - 31st October 2013 Ecole Normale Superieure, Paris. with a special session on "Computing and the Arts" at Ecole Nationale Superieure des Arts Decoratifs http://hapoc2013.sciencesconf.org We are happy to announce that the 2nd International Conference on the History and Philosophy of Computing (HaPoC 2013) will take place from the 28th to the 31st of October 2013 at the Ecole Normale Superieure in Paris (France). The birth of the computing and its sciences has often been the topic of philosophical and historical reflection. The HaPoC-conferences have decided to bring together the historical and the philosophical viewpoints. They want to create an environment for a true interdisciplinary convergence around computer science, reenforcing research on the science(s) of computing and its history and stimulating a theoretical dialogue between these domains. To furter this dialogue HaPoC has chosen to have no parallel sessions. Our invited speakers are: Janet Abbate; Bernard Chazelle (tbc); Walter Dean; Nathan Ensmenger; Jean-Yves Girard; Barbara Liskov (tbc); Margit Rosen and Franck Varenne. HaPoC 2013 is the follow-up conference to HaPoC 2011 (Gent, Belgium). Please check out the website of HaPoC 2013 for more information on the conference: http://hapoc2013.sciencesconf.org For HaPoC 2013 we welcome contributions from logicians, philosophers and historians of computing as well as from philosophically aware computer scientists and mathematicians. Topics include but are not limited to: 1. Approaches to the notion of computing a. History and Philosophy of Computability b. History and Philosophy of Computation c. History and Philosophy of Programming d. History and Philosophy of the Computer 2. Applications and uses of Computing a. History and Epistemology of the use of Computing in the sciences b. Computing and the Arts : historical and conceptual issues c. Social, ethical and paedagogical aspects of Computing We cordially invite researchers working in a field relevant to the main topics of the conference to submit a short abstract of approximately 200 words and an extended abstract of at most a 1000 words (references included) to https://www.easychair.org/conferences/?conf=hapoc2 Abstracts must be written in English and anonymized. Please note that the format of uploaded files must be .pdf or .doc. The submission deadline is: April 30th, 2013 Best regards, the organisers, Maarten Bullynck (Paris 8 & SPHERE) Jean-Baptiste Joinet (Lyon 3, IRPhil & Cirphles) ------------------------------------------ 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 YOKOYAMA Keita 08 Feb '13

08 Feb '13

皆様，東京工業大学の横山です．下記の要領でセミナーを行います．どうぞご参加ください．数理論理学セミナー (JSPS-FWO joint research seminar on mathematical logic) 日時：2月15日(金)14:30--18:00 (3講演) 場所：東京工業大学大岡山西８号館W棟11階 W1101セミナー室 14:30--15:30 Sam Sanders (Ghent University, Munich Center for Mathematical Philosophy of LMU) Title: Reuniting the antipodes: bringing together nonstandard analysis and constructive analysis Abstract: Recently, Sanders introduced an interpretation of Errett Bishop’s Constructive Analysis (BISH) inside a particular system of classical Nonstan- dard Analysis called NSA. The role of ‘algorithm’ is played by the notion Ω-invariance; Intuitively, an object is Ω-invariant if it does not depend on the choice of infinitesimal used in its definition. The role of ‘proof’ is played by the Transfer Principle of Nonstandard Analysis as follows: In the same way as the Brouwer-Heyting-Kolmogorov-interpretation is limited to provable formulas, we only consider formulas A such that A ↔ ∗A in NSA, i.e. formulas which ‘satisfy Transfer’. As NSA does not include non-trivial Transfer Principles, only some formulas A satisfy A ↔ ∗A. This interpretation from BISH into Nonstandard Analysis can be called ‘natural’ and ‘faithful’ in the following threefold way: (i) Non-constructive principles (LPO, LLPO, MP, etc.) are interpreted as Transfer Principles which are not available in the system NSA. (ii) The interpretation preserves the equivalences of Constructive Reverse Mathematics. (iii) The interpretation preserves the property that the BISH-notion of algo- rithm is weaker than that of recursive function. We discuss the interpretation from BISH into NSA, and related topics. 15:45--16:45 Tin Lok Wong (Ghent University) Title: Countable numbers in a model of arithmetic: a survey Abstract: A *countable number* in a model M of Peano arithmetic is a number that has countably many predecessors in M. I will survey some results about these countable numbers as an initial segment of the model M. Most of this talk will be accessible to everyone who has some basic knowledge in cardinals and in the Completeness Theorem for first-order logic. 17:00--18:00 Florian Pelupessy (Ghent University) Title: Unprovable theorems. Abstract: We will provide a gentle introduction to some interesting natural theorems which are not provable in Peano Arithmetic. These theorems are natural in the sense that they are similar to ordinary theorems from the mathematics literature. We will discuss two important methods of showing unprovability for these theorems, one using results from proof theory and one from model theory. ------ 問い合わせ先：横山　啓太（東京工業大学） yokoyama.k.ai(a)m.titech.ac.jp 横山啓太 -- Keita Yokoyama yokoyama.k.ai(a)m.titech.ac.jp

1 0

PPL2013 参加募集
by Shinya Katsumata 08 Feb '13

08 Feb '13

京都大学の勝股です。 PPL2013の参加募集案内をお送りいたします。本日参加登録が可能となりました。参加登録の締切(2/18)まであまり時間がないため、もし周りに参加を検討されていらっしゃる方がおられましたら、お声掛けをしていただければ幸いです。＃この案内を重複して受け取られた場合、ご容赦ください。 ---------- 東北大学の上野です． 3月に福島県会津若松市東山温泉で開催される第15回プログラミングおよびプログラミング言語ワークショップ (PPL2013) につきまして，参加登録を開始いたしましたのでお知らせします．参加登録要領 http://www.pllab.riec.tohoku.ac.jp/ppl2013/registration.html をご参照の上，日本旅行の参加登録受付ページからご登録ください．皆様のご参加をお待ちしております．最新情報は引き続き下記webページにてお知らせします． -------------------------------------------------------------------------- 第15回プログラミングおよびプログラミング言語ワークショップ（PPL2013） http://www.pllab.riec.tohoku.ac.jp/ppl2013/ 主催: 日本ソフトウェア科学会プログラミング論研究会日程: 2013年3月4日(月)〜3月6日(水) 会場: 福島県会津若松東山温泉「御宿東鳳」 http://www.onyado-toho.co.jp/ ====================================================================== 参加申し込み締切： 2013年2月18日（月）参加登録要領 http://www.pllab.riec.tohoku.ac.jp/ppl2013/registration.html をご参照の上，日本旅行の参加登録受付ページからご登録ください．皆様のご参加をお待ちしております． ====================================================================== PPL2013は，プログラミングおよびプログラミング言語に関する研究者が一堂に会し，最新の研究成果の発表，および新たな研究課題についての討論やアイディア交換等を行うことを目的とした，合宿形式のワークショップです．プログラミングおよびプログラミング言語の理論・設計・実装・処理系などに関する研究発表を，カテゴリ別に幅広く募集しています．カテゴリ１: 国内外で未発表の論文の発表カテゴリ２: 国際会議・学術雑誌等で既発表であるが，国内では未発表の研究の紹介カテゴリ３: ポスター・デモ発表（既発表・未発表の別を問いません） ※ショートプレゼンテーションは行いませんカテゴリ１の採択論文の中から，特に独創的なアイディアや顕著な成果を含むものに対して論文賞を授与する予定です．また，ポスター・デモを含む全発表のなかから，聴衆の投票により，最も優秀なプレゼンテーションに発表賞（一般の部，学生の部）を授与する予定です．詳細および最新情報は下記webページをご覧下さい． http://www.pllab.riec.tohoku.ac.jp/ppl2013/ ワークショップ全般に関する問い合わせ先：oc-ppl2013(a)kurims.kyoto-u.ac.jp

1 0

Seminar on Thu Feb 21
by Akitoshi Kawamura 08 Feb '13

08 Feb '13

皆様東京大の河村ですお世話になっております新学術領域研究「計算限界解明」（ELC）A01班「数理論理学からの計算限界解析」では 2月21日（木）午後に東大本郷キャンパスで下記の講演会を開催致します詳しくはウェブ頁を御覧下さい http://www-imai.is.s.u-tokyo.ac.jp/~kawamura/elc/seminar_H250221.html 計算理論と数理論理学の両方から多くの皆様の参加をお待ちしております講演会そのものに参加申込は不要ですが懇親会に御参加の場合はウェブ頁よりお早めに申込をお願い致します（締切2/17または定員になるまで） # なお「計算限界解明」のイベントとしましては # 先日垂井先生からも案内のありました # キックオフシンポジウム（3月14〜17日、東京品川）も是非御参加下さい # こちらも参加費は（宴会等を除いて）ありませんが # 登録をお願いしておりますのでお早めにお願い致します -- 河村彰星東京大学大学院情報理工学系研究科コンピュータ科学専攻助教（今井研究室） 03-5841-4097 http://www-imai.is.s.u-tokyo.ac.jp/~kawamura/index_j.html 記 ELC Seminar on February 21, 2013 http://www-imai.is.s.u-tokyo.ac.jp/~kawamura/elc/seminar_H250221.html Speakers * Kazushige Terui (Kyoto University) * Sebastian Müller (Charles University) * Martin Ziegler (TU Darmstadt) Time Thursday 13:45-, February 21, 2013 Place Room 214, Science Building 7 (理学部七号館214室), University of Tokyo ---- 13:50-14:50 Kazushige Terui (Kyoto University) Type Theoretic Approaches to Implicit Computational Complexity Implicit computational complexity (ICC) aims at giving a qualitative accout to various complexity classes. A typical approach to ICC is to consider a computational model (in finite model theory, recursion theory, term rewriting, functional programming, etc.) and propose a　*qualitative* criterion/certificate for a program in the model to be executed within a given time/space bound (e.g. polynomial time). Here we are particularly interested in higher order functional programming languages, which are often modeled by lambda calculus. It is then types that give a criterion/certificate for the resource bound. Because of the Curry-Howard correspondence, it is also linked to constructive logics. Linear logic plays a prominent role in this context. The purpose of this talk is to give a general overview of the type-theoretic approaches to ICC. It will be neither comprehensive nor detailed. I will just review some nice ideas in the past development, and discuss their future possibilities from my very personal (and sometimes critical) point of view. The topics will be chosen from the following list: - safe recursion in higher order - linearity and various modalities - arithmetic systems based on ICC - realizability semantics - denotational semantics - time-space tradeoff in lambda calculus ---- 15:10-16:10 Sebastian Müller (Charles University) Short Refutations of Random 3CNF in TC0-Frege (joint work with Iddo Tzameret) A classical result by Chvatal and Szemeredi states that with high probability, a given random 3CNF is unsatisfiable, if the clause-to-variable ratio is larger than 8 ln(2). On the other hand, on almost all unsatisfiable random 3CNF with a clause-to-variable ratio of less than n^0,5 (where n is the number of variables) Resolution fails to witness that unsatisfiability efficiently (due to Ben-sasson and Wigderson). On the other hand, Feige, Kim and Ofek constructed a witness for unsatisfiability that is polynomial-time constructable and works for random 3CNF with a clause-to-variable ratio above n^0,4. Iddo Tzameret and me formalized this witness in a weak bounded arithmetic theory called VTC^0. I will explain this result and sketch the main steps of the proof and later eloborate on the consequences for propositional proof system. As a direct consequence we receive efficient refutability of such formulas in TC^0-Frege proof systems and, with the above, a separation between such systems and Resolution on a random, dense set. ---- 16:30-17:30 Martin Ziegler (TU Darmstadt) Real Benefit of Promises and Advice (joint work with Ulrike Brandt and Klaus Ambos-Spies) Promises are a standard way to formalize partial algorithms; and advice quantifies nonuniformity. For decision problems, the latter it is captured in common complexity classes such as P/poly, that is, with advice growing in size with that of the input. We advertise constant-size advice and explore its theoretical impact on the complexity of classification problems – a natural generalization of promise problems -- and on real functions and operators. Specifically we exhibit problems that, without any advice, are decidable/computable but of high complexity while, with (each increase in the permitted size of) advice, (gradually) drop down to polynomial-time. ---- 18:00- Dinner (Please register on the webpage if you are coming to the dinner.)

1 0

Prof. Helmut Schwichtenberg Lecture at NII Logic Seminar
by Makoto Tatsuta 08 Feb '13

08 Feb '13

Prof. Helmut Schwichtenberg Lecture at NII Logic Seminar Date: February 21, 2013, 14:00--16:00 Place: National Institute of Informatics, Lecture Room 1208 (12th floor) 場所: 国立情報学研究所 12階 1208室 (半蔵門線,都営地下鉄三田線・新宿線神保町駅または東西線竹橋駅より徒歩5分) (地図 http://www.nii.ac.jp/about/access/) Speaker: Prof. Helmut Schwichtenberg (Ludwig Maximilian University of Munich) Title: Proofs and computations with infinite data Abstract: Ulrich Berger and Monika Seisenberger recently studied extraction from proofs involving (only) abstract reals. They considered a proof using coinduction of the proposition that any two reals in [-1,1] have their average in the same interval, and informally extract a Haskell program working with stream representations of reals. We report on a formalization of this proof, and a machine-extraction of its computational content, in the Minlog proof assistant. This required an extension of this system to also take coinduction into account. The underlying formal system is a theory TCF of computable functionals. It is similar to Heyting arithmetic in all finite types, but with the Scott/Ershov partial continuous functionals as the domain of quantifiers. TCF has free type, predicate and function variables, to allow for abstract developments (groups, fields, real analysis). The underlying inference machinery is minimal logic (implication, universal quantification plus inductively and coinductively defined predicates). Computable functionals (of finite type, with free algebras at ground types) are given by their defining equations. Since the logic is constructive, program extraction by means of a realizability interpretation is possible and a soundness theorem holds. 問合せ先: 龍田真 (国立情報学研究所) e-mail: tatsuta(a)nii.ac.jp http://research.nii.ac.jp/~tatsuta

1 0

Dr. Sam Sanders Lecture at NII Logic Seminar
by Makoto Tatsuta 08 Feb '13

08 Feb '13

Dr. Sam Sanders Lecture at NII Logic Seminar Date: February 13, 2013, 13:30--15:30 Place: National Institute of Informatics, Lecture Room 1904 (19th floor) 場所: 国立情報学研究所 19階 1904室 (半蔵門線,都営地下鉄三田線・新宿線神保町駅または東西線竹橋駅より徒歩5分) (地図 http://www.nii.ac.jp/about/access/) Speaker: Dr. Sam Sanders (University of Ghent) Title: Reuniting the antipodes: Bringing together Nonstandard Analysis and Constructive Analysis Abstract: Constructive Analysis (aka BISH) was introduced by Errett Bishop as a redevelopment of Mathematics with a focus on computational content. As such, BISH is based on the BHK (Brouwer-Heyting-Kolmogorov) interpretation of logic, where the notions of `proof' and `algorithm' are central. Constructive Reverse Mathematics (CRM) is a spin-off from Harvey Friedman's `Reverse Mathematics' program where the base theory is based on BISH. In this talk, we introduce an interpretation of BISH in classical Nonstandard Analysis. The role of `proof' in this interpretation is played by the Transfer Principle of Nonstandard Analysis. The role of `algorithm' is played by `$\Omega$-invariance'. Intuitively, an object is $\Omega$-invariant if it does not depend on the *choice* of infinitesimal used in its definition. Using this new interpretation, we obtain many of the well-known results form CRM. In particular, all non-constructive principles (like LPO, LLPO, MP, etc) are interpreted as Transfer Principles, which are not available in our nonstandard base theory. Finally, the interpretation preserves the property that not all $\Delta_1$-formulas are decidable in BISH. We discuss applications in (Homotopy) Type Theory. 問合せ先: 龍田真 (国立情報学研究所) e-mail: tatsuta(a)nii.ac.jp

1 0

Prof. Yue Yang Lecture at NII Logic Seminar
by Makoto Tatsuta 08 Feb '13

08 Feb '13

Prof. Yue Yang Lecture at NII Logic Seminar Date: February 12, 2013, 14:00--16:00 Place: National Institute of Informatics, Lecture Room 1210 (12th floor) 場所: 国立情報学研究所 12階 1210室 (半蔵門線,都営地下鉄三田線・新宿線神保町駅または東西線竹橋駅より徒歩5分) (地図 http://www.nii.ac.jp/about/access/) Speaker: Prof. Yue Yang (National University of Singapore) Title: The strength of Ramsey Theorem for Pairs Abstract: Ramsey Theorem is a well-known theorem in combinatorics. However, a special weak form of it (Ramsey Theorem for Pairs) has been a hot topic in Recursion Theory and Reverse Mathematics. In this talk I will give a survey on some recent progresses related to combinatoric principles weaker than Ramsey's Theorem for Pairs. In particular, I will speak about some results obtained by Chitat Chong, Ted Slaman and me on the first order and second order arithmetical consequences of Ramsey Theorem for Pairs. 問合せ先: 龍田真 (国立情報学研究所) e-mail: tatsuta(a)nii.ac.jp http://research.nii.ac.jp/~tatsuta

1 0

=?ISO-2022-JP?B?UmU6IEVMQxskQjgmNWY9ODJxIScbKEIzGyRCN24bKEI=?=14( 木） ), 13(水), 17(日)午後午後
by Jun Tarui 05 Feb '13

05 Feb '13

みなさま，１月３０日のメール（このメールの最後にあるもの）でお伝えしましたスケジュールの最新版をみなさまの参考のためお伝えします。主な変更点は、TBAとなっていたいくつかの講演タイトルが決定したことです。参加ご検討くださるようお願いします。垂井 -------------------------------- Mar13(Wed) Satellite Mini-Workshop, Shinagawa venue: Kyoto Univ Shinagawa Office, Shinagawa (in: Intercity Shinagawa Building A, 27th floor) http://www.kyoto-u.ac.jp/ja/tokyo-office http://goo.gl/aCgSE registration not necessary; no participation fee; everybody is welcome organizers: Yoshio Okamoto (UEC), Suguru Tamaki (Kyoto U), Jun Tarui (UEC) each talk will have a 15-min break in the middle 10:30--12:15 David Zuckerman: Randomness Extraction: A Survey 12:15--13:40 lunch (on your own) 13:40--15:25 Ran Raz: Parallel Repetition of Two Prover Games: A Survey 15:25--15:45 break 15:45--17:30 Noam Nisan: Algorithmic Mechanism Design: Multi-unit Auctions 18:00-- impromptu dinner party at Shinagawa ------------------------------- Tokyo Complexity Workshop (Main Workshop): venue: Shinagawa Prince Hotel, Main Tower 8th floor, Room: "Turquoise 8" http://www.al.ics.saitama-u.ac.jp/elc/ws/ http://goo.gl/aCgSE fee for reception/banquet; no fee otherwise; please register in all cases Mar14(Thu) 13:20--13:30 opening 13:30--14:20 Umesh Varirani: Quantum Hamiltonian Complexity: through the computational lens 14:20--14:35 break 14:35--15:25 Rahul Jain: TBA 15:25--15:40 break 15:40--16:30 Pavel Pudlak: Polynomial Hierarchy and Bounded Arithmetic Hierarchy. 16:30--16:45 break 16:45--17:35 Ryan O'Donnell: Approximability and Proof Complexity 18:00--20:00 reception Mar15(Fri) 09:00--09:50 Noam Nisan: Selling Two Objects (in Three Models) 09:50--10:15 break 10:15--11:05 Ketan Mulmuley: The GCT Chasm 11:05--11:30 break 11:30--12:20 Joshua Grochow: Geometric Complexity Theory unifies and generalizes many known lower bounds (an introduction to GCT) 12:20--14:00 lunch (on your own) 14:00--14:50 Shachar Lovett: The probabilistic method - new frontiers 14:50--15:15 break 15:15--16:05 Zeev Dvir: Locally Decodable Codes: recent progress and open problems 16:05--16:30 break 16:30--17:20 Luca Trevisan: Spectral Graph Theory Mar16(Sat) 09:00--09:50 Raghu Meka: Recent Progress in Unconditional Derandomization 09:50--10:15 break 10:15--11:05 David Zuckerman: Pseudorandomness from Shrinkage 11:05--11:30 break 11:30--12:20 Irit Dinur: TBA 12:20--14:00 lunch (lunch on your own) 14:00--14:50 Rocco Servedio: TBA 14:50--15:15 break 15:15--16:05 Pinyan Lu: Complexity Dichotomies of Counting Problems 16:05--16:30 break 16:30--17:20 Ran Raz: Interactive Channel Capacity 18:00--20:00 banquet Mar17(Sun) 09:00--09:50 Valentine Kabanets: Yin and Yang of computing: From circuit lower bounds to compression and SAT algorithms, and back 09:50--10:05 break 10:05--10:55 Eric Allender: Strengthening the Link between Complexity Classes and Kolmogorov Complexity 10:55--11:10 break 11:10--12:00 Yuichi Yoshida: Robust approximation of CSPs: Universal algebra meets optimization -------------------------------- Mar17(Sun) Satellite Mini-Workshop on Geometric Complexity Theory(GCT) venue: 2nd floor meeting room, Campus Innovation Center, Tamachi http://www.cictokyo.jp/access.html http://goo.gl/aCgSE registration not necessary; no participation fee; everybody is welcome organizers: Takeshi Tokuyama (Tohoku U), Susumu Ariki (Osaka U), Jun Tarui (UEC) speakers: Ketan Mulmuley and Joshua Grochow 14:00--18:15 (with 3 breaks) 18:30-- impromptu dinner party at Tamachi ------------------------------- Mar19(Tue) Satellite Mini-Workshp, Kyoto venue: Room 111, RIMS, Kyoto Univ, Kyoto http://www.kurims.kyoto-u.ac.jp/en/access-01.html http://goo.gl/aCgSE registration not necessary; no participation fee; everybody is welcome organizers: Shin-ichi Tanigawa (RIMS), Suguru Tamaki (Kyoto U), Jun Tarui (UEC) 13:15--14:15 Raghu Meka: Beating the Union Bound via Gaussian Geometry 14:15--14:30 break 14:30--15:30 Zeev Dvir: Locally Decodable Codes: recent progress and open problems 15:30--15:45 break 15:45--17:15 Ketan Mulmuley: talk on geometric complexity theory 18:00-- impropmtu dinner party around Sanjo/Shijo-Kawara-machi -------------------------------- Speakers: Eric Allender (Rutgers) www.cs.rutgers.edu/~allender/ Irit Dinur (Weizmann) www.wisdom.weizmann.ac.il/~dinuri/ Zeev Dvir (Princeton) www.cs.princeton.edu/~zdvir/ Josh Grochow (U Toronto) www.cs.toronto.edu/~jgrochow/ Rahul Jain (Nat Univ Singapore) www.comp.nus.edu.sg/~rahul/ Valentine Kabanets (Simon Fraser) www.cs.sfu.ca/~kabanets/ Shachar Lovett (UCSD) https://sites.google.com/site/shacharlovetthomepage/ Pinyan Lu (Microsoft Research Asia and Shanghai Jiao Tong Univ) http://research.microsoft.com/en-us/people/pinyanl/ Raghu Meka (Princeton, IAS) www.math.ias.edu/~raghu/ Ketan Mulmuley (Chicago) www.cs.uchicago.edu/people/mulmuley Noam Nisan (Hebrew U) www.cs.huji.ac.il/~noam/ Ryan O'Donnell (CMU) www.cs.cmu.edu/~odonnell/ Pavel Pudlak (Math Institute of Czech Republic) www.math.cas.cz/~pudlak/ Ran Raz (Weizmann) www.wisdom.weizmann.ac.il/~ranraz/ Rocco Servedio (Columbia) www.cs.columbia.edu/~rocco/ Luca Trevisan (Stanford) http://theory.stanford.edu/~trevisan/ Umesh Vazirani (UC Berkeley) http://www.cs.berkeley.edu/~vazirani/ Yuichi Yoshida (National Institute of Informatics, Tokyo) http://research.nii.ac.jp/~yyoshida/ David Zuckerman (U Texas, Austin) www.cs.utexas.edu/~diz/ At 10:08 13/01/30, Jun Tarui wrote: >みなさま， > >電通大の垂井です． > >計算限界解明プロジェクト http://www.al.ics.saitama-u.ac.jp/elc/ >のキックオフメイン集会とサテライト集会に関して >プログラム作成と企画の主担当をしています． > >まだ調整中の部分もあるのですが，みなさまの参考のために >現時点での予定をお伝えします．ぜひ参加ご検討ください． > > >サテライト集会：参加費なしで登録不要です． >当日夕方に参加希望を現地で尋ねる形の懇親食事会を予定しています． > >メイン集会：参加費はなしですが，一部講演のみ聴講の場合でも >登録をお願いしています．登録締め切りは２月２８日です． > >よろしくお願いします． > >垂井淳 >-------------------------------------------- >Exploring the Limits of Computation (ELC) >Tokyo Complexity Workshop and Satellite Mini-Workshops: >http://www.al.ics.saitama-u.ac.jp/elc/ws/ > > >Mar13(Wed) Satellite Mini-Workshop, Shinagawa > >venue: Kyoto Univ Shinagawa Office, Shinagawa >http://www.kyoto-u.ac.jp/ja/tokyo-office http://goo.gl/aCgSE >registration not necessary; no participation fee; everybody is welcome >organizers: Yoshio Okamoto(UEC), Suguru Tamaki(Kyoto U), Jun Tarui(UEC) > >each talk will have a 15-min break in the middle >10:30--12:15 TBA >12:15--13:40 lunch (on your own) >13:40--15:25 Ran Raz: Parallel Repetition of Two Prover Games: A Survey >15:25--15:45 break >15:45--17:30 Noam Nisan: Algorithmic Mechanism Design: Multi-unit Auctions >18:00-- impromptu dinner party at Shinagawa > > >Mar17(Sun) Satellite Mini-Workshop on Geometric Complexity Theory(GCT) > >venue: 2nd floor meeting room, Campus Innovation Center, Tamachi >http://www.cictokyo.jp/access.html http://goo.gl/aCgSE >registration not necessary; no participation fee; everybody is welcome >organizers: Takeshi Tokuyama(Tohoku U), Susume Ariki(Osaka U), Jun Tarui(UEC) > >speakers: Ketan Mulmuley and Joshua Grochow > >14:00--18:15 (with 3 breaks) >18:30-- impromptu dinner party at Tamachi > > >Mar19(Tue) Satellite Mini-Workshp, Kyoto >venue: Room 111, RIMS, Kyoto Univ, Kyoto >http://www.kurims.kyoto-u.ac.jp/en/access-01.html http://goo.gl/aCgSE >registration not necessary; no participation fee; everybody is welcome >organizers: Shin-ichi Tanigawa(RIMS), Suguru Tamaki(Kyoto U), Jun Tarui(UEC) > >13:15--14:15 Raghu Meka: Beating the Union Bound via Gaussian Geometry >14:15--14:30 break >14:30--15:30 Zeev Dvir: Locally Decodable Codes: recent progress and open problems >15:30--15:45 break >15:45--17:15 Ketan Mulmuley: talk on geometric complexity theory >18:00-- impropmtu dinner party around Sanjo/Shijo-Kawara-machi > > >Tokyo Complexity Workshop (Main Workshop): tentative schedule as of Jan 30th >venue: Shinagawa Prince Hotel, Main Tower 8th floor, Room: "Turquoise 8" >http://www.al.ics.saitama-u.ac.jp/elc/ws/ http://goo.gl/aCgSE >fee for reception/banquet; no fee otherwise; please register in all cases > >Mar14(Thu) >13:20--13:30 opening >13:30--14:20 Umesh Varirani: Quantum Hamiltonian Complexity: > through the computational lens >14:20--14:35 break >14:35--15:25 Rahul Jain: TBA >15:25--15:40 break >15:40--16:30 Pavel Pudlak: Polynomial Hierarchy and Bounded Arithmetic Hierarchy. >16:30--16:45 break >16:45--17:35 Ryan O'Donnell: Approximability and Proof Complexity >18:00--20:00 reception > >Mar15(Fri) >09:00--09:50 Noam Nisan: Selling Two Objects (in Three Models) >09:50--10:15 break >10:15--11:05 Ketan Mulmuley: The GCT Chasm >11:05--11:30 break >11:30--12:20 Joshua Grochow: Geometric Complexity Theory unifies and generalizes > many known lower bounds (an introduction to GCT) >12:20--14:00 lunch >14:00--14:50 Shachar Lovett: The probabilistic method - new frontiers >14:50--15:15 break >15:15--16:05 Zeev Dvir: Locally Decodable Codes: recent progress and open problems >16:05--16:30 break >16:30--17:20 Luca Trevisan: TBA > >Mar16(Sat) >09:00--09:50 Raghu Meka: Recent Progress in Unconditional Derandomization >09:50--10:15 break >10:15--11:05 David Zuckerman: Pseudorandomness from Shrinkage >11:05--11:30 break >11:30--12:20 Irit Dinur: TBA >12:20--14:00 lunch >14:00--14:50 Rocco Servedio: TBA >14:50--15:15 break >15:15--16:05 Pinyan Lu: TBA >16:05--16:30 break >16:30--17:20 Ran Raz: Interactive Channel Capacity >18:00--20:00 banquet > >Mar17(Sun) >09:00--09:50 Valentine Kabanets: Yin and Yang of computing: From circuit lower bounds > to compression and SAT algorithms, and back >09:50--10:05 break >10:05--10:55 Eric Allender: Strengthening the Link between Complexity Classes > and Kolmogorov Complexity >10:55--11:10 break >11:10--12:00 Yuichi Yoshida: Robust approximation of CSPs: > Universal algebra meets optimization > >Speakers: > >Eric Allender (Rutgers) www.cs.rutgers.edu/~allender/ >Irit Dinur (Weizmann) www.wisdom.weizmann.ac.il/~dinuri/ >Zeev Dvir (Princeton) www.cs.princeton.edu/~zdvir/ >Josh Grochow (U Toronto) www.cs.toronto.edu/~jgrochow/ >Rahul Jain (Nat Univ Singapore) www.comp.nus.edu.sg/~rahul/ >Valentine Kabanets (Simon Fraser) www.cs.sfu.ca/~kabanets/ >Shachar Lovett (Princeton, IAS) > https://sites.google.com/site/shacharlovetthomepage/ >Pinyan Lu (Microsoft Research Asia and Shanghai Jiao Tong Univ) > http://research.microsoft.com/en-us/people/pinyanl/ >Raghu Meka (Princeton, IAS) www.math.ias.edu/~raghu/ >Ketan Mulmuley (Chicago) www.cs.uchicago.edu/people/mulmuley >Noam Nisan (Hebrew U) www.cs.huji.ac.il/~noam/ >Ryan O'Donnell (CMU) www.cs.cmu.edu/~odonnell/ >Pavel Pudlak (Math Institute of Czech Republic) > www.math.cas.cz/~pudlak/ >Ran Raz (Weizmann) www.wisdom.weizmann.ac.il/~ranraz/ >Rocco Servedio (Columbia) www.cs.columbia.edu/~rocco/ >Luca Trevisan (Stanford) > http://theory.stanford.edu/~trevisan/ >Umesh Vazirani (UC Berkeley) > http://www.cs.berkeley.edu/~vazirani/ >Yuichi Yoshida (National Institute of Informatics, Tokyo) > http://research.nii.ac.jp/~yyoshida/ >David Zuckerman (U Texas, Austin) www.cs.utexas.edu/~diz/

1 0

仙台ロジックスクール
by Tanaka Kazuyuki 05 Feb '13

05 Feb '13

仙台ロジックスクール SLS2013 （日本ベルギー合同勉強会）すでにご案内申し上げておりますCTFM研究集会(２月１８日〜２１日，東工大) http://sendailogic.math.tohoku.ac.jp/CTFM/ のサテライトとして，仙台にて学生・若手のための勉強会を下記の通り行います。【日程】　２月２２日（金）・２３日（土）9:00 開場【場所】　仙台国際センター　小会議室８【講師】　S. Simpson，Yang Yue，Wu Guohua 　　　　　照井一成，宮部賢志，秋吉亮太（敬称略） ※詳細は，下記ウェブ・ページをご覧ください。 http://sendailogic.math.tohoku.ac.jp/SLS/ 　――――――――――――――――――――――― 参加費は無料ですが，会場準備の都合上，参加される方は事前申し込みをお願いします。【申し込み期限】　2月11日（祝）【申し込み・問い合わせ先】　sendailogic(a)gmail.com 　(担当：朴) 下の申込書をカット＆ペーストして必要事項を記入のうえ，上のアドレス（朴）までお送りください。２２日の夜に懇親会（参加費３千円程度）を予定しておりますので、出欠を併せてお知らせください。 ※　宿泊については，近くのホテルの部屋をいくつかおさえてありますので，必要な方はお問い合わせください。幹事：田中一之，山崎武（東北大学・理学研究科）　――――――――――――――――――――――― 仙台ロジックスクール SLS2013　申込書　お名前　所属・身分　ご連絡先　講演会参加　　22日（　）　23日（　）　懇親会参加　　22日（　）　―――――――――――――――――――――――

1 0

Kobe Colloquium (Feb 6, 2013, Pelupessy)
by Makoto Kikuchi 04 Feb '13

04 Feb '13

Kobe Colloquium on Logic, Statistics and Informatics 以下の要領でコロキウムを開催します。日時：2013年2月6日（水）15:10-16:40 場所：神戸大学自然科学総合研究棟3号館4階421室（プレゼンテーション室）講演者：Florian Pelupessy (Ghent) ======================================================================== 題目：Connecting the provable with the unprovable アブストラクト： Since Gödels famous incompleteness theorems it is well known that there exist theorems which are not provable in Peano Arithmetic. In the last decades of the last century many mathematically interesting examples of such unprovable statements emerged, for example: the Paris-Harrington theorem, the Kanamori-McAloon theorem, Kruskal's tree theorem, Hydra battles and Goodstein sequences. In these theorems it is possible to insert a parameter function, where the resulting theorem variant with constant parameter is provable, but the variant with as parameter the identity function is unprovable. An obvious question in these cases is at which threshold between those functions (ordered by eventual domination) the resulting theorem changes from provable to unprovable: the phase transition for provability of the theorem. We study these phase transitions with the goal of better understanding unprovability. We will be examining the transition results for three Ramsey theorem variants: Friedman's adjacent Ramsey theorem, the Paris-Harrington theorem and the Kanamori-McAloon theorem. For these theorems it is possible to show a deep connection between lower/upper bound estimates for the variants with constant parameter values and the threshold values for the parametrised theorems. This shows an influence of mathematics which is provable at a level slightly stronger than exponential function arithmetic on provabiltiy at the level of Peano Arithmetic. ======================================================================== 交通：阪急六甲駅またはJR六甲道駅から神戸市バス36系統「鶴甲団地」行きに乗車，「神大本部工学部前」停留所下車，徒歩すぐ． http://www.kobe-u.ac.jp/info/access/rokko/rokkodai-dai2.htm 連絡先：菊池誠　mkikuchi(a)kobe-u.ac.jp

1 0

重要なご連絡ーアブストラクトの公開について（訂正）
by Masahiro Kumabe 02 Feb '13

02 Feb '13

皆様複数受け取られた場合はご容赦ください。こんにちは。日本数学会の数学基礎論及び歴史分科会の連絡評議委員の隈部です。先日、学会発表におけるアブストラクトの公開についてのご連絡を、メールにてお知らせしましたが、訂正があります。重要な内容ですので、是非ご一読お願い致します。＊学会における一般講演のアブストラクトについて２０１３年度年会から、数学会として、一般講演のアブストラクトをPDFファイルとして、学会開催前に、数学会のホームペジにて公開することをご連絡しましたが、これは、数学基礎論及び歴史分科会においては、学会会員内だけの公開です。昨年９月の分科会総会でそのように決まっていました。ここにお詫びして訂正致します。申し訳ありませんでした。従いまして、学会会員でない方は、アブストラクトの冊子を学会会場で購入してご覧になれます。以上の件、お間違いのないようにご理解ください。隈部

1 0

【参加申込締切2013年2月4日(月)】CTFM 2013, Tokyo, 18-20, Feb 2013
by Naohi Eguchi 01 Feb '13

01 Feb '13

Logic-ml の皆様，以下の研究会の参加申込締切が迫ってまいりましたのでご案内させていただきます． Computability Theory and Foundations of Mathematics (CTFM 2013) (2013年2月18日(月)～2月20日(水)，東京工業大学大岡山キャンパス) 参加ご希望の方は参加登録ページよりお申込ください． http://sendailogic.math.tohoku.ac.jp/CTFM/registration.html 参加申込締切：2013年2月4日(月) 多くの方々の参加申込をお待ちいたしております．江口直日，Sam Sanders, 田中一之 CTFM(a)math.tohoku.ac.jp ============================================================ Computability Theory and Foundations of Mathematics (Tokyo Institute of Technology, Tokyo, Japan, February 18 - 20, 2013) http://sendailogic.math.tohoku.ac.jp/CTFM/ ============================================================ 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, Constructive Mathematics, Theory of Randomness and Computational Complexity Theory. This is a successor workshop to Workshop on Proof Theory and Computability Theory 2012 - Philosophical Frontiers in Reverse Mathematics (February 20 - 23, 2012, Tokyo, Japan). -------------------------------------------- Deadline of Registration: February 4th, 2013 -------------------------------------------- Invited Speakers: Chi Tat Chong (National University of Singapore) Erik Palmgren (Stockholm University) Michael Rathjen (University of Leeds) Helmut Schwichtenberg (LMU Munich) Stephen G. Simpson (Pennsylvania State University) Yang Yue (National University of Singapore) Wu Guohua (Nanyang Technological University) -------------------------------------------- Programme Committee: Toshiyasu Arai (Chiba) Naohi Eguchi (Tohoku) Hajime Ishihara (JAIST) Ryo Kashima (Tokyo Institute of Technology) Sam Sanders (Ghent) Kazuyuki Tanaka (Tohoku, Co-chair) Andreas Weiermann (Ghent, Co-chair) Takeshi Yamazaki (Tohoku) Keita Yokoyama (Tokyo Institute of Technology) --------------------------------------------

1 0

Eighth NII Type Theory Workshop
by Makoto Tatsuta 01 Feb '13

01 Feb '13

Eighth NII Type Theory Workshop Date: February 6, 2013, 10:40--16:50 Place: National Institute of Informatics, Room 1904 (19th floor) 場所: 国立情報学研究所 19階 1904室 (半蔵門線,都営地下鉄三田線・新宿線神保町駅または東西線竹橋駅より徒歩5分) (地図 http://www.nii.ac.jp/about/access/) Program: 10:40--11:20 Toshihiko Uchida (The Graduate University for Advanced Studies) Title: A Partial Translation from lambda U to lambda 2 11:20--12:00 Daisuke Kimura (National Institute of Informatics) Title: Linear Pure Type Systems 12:00--14:00 Lunch Break 14:00--14:40 Kazuyuki ASADA (National Institute of Informatics) Title: Curry-Howard Correspondence between Dialectica Interpretation and Bidirectional Transformation 14:40--15:20 Makoto Tatsuta (National Institute of Informatics) Title: Dual Calculus with Inductive and Coinductive Types 15:20--15:50 Tea Break 15:50--16:50 Stefano Berardi (Torino University) Title: A Curry-Howard result for various subclassical logics Abstracts: ---------------------------------------------------------------------- Toshihiko Uchida (The Graduate University for Advanced Studies) Title: A Partial Translation from lambda U to lambda 2 Abstract: Girard showed that every type of sort * (i.e., proposition) is inhabited in lambda U. Barendregt state without proof that every type of sort Box (i.e., domain) is also inhabited in the system. In this talk, we show that the second statement is not the case by giving a partial translation from lambda U to lambda 2. ---------------------------------------------------------------------- Daisuke Kimura (National Institute of Informatics) Title: Linear Pure Type Systems Abstract: This talk proposes a linear variant of Pure Type Systems (PTSs), called linear pure type systems (LPTSs). It is a general framework, which provides a uniform way to treat various linear type systems that have the features of linear logic. We first introduce a subframework of LPTSs, called multiplicative linear pure type systems (MLPTSs), in which only variables that linearly occur are abstracted. All MLPTSs are consistent and satisfy strong normalization. However their expressive power is rather weak. We then give LPTSs by extending MLPTSs with exponentials. Each PTS can be embedded into a LPTS. We also show the equivalence of strong normalizability of PTSs and LPTSs by giving mutual translations between them. ---------------------------------------------------------------------- Kazuyuki ASADA (National Institute of Informatics) Title: Curry-Howard Correspondence between Dialectica Interpretation and Bidirectional Transformation Abstract: We give Curry-Howard style correspondence between (propositional logic part of) Dialectica interpretation and bidirectional transformation. Dialectica interpretation was introduced by Godel to show relative consistency of Heyting Arithmetic to System T. Independently, bidirectional transformation arose in database community for automatic view-update problem, and recently have been studied in programming language community to formulate languages for bidirectional transformations. A bidirectional transformation consists of a pair of forward ("usual") transformation and a backward ("inverse") transformation, and we usually assume that they satisfy some standard axioms called GetPut law and PutGet law. We show GetPut law naturally fits the above correspondence to Dialectica interpretation, and this gives a way of extending a language for bidirectional transformations with GetPut law. Then we modify the above scheme for PutGet law and the combination of GetPut and PutGet laws. We also show that Paiva's variant of Dialectica model, GC, corresponds to the category for inverse computation. Then for the result by Paiva that the original Dialectica category is the coKleisli category of some comonad on GC, we give similar result for PutGet law, and we utilize this to investigate further categorical structures of these models. Also we see that a kind of Diller-Nahm variant of Dialectica interpretation corresponds to backward-partial bidirectional transformation. ---------------------------------------------------------------------- Makoto Tatsuta (National Institute of Informatics) Title: Dual Calculus with Inductive and Coinductive Types Abstract: This talk gives an extension of Dual Calculus by introducing inductive types and coinductive types. The same duality as Dual Calculus is shown to hold in the new system, that is, this talk presents its involution for the new system and proves that it preserves both typing and reduction. The duality between inductive types and coinductive types is shown by the existence of the involution that maps an inductive type and a coinductive type to each other. The strong normalization in this system is also proved. First, strong normalization in second-order Dual Calculus is shown by translating it into second-order symmetric lambda calculus. Next, strong normalization in Dual Calculus with inductive and coinductive types is proved by translating it into second-order Dual Calculus. This is a joint work with Daisuke Kimura. ---------------------------------------------------------------------- Stefano Berardi (Torino University) Title: A Curry-Howard result for various subclassical logics Abstract: We introduce games with Sequential Backtracking as a model for various sub-classical logic that have implication as a primitive connective. We define a one-sided version of the logical systems, whose proofs have a tree isomorphism (a kind of ``Curry Howard'' isomorphism) with respect to the winning strategies of the game semantics. We use this correspondence to interpret various classical proofs as learning algorithms. ---------------------------------------------------------------------- 問合せ先　龍田 (tatsuta(a)nii.ac.jp)

1 0

数学基礎論及び歴史分科会からの重要なお知らせ
by Masahiro Kumabe 31 Jan '13

31 Jan '13

皆様複数受け取られた場合はご容赦ください。こんにちは。日本数学会の数学基礎論及び歴史分科会の連絡評議委員の隈部です。学会に関して、以下の通りお知らせします。重要な内容ですので、是非ご一読お願い致します。（１）学会における一般講演のアブストラクトについて２０１３年度年会から、数学会として、一般講演のアブストラクトをPDFファイルとして、学会開催前に、数学会のホームペジにて公開することになりました。公開する時期は、学会が開催される２週間前までには公開する予定でいますが、詳しい内容については、学会のホームページにアクセスして、その都度ご確認ください。なおアブストラクトは、学会の会員外の方もダウンロードできるようにする予定です。これにより、アブストラクトを事前に各個人がプリントアウトし、それを持参して、学会に臨むことができるようになります。（２）（１）の対応に関連して、学会会場にて販売されていたアブストラクトの冊子の販売については、分科会として、以下の通りとすることになりました。アブストラクトの冊子での販売は、上記変更による混乱を避けるため、２０１３年度年会においては、続けます。ただし販売部数が減少することが予想されるため、用意する部数を減らします。アブストラクトの冊子の購入を希望される方は、この点ご了解ください。また出来る限り、事前にアブストラクトをプリントアウトあるいはダンロードして、学会に臨まれることをお願いします。当分科会のアブストラクトは、会員外の方もダウンロードできますので、できるだけそのようにお願いします。アブストラクトの冊子での販売は、赤字が予想されますので、なるべく早い時期に廃止する方向で考えています。そのためにもスムーズな移行ができるよう、ご協力お願いします。（３）２０１３年度年会は京都で行われますが、開催期間の京都のホテルが既に混み合っていると数学会から連絡を受けました。ですから、至急ホテルの予約をしていただきますようお願いいたします。以上です。連絡評議委員隈部正博

1 0

CAPE Truth theory and Logic Workshopのお知らせ
by Shunsuke Yatabe 31 Jan '13

31 Jan '13

みなさま複数受け取られた場合はご容赦ください。 2月13日に京都大学で行われる CAPE Truth theory and Logic Workshop のご案内をご転送させて頂きます。矢田部俊介 ---------- Forwarded message ---------- CAPE Truth theory and Logic Workshopのお知らせ皆様京都大学大学院文学研究科附属応用哲学・倫理学教育研究センター（CAPE）の主催にて、 CAPE Truth theory and Logic Workshopが下記のように開催されます。今回は特別講演として、ブリストル大学のPhilip Welch先生に、チューリングの数学の業績に関する一般向け講演（元々は6'th European Cogress of Mathematics で行われたもの）をお願いしました（1600-1745の最終枠です）。専門家以外の方も、ぜひお越し下さい。京都大学大学院文学研究科附属応用哲学・倫理学教育研究センター http://www.bun.kyoto-u.ac.jp/cape/cape-top_page/ 事務補佐　　竹中利彦〒606-0085 京都市左京区吉田本町　京都大学文学部内 CAPE(a)bun.kyoto-u.ac.jp **************************************************************************************** CAPE Truth theory and Logic Workshop Date: February 13 (Wed) 9:00-17:00, Place: The 8th lecture room, "Research Bldg. No. 2 (Sougou Kenkyu 2-Goukan)" of Kyoto University, No34 of the map in http://www.kyoto-u.ac.jp/en/access/campus/main.htm （京都大学総合研究2号館第8講義室） CAPE Website: http://www.bun.kyoto-u.ac.jp/cape/cape-top_page/ Timetable: 9:00-10:15 Shunsuke Yatabe "Yablo paradox and semantics of coinductive language" 10:30-11:45 Graham E. Leigh "Global reflection and theories of truth" 13:15-14:30 Katsuhiko Sano "What is the corresponding first-order logic to coalgebraic modal logic?" 14:30-15:45 Leon Horsten " One hundred years of semantic paradox" 16:00-17:15 Philip Welch "Alan Turing's Mathematical work" Abstracts: Shunsuke Yatabe (Kyoto University) title: Yablo paradox and semantics of coinductive language Abstract: We generalize the framework of Barwise and Etchmendy's "the liar" to that of coinductive language, and focus on a diﬃculty of constructing semantics. We deﬁne a game theoretic semantics, which can be regarded as a version of Austin semantics. Graham E. Leigh (University of Oxford) title: Global reflection and theories of truth Abstract: This talk explores the relationship between the global reflection principle ("If A is provable, A is true") and its arithmetic cousins ("If A is provable then A"). I will provide a proof-theoretic analysis of a number of axiomatic theories of truth expanded by transfinite hierarchies of reflection principles. Katsuhiko Sano (School of Information Science, Japan Advanced Institute of Science and Technology) title: What is the corresponding first-order logic to coalgebraic modal logic? Abstract: It is well-known that modal logic over Kripke models can be regarded as the bisimulation-invariant fragment of first-order logic, where the notion of bisimulation tells us when given two Kripke models are `similar' with each other. This is called Van Benthem's characterization theorem. The main aim of this talk is to propose a corresponding first-order syntax with Van Benthem-style characterization to coalgebraic modal logic, a uniform framework to cover modal logic over Kripke models, modal logic over neighborhood models, graded modal logic, probabilistic modal logic, etc. This talk focuses on a conceptual background to explain our strategy of finding a corresponding FO syntax for coalgebraic modal logic. A key idea consists in Arthur Prior's early idea of hybrid logic (esp. modal operators for pointed truth) and C. C. Chang's FO syntax for neighborhood models. This talk is based on a joint work with Dirk Pattinson (ANU), Tadeusz Litak (Friedrich-Alexander University of Erlangen and Nuremberg (FAU)), and Lutz Schroeder (FAU). Leon Horsten (University of Bristol) title: One hundred years of semantic paradox Abstract: This article contains an overview of the main problems, themes and theories relating to the semantic paradoxes in the twentieth century. From this historical overview I tentatively draw some lessons about the way in which the field may evolve in the next decade. Philip Welch (University of Bristol) title: Alan Turing's Mathematical work -- このメールは Google グループのグループ「京都現代哲学コロキアム」の登録者に送られています。このグループから退会し、メールの受信を停止するには、kyoto_colloquium+unsubscribe(a)googlegroups.com にメールを送信します。その他のオプションについては、https://groups.google.com/groups/opt_out にアクセスしてください。

1 0

ELC研究集会：3月14(木） ), 13(水), 17(日)午後午後
by Jun Tarui 30 Jan '13

30 Jan '13

みなさま，電通大の垂井です．計算限界解明プロジェクト http://www.al.ics.saitama-u.ac.jp/elc/ のキックオフメイン集会とサテライト集会に関してプログラム作成と企画の主担当をしています．まだ調整中の部分もあるのですが，みなさまの参考のために現時点での予定をお伝えします．ぜひ参加ご検討ください．サテライト集会：参加費なしで登録不要です．当日夕方に参加希望を現地で尋ねる形の懇親食事会を予定しています．メイン集会：参加費はなしですが，一部講演のみ聴講の場合でも登録をお願いしています．登録締め切りは２月２８日です．よろしくお願いします．垂井淳 -------------------------------------------- Exploring the Limits of Computation (ELC) Tokyo Complexity Workshop and Satellite Mini-Workshops: http://www.al.ics.saitama-u.ac.jp/elc/ws/ Mar13(Wed) Satellite Mini-Workshop, Shinagawa venue: Kyoto Univ Shinagawa Office, Shinagawa http://www.kyoto-u.ac.jp/ja/tokyo-office http://goo.gl/aCgSE registration not necessary; no participation fee; everybody is welcome organizers: Yoshio Okamoto(UEC), Suguru Tamaki(Kyoto U), Jun Tarui(UEC) each talk will have a 15-min break in the middle 10:30--12:15 TBA 12:15--13:40 lunch (on your own) 13:40--15:25 Ran Raz: Parallel Repetition of Two Prover Games: A Survey 15:25--15:45 break 15:45--17:30 Noam Nisan: Algorithmic Mechanism Design: Multi-unit Auctions 18:00-- impromptu dinner party at Shinagawa Mar17(Sun) Satellite Mini-Workshop on Geometric Complexity Theory(GCT) venue: 2nd floor meeting room, Campus Innovation Center, Tamachi http://www.cictokyo.jp/access.html http://goo.gl/aCgSE registration not necessary; no participation fee; everybody is welcome organizers: Takeshi Tokuyama(Tohoku U), Susume Ariki(Osaka U), Jun Tarui(UEC) speakers: Ketan Mulmuley and Joshua Grochow 14:00--18:15 (with 3 breaks) 18:30-- impromptu dinner party at Tamachi Mar19(Tue) Satellite Mini-Workshp, Kyoto venue: Room 111, RIMS, Kyoto Univ, Kyoto http://www.kurims.kyoto-u.ac.jp/en/access-01.html http://goo.gl/aCgSE registration not necessary; no participation fee; everybody is welcome organizers: Shin-ichi Tanigawa(RIMS), Suguru Tamaki(Kyoto U), Jun Tarui(UEC) 13:15--14:15 Raghu Meka: Beating the Union Bound via Gaussian Geometry 14:15--14:30 break 14:30--15:30 Zeev Dvir: Locally Decodable Codes: recent progress and open problems 15:30--15:45 break 15:45--17:15 Ketan Mulmuley: talk on geometric complexity theory 18:00-- impropmtu dinner party around Sanjo/Shijo-Kawara-machi Tokyo Complexity Workshop (Main Workshop): tentative schedule as of Jan 30th venue: Shinagawa Prince Hotel, Main Tower 8th floor, Room: "Turquoise 8" http://www.al.ics.saitama-u.ac.jp/elc/ws/ http://goo.gl/aCgSE fee for reception/banquet; no fee otherwise; please register in all cases Mar14(Thu) 13:20--13:30 opening 13:30--14:20 Umesh Varirani: Quantum Hamiltonian Complexity: through the computational lens 14:20--14:35 break 14:35--15:25 Rahul Jain: TBA 15:25--15:40 break 15:40--16:30 Pavel Pudlak: Polynomial Hierarchy and Bounded Arithmetic Hierarchy. 16:30--16:45 break 16:45--17:35 Ryan O'Donnell: Approximability and Proof Complexity 18:00--20:00 reception Mar15(Fri) 09:00--09:50 Noam Nisan: Selling Two Objects (in Three Models) 09:50--10:15 break 10:15--11:05 Ketan Mulmuley: The GCT Chasm 11:05--11:30 break 11:30--12:20 Joshua Grochow: Geometric Complexity Theory unifies and generalizes many known lower bounds (an introduction to GCT) 12:20--14:00 lunch 14:00--14:50 Shachar Lovett: The probabilistic method - new frontiers 14:50--15:15 break 15:15--16:05 Zeev Dvir: Locally Decodable Codes: recent progress and open problems 16:05--16:30 break 16:30--17:20 Luca Trevisan: TBA Mar16(Sat) 09:00--09:50 Raghu Meka: Recent Progress in Unconditional Derandomization 09:50--10:15 break 10:15--11:05 David Zuckerman: Pseudorandomness from Shrinkage 11:05--11:30 break 11:30--12:20 Irit Dinur: TBA 12:20--14:00 lunch 14:00--14:50 Rocco Servedio: TBA 14:50--15:15 break 15:15--16:05 Pinyan Lu: TBA 16:05--16:30 break 16:30--17:20 Ran Raz: Interactive Channel Capacity 18:00--20:00 banquet Mar17(Sun) 09:00--09:50 Valentine Kabanets: Yin and Yang of computing: From circuit lower bounds to compression and SAT algorithms, and back 09:50--10:05 break 10:05--10:55 Eric Allender: Strengthening the Link between Complexity Classes and Kolmogorov Complexity 10:55--11:10 break 11:10--12:00 Yuichi Yoshida: Robust approximation of CSPs: Universal algebra meets optimization Speakers: Eric Allender (Rutgers) www.cs.rutgers.edu/~allender/ Irit Dinur (Weizmann) www.wisdom.weizmann.ac.il/~dinuri/ Zeev Dvir (Princeton) www.cs.princeton.edu/~zdvir/ Josh Grochow (U Toronto) www.cs.toronto.edu/~jgrochow/ Rahul Jain (Nat Univ Singapore) www.comp.nus.edu.sg/~rahul/ Valentine Kabanets (Simon Fraser) www.cs.sfu.ca/~kabanets/ Shachar Lovett (Princeton, IAS) https://sites.google.com/site/shacharlovetthomepage/ Pinyan Lu (Microsoft Research Asia and Shanghai Jiao Tong Univ) http://research.microsoft.com/en-us/people/pinyanl/ Raghu Meka (Princeton, IAS) www.math.ias.edu/~raghu/ Ketan Mulmuley (Chicago) www.cs.uchicago.edu/people/mulmuley Noam Nisan (Hebrew U) www.cs.huji.ac.il/~noam/ Ryan O'Donnell (CMU) www.cs.cmu.edu/~odonnell/ Pavel Pudlak (Math Institute of Czech Republic) www.math.cas.cz/~pudlak/ Ran Raz (Weizmann) www.wisdom.weizmann.ac.il/~ranraz/ Rocco Servedio (Columbia) www.cs.columbia.edu/~rocco/ Luca Trevisan (Stanford) http://theory.stanford.edu/~trevisan/ Umesh Vazirani (UC Berkeley) http://www.cs.berkeley.edu/~vazirani/ Yuichi Yoshida (National Institute of Informatics, Tokyo) http://research.nii.ac.jp/~yyoshida/ David Zuckerman (U Texas, Austin) www.cs.utexas.edu/~diz/

1 0

Logic Zoo Workshop 2013 プログラム (1月31日東京)
by Yoichi Hirai 25 Jan '13

25 Jan '13

みなさま東京大学萩谷研の平井洋一です。先般ご案内のLogic Zooワークショップのプログラムを流します。ご参加お待ちしております。平井洋一 ◆日時と場所 2013年1月31日(木) 10:00〜17:00 東京大学本郷キャンパス化学東館236室(理学部7号館より入る) ◆プログラム 10:00〜11:30 (TBA) ・Kazuyuki Asada (NII) 　Curry-Howard Correspondence between Dialectica Interpretation and Bidirectional Transformation ・Yoshihiko Kakutani (Univ. Tokyo) and/or Daisuke Kimura (NII) 　What is natural numbers in call-by-name lambda-mu? ・Ichiro Hasuo (Univ. Tokyo) 　Nonstandard Static Analysis: Discrete Verification Methodologies Transferred to Hybrid Applications 12:00〜13:00 (TBA) ・Mamoru Kaneko (Univ. Tsukuba) 　Infinite Regresses arising from Prediction/Decision Making in Games (with Tai-Wei Hu) ・Yoichi Hirai (Univ. Tokyo) 　Complexity of Conditinal XPath Containment 14:00〜15:00 (TBA) ・Andrzej Murawski (Univ. Warwick) 　TBA ・Kensuke Kojima (Kyoto University) 　A Hoare logic for SIMT programs 15:30〜17:00 (Yoichi Hirai) ・Shunsuke Yatabe (Kyoto University (AIST)) 　Naive Set Theory and Coinduction ・Masaki Hara (Univ. Tokyo) 　Coqで直観主義命題論理の決定性を証明する (On proving decidability of Intuitionistic Propositional Calculus on Coq) ・Toshiki Takahashi (Free Scientist) 　Botanical Shapes Generated by 3rd Data Structure, "Poker" ◆その他情報 http://logiczoo13.pira.jp/

1 0

証明論と書換えに関するワークショップのご案内
by Nao Hirokawa 23 Jan '13

23 Jan '13

皆様３月４日〜８日に金沢市石川県立美術館で開催されます「第３回証明論と書換えに関するワークショップ」のご案内を致します。このワークショップは証明論と計算論研究者の交流を目的としたインフォーマルワークショップです。参加希望される方は廣川 <pr2013(a)jaist.ac.jp> までご連絡下さい。廣川 ====================================================================== Call for Participants PR 2013 3rd Workshop on Proof Theory and Rewriting 4 (Mon) - 8 (Fri) March, 2013 Kanazawa, Japan http://www.jaist.ac.jp/~hirokawa/pr2013/ ====================================================================== The workshop aims at bringing together researchers in proof theory and rewriting to facilitate the exchange of ideas between these tightly connected fields. The workshop is organised as informal one, and not only presentations about published results but also about work in progress are welcome. We welcome participants from all areas, but due to space restrictions in the venue, we kindly ask to contact Nao Hirokawa <pr2013(a)jaist.ac.jp> beforehand. Previous editions of the workshop were held in Obergurgl (2010) and Obergurgl (2006). SCOPE - proof theory and applications - classical logic, intuitionistic logic, linear logic - term rewriting, higher-order rewriting, graph rewriting - typed/untyped lambda calculi - complexity analysis, implicit computational complexity - decidability, computability - theorem proving ... VENUE Ishikawa Prefectural Museum of Art 2-1 Dewa-machi, Kanazawa, Ishikawa, Japan SPEAKERS Toshiyasu Arai (Chiba University) Martin Avanzini (University of Innsbruck) Matthias Baaz (University of Technology, Vienna) Arnold Beckmann (Swansea University) Josef Berger (University of Greifswald) Frederic Blanqui (INRIA-LIAMA) Guillaume Bonfante (LORIA) Ulrik Buchholtz Ugo Dal Lago (Bologna) Naohi Eguchi (Tohoku University) Nao Hirokawa (JAIST) Dieter Hofbauer (ASW BA Saarland) Martin Hofmann (LMU Muenchen) Jean-Pierre Jouannaud (Ecole Polytechnique) Ulrich Kohlenbach (TU Darmstadt) Gyesik Lee (Hankyong National University) Jean-Yves Marion (LORIA) Aart Middeldorp (University of Innsbruck) Georg Moser (University of Innsbruck) Keisuke Nakano (University of Electro-Communications, Tokyo) Erik Palmgren (Stockholm University) Michel Parigot (CNRS, Paris) Norbert Preining (JAIST) Sam Sanders (Ghent University) Masahiko Sato (Kyoto University) Helmut Schwichtenberg (LMU Muenchen) Christian Sternagel (JAIST) Kazushige Terui (Kyoto University) Toshihiko Uchida (SOKENDAI, Tokyo) Johannes Waldmann (HTWK Leipzig) Gunnar Wilken (OIST) ORGANISING COMMITTEE Nao Hirokawa (JAIST) Hajime Ishihara (JAIST) Georg Moser (University of Innsbruck) Mizuhito Ogawa (JAIST) Norbert Preining (JAIST) Satoshi Tojo (JAIST)

1 0

RTA 2013: Last Call for Papers
by Nao Hirokawa 23 Jan '13

23 Jan '13

皆様 RTA 2013 の論文募集をご案内致します。今回の RTA はオランダ Eindhoven で行われ、TLCA 2013 との共催です。ぜひ投稿をご検討下さい。なお投稿締切は strict deadline となっております。廣川　直 (JAIST) ************************************************************************* RTA 2013: LAST CALL FOR PAPERS 24th International Conference on Rewriting Techniques and Applications June 24 - 26, 2013 Eindhoven, The Netherlands co-located with TLCA 2013 as part of RDP 2013 http://rta2013.few.vu.nl/ ************************************************************************* abstract submission February 1 2013 paper submission February 5 2013 (THIS IS A STRICT DEADLINE !) rebuttal period March 18-21 2013 notification April 4 2013 final version April 26 2013 ************************************************************************* The 24th International Conference on Rewriting Techniques and Applications (RTA 2013) is organized as part of the Federated Conference on Rewriting, Deduction, and Programming (RDP 2013), together with the 11th International Conference on Typed Lambda Calculi and Applications (TLCA 2013), and several workshops. RDP 2013 will be held at the Eindhoven University of Technology in the Netherlands. *** INVITED SPEAKERS *** - Simon Peyton-Jones (Microsoft Research, UK) joint invited speaker for TLCA+RTA 2013 - Jarkko Kari (University of Turku, Finland) invited speaker for RTA 2013 - Mitsu Okada (Keio University, Japan) invited speaker for RTA 2013 *** TOPICS OF INTEREST *** RTA is the major forum for the presentation of research on all aspects of rewriting. Typical areas of interest include (but are not limited to): Applications: case studies; analysis of cryptographic protocols; rule-based (functional and logic) programming; symbolic and algebraic computation; SMT solving; theorem proving; system synthesis and verification; proof checking; reasoning about programming languages and logics; program transformation; XML queries and transformations; systems biology; homotopy theory; implicit computational complexity; Foundations: equational logic; universal algebra; rewriting logic; rewriting models of programs; matching and unification; narrowing; completion techniques; strategies; rewriting calculi; constraint solving; tree automata; termination; complexity; modularity; Frameworks: string, term, and graph rewriting; lambda-calculus and higher-order rewriting; constrained rewriting/deduction; categorical and infinitary rewriting; stochastic rewriting; net rewriting; binding techniques; Petri nets; higher-dimensional rewriting; Implementation: implementation techniques; parallel execution; rewrite and completion tools; certification of rewriting properties; abstract machines; explicit substitutions; automated (non)termination and confluence provers; automated complexity analysis. *** PUBLICATION *** The proceedings will be published by LIPIcs (Leibniz International Proceedings in Informatics). LIPIcs is open access, meaning that publications will be available online and free of charge, and authors keep the copyright for their papers. LIPIcs publications are indexed in DBLP. For more information about LIPIcs please consult: <http://www.dagstuhl.de/en/publications/lipics> Also, authors of selected papers will be invited to submit an extension of their RTA 2013 paper to a special issue of Logical Methods in Computer Science (LMCS) <http://www.lmcs-online.org/index.php>. *** SUBMISSION GUIDELINES *** Submissions must be - original and not submitted for publication elsewhere, - written in English, - a research paper, or a problem set, or a system description, - in pdf prepared with pdflatex using the LIPIcs stylefile: <http://drops.dagstuhl.de/styles/lipics/lipics-authors.tgz>, - at most 10 pages for system description, at most 15 pages for the other two types of submissions - submitted electronically through the EasyChair system at: <https://www.easychair.org/conferences/?conf=rta2013>. The page limit and the deadline for submission are strict. Additional material for instance proof details, may be given in an appendix which is not subject to the page limit. However, submissions must be self-contained within the respective page limit; reading the appendix should not be necessary to assess the merits of a submission. *** PROGRAMME COMMITTEE CHAIR *** Femke van Raamsdonk (VU University Amsterdam, The Netherlands) *** PROGRAMME COMMITTEE *** Eduardo Bonelli National University of Quilmes, Argentina Byron Cook Microsoft Research Cambridge, UK Stephanie Delaune ENS Cachan, France Gilles Dowek Inria Paris-Rocquencourt, France Maribel Fernandez King's College London, UK Nao Hirokawa JAIST Ishikawa, Japan Delia Kesner University Paris-Diderot, France Helene Kirchner Inria Paris-Rocquencourt, France Barbara Koenig University Duisburg Essen, Germany Temur Kutsia Johannes Kepler University Linz, Austria Aart Middeldorp University of Innsbruck, Austria Vincent van Oostrom Utrecht University, The Netherlands Femke van Raamsdonk VU University Amsterdam, The Netherlands Kristoffer Rose IBM Research New York, USA Manfred Schmidt-Schauss Goethe University Frankfurt, Germany Peter Selinger Dalhousie University, Canada Paula Severi University of Leicester, UK Aaron Stump The University of Iowa, USA Tarmo Uustalu Institute of Cybernetics Tallinn, Estonia Roel de Vrijer VU University Amsterdam, The Netherlands Johannes Waldmann HTWK Leipzig, Germany Hans Zantema Eindhoven University of Technology, The Netherlands *** CONFERENCE CHAIR *** Hans Zantema (Eindhoven University of Technology, The Netherlands) *** STEERING COMMITTEE *** Mauricio Ayala-Rincon Brasilia University, Brasilia Frederic Blanqui INRIA Tsinghua University Beijing, China Salvador Lucas Technical University of Valencia, Spain Georg Moser (chair) University of Innsbruck, Austria Masahiko Sakai Nagoya University, Japan Sophie Tison University of Lille, France *** FURTHER INFORMATION *** Questions related to submission, reviewing, and programme should be sent to the programme committee chair Femke van Raamsdonk, email femke at few.vu.nl.

1 0

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

21 Jan '13

数理論理学セミナーのご案内日時：1月25日(金)15:00から場所：東京工業大学大岡山西８号館W棟11階 W1101セミナー室話者：宮部賢志（京大数解研）題目：一様Kurtzランダムネスに対する独立性定理概要：アルゴリズム的ランダムネスでは，ある2進無限列がランダムかどうかについて，様々な定式化を与える． Martin-L\"ofランダムネスはそのうちの一つで，次のような結果が知られている．「ある列がMLランダムであることと，その列の奇数番目の文字の列AがMLランダムかつ，偶数番目の文字の列が，Aから見てMLランダムであること，が同値となる」この定理はvan Lambalgen's Theoremと呼ばれているが，日本語では独立性定理と呼んでいる．ランダムネスの理論では様々なランダムの概念を考察する．他のランダムの概念に付いては，独立性定理が成り立たないことが知られていたが，筆者は一様相対化の場合は，Schnorrや計算可能ランダムについて，独立性定理が成り立つことを主張した．その後，Demuthランダムネスについても同様の結果が知られている．本発表では，Kurtzランダムネスの一様相対化の場合の独立性定理について報告する． ------ 問い合わせ先：鹿島亮（東京工業大学） kashima(a)is.titech.ac.jp

1 0

European Master's Program in Computational Logic
by Bertram Fronhöfer 17 Jan '13

17 Jan '13

Dear all, I'd like to draw your attention to the fact that fresh Erasmus Mundus scholarships are available for Non-European AND European students who enroll in our European Master's Program in Computational Logic in the fall of 2013. The deadline for application is 31 January, 2013. More details are given below. In particular, I'd like to draw your attention to the fact that we are able to provide grants to EU-students for doing their project at the National ICT of Australia (NICTA). Please spread this information as wide as possible among friends and colleagues, at your old universities and the places, where you currently live and work. Many thanks -- Steffen ******************************************************************************************************* The European Master's Program in Computational Logic We are glad to announce to you the possibility to join our European Master's Program of Computational Logic. This program is offered jointly at the Free-University of Bozen-Bolzano in Italy, the Technische Universität Dresden in Germany, the Universidade Nova de Lisboa in Portugal and the Technische Universität Wien in Austria. Within this program you have the choice to study at two /three of the four European universities. In addition, you can do your project work at the National ICT of Australia (NICTA). You will graduate with a MSc in Computer Science and obtain a joint degree. Information on the universities and the program including the application procedure is provided here: http://www.emcl-study.eu/home.html Language of instruction is English. Tuition fees are 3.000 EUR (for non-European students) and 1.000 (for European students) per year. We would like to draw your attention to the ERASMUS-MUNDUS scholarship program. The ERASMUS-MUNDUS consortium offers 2-year scholarships up to 48.000 EUR for non-EU students and up to 23.000 EUR for EU students of our European Master's Program in Computational Logic. More information on the scholarship program is available from: http://www.emcl-study.eu/fileadmin/emcl_booklet_tree/ma_em_grant.html Do not hesitate to contact us if you have any further questions. Kind regards -- Steffen Hölldobler Prof. Dr. Steffen Hoelldobler International Center for Computational Logic Technische Universität Dresden 01062 Dresden, Germany phone: [+49](351)46 33 83 40 fax: [+49](351)46 33 83 42 email: sh(a)iccl.tu-dresden.de

1 0

CfPart: CTFM 2013, Tokyo, 18-20, Feb 2013
by Naohi Eguchi 15 Jan '13

15 Jan '13

研究会のご案内以下の要領で計算可能性，逆数学等に関する研究会を開催いたします． Computability Theory and Foundations of Mathematics (CTFM 2013) (2013年2月18日(月)〜2月20日(水)，東京工業大学大岡山キャンパス) 参加ご希望の方は参加登録ページよりお申込ください． http://sendailogic.math.tohoku.ac.jp/CTFM/registration.html 参加申込締切：2013年2月4日(月) 多くの方々の参加申込をお待ちいたします．江口直日，Sam Sanders, 田中一之 CTFM(a)math.tohoku.ac.jp ============================================================ Computability Theory and Foundations of Mathematics (Tokyo Institute of Technology, Tokyo, Japan, February 18 - 20, 2013) http://sendailogic.math.tohoku.ac.jp/CTFM/ ============================================================ 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, Constructive Mathematics, Theory of Randomness and Computational Complexity Theory. This is a successor workshop to Workshop on Proof Theory and Computability Theory 2012 - Philosophical Frontiers in Reverse Mathematics (February 20 - 23, 2012, Tokyo, Japan). -------------------------------------------- Deadline of Registration: February 4th, 2013 -------------------------------------------- Invited Speakers: Chi Tat Chong (National University of Singapore) Erik Palmgren (Stockholm University) Michael Rathjen (University of Leeds) Helmut Schwichtenberg (LMU Munich) Stephen G. Simpson (Pennsylvania State University) Yang Yue (National University of Singapore) Wu Guohua (Nanyang Technological University) -------------------------------------------- Programme Committee: Toshiyasu Arai (Chiba) Naohi Eguchi (Tohoku) Hajime Ishihara (JAIST) Ryo Kashima (Tokyo Institute of Technology) Sam Sanders (Ghent) Kazuyuki Tanaka (Tohoku, Co-chair) Andreas Weiermann (Ghent, Co-chair) Takeshi Yamazaki (Tohoku) Keita Yokoyama (Tokyo Institute of Technology) --------------------------------------------

1 0

NIIレクチャーシリーズのお知らせ(Randy Goebel)
by Ken Satoh 11 Jan '13

11 Jan '13

NIIレクチャーシリーズのお知らせ国立情報学研究所(NII)では、海外の情報学に関係する著名研究者を招聘し、レクチャーシリーズを行っております。今回は、ＡＩの黎明期からＡＩの研究をされてきたカナダ・アルバータ大学のRandy Goebel先生の連続レクチャーのお知らせです。今回はＡＩ原理をビッグデータに応用する最先端の研究の講演を行っていただきます。講師:Prof. Randy Goebel (department of Computing Science at the University of Alberta, in Edmkonton, Alberta, Canada) 講義名：Do the emerging tools for managing big data fit with the founding principles of Artificial Intelligence? http://www.nii.ac.jp/en/event/list/0212 場所：国立情報学研究所 20階 2010室講義日：2013/2/12, 20, 26, 3/1 時間: 13:30-15:00 出席は無料で、どなたでも参加できます。参加のご検討よろしくお願いします。佐藤　健国立情報学研究所および総研大 ======= NII Lecture Series Title: Do the emerging tools for managing big data fit with the founding principles of Artificial Intelligence? ideas on the integration of the advice taker, structured inference, reasoning with incomplete information, and building multi-scale models from data. Speaker: Prof. Randy Goebel (department of Computing Science at the University of Alberta, in Edmkonton, Alberta, Canada) He is also vice president of the innovates Centre of Research Excellence (iCORE) at Alberta Innovates Technology Futures (AITF), chair of the Alberta Innovates Academy, and principle investigator in the Alberta Innovates Centre for Machine Learning. He received the B.Sc. (Computer Science), M.Sc. (Computing Science), and Ph.D. (Computer Science) from the Universities of Regina, Alberta, and British Columbia, respectively. At AITF, Randy is in charge of reshaping research investments (graduate student scholarships, research chairs, research centres). His research interests include applications of machine learning to systems biology, visualization, and web mining, as well as work on natural language processing, web semantics, and belief revision. Randy has experience working on industrial research projects in crew scheduling, pipeline scheduling, and steel mill scheduling, as well as scheduling and optimization projects for the energy industry in Alberta. Randy has held appointments at the University of Waterloo, University of Tokyo, Multimedia University (Malaysia), Hokkaido University (Sapporo), and has had research collaborations with DFKI (German Research Centre for Artificial Intelligence), NICTA (National ICT Australia), RWC (Real World Computing project, Japan), ICOT (Institute for New Generation Computing, Japan), NII (National Institute for Informatics, Tokyo), and is actively involved in academic and industrial collaborative research projects in Canada, Australia, Europe, and China. Abstract: The modern discipline of computer science has many facets, but what has clearly emerged in the last decade are three themes based on 1) rapidly accumulating volumes of data, 2) inter- and cross-disciplinary application of computer science to all scientific disciplines, and 3) a renewed interest in the semantics of complex information models, spanning a spectrum from semantic web, natural language, to multi-scale systems biology. This series of four lectures will attempt to knit together these three themes, by presenting the ideas that have emerged in their support: the rapid development and extension of machine learning theory and methods to help make sense of accumulating volumes of data, the application of computer science to nearly all scientific disciplines, especially those whose progress now necessarily relies on the management and interpretation of large data, and finally, the revival of a focus on semantics of information models based on data. Outline: Lecture 1: Connecting Advice Taking and Big Data Lecture 2: Structured inference and incomplete information Lecture 3: Natural Language Processing: Compressing Data to Models Lecture 4: Hypothesis Management with Symbols and Pictures Place: Lecture room 2010, 20th floor, National Institute of Informatics Date: 13:30pm-15:00pm, February 12, 20, 26, March 1, 2013 Lecture 1 Connecting Advice Taking and Big Data Tuesday, February 12, 2013, 13:30 - 15:00 A fundamental premise of Artificial Intelligence (AI) is the ability for a computer program to improve its behaviour by taking advice. Incremental accumulation of advice or knowledge has never been easier than today, when the rate of data capture is higher than ever before, and the management of big data and deployment of machine learning are coupled to help manage the transition from data to knowledge. This lecture uses simple technical concepts from nearly sixty years of AI, to identify some of the research challenges of managing big data, and exploiting knowledge emergent from big data. The goal is to find some important research priorities based on the motivation of the Advice Taker, and the current state of big data management and machine learning. Lecture 2 Structured inference and incomplete information Wednesday. February. 20, 13:30 - 15:00 If the foundation of Artificial Intelligence (AI) is the accumulation and use of knowledge, then a necessary stop is the structuring knowledge to be able to make inferences. The organization structures required to facilitate inference now span a broad spectrum of mathematical methods, including everything from simple propositional logic to sophisticated statistical and probabilistic inference. The two foundational components of computational inference are semantics of formal reasoning, and the development of reasoning methods to deal with incomplete information. This lecture reviews the foundational components of semantics and reasoning systems, including the development of goal-oriented reasoning based on abductive reasoning, the connection between logical and probabilistic systems, and especially how the architecture of reasoning systems can provide the basis for managing hypotheses in the face of incomplete information. Lecture 3 Natural Language Processing: Compressing Data to Models Tuesday. February. 26, 13:30 - 15:00 The problem of machine processing of natural language (NLP) has long been a research focus of artificial intelligence. This is partly because the use of natural language is easily conceived as a cognitive task requiring human-like intelligence. It is also because the rational structures for computer interpretation of language require the full suite of computational tools developed over the last hundred years (grammar, dictionaries, logic, parsing, inference, and context management). Most of the recent practical advances in NLP have arisen in the context of simple machine learning applied to large language corpora, to induce fragments of language models that provide the basis for interpretive and generative manipulation of language. These largely statistical models are arisen in what has been called the "pendulum swing" of NLP, in which statistical models have recently dominated those based on structural linguistics. In this lecture, we look at the concept of noisy corpora and their role in language models, including some interesting alternative sources of data for building language models. The applications range from complex language summary to the information extraction from medical, legal, and historical documents. Lecture 4 Hypothesis Management with Symbols and Pictures Friday. March. 1, 13:30 - 15:00 The current suite of Artificial Intelligence (AI) tools has provided a basis for sophisticated human-computer interfaces based on more than typing in language. In fact, one can develop multi-level representations that provide the basis for direct manipulation of visualizations. By constraining the repertoire of direct manipulations, one can enrich human computer interaction so that both humans and machines can understand and exploit visual interaction. This lecture shows how such direction manipulation requires a large repertoire of formal reasoning methods, and provides the sketch of formal framework and the problems arising in its development.

1 0

Cristian S. Calude氏、Elena Calude氏講演会のお知らせ（中央大学研究開発機構）
by Kohtaro Tadaki 11 Jan '13

11 Jan '13

＜重複してお受け取りの方はご容赦ください＞皆様：中央大学の只木と申します。中央大学研究開発機構では、来週19日土曜日、ニュージーランド研究者Cristian S. Calude氏（オークランド大学）およびElena Calude氏（マッセイ大学）をお招きし、下記要領で講演会を開催します。皆様、奮ってご参加下さい。 ---------------------------------- 只木孝太郎 (Kohtaro Tadaki) 中央大学研究開発機構〒112-8551 東京都文京区春日1-13-27 E-mail: tadaki(a)kc.chuo-u.ac.jp WWW: http://www2.odn.ne.jp/tadaki/ ---------------------------------------------------------- Cristian S. Calude氏、Elena Calude氏講演会 ◆日時： 2013年1月19日（土）15時00分〜 17時30分 ◆場所：中央大学後楽園キャンパス 5号館1階 5138号室（下記参照） ◆参加申込：不要 ---------------------------------------------------------- [ 講演内容 ] ◆15時00分〜16時00分講演題目：The complexity of mathematical problems 講演者：Cristian S. Calude (University of Auckland, NZ) and Elena Calude (Massey University, NZ) 講演要旨： Evaluating (or even guessing) the degree of complexity of an open problem, conjecture or mathematically proven statement is not an easy task not only for beginners, but also for the most experienced mathematicians. Is there a (uniform) method to evaluate, in some objective way, the difficulty of a mathematical statement or problem? The question is not trivial because mathematical problems can be so diverse. But, is there any indication that all, or most, or even a large part of mathematical problems have a kind of "commonality" allowing a uniform evaluation of their complexity? How could one compare a problem in number theory with a problem in complex analysis, a problem in algebraic topology or a theorem in dynamical systems? Surprisingly enough, such "commonalities" do exist for many mathematical problems. One of them is based on the possibility of expressing the problem in terms of (very) simple programs reducible to a (natural) question in theoretical computer science, the so-called "halting problem". A more general "commonality" can be discovered using the inductive type of computation, a computation more general the Turing computability. As a consequence, uniform approaches for evaluating the complexity of a large class of mathematical problems/conjectures/statements can be, and have been, developed. This talks reviews current progress and some open problems. ◆16時30分〜17時30分講演題目： The Kochen-Specker theorem and quantum randomness 講演者： Cristian S. Calude (University of Auckland, NZ) 講演要旨： The Kochen-Specker theorem shows the impossibility for a hidden variable theory to consistently assign values to certain (finite) sets of observables in a way that is noncontextual and consistent with quantum mechanics. If we require noncontextuality, the consequence is that many observables must not have pre-existing definite values. However, the Kochen-Specker theorem does not allow one to determine which observables must be value indefinite. In this talk we present an improvement on the Kochen-Specker theorem which allows one to actually locate observables which are provably value indefinite. Various technical and subtle aspects relating to this formal proof and its connection to quantum mechanics are discussed. This result is then utilized for the proposal and certification of a dichotomic quantum random number generator operating in a three-dimensional Hilbert space. ------------------------------------------------------------ 会場への道順： [中央大学後楽園キャンパスへのアクセスガイド] http://www.chuo-u.ac.jp/chuo-u/access/index_j.html http://www.chuo-u.ac.jp/chuo-u/access/access_korakuen_j.html [中央大学後楽園キャンパスマップ] http://www.chuo-u.ac.jp/chuo-u/campusmap/korakuen_j.html ------------------------------------------------------------

1 0

HAS 2013: Deadline Extended
by Ichiro Hasuo 06 Jan '13

06 Jan '13

みなさま，東京大学の蓮尾です．あけましておめでとうございます．以前お知らせした ETAPS 併設ワークショップの HAS，締切が 1/21 に延長になりました．Post-proceeding ですので，論文の preliminary version でも大歓迎，とのことです．ご投稿を検討いただければ幸いです．どうかよろしくお願いいたします．それでは！蓮尾一郎 http://www-mmm.is.s.u-tokyo.ac.jp/~ichiro/ =========================== [Apologies for multiple copies] [Please note: submission deadline extended to January, 12] ************************************************************************************************************ ********* CALL FOR PAPERS Third Workshop on Hybrid Autonomous Systems (HAS 2013) A satellite event of European Joint Conferences on Theory and Practice of Software, ETAPS 2013 March 17, 2013, Rome, Italy http://www2.warwick.ac.uk/fac/sci/maths/people/staff/bujorianu/has2013/ ************************************************************************************************************ ********* SCOPE: The interest on autonomous systems is increasing both in industry and academia. Such systems must operate with limited human intervention in a changing environment and must be able to compensate for significant system failures without external intervention. The hybrid discrete-continuous models constitute appropriate models of autonomous systems . Hybrid systems have behaviours characterised by the interaction between continuous and discrete dynamics and research in the area is driven by several school of thoughts. One approach is mainly focussed on applications to automation systems and the models and methods are centred on the concept of hybrid automaton (deterministic or probabilistic). A distinct school of thought interprets hybrid systems as control systems with regime change. Such systems are highly adaptive and suitable for modelling autonomic behaviours. The most prominent models of this approach are the stochastic hybrid systems and the mixed logical and dynamical systems. There is a clear research opportunity to combine these approaches for developing models, methods, techniques, methodologies, tools and environments for autonomous systems engineering. This workshop brings together researchers interested in all aspects of autonomy and resilience of hybrid systems. TOPICS: Topics include (but are not limited to): Ø new modelling paradigms for autonomous systems; Ø verification and safety certification techniques; Ø modelling, analysis and control of hybrid systems; Ø uncertainty and stochastic modelling; Ø multi-agent systems; Ø algebraic and categorical methods; Ø interaction between hybrid modelling and complexity science; Ø reports on case studies and practical experiments; Ø autonomous systems in natural science (e.g. from biology, ecology, climate). INVITED SPEAKERS: * Maria Domenica di Benedetto, L'Aquila University, IT * Radu Grosu, Vienna University of Technology, AU * Rafael Wisniewski, Aalborg University, DEN SUBMISSIONS: In order to encourage participation and discussion, this workshop solicits the submission of regular papers, which must contain original work, and must not have been previously published, nor be under consideration for publication elsewhere. The accepted submissions should clearly indicate the membership to one of the following categories: - technical contributions; - tutorials on a topic of importance; - surveys on large extent cross-disciplinary research (e.g., project outcomes);wor - reports on early stage or ongoing work. For each category of submission the novelty of the submission has to be clearly stated and the page limit should vary between 6 and 15 pages. All submissions must be in PDF format and use the EPTCS latex style, see http://style.eptcs.org/. Submissions can be made on the following website: https://www.easychair.org/conferences/login_as_yes.cgi?a=3413468 The workshop PC will review all regular paper submissions to select appropriate ones, ones for acceptance in each category, based on their relevance, merit, originality, and technical content. The authors of accepted submissions are expected to present and discuss their work at the workshop. Accepted regular papers will be published in the Electronic Proceedings in Theoretical Computer Science (EPTCS). A special issue in a journal is under consideration. IMPORTANT DATES: Submission (regular paper): *extended* January 12, 2013 Notification: January 24, 2013 Final version (ETAPS proceedings): February 14, 2013 Workshop: March 17, 2013 Final version (EPTCS post proceedings): TBA ORGANIZATION: PC Chairs: * Luca Bortolussi, University of Trieste, IT * Manuela Bujorianu, University of Warwick, UK * Giordano Pola, University of L’Aquila, IT Program Committee: * Ezio Bartocci, TU Wien, AU * Maria Domenica di Benedetto, L'Aquila University, IT * Luca Bortolussi, University of Trieste, IT (co-Chair) * Manuela Bujorianu, University of Warwick, UK (co-Chair) * Alberto Casagrande, Univeristy of Trieste, IT * Thao Dang, Verimag, FR * Louise Dennis, University of Liverpool, UK * Clare Dixon, University of Liverpool, UK * Alexandre Donzé, UC Berkeley, US * Martin Fränzle, Carl von Ossietzky Universität, DE * Ichiro Hasuo, University of Tokio, JP * Agung Julius, Rensselaer Polytechnic Institute, US * Toshimitsu Ushio, Osaka University, JP * Giordano Pola, L'Aquila University, IT (co-Chair) * Rom Langerak, University of Twente, NL * David Parker, University of Birmingham, UK * Guido Sanguinetti, University of Edinburgh, UK * Olaf Stursberg, University of Kassel, DE

1 0

CALCO 2013: Second Call for Papers
by Ichiro Hasuo 04 Jan '13

04 Jan '13

みなさま，こんにちは！東京大学の蓮尾です．国際会議 CALCO 2013 の案内を（再度）お送りします．トピックは代数・余代数・形式検証の理論一般，開催地はポーランド・ワルシャワ，締切は2月末です．どうか投稿をご検討ください．それでは！蓮尾一郎 http://www-mmm.is.s.u-tokyo.ac.jp/ [Apologies for multiple copies] ========================================================================= SECOND CALL FOR PAPERS: CALCO 2013 5th International Conference on Algebra and Coalgebra in Computer Science September 3 - 6, 2013 Warsaw, Poland http://coalg.org/calco13/ ========================================================================= Abstract submission: February 22, 2013 Paper submission: March 1, 2013 Author notification: May 6, 2013 Final version due: June 3, 2013 ========================================================================= -- SCOPE -- CALCO aims to bring together researchers and practitioners with interests in foundational aspects, and both traditional and emerging uses of algebra and coalgebra in computer science. It is a high-level, bi-annual conference formed by joining the forces and reputations of CMCS (the International Workshop on Coalgebraic Methods in Computer Science), and WADT (the Workshop on Algebraic Development Techniques). Previous CALCO editions took place in Swansea (Wales, 2005), Bergen (Norway, 2007), Udine (Italy, 2009) and Winchester (UK, 2011). The fifth edition will be held in Warsaw, the capital of Poland. -- INVITED SPEAKERS -- Andrej Bauer - University of Lubljana, Sl Miko??aj Boja??czyk - Warsaw University, PL Neil Ghani - University of Strathclyde, UK Damien Pous - CNRS, ENS-Lyon, F -- TOPICS OF INTEREST -- We invite submissions of technical papers that report results of theoretical work on the mathematics of algebras and coalgebras, the way these results can support methods and techniques for software development, as well as experience with the transfer of the resulting technologies into industrial practice. We encourage submissions in topics included or related to those listed below. * Abstract models and logics - Automata and languages - Categorical semantics - Modal logics - Relational systems - Graph transformation - Term rewriting - Adhesive categories * Specialised models and calculi - Hybrid, probabilistic, and timed systems - Calculi and models of concurrent, distributed, mobile, and context-aware computing - General systems theory and computational models (chemical, biological, etc.) * Algebraic and coalgebraic semantics - Abstract data types - Inductive and coinductive methods - Re-engineering techniques (program transformation) - Semantics of conceptual modelling methods and techniques - Semantics of programming languages * System specification and verification - Algebraic and coalgebraic specification - Formal testing and quality assurance - Validation and verification - Generative programming and model-driven development - Models, correctness and (re)configuration of hardware/middleware/architectures, - Process algebra -- NEW TOPICS -- This edition of CALCO will feature two new topics, and submission of papers on these topics is especially encouraged. * Corecursion in Programming Languages - Corecursion in logic / constraint / functional / answer set programming - Corecursive type inference - Coinductive methods for proving program properties - Implementing corecursion - Applications * Algebra and Coalgebra in quantum computing - Categorical semantics for quantum computing - Quantum calculi and programming languages - Foundational structures for quantum computing - Applications of quantum algebra -- SUBMISSION GUIDELINES -- Prospective authors are invited to submit full papers in English presenting original research. Submitted papers must be unpublished and not submitted for publication elsewhere. Experience papers are welcome, but they must clearly present general lessons learned that would be of interest and benefit to a broad audience of both researchers and practitioners. As with previous editions, the proceedings will be published in the Springer LNCS series. Final papers should be no more than 15 pages long in the format specified by Springer (see http://www.springer.de/comp/lncs/authors.html). It is recommended that submissions adhere to that format and length. Submissions that are clearly too long may be rejected immediately. Proofs omitted due to space limitations may be included in a clearly marked appendix. Both an abstract and the full paper must be submitted by their respective submission deadlines. A special issue of the open access journal Logical Methods in Computer Science (http://www.lmcs-online.org), containing extended versions of selected papers, is also being planned. Submissions will be handled via EasyChair https://www.easychair.org/conferences/?conf=calco2013 -- BEST PAPER AND BEST PRESENTATION AWARDS -- For the first time, this edition of CALCO will feature two kinds of awards: a best paper award whose recipients will be selected by the PC before the conference and a best presentation award, elected by the participants. -- IMPORTANT DATES -- Abstract submission: February 22, 2013 Paper submission: March 1, 2013 Author notification: May 6, 2013 Final version due: June 3, 2013 -- PROGRAMME COMMITTEE -- Luca Aceto - Reykjavik University, Iceland Ji???? Ad??mek - TU Braunschweig, D Lars Birkedal - IT University of Copenhagen, DK Filippo Bonchi - CNRS, ENS-Lyon, F Corina Cirstea - University of Southhampton, UK Bob Coecke - University of Oxford, UK Andrea Corradini - University of Pisa, I Mai Gehrke - Universit?? Paris Diderot - Paris 7, F H. Peter Gumm - Philipps University Marburg, D Gopal Gupta - University of Texas at Dallas, USA Ichiro Hasuo - Tokyo University, Japan Reiko Heckel - University of Leicester, UK (cochair) Bart Jacobs - Radboud University Nijmegen, NL Ekaterina Komendantskaya - University of Dundee, Scotland, UK Barbara K??nig - University of Duisburg-Essen, D Jos?? Meseguer - University of Illinois, Urbana-Champaign, USA Marino Miculan - University of Udine, I Stefan Milius - Friedrich-Alexander Universit??t Erlangen-N??rnberg, D (cochair) Larry Moss - Indiana University, Bloomington, USA Till Mossakowski - DFKI Lab Bremen and University of Bremen, D Prakash Panangaden - McGill University, Montreal, Canada Dirk Pattinson - Imperial College London, UK Dusko Pavlovic - Royal Holloway, University of London, UK Daniela Petrisan - University of Leicester, UK John Power - University of Bath, UK Jan Rutten - CWI Amsterdam and Radboud University Nijmegen, NL Lutz Schr??der - Friedrich-Alexander Universit??t Erlangen-N??rnberg, D Monika Seisenberger - Swansea University, UK Sam Staton - University of Cambridge, UK Alexandra Silva - Radboud University Nijmegen and CWI Amsterdam, NL Pawel Sobocinski - University of Southampton, UK Yde Venema - University of Amsterdam, NL Uwe Wolter - University of Bergen, NO -- ORGANISING COMMITTEE -- Bartek Klin (University of Warsaw, Poland) Andrzej Tarlecki (University of Warsaw, Poland) -- LOCATION -- Warsaw, the capital of Poland, is a lively city with many historic monuments and sights, but also with a thriving business district. It is easily accessible via two airports: the main Chopin Airport, used by most international carriers, and the recently open Warsaw Modlin Airport (30 minutes away by rail), used by budget airlines. -- SATELLITE WORKSHOPS -- CALCO 2013 will be preceded by the CALCO Early Ideas Workshop, chaired by Monika Seisenberger (Swansea University). The workshop is dedicated to presentation of work in progress and original research proposals. PhD students and young researchers are particularly encouraged to contribute. Attendance at the workshop is open to all - it is anticipated that many CALCO conference participants will want to attend the CALCO Early Ideas workshop (and vice versa). A workshop dedicated to tools based on algebraic and/or coalgebraic principles, CALCO Tools, will be held alongside the main conference, chaired by Lutz Schr??der (Friedrich Alexander Universit??t Erlangen-N??rnberg). Papers of this workshop will be included in the CALCO proceedings. -- CALCO Early Ideas Overview -- The CALCO Early Ideas Workshop invites submissions on the same topics as the CALCO conference: reporting results of theoretical work on the mathematics of algebras and coalgebras, the way these results can support methods and techniques for software development, as well as experience with the transfer of the resulting technologies into industrial practice. The list of topics of particular interest is shown on the main CALCO 2013 page. CALCO Early Ideas presentations will be selected according to originality, significance, and general interest, on the basis of submitted 2-page short contributions. It can be work in progress, a summary of work submitted to a conference or workshop elsewhere, or work that in some other way might be interesting to the CALCO audience. A booklet with the accepted short contributions will be available at the workshop. Submissions will be handled via EasyChair https://www.easychair.org/conferences/?conf=calcoearlyideas2013 The use of LNCS style is strongly encouraged. After the workshop, authors will have the opportunity to submit a full 10-15 page paper on the same topic. The reviewing will be carried out by the CALCO Early Ideas PC, with the support of the CALCO PC. The volume of selected papers will be available online. Authors will retain copyright, and are also encouraged to disseminate the results by subsequent publication elsewhere. http://coalg.org/calco13/workshops.html#ei -- CALCO Early Ideas Dates -- 2-page short contribution submission: May 27, 2013 Notification for short contribution: June 24, 2013 Final short contribution due: July 15, 2013 CALCO Early Idead Workshop: September 2, 2013 10-15 page paper submission: October 15, 2013 Notification for paper: December 15, 2013 Final paper version due: January 15, 2014 -- CALCO Early Ideas Program Committee -- Bartek Klin, University of Warsaw, Poland John Power, University of Bath, UK Monika Seisenberger, Swansea University, UK (chair) -- CALCO-Tools Overview -- CALCO-Tools will take place on the same dates as the main CALCO conference, with no overlap between the technical programmes of the two events. Topics of interest include systems, prototypes, and tools developed specifically for the design, checking, execution, and verification of (co)algebraic specifications, but also tools targeting different application domains while making core or interesting use of (co)algebraic techniques. Tool submissions should not exceed 5 pages in LNCS format. The accepted tool papers will be included in the final proceedings of the conference. The tools should be made available on the web at the time of submission. Each submission will be evaluated by at least three reviewers; one or more of the reviewers will be asked to download and use the tool. At least one of the authors of each tool paper must attend the conference to demo the tool. http://coalg.org/calco13/workshops.html#tools -- CALCO-Tools Dates -- Paper submission: April 8, 2013 Author notification: May 6, 2013 Final version due: June 3, 2013 -- CALCO-Tools Programme Committee -- Einar Broch Johnsen, University of Oslo, Norway Mark Hills, CWI Amsterdam, The Netherlands Barbara K??nig, University of Duisburg-Essen, Germany Dorel Lucanu, Alexandru Ioan Cuza University, Romania Dominik Luecke, CWI Amsterdam, The Netherlands Till Mossakowski, DFKI, Germany Lutz Schr??der, Friedrich-Alexander Universit??t Erlangen-N??rnberg, Germany (chair) Alexandra Silva, Radboud University Nijmegen and CWI Amsterdam, The Netherlands -- FURTHER INFORMATION -- Queries related to submission, reviewing, and programme should be sent to the relevant conference or workshop chairs. Queries related to the organisation should be emailed to calco2013(a)mimuw.edu.pl . [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

ESSS 2013 -- submission deadline extended
by 山形賴之 26 Dec '12

26 Dec '12

ESSS 2013の論文投稿締め切りが延長されました。皆様の投稿をお待ちしております。 ================================================== 2nd International Workshop on Engineering Safety and Security Systems March 18, 2013, Luxembourg Co-located with ICST 2013 in Luxembourg, March 18-22, 2013 More information: http://www.comp.nus.edu.sg/~pat/esss2013/ =================================================== Important dates ----------------- * January 6th 2013: Submission deadline (extended) * February 11th 2013: Notification of acceptance/rejection (extended) * March 18th 2013: Workshop 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=esss2013. Submitted manuscripts should be in English and formatted in the style of the IEEE Computer Society Proceedings Format (see http://www.ieee.org/conferences_events/conferences/publishing/templates.html ). Papers should not exceed 6 pages for full papers and 2 pages for short papers, including figures, references, and appendices. All submissions should be in PDF format. Submissions not adhering to the specified format and length may be rejected immediately, without review. All workshop papers will be published in the IEEE Digital Library in the form of a post-proceedings. A pre-workshop version of the papers will be available on the workshop website prior. Publication of accepted articles requires the commitment of one of the authors to register for the workshop and present the paper. General chair ----------------- Sjouke Mauw, University of Luxembourg, Luxembourg Program chairs ----------------- Yang Liu, Nanyang Technological University, Singapore Jun Pang, University of Luxembourg, Luxembourg Program committee ----------------- Etienne Andre, Universite Paris 13, France Cyrille Artho, AIST, Japan Marieke Huisma, University of Twente, The Netherlands Weiqiang Kong, Kyushu University, Japan Keqin Li, SAP Research, France Yang Liu, Nanyang Technological University, Singapore Zhiming Liu, UNU/IIST Macao, China Sjouke Mauw, University of Luxembourg, Luxembourg Jun Pang, University of Luxembourg, Luxembourg Geguang Pu, East China Normal University, China Mohammad Torabi Dashti, ETH Zurich, Switzerland Anton Wijs, Eindhoven University of Technology Yoriyuki Yamagata, AIST, Japan -- 山形頼之独立行政法人産業技術総合研究所研究員 E-mail: yoriyuki.yamagata(a)aist.go.jp http://staff.aist.go.jp/yoriyuki.yamagata/

1 0

QIT28のご案内
by NISHIMURA Harumichi 26 Dec '12

26 Dec '12

logic-mlの皆様，来年５月に開催される第２８回量子情報技術研究会（QIT28）のご案内をQIT28世話人に代わって投稿させていただきます．よろしくお願いいたします．名古屋大学大学院情報科学研究科西村治道 http://www.math.cm.is.nagoya-u.ac.jp/~hnishimura/ --- 第28回量子情報技術研究会研究会の内容情報科学と量子力学を融合させた新しい分野、量子情報科学に関する研究会です。情報を担う物理系の量子力学的側面を積極的に活かした新しい情報処理原理の研究とそこから開かれる新しい学問体系の構築および新しい情報技術パラダイムの創生を目指して、情報科学、物理学、光エレクトロニクスを含む理学、工学、数理科学に携わる研究者間に自由な討論の場を提供し、この研究分野の発展を図ることを目的としています。期日 2013年5月27日（月）, 28日（火）会場北海道大学創成科学研究棟大会議室（〒001-0021 札幌市北区北21条西10丁目）発表募集内容発表募集分野（申込状況によっては査読可能性あり）：量子情報、量子計算、量子暗号など広く量子情報技術に関わる理論的研究、実験的研究、計算機科学的研究、数学的研究、およびその他関連分野定員 150名参加費事前振込み一般6,000円, 学生1,000円． (当日会場払いは一般7,000円, 学生2,000円) (懇親会は別途）研究会参加申込要領参加申込は下記Webにて受付けます． http://staff.aist.go.jp/s-kawabata/qit/ 講演（口頭，ポスター）申込，予稿集原稿PDF提出は電子情報通信学会のWebシステムを使用する予定．【講演申込締切】 2013年4月12日（金）；口頭講演 2013年4月26日（金）；ポスター講演【予稿集原稿提出】 2013年4月26日（金）【参加申込締切】 2013年5月2日（木）【問合先】富田章久（北海道大学大学院情報科学研究科）竹内繁樹（北海道大学電子科学研究所/大阪大学産業科学研究所）長谷川俊夫（三菱電機株式会社情報技術総合研究所） E-mail: qit28(a)ml.hokudai.ac.jp 主催量子情報技術時限研究専門委員会 (委員長枝松圭一(東北大)) 共催応用物理学会量子エレクトロニクス研究会物質・デバイス領域共同研究拠点北海道大学電子科学研究所

1 0

SAT 2013 Call For Papers
by Naoyuki Tamura 25 Dec '12

25 Dec '12

# 重複の場合はご容赦ください．神戸大学の田村と申します．メーリングリストをお借りして，来年7月にヘルシンキで開催されます SAT 2013 の Call For Papers をお送りします． -- 田村直之 (tamura(a)kobe-u.ac.jp) 神戸大学情報基盤センター〒657-8501 神戸市灘区六甲台町1-1 Phone: 078-803-5364, Fax: 078-803-5375 http://bach.istc.kobe-u.ac.jp/tamura-jp.html COPRIS+SCALA+CSP=SOLVER ------------------------------------------------------------------------- 1st CALL FOR PAPERS Sixteenth International Conference on THEORY AND APPLICATIONS OF SATISFIABILITY TESTING --- SAT 2013 --- Helsinki, Finland, July 8-12, 2013 http://sat2013.cs.helsinki.fi/ Abstract submission deadline: February 1, 2013 Paper submission deadline: February 8, 2013 ------------------------------------------------------------------------- The International Conference on Theory and Applications of Satisfiability Testing (SAT) is the primary annual meeting for researchers studying the theory and applications of the propositional satisfiability problem, broadly construed. Besides plain propositional satisfiability, it includes Boolean optimization (including MaxSAT and Pseudo-Boolean (PB) constraints), Quantified Boolean Formulas (QBF), Satisfiability Modulo Theories (SMT), and Constraint Programming (CP) for problems with clear connections to Boolean-level reasoning. Many hard combinatorial problems can be encoded as SAT instances, in the broad sense mentioned above, including problems in formal verification (hardware and software), artificial intelligence, and operations research. More recently, biology, cryptology, data mining, machine learning, and mathematics have been added to the growing list. The SAT conference aims to further advance the field by soliciting original theoretical and practical contributions in these areas with a clear connection to satisfiability. SAT 2013 takes place in Helsinki, the capital of Finland. Helsinki is a vibrant Scandinavian and international city with a lot to offer to visitors. SAT 2013 takes place during the main summer season, allowing one to experience the whitenights during which the sun almost never sets. IMPORTANT DATES =============== (Follow http://sat2013.cs.helsinki.fi/ for updates.) February 1, 2013: Abstract Submission February 8, 2013: Paper Submission March 18, 2013 (approx.): Response from Authors begins, lasts 72 hours April 3, 2013: Acceptance Notifications April 22, 2013: Final Camera-Ready Versions July 8, 2013: Workshops begin July 9-12, 2013: Main Conference SCOPE ===== SAT 2013 welcomes scientific contributions addressing different aspects of the satisfiability problem. interpreted in a broad sense. Domains include MaxSAT and Pseudo-Boolean (PB) constraints, Quantified Boolean Formulae (QBF), Satisfiability Modulo Theories (SMT), Constraint Satisfaction Problems (CSP). Topics include (but are not restricted to) Theoretical advances (including exact algorithms, proof complexity, and other complexity issues); Practical search algorithms; Knowledge compilation; Implementation-level details of SAT solving tools and SAT-based systems; Problem encodings and reformulations; Applications (including both novel applications domains and improvements to existing approaches); Case studies and reports on insightful findings based on rigorous experimentation. OUT OF SCOPE ============ Papers claiming to resolve a major long-standing open theoretical question in mathematics or computer science (such as those for which a Millennium Prize is offered, see http://www.claymath.org/millennium) are outside the scope of the conference because there is insufficient time in the schedule to referee such papers; instead, such papers should be submitted to an appropriate technical journal. SUBMISSIONS =========== Submissions to SAT 2013 are solicited in three paper categories, describing original contributions: REGULAR PAPERS (9 to 15 pages, excluding references) Regular papers should contain original research, with sufficient detail to assess the merits and relevance of the contribution. For papers reporting experimental results, authors are strongly encouraged to make their data and implementations available with their submission. Submissions reporting on case studies are also encouraged, and should describe details, weaknesses, and strengths in sufficient depth. SHORT PAPERS (up to 8 pages, excluding references) The same evaluation criteria apply to short papers as to regular papers. They will be reviewed to the same standards of quality as regular papers, but will naturally contain less quantity of new material. Short papers will have the same status as regular papers and be eligible for the same awards (to be announced later). TOOL PAPERS (up to 6 pages, excluding references) A tool paper should describe the implemented tool and its novel features. Here "tools" are interpreted in a broad sense, including descriptions of implementations of core SAT solving techniques (solvers, preprocessors, etc.), systems exploiting SAT solvers or their extensions for solving interesting problem domains, etc. A demonstration is expected to accompany a tool presentation. Papers describing tools that have already been presented previously are expected to contain significant and clear enhancements to the tool. The software for the tool should be made publicly available, for accepted tool papers, and should at least be available to reviewers for evaluation during the review period. Evaluation criteria will include (but not be limited to) accurate documentation, usability, and potential for furthering the state of the art. For the latter criterion, availability of source code will be a significant factor. This is an evolving category, and technical issues involving software availability should be discussed with the program chairs. Be sure to check the conference web page for updates on this category. Papers describing unpublished tool-related work, providing details on a system and the novel algorithms it implements, as well as an experimental evaluation of the system's performance, can also be submitted as regular papers. For all paper categories, the page limits stated above do not include references, but do include all other material intended to appear in the conference proceedings. An additional technical appendix may be included, but it must be clearly labeled as supplementary material and may or may not be examined during review based of the considerations of individual reviewers. The appendix may contain detailed proofs, examples, descriptions of publicly available software related to the submission, or other information that does not fit the page limit. However, the appendix will not be included in the conference proceedings. The main contributions should be made accessible within the page limits, without having to rely on the appendix. Submissions should not be under review elsewhere nor be submitted elsewhere while under review for SAT 2013, and should not consist of previously published material. Submissions must use the Springer LNCS style without modifications, and must be written in English. All papers submissions are done exclusively via the SAT 2013 EasyChair Conference Service at http://www.easychair.org/conferences/?conf=sat2013 . PROCEEDINGS =========== All accepted papers will be published in the proceedings of the conference, which will be published within the Springer LNCS series. PROGRAM CHAIRS ============== Matti Jarvisalo University of Helsinki, Finland Allen Van Gelder University of California at Santa Cruz, USA PROGRAM COMMITTEE ================= Gilles Audemard Fahiem Bacchus Armin Biere Maria Luisa Bonet Lucas Bordeaux Uwe Bubeck Samuel Buss Nadia Creignou Leonardo de Moura John Franco Enrico Giunchiglia Ziyad Hanna Marijn Heule Holger H. Hoos Jinbo Huang Tommi Junttila Matti Jarvisalo Arist Kojevnikov Daniel Kroening Oliver Kullmann Daniel Le Berre Florian Lonsing Ines Lynce Joao Marques-Silva Alexander Nadel Jakob Nordstrom Albert Oliveras Ramamohan Paturi Jussi Rintanen Olivier Roussel Ashish Sabharwal Lakhdar Sais Roberto Sebastiani Bart Selman Peter Stuckey Stefan Szeider Naoyuki Tamura Allen Van Gelder Toby Walsh ================================================================

1 0

[CFP] ATVA 2013 (Hanoi, 10/15-18, 2013)
by Ogawa Mizuhito 23 Dec '12

23 Dec '12

$B3'MM(B $B!v!vJ#?t<u$1<h$i$l$?J}$O$4MF<O$/$@$5$$!#!v!v(B $B>.@n!w(BJAIST $B$G$9!#(B2013$BG/(B10$B7n$K%O%N%$$G9T$o$l$^$99q:]2q5D(BATVA$B$N(B 1st call for paper $B$r$*Aw$j$$$?$7$^$9!#O@J8Ej9FDy$a@Z$j$O(B4$B7n(B6$BF|(B $B$H$^$@@h$G$9$,!"(B10$B7n$N%O%N%$$OAV$d$+$J;~4|$G$9!#$U$k$C$FEj9F$r(B $B$47W2h$/$@$5$$!#(B $B>.@n?p;K(B (JAIST) http://www.jaist.ac.jp/~mizuhito --------------------------------------------------------------- CALL FOR PAPERS ATVA 2013 11th International Symposium on Automated Technology for Verification and Analysis October 15 - 18, 2013, Hanoi, Vietnam ==================== The ATVA series of symposia is intended to promote research in theoretical and practical aspects of automated analysis, verification and synthesis in Asia by providing a forum for interaction between the regional and international research communities and industry in the field. The previous editions of the symposium were held in Taiwan, Beijing, Tokyo, Seoul, Macao, Singapore, Taipei and Thiruvananthapuram. Organised by the University of Engineering and Technology VNU Hanoi, ATVA 2013 will be held in the campus of Vietnam National University, Hanoi from October 15th to October 18th, 2013. SCOPE ATVA 2013 solicits high quality submissions in areas related to the theory and practice of automated analysis and verification of hardware and software systems. Topics of interest include, but are not limited to: - Formalisms for modeling hardware, software and embedded systems - Specification and verification of finite-state, infinite-state and parameterized system - 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 Theory papers should preferably be motivated by practical problems, and applications should be based on sound theory and should solve problems of practical interest. SUBMISSION Submissions are invited in two categories: regular research papers and tool papers. Submitted papers must present original and unpublished work, and must not be concurrently submitted to any other conference or journal. Regular paper submissions are restricted to 15 pages inSpringer's LNCS format, and tool paper submissions are restricted to 4 pages in the same format. Proofs and details omitted due to space constraints may be put in an appendix. Any such additional material will be read by reviewers/program committee members at their discretion. Authors are therefore urged to include details necessary for evaluation of the technical merit of their work within the prescribed page limits. Tool papers must include information about a URL from where the tool can be downloaded or accessed on-line for evaluation. The URL must also contain a set of examples, and a user's manual that describes usage of the tool through examples. In case the tool needs to be downloaded and installed, the URL must also contain a document clearly giving instructions for installation of the tool on Linux/Windows/MacOS. Authors must upload PDF files of their papers throughEasyChair at: https://www.easychair.org/conferences/?conf=atva2013 Accepted papers in both categories will be published by Springer as a LNCS volume. At least one author of each accepted paper must also register for the conference and present the paper. KEYNOTE TALKS AND TUTORIALS Keynote talks and tutorials will be given by: - Alessandro Cimatti (ITC-IRST, Italy) - Marta Kiwakowska (Oxford, UK) - Jerome Leroux (Bordeaux, France) IMPORTANT DATES - April 06, 2013: Paper submission deadline - Jun 1, 2013: Paper acceptance/rejection notification - July 5, 2013: Camera-ready copy deadline - October 15 - 18, 2013: Main conference & Tutorials ORGANIZING COMMITTEES General Chair - Nguyen Ngoc Binh (UET-VNU Hanoi, Vietnam) Steering Committee - E. Allen Emerson (U. of Texas-Austin, USA) - Teruo Higashino (Osaka Univeristy, Japan) - Insup Lee (U. of Pennsylvania, USA) - Doron A. Peled (Bar Ilan University, Israel) - Farn Wang (National Taiwan University, Taiwan) - Hsu-Chun Yen (National Taiwan University, Taiwan) Programme Committee Co-Chairs - Hung Dang-Van (UET-VNU Hanoi, Vietnam) - Mizuhito Ogawa (JAIST, Japan) Publicity Chair - Thao Dang (Verimag, France) Finance/Registration Chair - Thanh-Tho Quan (HCMUT, Vietnam) Local Chair - Hoang Truong (UET-VNU Hanoi, Vietnam) PROGRAMME COMMITTEE - Christel Baier (Germany) - Jonathan Billington (Australia) - Gianpiero Cabodi (Italy) - Supratik Chakraborty (India) - Wei-Ngan Chin (Singapore) - Thao Dang (France) - Hung Dang-Van (Vietnam, Co-chair) - Deepak D'Souza (India) - E.Allen Emerson (USA) - Martin Frnzle (Germany) - Masahiro Fujita (Japan) - Susanne Graf (France) - Teruo Higashino (Japan) - Alan Hu (Canada) - Franjo Ivancic (USA) - Jie-Hong Roland Jiang (Taiwan) - Joost-Pieter Katoen (Germany) - Zurab Khasidashvili (Israel) - Moonzoo Kim (Korea) - Gerwin Klein (Australia) - Fribourg Laurent (France) - Insup Lee (USA) - Xuandong Li (China) - Annabelle McIver (Australia) - Madhavan Mukund (India) - Pham Ngoc-Hung (Vietnam) - Thanh-Binh Nguyen (Vietnam) - Viet-Ha Nguyen (Vietnam) - Mizuhito Ogawa (Japan, Co-chair) - Thanh-Tho Quan (Vietnam) - Venkatesh R (India) - Ganesan Ramalingam (India) - Abhik Roychoudhury (Singapore) - Hiroyuki Seki (Japan) - Martin Steffen (Norway) - Sofiene Tahar (Canada) - Hoang Truong (Vietnam) - Mahesh Viswanathan (USA) - Farn Wang (Taiwan) - Bow-Yaw Wang (China) - Ji Wang (China) - Hsu-Chun Yen (Taiwan) - Wang Yi (Sweden) - Shoji Yuen (Japan) - Wenhui Zhang (China) CONFERENCE VENUE Historical Campus, Vietnam National University, 19 Le Thanh Tong street, Hoan Kiem district, Hanoi, Vietnam.

1 0

LICS 2013 Last Call for Papers
by Kazushige TERUI 20 Dec '12

20 Dec '12

LAST CALL FOR PAPERS Twenty-Eighth Annual ACM/IEEE Symposium on LOGIC IN COMPUTER SCIENCE (LICS 2013) June 25-28, 2013, New Orleans, USA http://lii.rwth-aachen.de/lics/lics13/ LICS 2013 will be hosted by Tulane University, in New Orleans, LA USA, from June 25th to 28th, 2013. LICS 2013 will be co-located with MFPS13 (23-25 June) and CSF13 (28-30 June). The LICS Symposium is an annual international forum on theoretical and practical topics in computer science that relate to logic, broadly construed. We invite submissions on topics that fit under that rubric. Suggested, but not exclusive, topics of interest include: automata theory, automated deduction, categorical models and logics, concurrency and distributed computation, constraint programming, constructive mathematics, database theory, decision procedures, description logics, domain theory, finite model theory, theory of automatic structures, formal aspects of program analysis, formal methods, foundations of computability, higher-order logic, lambda and combinatory calculi, linear logic, logic in artificial intelligence, logic programming, logical aspects of bioinformatics, logical aspects of computational complexity, logical aspects of quantum computation, logical frameworks, logics of programs, modal and temporal logics, model checking, probabilistic systems, process calculi, programming language semantics, proof theory, real-time systems, reasoning about security, rewriting, type systems and type theory, and verification. Important Dates: Authors are required to submit a paper title and a short abstract of about 100 words in advance of submitting the extended abstract of the paper. Titles & Short Abstracts Due : January 7, 2013 Extended Abstracts Due : January 14, 2013 Author Notification (approximate) : March 22, 2013 Final Versions Due for Proceedings: April 26, 2013 Deadlines are firm; late submissions will not be considered. All submissions will be electronic via http://easychair.org/conferences/?conf=lics2013. Submission Instructions: Every extended abstract must be submitted in the IEEE Proceedings 2-column 10pt format and may not be longer than 10 pages, including references. LaTeX style files will be available on the conference website. The extended abstract must be in English and provide sufficient detail to allow the program committee to assess the merits of the paper. It should begin with a succinct statement of the issues, a summary of the main results, and a brief explanation of their significance and relevance to the conference and to computer science, all phrased for the non-specialist. Technical development directed to the specialist should follow. References and comparisons with related work must be included. (If necessary, detailed proofs of technical results may be included in a clearly-labeled appendix, to be consulted at the discretion of program committee members.) Extended abstracts not conforming to the above requirements will be rejected without further consideration. Papers selection will be merit-based, with no a priori limit on the number of accepted papers. Results must be unpublished and not submitted for publication elsewhere, including the proceedings of other symposia or workshops. The program chair must be informed, in advance of submission, of any closely related work submitted or about to be submitted to a conference or journal. Authors of accepted papers are expected to sign copyright release forms. One author of each accepted paper is expected to present it at the conference. Short Presentations: A session of short presentations, intended for descriptions of student research, works in progress, and other brief communications, is planned. These abstracts will not be published. Dates and guidelines will be posted on the LICS website. Kleene Award for Best Student Paper: An award in honor of the late Stephen C. Kleene will be given for the best student paper(s), as judged by the program committee. Special Issues: Full versions of up to three accepted papers, to be selected by the program committee, will be invited for submission to the Journal of the ACM. Additional selected papers will be invited to a special issue of Logical Methods in Computer Science. Sponsorship: The symposium is sponsored by the IEEE Technical Committee on Mathematical Foundations of Computing and by ACM SIGACT, in cooperation with the Association for Symbolic Logic and the European Association for Theoretical Computer Science. Program Chair: Orna Kupferman, Hebrew University Program Committee: Parosh A. Abdulla, Uppsala University Amal Ahmed, Northeastern Universtiy Sergei Artemov, City University of New York Andrei Bulatov, Simon Fraser University Yijia Chen, Shanghai Jiao Tong University Veronique Cortier, CNRS, Loria Mariangiola Dezani-Ciancaglini, Univ. di Torino Thomas Ehrhard, CNRS, Universite Paris Diderot Javier Esparza, Technische Universitaet Muenchen Kousha Etessami, University of Edinburgh Maribel Fernandez, King’s College London Santiago Figueira, University of Buenos Aires Simon Gay, University of Glasgow Martin Grohe, Humboldt-Universitaet zu Berlin Martin Hofmann, LMU Munich Petr Jancar, Technical University Ostrava Barbara Jobstmann, CNRS, Verimag and Jasper DA Patricia Johann, University of Strathclyde Bakhadyr Khoussainov, The University of Auckland Antonina Kolokolova, University of Newfoundland Victor Marek, University of Kentucky Angelo Morzenti, Politecnico di Milano Lawrence Moss, Indiana University Madhavan Mukund, Chennai Math. Institute Anca Muscholl, Universite Bordeaux Mogens Nielsen, Aarhus University Catuscia Palamidessi, INRIA, Ecole Polytechnique Luc Segoufin, INRIA, ENS Cachan Natarajan Shankar, SRI International Alexandra Silva, Radboud University Nijmegen Balder ten Cate, UC Santa Cruz Kazushige Terui, Kyoto University Ron van der Meyden, Univ. of New South Wales Jeannette M. Wing, Carnegie Mellon University Nobuko Yoshida, Imperial College London Conference Chair: Mike Mislove, Tulane University Workshop Chair: Patricia Bouyer-Decitre, CNRS, ENS Cachan Publicity Chair: Andrzej Murawski, University of Leicester General Chair: Luke Ong, University of Oxford Organizing Committee: Martin Abadi, Luca Aceto, Rajeev Alur, Franz Baader, Paul Beame, Patricia Bouyer-Decitre, Adriana Compagnoni, Anuj Dawar, Nachum Dershowitz, Martin Escardo, Maribel Fernandez, Martin Grohe, Orna Grumberg, Jean-Pierre Jouannaud, Phokion Kolaitis, Orna Kupferman, Benoit Larose, Vlatko Lipovac, Michael Mislove, Georg Moser, Andrzej Murawski, Luke Ong (chair), Andre Scedrov, Philip Scott, David Shmoys, Matt Valeriote Advisory Board: Martin Abadi, Samson Abramsky, Rajeev Alur, Bob Constable, Thierry Coquand, Thomas Henzinger, Phokion Kolaitis, Dexter Kozen, Dale Miller, John Mitchell, Prakash Panangaden, Andrew Pitts, Gordon Plotkin, Moshe Vardi, Glynn Winskel ------------------------------------------ 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

First Announcement ― TACL 2013
by Hiroakira Ono 18 Dec '12

18 Dec '12

[Apologies for multiple copies] ====================================================== TOPOLOGY, ALGEBRA AND CATEGORIES IN LOGIC (TACL 2013) ====================================================== July 28 - August 1, 2013 Department of Mathematics, Vanderbilt University Nashville, Tennessee USA http://www.math.vanderbilt.edu/~tacl2013/ The Sixth International Conference on Topology, Algebra and Categories in conjunction with the 28th Annual Shanks Lecture Series Scope --------- 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 program of the conference TACL 2013 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 sixth conference in the series Topology, Algebra and Categories in Logic (TACL, formerly TANCL). Earlier installments of this conference have been organized in Tbilisi (2003), Barcelona (2005), Oxford (2007), Amsterdam (2009), Marseilles (2011). Confirmed invited speakers ------------------------------------- Vladimir Voevodsky, Institute for Advanced Studies, USA (Shanks Lecturer) Nick Bezhanishvili, Utrecht University, The Netherlands Leo Cabrer, University of Oxford, UK Silvio Ghilardi, University of Milan, Italy George Metcalfe, University of Bern, Switzerland Alex Simpson, University of Edinburgh, UK Featured topics --------------------- Contributed talks can deal with any topic dealing with 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 Submissions ----------------- Contributed presentations will be of two types: o 20 minutes long presentations in parallel sessions and o featured, 30 minutes long, plenary presentations. The submission of an abstract will be required to be selected for a contributed presentation of either kind. While preference will be given to new work, results that have already been published or presented elsewhere will also be considered. More information on the submission procedure, as well as a link to the EasyChair system, can be found at the conference web site. Important dates ---------------------- April 1, 2013: Abstract submission deadline May 1, 2013: Notification to authors July 28-August 1, 2013: Conference Program Committee --------------------------- Steve Awodey, Carnegie Mellon University Guram Bezhanishvili, New Mexico State University David Gabelaia, Razmadze Mathematical Institute, Tbilisi Nick Galatos (co-chair), University of Denver Mai Gehrke, LIAFA, University of Paris Diderot Rob Goldblatt, Victoria University, Wellington John Harding, New Mexico State University Ramon Jansana, University of Barcelona Peter Jipsen, Chapman University Achim Jung, University of Birmingham Alexander Kurz (co-chair), University of Leicester Vincenzo Marra, University of Milan Hiroakira Ono, Japan Advanced Institute of Science and Technology Alessandra Palmigiano, University of Amsterdam Hilary Priestley, St Anne's College, Oxford James Raftery, University of KwaZulu-Natal, Durban Thomas Streicher, Technical University of Darmstadt Kazushige Terui, Kyoto University Constantine Tsinakis, Vanderbilt University Yde Venema, University of Amsterdam Michael Zakharyaschev, Birkbeck College, University of London Organizing Committee ------------------------------- Chris Conidis, Vanderbilt University Lianzhen Liu, Jiangnan University, China Warren McGovern, Florida Atlantic University Francesco Paoli, University of Cagliari Rebecca Steiner, Vanderbilt University Constantine Tsinakis (chair), Vanderbilt University William Young, Vanderbilt University Expression of interest ------------------------------ We would greatly appreciate your taking two minutes to express your level of interest in the conference by filling out a simple form on the conference web site under "Express Interest". This will help the Organizing Committee with their planning. You can also opt-out from receiving future announcements by clicking the link at the bottom of this email. More Information ----------------------- TACL 2013 web site: http://www.math.vanderbilt.edu/~tacl2013/ Use this site for local information, including hotel accommodations, for travel information and registration, and for submitting a request for financial support. Any queries for the Program Committee (such as usage of the EasyChair conference system, abstract submission guidelines, conference program, etc.) should be sent to tacl2013(a)gmail.com. Queries for the local Organizing Committee (registration, hotel accommodations, financial support and reimbursements, technology infrastructure, etc.) should be sent to tacl2013oc(a)vanderbilt.edu.

1 0

First Announcement — TACL 2013 TACL 2013
by Kent, Curt 17 Dec '12

17 Dec '12

[Apologies for multiple copies] ====================================================== TOPOLOGY, ALGEBRA AND CATEGORIES IN LOGIC (TACL 2013) ====================================================== July 28 - August 1, 2013 Department of Mathematics, Vanderbilt University Nashville, Tennessee USA http://www.math.vanderbilt.edu/~tacl2013/ The Sixth International Conference on Topology, Algebra and Categories in conjunction with the 28th Annual Shanks Lecture Series Scope --------- 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 program of the conference TACL 2013 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 sixth conference in the series Topology, Algebra and Categories in Logic (TACL, formerly TANCL). Earlier installments of this conference have been organized in Tbilisi (2003), Barcelona (2005), Oxford (2007), Amsterdam (2009), Marseilles (2011). Confirmed invited speakers ------------------------------------- Vladimir Voevodsky, Institute for Advanced Studies, USA (Shanks Lecturer) Nick Bezhanishvili, Utrecht University, The Netherlands Leo Cabrer, University of Oxford, UK Silvio Ghilardi, University of Milan, Italy George Metcalfe, University of Bern, Switzerland Alex Simpson, University of Edinburgh, UK Featured topics --------------------- Contributed talks can deal with any topic dealing with 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 Submissions ----------------- Contributed presentations will be of two types: o 20 minutes long presentations in parallel sessions and o featured, 30 minutes long, plenary presentations. The submission of an abstract will be required to be selected for a contributed presentation of either kind. While preference will be given to new work, results that have already been published or presented elsewhere will also be considered. More information on the submission procedure, as well as a link to the EasyChair system, can be found at the conference web site. Important dates ---------------------- April 1, 2013: Abstract submission deadline May 1, 2013: Notification to authors July 28-August 1, 2013: Conference Program Committee --------------------------- Steve Awodey, Carnegie Mellon University Guram Bezhanishvili, New Mexico State University David Gabelaia, Razmadze Mathematical Institute, Tbilisi Nick Galatos (co-chair), University of Denver Mai Gehrke, LIAFA, University of Paris Diderot Rob Goldblatt, Victoria University, Wellington John Harding, New Mexico State University Ramon Jansana, University of Barcelona Peter Jipsen, Chapman University Achim Jung, University of Birmingham Alexander Kurz (co-chair), University of Leicester Vincenzo Marra, University of Milan Hiroakira Ono, Japan Advanced Institute of Science and Technology Alessandra Palmigiano, University of Amsterdam Hilary Priestley, St Anne's College, Oxford James Raftery, University of KwaZulu-Natal, Durban Thomas Streicher, Technical University of Darmstadt Kazushige Terui, Kyoto University Constantine Tsinakis, Vanderbilt University Yde Venema, University of Amsterdam Michael Zakharyaschev, Birkbeck College, University of London Organizing Committee ------------------------------- Chris Conidis, Vanderbilt University Lianzhen Liu, Jiangnan University, China Warren McGovern, Florida Atlantic University Francesco Paoli, University of Cagliari Rebecca Steiner, Vanderbilt University Constantine Tsinakis (chair), Vanderbilt University William Young, Vanderbilt University Expression of interest ------------------------------ We would greatly appreciate your taking two minutes to express your level of interest in the conference by filling out a simple form on the conference web site under "Express Interest". This will help the Organizing Committee with their planning. You can also opt-out from receiving future announcements by clicking the link at the bottom of this email. More Information ----------------------- TACL 2013 web site: http://www.math.vanderbilt.edu/~tacl2013/ Use this site for local information, including hotel accommodations, for travel information and registration, and for submitting a request for financial support. Any queries for the Program Committee (such as usage of the EasyChair conference system, abstract submission guidelines, conference program, etc.) should be sent to tacl2013(a)gmail.com<mailto:tacl2013@gmail.com>. Queries for the local Organizing Committee (registration, hotel accommodations, financial support and reimbursements, technology infrastructure, etc.) should be sent to tacl2013oc(a)vanderbilt.edu<mailto:tacl2013oc@vanderbilt.edu>. To unsubscribe from this list, please send an email to LISTSERV(a)LIST.VANDERBILT.EDU<mailto:LISTSERV@LIST.VANDERBILT.EDU> with "SIGNOFF TACL2013" as the body of message.

1 0

ESSLLI Student Seminar 2013 - First Call for Papers
by Mauricio Hernandes 17 Dec '12

17 Dec '12

mlの皆様, As asked by the Chair of the Student Seminar I am forwarding the information below. Regards Mauricio Hernandes First Call for Papers ESSLLI 2013 STUDENT SESSION Held during The 25th European Summer School in Logic, Language and Information Düsseldorf, Germany, August 5-16, 2013 Deadline for submissions: April 1st, 2013 https://www.easychair.org/conferences/?conf=essllistus2013 *ABOUT*: The Student Session of the 25th European Summer School in Logic, Language, and Information (ESSLLI) will take place in *Düsseldorf, Germany on August 5-16, 2013*. We invite submissions of original, unpublished work from students in any area at the intersection of Logic & Language, Language & Computation, or Logic & Computation. Submissions will be reviewed by several experts in the field, and accepted papers will be presented orally or as posters and will appear in the student session proceedings in Springer. This is an excellent opportunity to receive valuable feedback from expert readers and to present your work to a diverse audience. *A SEPARATE POSTER SESSION*: Note that this year there are two separate kinds of submissions, one for the oral presentations and one for the posters. This means that papers can be directly submitted as posters. Reviewing and ranking will be done separately. We particularly encourage submissions for posters. More detailed guidelines regarding submission can be found on the Student Session website: http://stus2013.loriweb.org/, (links to previous years' proceedings are also available there). Please direct inquiries about submission procedures or other matters relating to the Student Session to margotcolinet(a)gmail.com For general inquiries about ESSLLI 2013, please consult the main ESSLLI 2013 page, http://esslli2013.de/. Kind regards, *The ESSLLI 2013 Student Session Organization Committee*, Chair: Margot Colinet (Université Paris Diderot-Paris 7) LOCO (LOgic and Computation) co-chairs: Ronald de Haan (Technische Universität Wien) Michał Zawidzki (Uniwersytet Łódzki) LOLA (LOgic and LAnguage) co-chairs: Agata Renans (Universität Potsdam) Barbara Tomaszewicz (University of Southern California) LACO (LAnguage and Computation) co-chairs: Pierre Bourreau (Heinrich-Heine-Universität Düsseldorf) Julia Zinova (Heinrich-Heine-Universität Düsseldorf)

1 0

*** 場所と時間を変更しました *** Talk by Keiko Nakata (Tallinn U of Tech), Tue 18 December 2012
by Ichiro Hasuo 17 Dec '12

17 Dec '12

みなさま，念のため，明日の中田景子さんのご講演について場所と時間の変更のご案内を再度お送りします．どうかよろしくお願いいたします！蓮尾一郎 ---------- Forwarded message ---------- From: Ichiro Hasuo <ichiro(a)is.s.u-tokyo.ac.jp> Date: Thu, Dec 13, 2012 at 9:06 AM Subject: *** Time & Venue Changed *** Talk by Keiko Nakata (Tallinn U of Tech), Tue 18 December 2012 To: logic-ml <logic-ml(a)sato.kuis.kyoto-u.ac.jp>, sonoteno <sonoteno(a)m.aist.go.jp>, jssst-ppl(a)kb.ecei.tohoku.ac.jp みなさま，こんにちは！東京大学の蓮尾と申します．先日お知らせした，タリン工科大学の中田景子さんによるご講演ですが，＊＊時間と場所を変更＊＊させてください．（日程は同じです）急なお知らせで申し訳ありません．また，会場の国立情報学研究所では，中田さんのご講演の前（13:30-15:30）に ToPS セミナーが開催されます．そちらにも是非どうぞ！ http://takeichi.ipl-lab.org/~tops/upcoming_seminar.html 蓮尾一郎 http://www-mmm.is.s.u-tokyo.ac.jp/ ============================================= Tue 18 December 2012, 16:00-17:30 Keiko Nakata (Tallinn University of Technology), 2 Talks 国立情報学研究所 12階 1208号室 Rm. 1208, 12F, National Institute of Informatics Access: http://www.nii.ac.jp/en/about/access *** 場所・時間が変わりました *** *** The time and venue have been changed *** 中田さんのご講演の前（13:30-15:30）に，同じ場所で ToPS セミナーが開催されます．そちらにも是非どうぞ！http://takeichi.ipl-lab.org/~tops/upcoming_seminar.h… Prior to Dr. Nakata’s talk there will be a “ToPS seminar” at the same location. The talks will be of similar research interests. http://takeichi.ipl-lab.org/~tops/upcoming_seminar.html Talk 1: Proving open induction using delimited control operators Open Induction (OI) is a principle classically equivalent to Dependent Choice, which is, unlike the later, closed under double-negation translation and A-translation. In the context of Constructive Reverse Mathematics, Wim Veldman has shown that, in presence of Markov's Principle, OI on Cantor space is equivalent to Double-negation Shift (DNS). With Danko Ilik, we have reworked Veldman's proof to give a constructive proof of OI, where DNS is interpreted using delimited control operators. Joint work with Danko Ilik. Talk 2: Walking through infinite trees with mixed induction and coinduction: A Proof Pearl with the Fan Theorem and Bar Induction. We study temporal properties over infinite binary red-blue trees in the setting of constructive type theory. We consider several familiar path-based properties, typical to linear-time and branching-time temporal logics like LTL and CTL*, and the corresponding tree-based properties, in the spirit of the modal mu-calculus. We conduct a systematic study of the relationships of the path-based and tree-based versions of ``eventually always blueness '' and mixed inductive-coinductive ``almost always blueness'' and arrive at a diagram relating these properties to each other in terms of implications that hold either unconditionally or under specific assumptions (Weak Continuity for Numbers, the Fan Theorem, Lesser Principle of Omniscience, Bar Induction). Joint work with Marc Bezem and Tarmo Uustalu.

1 0

Logic Zoo Workshop 2013 (Jan. 31, Tokyo)
by Yoichi Hirai 13 Dec '12

13 Dec '12

みなさま東京大学萩谷研の平井洋一より、Logic Zooワークショップのご案内です。 2013年1月31日(木)東京開催です(前日30日には平井洋一の博士論文公聴会)。講演・前日夕食の申込は 2013年1月15日(火) 締切です。詳細及び申込 http://logiczoo13.pira.jp 論理をみつける話から論理を調べる話、論理を使う話までご講演、ご参加をお待ちしております。平井洋一 Logic Zoo Workshop 2013 (Jan. 31, Tokyo) ======================================== A workshop on living, playing or working logics. Topics include: - substructural and more exotic logics - type systems - programming languages - mathematics on non-classical logics - software verification - logics for social, economical, legal or linguistic analysis. Organizer: Yoichi Hirai yh(a)lyon.is.s.u-tokyo.ac.jp Schedule and Location --------------------- - 2013 Jan. 31 (Thu), 10:00--17:00 - Room 236, through Science Bldg. 7, 理学部7号館2階より化東236室 Hongo campus, the Univ. of Tokyo 東京大学本郷キャンパス - with four blackboards 黒板4枚あり Registration ------------ Please register for your talk slot and/or dinner by Jan. 15, 2013. A talk will be 30-minute long (tentative estimation). Fill this form and send it to yh(a)lyon.is.s.u-tokyo.ac.jp ================================== Logic Zoo (Jan. 31) Registration name: affiliation: eve-dinner on 30th: yes / no / not decided giving a talk: yes / not decided title: TBD or a title ================================== Some Other Events ----------------- 2013-01-30 (Wed): Defense and Dinner 12:00--14:00 Yoichi Hirai's defense (first half is public): Hyper-Lambda Calculi Room 102, Science Bldg. 7, Hongo campus, the Univ. of Tokyo 19:00--21:00 Dinner: Logic Zoo Eve nearby restaurant 2013-01-31 (Thu): Workshop 10:00--17:00 Logic Zoo Workshop Room 236, through Science Bldg. 7, Hongo campus, the Univ. of Tokyo

1 0

*** Time & Venue Changed *** Talk by Keiko Nakata (Tallinn U of Tech), Tue 18 December 2012
by Ichiro Hasuo 13 Dec '12

13 Dec '12

みなさま，こんにちは！東京大学の蓮尾と申します．先日お知らせした，タリン工科大学の中田景子さんによるご講演ですが，＊＊時間と場所を変更＊＊させてください．（日程は同じです）急なお知らせで申し訳ありません．また，会場の国立情報学研究所では，中田さんのご講演の前（13:30-15:30）に ToPS セミナーが開催されます．そちらにも是非どうぞ！ http://takeichi.ipl-lab.org/~tops/upcoming_seminar.html 蓮尾一郎 http://www-mmm.is.s.u-tokyo.ac.jp/ ============================================= Tue 18 December 2012, 16:00-17:30 Keiko Nakata (Tallinn University of Technology), 2 Talks 国立情報学研究所 12階 1208号室 Rm. 1208, 12F, National Institute of Informatics Access: http://www.nii.ac.jp/en/about/access *** 場所・時間が変わりました *** *** The time and venue have been changed *** 中田さんのご講演の前（13:30-15:30）に，同じ場所で ToPS セミナーが開催されます．そちらにも是非どうぞ！http://takeichi.ipl-lab.org/~tops/upcoming_seminar.h… Prior to Dr. Nakata’s talk there will be a “ToPS seminar” at the same location. The talks will be of similar research interests. http://takeichi.ipl-lab.org/~tops/upcoming_seminar.html Talk 1: Proving open induction using delimited control operators Open Induction (OI) is a principle classically equivalent to Dependent Choice, which is, unlike the later, closed under double-negation translation and A-translation. In the context of Constructive Reverse Mathematics, Wim Veldman has shown that, in presence of Markov's Principle, OI on Cantor space is equivalent to Double-negation Shift (DNS). With Danko Ilik, we have reworked Veldman's proof to give a constructive proof of OI, where DNS is interpreted using delimited control operators. Joint work with Danko Ilik. Talk 2: Walking through infinite trees with mixed induction and coinduction: A Proof Pearl with the Fan Theorem and Bar Induction. We study temporal properties over infinite binary red-blue trees in the setting of constructive type theory. We consider several familiar path-based properties, typical to linear-time and branching-time temporal logics like LTL and CTL*, and the corresponding tree-based properties, in the spirit of the modal mu-calculus. We conduct a systematic study of the relationships of the path-based and tree-based versions of ``eventually always blueness '' and mixed inductive-coinductive ``almost always blueness'' and arrive at a diagram relating these properties to each other in terms of implications that hold either unconditionally or under specific assumptions (Weak Continuity for Numbers, the Fan Theorem, Lesser Principle of Omniscience, Bar Induction). Joint work with Marc Bezem and Tarmo Uustalu.

1 0

講演のお知らせ
by minami＠kurt.cla.kobe-u.ac.jp 12 Dec '12

12 Dec '12

皆様，重複してお受け取りの際はご容赦ください。以下の要領で名古屋数学基礎論/集合論セミナーを開催します．興味のある方は是非参加を検討ください．日時：12月14日（金）15：30〜場所：場所：名古屋大学情報科学（研究科）棟1階105 講演者：嘉田勝（大阪府立大学）講演タイトル：強制拡大で位相空間の性質は保存されるか位相空間論の未解決問題に集合論的手法でアプローチするうえで、「強制拡大で位相空間の性質が保存されるか否か」が重要な鍵となることがある。ここで、位相空間の性質の保存とは、基底モデルに属する位相空間に対して、その強制拡大における対応物として「同一の点集合と開基で定まる位相空間」を考えるときに、基底モデルでみたされる空間の性質が強制拡大でもみたされることを意味するものとする。本講演では、半順序がみたす性質と、その半順序による強制拡大で保存される位相空間の性質との関係について、いくつかの結果を紹介する。 ================================================= アクセス：地下鉄名城線名古屋大学駅から徒歩5〜10分． http://www.nagoya-u.ac.jp/global-info/access-map/higashiyama/index.html http://www.is.nagoya-u.ac.jp/intro/contact.html この講演に関する情報は以下のHPでもご覧になれます． http://researchmap.jp/cardinal_invariants/research-blog/

1 0

Kobe Colloquium on Logic, Statistics and Informatics, Dec. 10 (David Aspero)
by Joerg Brendle 06 Dec '12

06 Dec '12

Kobe Colloquium on Logic, Statistics and Informatics 以下の要領でコロキウムを開催します。日時：2012年12月10日（月）13:20-14:50 場所：神戸大学自然科学総合研究棟3号館4階421室（プレゼンテーション室）講演者：David Aspero (Technische Universitaet Wien, Austria) ======================================================================== 題目：Some set theory with restricted choice アブストラクト：I am planning to present the proofs of three theorems involving set theory without the Axiom of Choice or with just restricted forms of AC. One is an observation of mine concerning very large cardinals in a ZF context, another one is a result from a paper by P. Larson and Shelah, and another one a result of Shelah from [Sh835]. ======================================================================== 交通：阪急六甲駅またはJR六甲道駅から神戸市バス36系統「鶴甲団地」行きに乗車，「神大本部工学部前」停留所下車，徒歩すぐ． http://www.kobe-u.ac.jp/info/access/rokko/rokkodai-dai2.htm 連絡先：ブレンドレヨーグ brendle(a)kurt.scitec.kobe-u.ac.jp

1 0

Post-doc position available at AIST Kansai: Test generation/optimization
by Takashi KITAMURA 05 Dec '12

05 Dec '12

みなさま、こんにちは。産総研の北村崇師と申します。本研究所の Cyrille Artho に代わり、ポスドク募集のご案内させて頂きます。応募のご検討、及び、関係各位へのご周知をいただけますと幸いです。 ==================================================== Post-doc position available at AIST Kansai: Test generation/optimization ==================================================== Research related to: • Test generation using model-based testing/constraint solving. • Test case minimization using heuristics like delta debugging. Start: 2013 (ideally April, but can be adjusted). Duration: 1 year (extensible dep. on evaluation and restrictions below). • Location: AIST Amagasaki, Japan (20 minutes from Osaka); Research Institute for Secure Systems, System Life-cycle Group. http://www.risec.aist.go.jp/ • Requirements: – Ph.D.at the time when the contract starts; degree must have been awarded less than 7 years ago. – Strong know-how in software analysis and algorithms. – Experience with Java or Scala, and C. – Good written and spoken communication in English. • If interested, please submit your résumé with your publications and a list software projects in which you have participated. • Contact:c.artho@aist.go.jp -- Takashi KITAMURA 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)

1 0

55th Tokyo Programming Seminar (Dec 18)
by Kazuyuki ASADA 05 Dec '12

05 Dec '12

[Apologies for multiple copies] Dear all, I am pleased to announce the 55th Tokyo Programming Seminar, which will be held at NII on December 18th (Tue). Oleg Kiselyov Non-deterministic choice in a conventional programming language: Enough for logic programming? Hugo Pacheco Bidirectional Data Transformation by Calculation A detailed program is attached below. I'm looking forward to meeting you at the seminar. Best regards, Kazuyuki Asada ---- The 55th ToPS http://takeichi.ipl-lab.org/~tops/upcoming_seminar.html Time: December 18th (Tue) 2012, 13:30--15:30 Place: Rm. 1208, 12F, National Institute of Informatics Speaker: 1. Oleg Kiselyov Non-deterministic choice in a conventional programming language: Enough for logic programming? Abstract: Logic programming is a fascinating approach, especially for AI and natural language processing. It is greatly appealing to declaratively state the properties of the problem and let the system find the solution. Most intriguing is the ability to run programs `forwards' and `backwards'. However, the built-in search methods of logic programming systems don't fit all problems and hardly if at all customizable. Mainly, quite many computations and models are mostly deterministic. Implementing them in a logic programming language is significantly inefficient and requires extensive use of problematic features such as cut. Another problem is interfacing logic programs with mainstream language libraries: if mode analysis is not available (as is often the case), one has to live with run-time instantiatedness errors. An alternative to logic programming, where non-determinism is default, is a deterministic programming system (such as Scheme, OCaml, Scala or Haskell -- or even C) with (probabilistic) non-determinism as an option. Is this a good alternative? We explore this question. We will use Hansei -- a probabilistic programming system implemented as a library in OCaml -- to solve a number of classic logic programming problems, from zebra to scheduling, to parser combinators, to reversible type checking. http://okmij.org/ftp/kakuritu/logic-programming.html 2. Hugo Pacheco Bidirectional Data Transformation by Calculation Abstract: The advent of bidirectional programming, in recent years, has led to the development of a vast number of approaches from various computer science disciplines. These are often based on domain-specific languages in which a program can be read both as a forward and a backward transformation that satisfy some desirable consistency properties. Despite the high demand and recognized potential of intrinsically bidirectional languages, they have still not matured to the point of mainstream adoption. We contemplate some usually disregarded features of bidirectional transformation languages that are vital for deployment at a larger scale. The first concerns efficiency. Most of these languages provide a rich set of primitive combinators that can be composed to build more sophisticated transformations. Although convenient, such compositional languages are plagued by inefficiency and their optimization is mandatory for a serious application. The second relates to configurability. As update translation is inherently ambiguous, users shall be allowed to control the choice of a suitable strategy. The third regards genericity. Writing a bidirectional transformation typically implies describing the concrete steps that convert values in a source schema to values a target schema, making it impractical to express very complex transformations, and practical tools shall support concise and generic coding patterns.

1 0

RTA 2013: Second Call for Papers
by Nao Hirokawa 03 Dec '12

03 Dec '12

皆様 RTA 2013 の論文募集をご案内致します。今回の RTA はオランダ Eindhoven で行われ、TLCA 2013 との共催となっています。ぜひ投稿をご検討下さい。廣川　直 (JAIST) ************************************************************************* RTA 2013: SECOND CALL FOR PAPERS 24th International Conference on Rewriting Techniques and Applications June 24 - 26, 2013 Eindhoven, The Netherlands collocated with TLCA 2013 as part of RDP 2013 http://rta2013.few.vu.nl/ ************************************************************************* abstract submission February 1 2013 paper submission February 5 2013 rebuttal period March 18-21 2013 notification April 4 2013 final version April 26 2013 ************************************************************************* The 24th International Conference on Rewriting Techniques and Applications (RTA 2013) is organized as part of the Federated Conference on Rewriting, Deduction, and Programming (RDP 2013), together with the 11th International Conference on Typed Lambda Calculi and Applications (TLCA 2013), and several workshops. RDP 2013 will be held at the Eindhoven University of Technology in the Netherlands. *** INVITED SPEAKERS (NEW) *** - Simon Peyton-Jones (Microsoft Research, UK) joint invited speaker for TLCA+RTA 2013 - Jarkko Kari (University of Turku, Finland) invited speaker for RTA 2013 - Mitsu Okada (Keio University, Japan) invited speaker for RTA 2013 *** TOPICS OF INTEREST *** RTA is the major forum for the presentation of research on all aspects of rewriting. Typical areas of interest include (but are not limited to): Applications: case studies; analysis of cryptographic protocols; rule-based (functional and logic) programming; symbolic and algebraic computation; SMT solving; theorem proving; system synthesis and verification; proof checking; reasoning about programming languages and logics; program transformation; XML queries and transformations; systems biology; homotopy theory; implicit computational complexity; Foundations: equational logic; universal algebra; rewriting logic; rewriting models of programs; matching and unification; narrowing; completion techniques; strategies; rewriting calculi; constraint solving; tree automata; termination; complexity; modularity; Frameworks: string, term, and graph rewriting; lambda-calculus and higher-order rewriting; constrained rewriting/deduction; categorical and infinitary rewriting; stochastic rewriting; net rewriting; binding techniques; Petri nets; higher-dimensional rewriting; Implementation: implementation techniques; parallel execution; rewrite and completion tools; certification of rewriting properties; abstract machines; explicit substitutions; automated (non)termination and confluence provers; automated complexity analysis. *** PUBLICATION *** The proceedings will be published by LIPIcs (Leibniz International Proceedings in Informatics). LIPIcs is open access, meaning that publications will be available online and free of charge, and authors keep the copyright for their papers. LIPIcs publications are indexed in DBLP. For more information about LIPIcs please consult: <http://www.dagstuhl.de/en/publications/lipics> *** SUBMISSION GUIDELINES *** Submissions must be - original and not submitted for publication elsewhere, - written in English, - a research paper, or a problem set, or a system description, - in pdf prepared with pdflatex using the LIPIcs stylefile: <http://drops.dagstuhl.de/styles/lipics/lipics-authors.tgz>, - at most 10 pages for system description, at most 15 pages for the other two types of submissions - submitted electronically through the EasyChair system at: <https://www.easychair.org/conferences/?conf=rta2013>. The page limit and the deadline for submission are strict. Additional material for instance proof details, may be given in an appendix which is not subject to the page limit. However, submissions must be self-contained within the respective page limit; reading the appendix should not be necessary to assess the merits of a submission. *** PROGRAMME COMMITTEE CHAIR *** Femke van Raamsdonk (VU University Amsterdam, The Netherlands) *** PROGRAMME COMMITTEE *** Eduardo Bonelli National University of Quilmes, Argentina Byron Cook Microsoft Research Cambridge, UK Stephanie Delaune ENS Cachan, France Gilles Dowek Inria Paris-Rocquencourt, France Maribel Fernandez King's College London, UK Nao Hirokawa JAIST Ishikawa, Japan Delia Kesner University Paris-Diderot, France Helene Kirchner Inria Paris-Rocquencourt, France Barbara Koenig University Duisburg Essen, Germany Temur Kutsia Johannes Kepler University Linz, Austria Aart Middeldorp University of Innsbruck, Austria Vincent van Oostrom Utrecht University, The Netherlands Femke van Raamsdonk VU University Amsterdam, The Netherlands Kristoffer Rose IBM Research New York, USA Manfred Schmidt-Schauss Goethe University Frankfurt, Germany Peter Selinger Dalhousie University, Canada Paula Severi University of Leicester, UK Aaron Stump The University of Iowa, USA Tarmo Uustalu Institute of Cybernetics Tallinn, Estonia Roel de Vrijer VU University Amsterdam, The Netherlands Johannes Waldmann HTWK Leipzig, Germany Hans Zantema Eindhoven University of Technology, The Netherlands *** CONFERENCE CHAIR *** Hans Zantema (Eindhoven University of Technology, The Netherlands) *** STEERING COMMITTEE *** Mauricio Ayala-Rincon Brasilia University, Brasilia Frederic Blanqui INRIA Tsinghua University Beijing, China Salvador Lucas Technical University of Valencia, Spain Georg Moser (chair) University of Innsbruck, Austria Masahiko Sakai Nagoya University, Japan Sophie Tison University of Lille, France *** FURTHER INFORMATION *** Questions related to submission, reviewing, and programme should be sent to the programme committee chair Femke van Raamsdonk, email femke at few.vu.nl.

1 0

Talk by Keiko Nakata (Tallinn University of Technology), Tue 18 December 2012
by Ichiro Hasuo 02 Dec '12

02 Dec '12

みなさま，東京大学の蓮尾と申します．来る12月18日，タリン工科大学の中田景子さんをお迎えしてご講演いただきます．（2題，連続講演です）詳細は以下です．ご興味のある方はぜひお越しください！蓮尾一郎 http://www-mmm.is.s.u-tokyo.ac.jp/ -------------------------------------------------------------------------------------------------------------- Tue 18 December 2012, 16:40-18:10 Keiko Nakata (Tallinn University of Technology), 2 titles 理学部7号館1階 102教室 Room 102, School of Science Bldg. No. 7 Title Proving open induction using delimited control operators Abstract Open Induction (OI) is a principle classically equivalent to Dependent Choice, which is, unlike the later, closed under double-negation translation and A-translation. In the context of Constructive Reverse Mathematics, Wim Veldman has shown that, in presence of Markov's Principle, OI on Cantor space is equivalent to Double-negation Shift (DNS). With Danko Ilik, we have reworked Veldman's proof to give a constructive proof of OI, where DNS is interpreted using delimited control operators. Joint work with Danko Ilik. --- Title Walking through infinite trees with mixed induction and coinduction: A Proof Pearl with the Fan Theorem and Bar Induction. Abstract We study temporal properties over infinite binary red-blue trees in the setting of constructive type theory. We consider several familiar path-based properties, typical to linear-time and branching-time temporal logics like LTL and CTL*, and the corresponding tree-based properties, in the spirit of the modal mu-calculus. We conduct a systematic study of the relationships of the path-based and tree-based versions of ``eventually always blueness '' and mixed inductive-coinductive ``almost always blueness'' and arrive at a diagram relating these properties to each other in terms of implications that hold either unconditionally or under specific assumptions (Weak Continuity for Numbers, the Fan Theorem, Lesser Principle of Omniscience, Bar Induction). Joint work with Marc Bezem and Tarmo Uustalu.

1 0

PPL2013論文募集
by Shinya Katsumata 30 Nov '12

30 Nov '12

（重複の場合はご容赦ください．）東京工業大学の権藤と京都大学の勝股と申します．来年3月に福島県会津若松東山温泉で開催される第15回プログラミングおよびプログラミング言語ワークショップ (PPL2013) のご案内（2回目）です．みなさまのご投稿，ご参加をお待ちしております．論文投稿・発表申込方法の詳細と招待講演者の情報を追加いたしました．カテゴリ1はeasy chairを通して，カテゴリ2, 3は下記投稿用メールアドレスまでお申込ください． -------------------------------------------------------------------------- 第15回プログラミングおよびプログラミング言語ワークショップ（PPL2013） http://www.pllab.riec.tohoku.ac.jp/ppl2013/ 論文募集主催: 日本ソフトウェア科学会プログラミング論研究会日程: 2013年3月4日(月)〜3月6日(水) 会場: 福島県会津若松東山温泉「御宿東鳳」http://www.onyado-toho.co.jp/ PPL2013は，プログラミングおよびプログラミング言語に関する研究者が一堂に会し，最新の研究成果の発表，および新たな研究課題についての討論やアイディア交換等を行うことを目的とした，合宿形式のワークショップです．プログラミングおよびプログラミング言語の理論・設計・実装・処理系などに関する研究発表を，カテゴリ別に幅広く募集します．カテゴリ１: 国内外で未発表の論文の発表カテゴリ２: 国際会議・学術雑誌等で既発表であるが，国内では未発表の研究の紹介カテゴリ３: ポスター・デモ発表（既発表・未発表の別を問いません） ※ショートプレゼンテーションは行いませんカテゴリ１の採択論文の中から，特に独創的なアイディアや顕著な成果を含むものに対して論文賞を授与する予定です．また，ポスター・デモを含む全発表のなかから，聴衆の投票により，最も優秀なプレゼンテーションに発表賞（一般の部，学生の部）を授与する予定です．カテゴリ１（国内外未発表論文） ------------------------------ 完成した理論やシステムの研究発表のみならず，萌芽的なアイディアや問題点の提示等も歓迎します．発展途上の研究内容も積極的に採録する方針です（ただし，PPLでの発表として相応しくないと判断される場合は，この限りではありません）．また，カテゴリ1で発表された研究については，会場での討議や査読コメントをもとにその完成度を高め，将来の学術雑誌・会議等での業績に結び付けることを奨励しています．そのため，予稿集の配布は参加者のみへの限定的なものとする予定です．採録された論文は，PPL2013参加者に配布される予稿集に掲載され，参加者のみがアクセス可能な形でWEB上で公開されます（論文へのリンク集ページを作成し，閲覧に必要なパスワードを参加者に連絡します）．カテゴリ１で発表された研究のうち，PPL2013プログラム委員会として優れていると認めるものは，PPL2013終了後（2013年4月下旬予定），「コンピュータソフトウェア」誌PPL2013推薦論文としての投稿が可能です．推薦論文は，PPL プログラム委員が引き続き査読を行うことによる，迅速な査読プロセスを特長としています．カテゴリ２（国外既発表論文） ---------------------------- 査読付の国際会議または学術雑誌等で既発表であるが，国内では未発表な研究の紹介をする場です．採録決定済みの研究も含みます．PPLへの関連をもとに採録を判定いたします．カテゴリ３（ポスター・デモ発表） ------------------------------------------ ２時間程度のセッション内でのポスター発表またはデモ発表です．既発表・未発表の別を問いません．PPLへの関連をもとに採録を判定いたします．また，申込多数の場合は抽選によって採否を決定する可能性があります．なお，PPL2013 ではポスターやデモによる活発な意見交換を促進したいという観点から，ショートプレゼンテーションのセッションは設けません．招待講演 -------- 鍋島英知 (山梨大学) 村主崇行 (京都大学) 以上のお二方の招待講演を予定しています． ====================================================================== 投稿・発表申込要領３つのカテゴリそれぞれに対して，投稿は以下のように行って下さい．最新の情報は上記Webページでご確認下さい．カテゴリ１（国内外未発表論文） ------------------------------ 投稿手続きは二段階です．発表申込を行った上で論文提出を行って下さい．発表申込先： https://www.easychair.org/conferences/?conf=ppl2013 発表申込締切：2012年12月21日(金) 17:00 (JST) 著者名，所属，論文タイトル，論文概要（日本語300〜400字程度もしくは英語200 words程度）を提出してください．論文提出締切：2013年1月11日(金) 17:00 (JST) 10ページ程度（最大15ページ）の論文（英語もしくは日本語，PDF形式）を提出して下さい．採否通知：2013年2月4日(月) 最終原稿提出締切：2013年2月15日(金) 17:00 (JST) 採録された論文の最終原稿の提出方法は，採否通知にてお知らせいたします． (注) カテゴリ１への投稿論文と類似の論文を，他の会議（予稿集を出版するもの）・論文誌などに同時投稿する場合は，査読の有無に関わらず，その旨を発表申込および論文提出の際に明記して下さい．PPLでは同時投稿の事実のみをもって論文を不採録とすることはありませんが，採否の決定に利用する場合があります（他の会議との重複を避けるため，発表内容についての条件付採録とすることもあります）．カテゴリ２（国外既発表論文） ---------------------------- 昨年同様，カテゴリ2の申込締切が少し早くなっていますのでご注意ください．発表申込時に採録が決定している国際会議または学術雑誌等の発表論文が対象です．理論系だけではなく実装系の論文の投稿も歓迎いたします．発表申込先： submit-ppl2013 [at] kurims.kyoto-u.ac.jp （[at]を@に置き換えて下さい）発表申込締切：2013年1月23日(水) 17:00 (JST) 原論文（ページ数不問，PDF形式）とabstract（テキスト形式）を，著者名，所属，論文タイトル，原論文の出典（発表会議名，掲載済／予定の別等）と併せて上記申込先宛にお送り下さい．採否通知：2013年2月4日(月) 最終原稿提出締切：2013年2月15日(金) 17:00 (JST) カテゴリ３（ポスター・デモ発表） ------------------------------------------ ポスター・デモの区別を行なわずに募集いたします．デモを行なう場合は，発表概要においてその旨をご説明ください．発表申込先： submit-ppl2013 [at] kurims.kyoto-u.ac.jp （[at]を@に置き換えて下さい）発表申込締切：2013年2月6日(水) 17:00 (JST) 著者名，所属，発表タイトル，発表概要（200〜300字程度），希望する発表形態（ポスター・デモの別），をテキスト形式で上記申込先宛にお送り下さい．採否通知：2013年2月15日(金) 問い合わせ先：oc-ppl2013 [at] kurims.kyoto-u.ac.jp （[at]を@に置き換えて下さい） ====================================================================== プログラム委員会青木利晃 (北陸先端科学技術大学院大学) 青谷知幸 (北陸先端科学技術大学院大学) 天野俊一 (IBM東京基礎研究所) 磯部祥尚 (産業技術総合研究所) 岩見宗弘 (島根大学) 角谷良彦 (東京大学) 勝股審也 (京都大学) [プログラム共同委員長] 小宮常康 (電気通信大学) 権藤克彦 (東京工業大学) [プログラム共同委員長] 田浦健次朗 (東京大学) 高田喜朗 (高知工科大学) 田辺良則 (国立情報学研究所) 中田景子 (Institute of Cybernetics at Tallinn University of Technology) 中野圭介 (電気通信大学) 長谷部浩二 (筑波大学) 番原睦則 (神戸大学) 松崎公紀 (高知工科大学) 実行委員会上野雄大 (東北大学電気通信研究所) [実行委員長] 鵜川始陽 (電気通信大学) [実行副委員長] 勝股審也 (京都大学) [プログラム共同委員長] 権藤克彦 (東京工業大学) [プログラム共同委員長] --------------------------------------------------------------------------

1 0

Talk by Kazushige Terui (11:00-, 29 Nov)
by Shinya Katsumata 27 Nov '12

27 Nov '12

京都大学数理解析研究所の勝股です。 11月29日11:00から、当研究所の照井一成氏が以下の講演をいたしますので、ご連絡いたします。どうぞお気軽にお越しください。 ========== Time: 11:00-12:00, 29 Nov, 2012 Place: Rm 478, Research Building 2, Main Campus, Kyoto University http://www.kyoto-u.ac.jp/en/access/campus/main.htm (See 34) 京都大学本部構内総合研究2号館 4階478号室 http://www.kyoto-u.ac.jp/ja/access/campus/map6r_y.htm (34番の建物) Speaker: Kazushige Terui (RIMS, Kyoto University) Title: Herbrand's theorem via hypercanonical extensions Abstract: よく知られているエルブランの定理を代数的に捉えたい。そのために古典論理のみならず、部分構造論理一般について考える。（様相などの単調／反単調な演算子を追加してもよい。たとえば直観主義論理、単調様相論理、線形論理、ファジー論理など）。 Lをそのような命題論理とし、その最小述語拡大をQLとすると、QLについてエルブランの定理が成り立つための代数的十分条件として、Lに対応する代数のクラスがコンパクトな完備化について閉じていることが挙げられる。そのような完備化の代表例はストーン双対性に基づくものであり、その一般化は正準拡大（canonical extensions）と呼ばれ広く研究されている。しかし部分構造論理の観点から興味深い代数のクラスの多くは、正準拡大について閉じているかどうか定かではない。そこで本講演では、新たなコンパクト完備化として超正準拡大（hypercanonical extensions）を導入する。これは非古典論理証明論における「シークエント計算⇒超シークエント計算」という発想に基づいて正準拡大を一般化したものである。それによりゲーデル＝ダメット論理、monoidal t-norm logicをはじめとする多くの論理についてエルブランの定理が系統的に成り立つことを示す。（今年度MLGにおける講演と同内容）

1 0

【訂正】Computability Theory and Foundations of Mathematics (CTFM)
by Naohi Eguchi 26 Nov '12

26 Nov '12

Logic-ml の皆様，先日ご案内しました計算可能性，逆数学等に関する研究会 Computability Theory and Foundations of Mathematics (CTFM) (2013年2月18日(月)〜2月20日(水)，東京工業大学大岡山キャンパス) http://sendailogic.math.tohoku.ac.jp/CTFM/ につきまして，講演申し込み締め切りが2013年12月18日となっていましたが*2012年*12月18日(火)の誤りでした．訂正してお詫び申し上げます．江口直日　(CTFM プログラム委員) 問い合わせ先　CTFM(a)math.tohoku.ac.jp ============================================================ Computability Theory and Foundations of Mathematics (Tokyo Institute of Technology, Tokyo, Japan, February 18 - 20, 2013) http://sendailogic.math.tohoku.ac.jp/CTFM/ ============================================================ 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, Constructive Mathematics, Theory of Randomness and Computational Complexity Theory. This is a successor workshop to Workshop on Proof Theory and Computability Theory 2012 - Philosophical Frontiers in Reverse Mathematics (February 20 - 23, 2012, Tokyo, Japan). -------------------------------------------- Deadline of Submission for Presentations: December 18, 2013 /*2012*/ -------------------------------------------- Invited Speakers: Chi Tat Chong (National University of Singapore) Erik Palmgren (Stockholm University) Michael Rathjen (University of Leeds) Helmut Schwichtenberg (LMU Munich) Stephen G. Simpson (Pennsylvania State University) Yang Yue (National University of Singapore) Wu Guohua (Nanyang Technological University) -------------------------------------------- Programme Committee: Toshiyasu Arai (Chiba) Naohi Eguchi (Tohoku) Hajime Ishihara (JAIST) Ryo Kashima (Tokyo Institute of Technology) Sam Sanders (Ghent) Kazuyuki Tanaka (Tohoku, Co-chair) Andreas Weiermann (Ghent, Co-chair) Takeshi Yamazaki (Tohoku) Keita Yokoyama (Tokyo Institute of Technology) --------------------------------------------

1 0

Postdoc positions, Tokyo/Kyoto, Computation Theory
by Akitoshi Kawamura 26 Nov '12

26 Nov '12

皆様東京大学の河村と申しますメーリングリストをお借りして新学術領域研究「計算限界解明」（代表：渡辺治）の研究員の公募（締切12月20日）について御案内させて頂きます計算量理論の諸問題への挑戦を目標とする研究領域ですがウェブページにありますように数理論理学的手法も中心テーマの一つでございます国内外を問わず皆様の周りの方々に広くお知らせ頂ければ幸いです -- 河村彰星東京大学大学院情報理工学系研究科コンピュータ科学専攻　助教 http://www-imai.is.s.u-tokyo.ac.jp/~kawamura/index_j.html ％％％％％％％％％％％％％％％％％％％％％％％％％％％ポスドク募集文部科学省科学研究費補助金新学術領域研究　「多面的アプローチの統合による計算限界の解明」代表者：渡辺治 (東京工業大学） http://www.al.ics.saitama-u.ac.jp/elc/ では、下記のように4名の研究員を募集いたします。国際公募する予定で英語での文章しかございませんが、ご容赦下さい。よろしくお願いいたします。 --------------------------------------------------------------------- Two-year post-doctoral positions, Tokyo and Kyoto, Computation Theory --------------------------------------------------------------------- http://www.al.ics.saitama-u.ac.jp/elc/en/?pd The newly established Center for Exploring the Limits of Computation (CELC, Tokyo, Japan) seeks applications for four post-doctoral fellow positions in Computational Complexity Theory and related areas. The appointments are for two years starting in April 2013 (or as soon as possible). A monthly salary of approximately 350,000 Japanese yen plus a research allowance will be offered. Applicants should hold a PhD in theoretical computer science or related fields (or be expected to do so by July 2013). Two of the fellows will be based at the Tokyo site (Tokyo Institute of Technology and the CELC) and two at the Kyoto site (Kyoto University). Collaboration with other research groups of the ELC project (including visits for several months) will be encouraged and supported. Applications should include * a curriculum vitae, * list of publications, * a research statement, and * three letters of referees (to be sent directly from the referees). Applications and letters of referees should be sent via email to elc-pd-application(a)is.titech.ac.jp. Priority will be given to applications received by December 20, 2012. Applicants may be invited to an interview in early 2013 (the travel expenses will be covered). --------- About ELC --------- Exploring the Limits of Computation (ELC) is a five-year research project funded by the Japanese Ministry of Education, Culture, Sports, Science and Technology. Project Title (formal): A multifaceted approach toward understanding the limitations of computation Short Title: Exploring the Limits of Computation (ELC) Project Term: 2012.7 - 2017.3 Researchers have proposed various techniques for investigating the limits of computation, many of which have been sharpened in depth during the last two decades. We may soon be entering the stage of expecting some big breakthrough results toward understanding the limits of computation. In this project, we investigate these techniques and relationships among them with the goal of finding the next steps toward a big breakthrough. We propose the following three lines of research, each of which will be conducted by three core research groups (i.e., nine core research groups altogether). A. Team for pushing the current frontier of research on the limits of computation. B. Team for investigating the limits of computation by using various algorithmic/optimization techniques (even by using supercomputers). C. Team for introducing new approaches to and interpretations of the existing techniques for investigating the limits of computation. We also create a research center (CELC) in Tokyo for investigating computational complexity theory by stimulating worldwide collaborations among researchers based on our core research groups, hosting short/long term visitors and postdoctoral researchers, and organizing various meetings and workshops. We welcome researchers working on subjects related to computational complexity theory to join us for various occasions. Project webpage http://www.al.ics.saitama-u.ac.jp/elc/en/

1 0

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Logic-ml