- 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 09 Feb '13

09 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 09 Feb '13

09 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 06 Feb '13

06 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 06 Feb '13

06 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 03 Feb '13

03 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 01 Feb '13

01 Feb '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 18 Jan '13

18 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

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Logic-ml