Logic-ml February 2013

logic-ml@fos.kuis.kyoto-u.ac.jp

15 participants
25 discussions

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

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Logic-ml February 2013