Logic-ml January 2012

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

14 participants
18 discussions

セミナー案内
by KASHIMA Ryo 12 Oct '12

12 Oct '12

数理論理学セミナーのご案内日時：12月22日(木)17時から場所：東京工業大学大岡山西８号館W棟11階 W1101セミナー室会場までの交通案内はこちらから： http://www.titech.ac.jp/about/campus/index.html 話者：藤原誠（東北大学）題目：結婚定理の逆数学概要： 1972年にManasterとRosensteinは可算版結婚定理を再帰理論的に分析し、通常の可算版結婚定理は計算可能には成立しないことを示した。一方、1983年にKiersteadは拡張Hall条件を導入し、計算可能に成立する結婚定理を得た。本発表では、拡張Hall条件を用いて考え得るあらゆる結婚定理の複雑さを逆数学的に分析する。また、Kiersteadとは別の観点から、計算可能に成立する結婚定理について考察する。 ----- 鹿島亮東京工業大学大学院情報理工学研究科数理・計算科学専攻 kashima(a)is.titech.ac.jp ＃＃＃木曜夕方を中心に不定期的にセミナーを開催しています＃＃＃＃＃＃詳細はお問い合わせください＃＃＃

1 1

NII Type Theory Workshop
by Makoto Tatsuta 01 Feb '12

01 Feb '12

Seventh NII Type Theory Workshop Date: February 6, 2012, 13:00--17:00 Place: National Institute of Informatics, Room 2005 (20th floor) 場所: 国立情報学研究所 20階 2005室 (半蔵門線,都営地下鉄三田線・新宿線神保町駅または東西線竹橋駅より徒歩5分) (地図 http://www.nii.ac.jp/introduce/access1-j.shtml) Program: 13:00--13:30 Daisuke Kimura (National Institute of Informatics) Title: A generalized modal lambda calculus 13:30--14:00 Kazuyuki Asada (National Institute of Informatics) Title: Semantics of Multi-rooted Graph with Ordered Branch 14:00--14:20 Tea Break 14:20--15:00 Makoto Tatsuta (National Institute of Informatics) Title: Type Inference for Bimorphic Recursion 15:00--15:40 Yukiyoshi Kameyama (University of Tsukuba) Title: Pseudo-Classical Modal Logic for Staged Computation 15:40--16:00 Tea Break 16:00--17:00 Stefano Berardi (Torino University) Title: A Game Semantic for various Subclassical Logics Abstracts: ---------------------------------------------------------------------- Daisuke Kimura (National Institute of Informatics) Title: A generalized modal lambda calculus Abstract: In this talk, we introduce a lambda calculus with modal types. The types of this system contain information of possible worlds explicitly. This information can be considered as a position which is an abstraction of time or place. The feature of our calculus is that we can change the property of modalities by changing information about the relationship between positions. The aim of our research is the following: (1) To clarify the computational meaning of necessity and possibility modal operators. (2) To give a uniform framework that can treat several calculi with modal types. ---------------------------------------------------------------------- Kazuyuki Asada (National Institute of Informatics) Title: Semantics of Multi-rooted Graph with Ordered Branch Abstract: Buneman et al. introduced a graph transformation language UnCAL, where graph has bisimilarity semantics. There structural recursion plays an important role, and in order to define it, they introduced multi-rooted graph and its algebraic representation. In this talk we give coalgebraic semantics for multi-rooted graph, and see that such final coalgebras has some call-by-value structure. Then we introduce a CBV equational theory. Next we modify the results of graph with un-ordered branch to that with ordered branch, which is important for application to XML. For this ordered graphs, bisimilarity is defined in some subtle way, but we can use the ordered version of above CBV equational theory for reasoning of the bisimilarity between ordered graphs. ---------------------------------------------------------------------- Makoto Tatsuta (National Institute of Informatics) Title: Type Inference for Bimorphic Recursion Abstract: This talk proposes bimorphic recursion, which is restricted polymorphic recursion such that every recursive call in the body of a function definition has the same type. Bimorphic recursion allows us to assign two different types to a recursively defined function: one is for its recursive calls and the other is for its calls outside its definition. Bimorphic recursion in this talk can be nested. This talk shows bimorphic recursion has principal types and decidable type inference. Hence bimorphic recursion gives us flexible typing for recursion with decidable type inference. This talk also shows that its typability becomes undecidable because of nesting of recursions when one removes the instantiation property from the bimorphic recursion. This is a joint work with Ferruccio Damiani. ---------------------------------------------------------------------- Yukiyoshi Kameyama (University of Tsukuba) Title: Pseudo-Classical Modal Logic for Staged Computation Abstract: In this talk, we study a pseudo-classical modal logic, which corresponds to the staged calculus with control operators introduced by our earlier work. Staged computation is a means for run-time code generation, and has been proved useful in improving efficiency and maintainability of software. We are interested in the use of control operators in staged computation, since they play an essential role to avoid the code duplication problem. Combining a staged calculus with control operators in a naive way results in an unsound calculus, and we need a restriction on the typing rule for lambda. We show that this restriction has a logical counterpart similar to Nakano's catch/throw calculus. ---------------------------------------------------------------------- Stefano Berardi (Torino University) Title: A Game Semantic for various Subclassical Logics Abstract: In this talk we describe the state of the art of game semantics for Logic and lambda-calculus, and the motivations for having a game semantics. Then we define a game semantic for Intuitionism extending both Coquands and Hyland-Ongs game semantics. The semantics refines a paper of TLCA 2007. We have two kind of results: (1) (Soundness and Completeness) The recursive winning strategy of our game semantics are isomorphic to the cut-free proofs of some variant of HA-omega (Infinitary Intuitionistic Arithmetic) (2) (Cut Elimination) Any debate between two terminating strategies terminates. This is an ongoing joint work with M. Tatsuta. ---------------------------------------------------------------------- 連絡先龍田真 (国立情報学研究所)

1 0

PPL2012 参加募集＆カテゴリ3発表募集
by Koji Nakazawa 31 Jan '12

31 Jan '12

logic-mlのみなさま，（重複の場合はご容赦ください．）京都大学の中澤です． 3月に和歌山県白浜温泉で開催される　第14回プログラミングおよびプログラミング言語ワークショップ (PPL2012) につきまして，参加登録を開始いたしましたのでお知らせします．参加登録要領 http://ppl2012.cs.uec.ac.jp/registration.html をご参照の上，日本旅行の専用ページからご登録ください．また，カテゴリ3（ポスター・デモ発表）の発表申込締切は　カテゴリ3 発表申込締切：2月6日(月) ですのであわせてお知らせいたします．必要事項をテキスト形式にて投稿用メールアドレス　ppl2012-submit(a)kuis.kyoto-u.ac.jp までお申込ください．皆様のご参加，ご発表をお待ちしております．最新情報は引き続き下記webページにてお知らせします． -------------------------------------------------------------------------- 第14回プログラミングおよびプログラミング言語ワークショップ（PPL2012） http://ppl2012.cs.uec.ac.jp/ 論文募集主催: 日本ソフトウェア科学会プログラミング論研究会日程: 2012年3月8日(木)〜3月10日(土) 会場: 和歌山県西牟婁郡白浜温泉むさし http://www.yado-musashi.co.jp/ PPL2012は，プログラミングおよびプログラミング言語に関する研究者が一堂に会し，最新の研究成果の発表，および新たな研究課題についての討論やアイディア交換等を行うことを目的とした，合宿形式のワークショップです．プログラミングおよびプログラミング言語の理論・設計・実装・処理系などに関する研究発表を，カテゴリ別に幅広く募集します．カテゴリ１: 国内外で未発表の論文の発表カテゴリ２: 国際会議・学術雑誌等で既発表であるが，国内では未発表の研究の紹介カテゴリ３: ポスター・デモ発表（既発表・未発表の別を問いません） ※ショートプレゼンテーションは行いませんカテゴリ１の採択論文の中から，特に独創的なアイディアや顕著な成果を含むものに対して論文賞を授与する予定です．また，ポスター・デモを含む全発表のなかから，聴衆の投票により，最も優秀なプレゼンテーションに発表賞（一般の部，学生の部）を授与する予定です．カテゴリ１（国内外未発表論文） ------------------------------ （投稿受付は終了しました）カテゴリ２（国外既発表論文） ---------------------------- （投稿受付は終了しました）カテゴリ３（ポスター・デモ発表） ------------------------------------------ ２時間程度のセッション内でのポスター発表またはデモ発表です．既発表・未発表の別を問いません．PPLへの関連をもとに採録を判定いたします．また，申込多数の場合は抽選によって採否を決定する可能性があります．なお，PPL2012 ではポスターやデモによる活発な意見交換を促進したいという観点から，ショートプレゼンテーションのセッションは設けません．招待講演 -------- 長谷川真人（京都大学）タイトル（予定）「プログラム意味論・テンソル圏・量子トポロジー - 意味論の「量子化」は可能か？」細谷晴夫（理化学研究所脳科学総合研究センター・科学技術振興機構さきがけ）タイトル（予定）「大脳皮質の計算論」以上のお二方の招待講演を予定しています． ====================================================================== 投稿・発表申込要領３つのカテゴリそれぞれに対して，投稿は以下のように行って下さい．最新の情報は上記Webページでご確認下さい．カテゴリ１（国内外未発表論文） ------------------------------ （投稿受付は終了しました）カテゴリ２（国外既発表論文） ---------------------------- （投稿受付は終了しました）カテゴリ３（ポスター・デモ発表） ------------------------------------------ ポスター・デモの区別を行なわずに募集いたします．デモを行なう場合は，発表概要においてその旨をご説明ください．発表申込先：ppl2012-submit(a)kuis.kyoto-u.ac.jp 発表申込締切：2012年2月6日(月) 著者名，所属，発表タイトル，発表概要（200〜300字程度），希望する発表形態（ポスター・デモの別），をテキスト形式で上記申込先宛にお送り下さい．採否通知：2012年2月13日(月) ワークショップ全般に関する問い合わせ先：ppl2012-oc(a)kuis.kyoto-u.ac.jp ====================================================================== プログラム委員会青戸等人 (東北大学) 稲葉一浩 (Google) 上野雄大 (東北大学) 小笠原啓 (ITプランニング) 角谷良彦 (東京大学) Jacques Garrigue (名古屋大学) 小宮常康 (電気通信大学) 立堀道昭 (IBM東京基礎研究所) 千代英一郎 (日立製作所) 中澤巧爾 (京都大学) 中田秀基 (産業技術総合研究所) 西村進 (京都大学) 長谷部浩二 (筑波大学) 浜名誠 (群馬大学) 前田敦司 (筑波大学) 八杉昌宏 (京都大学) 横山大作 (東京大学) 渡部卓雄 (東京工業大学) 実行委員会鵜川始陽 (電気通信大学) [実行委員長] 中澤巧爾 (京都大学) [プログラム共同委員長] 前田敦司 (筑波大学) [プログラム共同委員長] --------------------------------------------------------------------------

1 0

MSFP 2012 call for participation
by Ichiro Hasuo 31 Jan '12

31 Jan '12

みなさま， ETAPS 2012 附設ワークショップ MATHEMATICALLY STRUCTURED FUNCTIONAL PROGRAMMING のご案内です．ワークショップですが，歴史を持つトピックだけあり，選りすぐりでかっちりした論文が揃っています．せっかくタリンにおいでならば，ぜひご出席ください！蓮尾一郎（東大情報理工） https://www-mmm.is.s.u-tokyo.ac.jp/~ichiro/ ---------- Forwarded message ---------- From: Paul Levy <P.B.Levy(a)cs.bham.ac.uk> Date: Thu, Jan 26, 2012 at 11:38 PM Subject: categories: MSFP 2012 call for participation To: categories list <categories(a)mta.ca> Please note the deadline for early registration, including discounted hotel bookings: *Sunday 29 January* =========================== Fourth Workshop on MATHEMATICALLY STRUCTURED FUNCTIONAL PROGRAMMING 25 March, Tallinn, Estonia A satellite workshop of ETAPS 2012 http://cs.ioc.ee/msfp/msfp2012/ The fourth workshop on Mathematically Structured Functional Programming is devoted to the derivation of functionality from structure. It is a celebration of the direct impact of Theoretical Computer Science on programs as we write them today. Modern programming languages, and in particular functional languages, support the direct expression of mathematical structures, equipping programmers with tools of remarkable power and abstraction. Where would Haskell be without monads? Functional reactive programming without arrows? Call-by-push-value without adjunctions? Type theory without universes? The list goes on. This workshop is a forum for researchers who seek to reflect mathematical phenomena in data and control. The first MSFP workshop was held in Kuressaare, Estonia, in July 2006, affiliated with MPC 2006 and AMAST 2006. The second MSFP workshop was held in Reykjavik, Iceland as part of ICALP 2008. The third MSFP workshop was held in Baltimore, USA, as part of ICFP 2010. Invited Talks: ================= Dependently typed continuation monads as models in Logic Danko Ilik, Goce Delčev University of Štip, Republic of Macedonia Fibred Data Types Neil Ghani, University of Strathclyde, UK Accepted Papers ================== • A Formal Comparison of Approaches to Datatype-Generic Programming José Pedro Magalhães and Andres Löh • An Investigation of the Laws of Traversals Mauro Jaskelioff and Ondrej Rypacek • Evaluation strategies for monadic computations Tomas Petricek • From Mathematics to Abstract Machine: A formal derivation of an executable Krivine machine Wouter Swierstra • Irrelevance, Heterogenous Equality, and Call-by-value Dependent Type Systems Vilhelm Sjöberg, Chris Casinghino, Ki Yung Ahn, Nathan Collins, Harley D. Eades III, Peng Fu, Garrin Kimmell, Tim Sheard, Aaron Stump and Stephanie Weirich • Parametric Compositional Data Types Tom Hvitved and Patrick Bahr • Step-Indexed Normalization for a Language with General Recursion Chris Casinghino, Vilhelm Sjöberg and Stephanie Weirich • Tracing monadic computations and representing effects Maciej Piróg and Jeremy Gibbons ETAPS: ====== European Joint Conferences on Theory and Practice of Software (ETAPS) is the primary European forum for academic and industrial researchers working on topics relating to software science. ETAPS, established in 1998, is a confederation of six main annual conferences (one of them, POST, being new in 2012), accompanied by satellite workshops. ETAPS 2012 is the fifteenth event in the series. http://www.etaps.org/2012 Host City: ========== Tallinn, a city of 412,000 people, is the capital and largest city of Estonia, a small EU member country in Northern Europe, bordering Russia to the East and Latvia to the south. Located in the north of the country, on the southern shores of the Gulf of Finland, opposite Helsinki in Finland, Tallinn is most well known for its picturesque medieval Old Town, a UNESCO World Heritage site. But it also has a vivid cultural scene, outperforming most European centres of similar size. In 2011, Tallinn, along with Turku in Finland, is the Cultural Capital of Europe. Tallinn is easy to travel to. Estonia is part of Schengen and the Eurozone. The Lennart Meri International Airport of Tallinn /TLL) is only 4km from the city centre. Programme Committee: ==================== * James Chapman (co-chair), Institute of Cybernetics, Tallinn, Estonia * Paul Blain Levy (co-chair), University of Birmingham, UK * Thorsten Altenkirch, University of Nottingham, UK * Robert Atkey, University of Strathclyde, Glasgow, UK * Nils Anders Danielsson, Chalmers University and University of Gothenburg, Sweden * Martin Escardo, University of Birmingham, UK * Ichiro Hasuo, University of Tokyo, Japan * Ralf Hinze, University of Oxford, UK * Neelakantan Krishnaswami, Microsoft Research, Cambridge, UK * Daniel R. Licata, Carnegie Mellon University, Pittsburgh, PA * Ulrich Schoepp, LMU Munich, Germany * Alex Simpson, University of Edinburgh, UK * Matthieu Sozeau, INRIA, Paris, France * Sam Staton, University of Cambridge, UK Further Information: ==================== For more information about the workshop, go to: http://cs.ioc.ee/msfp/msfp2012/ With any other questions please do not hesitate to contact the co-chairs at msfp2012(a)easychair.org.

1 0

Philosophy, Mathematics, Linguistics: Aspects of Interaction 2012
by BEKKI Daisuke 29 Jan '12

29 Jan '12

------------------------------------------------------------------ The International Interdisciplinary Conference Philosophy, Mathematics, Linguistics: Aspects of Interaction 2012 (PhML 2012) St. Petersburg, Russia, May 22-25, 2012 http://www.pdmi.ras.ru/EIMI/2012/PhML/index.htm ------------------------------------------------------------------ AIM and SCOPE ============= The PhML 2012 is a sequel in the series of conferences "Philosophy, Mathematics, Linguistics: Aspects of Interaction" intended to provide a forum for presentation of current researches, and to stimulate a dialogue between mathematicians, logicians, philosophers, linguists and computer scientists who share an interest in cross-disciplinary research. The conference will have plenary sessions to present the latest researches. In addition to plenary sessions, the conference will feature a panel discussion entitled "The Heritage of Kant and Contemporary Formal Logic". Apart from plenary sessions, there will also be parallel sessions of thematic sections to present contributed papers. The PhML 2012 will be held on May 22$BK(J5, 2012, at the Euler International Mathematical Institute (EIMI), which is a part of the St. Petersburg Department of Steklov Mathematical Institute (PDMI). PLENARY SPEAKERS ================ Theodora Achourioti (University of Amsterdam, the Netherlands) Michel De Glas (CNRS - University Paris$BK%(Jiderot, France) Dmitry Grigoriev (CNRS - University Lille 1, France) Gerhard Heinzmann (Archives Henri-Poincare (UMR 7117) University of Lorraine/CNRS, France) Jaakko Hintikka (Boston University, USA) Edward Karavaev (St. Petersburg State University, Russia) Michiel van Lambalgen (University of Amsterdam, the Netherlands) Yuri Manin (Max Planck Institute for Mathematics, Germany)- to be confirmed Grigori Mints (Stanford University, USA) Andrey Patkul (St. Petersburg State University, Russia) Jeff Pelletier (University of Alberta, Canada) Graham Priest (City University of New York, USA, University of Melbourne, Australia) Oleg Prosorov (PDMI, St. Petersburg, Russia) Andrei Rodin (University Paris$BK%(Jiderot, France) Gabriel Sandu (University of Helsinki, Finland) Anatol Slissenko (University Paris$BK&(Jst Cr$BqU(Jeil, LACL, France) CALL for PAPERS =============== The PhML 2012 invites to submit papers relating to the interplay between philosophy, mathematics and linguistics for presentation at thematic sections. Each presentation of a contributed paper will be allotted 25 min, including 5 min for discussion. Presentations should be given in English. Papers from any tradition and from a wide variety of perspectives are welcome, including but in no way limited to the following topics: - New trends in the foundations of mathematics today; - Ontology of mathematics and the nature of mathematical truth; - The problem of abstract entities in mathematics, philosophy and linguistics; - Formalization of Kant's logic and theory of judgments; - The mathematical concept of a function: from the notions of mapping, transformation towards the notion of an algorithm; - Complexity of finite objects: limited possibilities of man and computer; - Novel computational models and paradigms; - Philosophical and mathematical aspects of informatics; - Philosophical aspects of the use of natural language in mathematics; - Mathematical investigation of natural language structures; - Mathematical models in the study of language. PAPER SUBMISSION ================ Papers should be prepared in LaTeX or MS Word using style files of PhML format and be submitted electronically as pdf and source files via e-mail: PhML_2012(a)pdmi.ras.ru IMPORTANT DATES: ================ - Submission deadline for contributed papers: March 1st, 2012 - Notification of acceptance: March 15th, 2012 - Final date for camera-ready copy: April 22nd, 2012 - Conference: May 22-25, 2012 - Panel discussion: May 23, 2012 PROCEEDINGS =========== The proceedings of PhML 2012 will be published by PDMI in the local series with ISBN no. ORGANIZING / PROGRAM COMMITTEE ============================== Edward Karavaev (St. Petersburg State University, Russia), Elena Lisanyuk (St. Petersburg State University, Russia), Ivan Mikirtumov (St. Petersburg State University, Russia), Yuri Nechitajlov (St. Petersburg State University, Russia), Vladimir Orevkov (PDMI, St. Petersburg, Russia), co-chair, Oleg Prosorov (PDMI, St. Petersburg, Russia), co-chair, Anatol Slissenko (University Paris$BK&(Jst Cr$BqU(Jeil, LACL, France). PARTICIPATION ============= For registration and further practical information, see: http://www.pdmi.ras.ru/EIMI/2012/PhML/index.htm

1 0

Talk by Stefano Berardi at RIMS, Kyoto U. (2/2)
by Kazushige TERUI 29 Jan '12

29 Jan '12

みなさま今週木曜日に催されるセミナーのご案内をさせていただきます。どうぞお気軽にお越しください。照井 --- RIMS-CS website http://www.kurims.kyoto-u.ac.jp/~cs/ ===== Speaker: Stefano Berardi (University of Torino) Title: A Topology over a set of Knowledge States and a Fixed Point Problem Date: 11.00 -, February 2nd (Thu) Place: Room 478, "Research Bldg. No. 2 (Sougou Kenkyu 2-Goukan)" http://www.kyoto-u.ac.jp/en/access/campus/main.htm (Next to our CS Lab) 総合研究2号館 478号室 (CS室のとなりです) http://www.kyoto-u.ac.jp/ja/access/campus/map6r_y.htm Abstract: We give an abstract formulation of the termination problem for realizer of Heyting Arithmetic plus various subsystem of classical logic. This termination problem is expressed as the existence of a fixed point for a class of continuous maps in a suitable topology. ------------------------------------------ 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

ポスドクの募集案内(Postdoc position in Quantum Information)
by Harumichi Nishimura 28 Jan '12

28 Jan '12

logic-mlの皆様，量子情報のポスドク募集に関する代理投稿をさせていただきます．大阪府立大学理学系研究科西村治道 ------------------------------------------------------------------------------- 立命館の山下茂と申します． Masaryk University, Brno, Czech Republik での以下のポスドクの募集案内を日本国内の量子情報関連MLへの配布を依頼されましたので、MLへ通して下記の案内をさせてください。複数お受け取りになったらご容赦ください。 Postdoc position in Quantum Information at Faculty of Informatics, Masaryk University, Brno, Czech Republik A 2-year (with possible extension to 3 years) postdoctoral position in Quantum Information Processing Theory is opening in Faculty of Informatics, Masaryk University, starting with September 2012, in the group of prof. Jozef Gruska (http://www.fi.muni.cz/quantum). Possible research areas includes - but are not restricted to - models of quantum computations, quantum algorithms, quantum cryptography, quantum entanglement, quantum (pseudo-telepathic) games. The successful candidate will be member of the Quantum information processing and cryptography laboratory that has currently 8 members including two postdocs. The group has close and intensive contacts with quantum groups in Bratislava and Vienna, Faculty of Informatics has more than 2500 students (http://www.fi.muni.cz) and close contacts with Departments of mathematics and Physics of the Faculty of Natural sciences. Applicants must hold a PhD - or be about to obtain one - in informatics, physics or mathematics and should be able to demonstrate very good English and strong research track record. Once application is successful, position should be taken during the period August 15 - September 1, 2012. The following information should be provided in an application: * CV * PhD diploma * A proof of good English (outcomes of TOEFL, CAE or an equivalent test). * Statement of research interest * Lists of publications and presentations * Two representative publications * Two letters of recommendations Electronic publications are preferred. They should be sent via email to gruska(a)fi.muni.cz or via postal mail to Prof. Jozef Gruska Faculty of Informatics Masaryk University Botanicka 68a 60200 Brno, Czech Republic For the official web side of the whole postdocs programs and conditions see http://www.mu.cz/research/postdoctoral ` An applicant will receive 55000 Kc per month (what corresponds concerning exchange rate to about 2200 EUR (and with respect to the living costs to about 3000-3300 EUR in Western Europe). In addition, he/she will receive standard health care insurance for himself/herself) Reasonable traveling and office money are also available

1 0

Workshop on Proof Theory and Computability Theory 2012
by Naohi Eguchi 27 Jan '12

27 Jan '12

Logic-ml の皆様，下記の要領で証明論及び計算可能性理論に関するワークショップを開催いたします． =========================================================== Workshop on Proof Theory and Computability Theory 2012 - Philosophical Frontiers in Reverse Mathematics 日時：2012年2月20日〜23日場所：晴海グランドホテル　(東京都中央区) ワークショップホームページ： http://www.math.tohoku.ac.jp/~eguchi/Workshop2012/Workshop_on_Proof_Theory_… =========================================================== 参加・講演申し込み締め切り： 2月3日(金)　（会場準備のため，早めにお申し込みください．）参加費(宿泊する場合)：一般：32,000円，学生：25,000円　(三泊＋参加費) (21日朝昼食，21日懇親会，22日朝昼夕食，23日朝食が含まれます． 20日の夕食は含まれません．) 宿泊短縮については，個別に相談に応じます．部屋はツインもしくはトリプルの相部屋になります．シングルはかなり高額になりますが，ご希望の方はご相談ください．参加費(宿泊しない場合)：一般：2,000円，学生：1,000円　(全日程で) (お茶代・資料印刷代等に利用させていただきます．食事は含まれません．) 懇親会(21日夜，晴海グランドホテル)：一般：5,000円，学生：3,000円程度参加をご希望の方は本文末のフォームにご記入いただき下記宛てにご返送ください．（★　講演しない場合にも，事前申し込みが必要です．）江口直日: eguchi(a)math.tohoku.ac.jp 皆様のご参加をお待ちいたしております． Kazuyuki Tanaka, Andreas Weiermann, Toshiyasu Arai, Naohi Eguchi, Hajime Ishihara, Sam Sanders, and Takeshi Yamazaki. ------------------- ここから ------------------------------------ 氏名(日本語)：氏名(英語)：所属(日本語)：所属(英語)：身分：　学生・一般　(どちらかをお選びください)　参加日程：宿泊：　有・無　(どちらかをお選びください) 2月21日(火)の懇親会：　参加・不参加　(どちらかをお選びください) 講演：　有・無　(どちらかをお選びください) 講演題目(英語)：講演要旨(英語)： (ごく標準的な Latex コマンド，Latex 環境はご使用いただけます) ------------------- ここまで ------------------------------------

1 0

計算機言語談話会（＠産総研尼崎）開催【2012/2/1】のお知らせ
by Takashi KITAMURA 25 Jan '12

25 Jan '12

皆様、こんにちは！産総研の北村崇師です。下記の通り、産総研組み込みシステム技術連携体（＠尼崎）は、計算機言語談話会（CLC:Computer Language Colloquium）を開催します。どなたでも無料で参加できます。皆様のご参加お待ちしております。また参加の際は、事前に北村（ t.kitamura(a)aist.go.jp ）までメールによるご連絡をお願いいたします。 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 日時：平成 24 年 2 月 1 日（水） 16：00--17: 30 場所：（独）産総研関西センター尼崎事業所 E 棟 2 階セミナー室 http://cfv.jp/cvs/access/index.html 演題：Automatic Specification-Based Program Testing 講演者：Prof. Shaoying Liu (Hosei University, Tokyo, Japan) 梗概： Automatic specification-based testing (ASBT) is a potentially effective and efficient technique for detecting errors in programs and attractive to industry due to its potential in saving time and cost. In this talk, after presenting the goals of the testing technique I will introduce a decompositional functional scenario-based testing technique, a specific ASBT, by explaining the strategy and criteria for test set generation, test oracle for test result analysis, and test process for tool support. I will also discuss the challenges and future research directions. Bio.: Shaoying Liu is Professor at Hosei University, Japan. He received a Ph.D in Computer Science from the University of Manchester, U.K in 1992. His research interests include Formal Engineering Methods, Specification-based Inspection and Testing, and Intelligent Software Engineering Environments. He has published a book titled "Formal Engineering for Industrial Software Development" with Springer-Verlag, four edited conference proceedings, and over 120 academic papers in refereed journals and international conferences. He is the chair of Steering Committee for ICFEM conference, and on the editorial board for the Journal of Software Testing, Verification and Reliability (STVR) and for ISRN Software Engineering Journal. He is a Fellow of British Computer Society, Senior member of IEEE Computer Society, and member of Japan Society for Software Science and Technology. ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 以上よろしくお願いいたします。 -------------------------- 北村崇師 PhD <t.kitamura(a)aist.go.jp> 特別研究員（独）産業技術総合研究所組込みシステム技術連携研究体〒661-0974 兵庫県尼崎市若王寺3-11-46 Tel: 06-6494-8054 Fax: 06-6494-8073

1 0

JAIST Verification Seminars by Yijia Chen and Yohji Akama (Jan 31, Feb 9)
by Nao Hirokawa 24 Jan '12

24 Jan '12

みなさま 1月31日(火)と2月9日(木)にJAISTで行われます、計算量・組合せ理論についての２つセミナーをご案内致します。どうぞお気軽にお越しください。 http://www.jaist.ac.jp/is/labs/ogawa-lab/vs12.html 廣川 - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - Seminars of Research Center for Software Verification, JAIST - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - == Seminar I == Date: 31st Jan (Tue) 13:00-17:00 (closing time is flexible) Place: JAIST IS school collaboration room 7 (5F) 1. Prof.Yijia Chen (Shanghai Jiao Tong University) "Parameterized complexity of SAT" Many natural computational problems are NP-hard, hence they have no polynomial time algorithms assuming NP \ne P. The traditional approaches for coping with such problems are heuristic and approximation algorithms. Nevertheless, the heuristic algorithms often lack a rigorous analysis, while the approximation algorithms cannot guarantee exact solutions. Parameterized algorithms offer another approach which achieves both criteria. The key observation is that many natural problem instances come with some parameters which can be expected to be small, e.g., the size of a vertex cover, the length of a database query, and the tree width of a graph. If an exponential time algorithm has its superpolynomial behavior restricted by the parameters, it might well be efficient in practice. As an example, there is an algorithm for SAT which is exponential in the tree width tw(\alpha) of a given instance \alpha and at the same time linear in the size of \alpha. Therefore, if there is a constant upper bound on tw(\alpha), we can solve the corresponding SAT in linear time. In this talk I will survey some major tools for designing parameterized algorithms, including bounded search tree, kernelization, tree width method, and algorithmic meta-theorems, etc, with a focus on applications to SAT. In passing, I will also discuss some corresponding lower bound results. 2. Dr. Yohji Akama (Tohoku University) "A new order theory of set systems, WQO and BQO" A set system over a set $T$, a subfamily of the power set $P(T)$, is a topic of (extremal) combinatorics, as well as a target of an algorithm to learn in computational learning theory of languages. A well quasi-ordering (WQO for short) is introduced by Higman and employed in algebra, combinatorics, formal language theory, and so on. A better quasi-ordering (BQO for short) is introduced by Nash-Williams and employed in infinitary combinatorics and verification of infinite-state systems. We generalize WQOs and BQOs by using set systems, define the order type of a set system from game-theoretic viewpoint and study nondeterministic, combinatorial operations on set systems, such as monotone (continuous) image and unbounded unions of set systems. The motivating examples are the union of two colored arithmetical progressions, and the discolorization, and new useful examples are shuffle-product and shuffle-closure from formal language theory Furthermore, we provide a neat correspondence : quasi-orderings vs finitely branching simulations, and set systems vs linear, monotone, continuous functions. Next, we introduce a set system that has order type and corresponds to a BQO. We prove that the class of set systems corresponding to BQOs is closed by any monotone function. In (Shinohara and Arimura. ``Inductive inference of unbounded unions of pattern languages from positive data.'', Theoretical Computer Science, pp.191-209, 2000), for any set system $L$, they considered the class of arbitrary (finite) unions of members of $L$. From viewpoint of WQOs and BQOs, we characterize the set systems $L$ such that the class of arbitrary (finite) unions of members of $L$ has order type. == Seminar II == Date: 9th Feb (Thu) 13:00-15:00 (closing time is flexible) Place: JAIST IS school collaboration room 7 (5F) * Prof.Yijia Chen (Shanghai Jiao Tong University) "A Logic for PTIME and a Parameterized Halting Problem" Whether there is a logic for polynomial time (PTIME) is the central problem in finite model theory. When formalizing this problem, Gurevich (1988), together with Blass, actually proposed a logic LFP_inv, which is a version of least fixed-point logic plus some additional invariance condition. Although they don't believe that LFP_inv captures PTIME, no proof was given. Later, in a work of Nash, Remmel, and Vianu (2005), it was shown that whether LFP_inv captures PTIME is equivalent to the parameterized complexity of a halting problem: input: A nondeterministic Turing machine M and a natural number n in unary. parameter: |M|, i.e., the size of M question: does M accept the empty input in at most n steps? Our recent work (2010-11) reveals that it is even equivalent to an open problem in proof complexity, i.e., whether there is a polynomial optimal proof system for the set TAUT of tautologies of propositional logic. In this talk, I will discuss all these equivalences and their extensions to some other complexity classes beside PTIME. It turns out that Levin's optimal inverters (1973) play a central role in the proofs. This is joint work with Joerg Flum.

1 0

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Logic-ml January 2012