Logic-ml

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

1792 discussions

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

Jump to page:

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Logic-ml