Logic-ml October 2011

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

17 participants
20 discussions

セミナー案内
by KASHIMA Ryo 24 Nov '11

24 Nov '11

数理論理学セミナーのご案内日時：10月27日(木)17時から場所：東京工業大学大岡山キャンパス西８号館Ｗ棟 10階 W1008セミナー室話者：堀畑佳宏（東北大）題目：弱い算術とconcatenationの理論概要：文字列の結合に関する理論（concatenationの理論） TC は、2005年に Grzegorczyk によって導入され、その決定不可能性が示された。一方、2009年にはVisser, Svejdar, Ganea がそれぞれ独立に、TC が Robinson 算術 Q と互いに翻訳可能であることを示した。本発表では、concatenation の理論 WTC を新たに導入し、この理論が Robinson と Tarski によって導入された非常に弱い算術 R と互いに翻訳可能となることを見る。 ---------- 会場までの交通案内はこちらから： http://www.titech.ac.jp/about/campus/index.html ----- 鹿島亮東京工業大学大学院情報理工学研究科数理・計算科学専攻 kashima(a)is.titech.ac.jp ＃＃＃木曜夕方を中心に不定期的にセミナーを開催しています。＃＃＃＃＃＃詳細はお問い合わせください。＃＃＃

1 1

Talk by Michele Basaldella, Tue 1 Nov at RIMS, Kyoto U
by Kenshi Miyabe 24 Oct '11

24 Oct '11

数理解析研究所　特定研究員の宮部です。重複して受け取られた場合はご容赦ください． RIMSでは、2週間に1度、GCOE tea timeを行っています。 http://www.kurims.kyoto-u.ac.jp/~kenkyubu/gcoe/2008teatime.html 来週、2011年11月1日(火)、第48回 GCOE tea timeでは、 Micheleが話をします。時間のご都合がよろしければ是非ご参加ください．講演者： Michele BASALDELLA (数理解析研究所　研究員) タイトル: Dilators: a gentle introduction 講演の概要: We aim to recall some basic aspects of the concept of dilator, a notion which has been introduced in proof-theory (a branch of mathematical logic) by J.-Y. Girard about 30 years ago. Essentially, a dilator is a certain kind of endofunctor of the category of the ordinal　numbers, which can be thought as an abstract counterpart of the more concrete system of ordinal notation which are abundant in proof-theory. In this introductory talk, we recall the notion of denotation system (a kind of generalization of the Cantor normal form representation of the ordinal numbers), the notion of dilator, and show a correspondence between them. なお、この講演は英語で行われます。時間(Time)：15:00-16:00 場所(Place)：数理解析研究所402号室(RIMS, Room 402) -- Kenshi Miyabe email: kmiyabe(a)kurims.kyoto-u.ac.jp Researcher Research Institute for Mathematical Sciences, Kyoto University Kyoto 606-8502 Japan Tel: +81-75-753-7202 / Fax: +81-75-753-7272

1 0

Workshop on Linear Logic (Program Available)
by Kazushige TERUI 23 Oct '11

23 Oct '11

皆様線型論理関連ワークショップ（１１月７日−１１日、京都大学）について、暫定プログラムができましたのでご案内させていただきます。人数把握のため、参加ご希望の方は添付の参加フォームをお送りいただけると助かります（当日参加も可）。 ※北白川学舎（RIMS宿泊施設）に１室空きがあります（バス・トイレ共用）。　ご希望の方はご連絡ください。 -------------------- Workshop on Linear Logic (Geometry of Interaction, Traced Monoidal Categories and Implicit Complexity) * Date: 7th - 11th, November (11th reserved for free discussion) * Location: Room 110, Faculty of Science Building No.3, Kyoto University 京都大学理学部３号館１１０号室 http://www.kyoto-u.ac.jp/ja/access/campus/map6r_n.htm ※数理解析研究所ではありませんのでご注意ください。 * Workshop Dinner 18:00-, 9th November. (cost: around 4,000 - 5,000yen) ※参加ご希望の方はなるべく事前に下記フォームにてお知らせください。 * Organizers Michele Basaldella: mbasalde(a)kurims.kyoto-u.ac.jp Kazushige Terui: terui(a)kurims.kyoto-u.ac.jp Claudia Faggian * Program (tentative) 7th November (Monday) 10:00-10:15 Opening 10:15-11:00 Masahito Hasegawa (Kyoto Univ.) TBA 11:00-11:30 Shin'ya Katsumata (Kyoto Univ.) Relating Computational Effects by TT-Lifting 13:00-14:30 Jean-Yves Girard (IML, Marseille) Lecture I 14:45-15:30 Masahiro Hamano (PRESTO, JST) A Geometry of Interaction for Polarized Linear Logic 15:45-16:30 Thomas Seiller (IML, Marseille) Graphs of Interaction 16:30-17:15 Jonas Frey (PPS, Paris) Characterizing Realizability Toposes 8th (Tuesday) 9:30-11:00 Jean-Yves Girard Lecture II 11:15-12:00 Claudia Faggian (PPS, Paris) Geometry of Interaction and Quantum Circuits (joint work with Ugo Dal Lago) 12:00-12:30 Kazuyuki Asada (National Institute of Informatics) Bidirectional Transformation and Int Construction 14:00-15:00 Stefano Guerrini (invited: LIPN, Paris) Jumps and Boxes 15:15-16:00 Michele Basaldella (Kyoto Univ.) Dilators: a Gentle Introduction 16:00-16:45 Etienne Duchesne (LIPN, Paris) TBA 9th (Wednesday) 9:30-11:00 Jean-Yves Girard Lecture III 11:15-12:00 Nao Hirokawa (JAIST) Runtime Complexity Analysis and Rewriting Techniques 12:00-12:30 Naohi Eguchi (Tohoku Univ.) Term-rewriting Approaches to Implicit Computational Complexity 14:00-15:00 Ugo Dal Lago (invited: Univ. Bologna) Measuring, Computing and Constraining: Three Ways to Exploit GoI in Implicit Complexity. 15:15-16:00 Michele Pagani (LIPN, Paris) The Computational Meaning of Probabilistic Coherence Spaces (joint work with Thomas Ehrhard and Christine Tasson) 16:00-16:45 Rene Vestergaard (JAIST) Towards a Geometry of Regulation 18:00- Workshop Dinner 10th (Thursday) 9:30-11:00 Jean-Yves Girard Lecture IV 11:15-12:15 Marco Gaboardi (invited: Univ. Pennsylvania) Linear Types for Function Sensitivity 13:45-14:30 Damiano Mazza (LIPN, Paris) Metrics on lambda-terms 14:30-15:00 Marc Bagnol (IML, Marseille) Cycles and Traces: On the Meaning of Syntaxe Transcendantale's Duality 15:15-15:45 Guillaume Munch-Maccagnoni (PPS, Paris) What can polarisation do for the proofs-as-programs correspondence? 15:45- Free Slots 11th (Friday) 9:30- Open Discussion ------------------------------------- 参加申し込みフォーム１．お名前・所属・身分２．参加日程：11月?日から〜11月?日まで３．９日の懇親会に参加する・しない -------------------------------------- ------------------------------------------ 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

IWC 2012 & CoCo 2012: First Call for Papers and Provers
by Nao Hirokawa 21 Oct '11

21 Oct '11

来年、名古屋で行われます RTA 2012 において、合流性 (チャーチ・ロッサ性) に関する第1回国際ワークショップ IWC 2012 と合流性自動証明のコンペティション CoCo 2012 が開催されます。最近は型安全が合流性により証明されるなど、興味深い応用が登場し始めています。投稿・参加を検討して頂けましたら幸いです。廣川　直（北陸先端科学技術大学院大学） This is a joint call for papers and provers for IWC 2012 and CoCo 2012. ====================================================================== First Call for Papers IWC 2012 1st International Workshop on Confluence 29 May 2012, Nagoya, Japan, collocated with RTA 2012 http://cl-informatik.uibk.ac.at/events/iwc-2012/ ====================================================================== Recently there is a renewed interest in confluence research, resulting in new techniques, tool support as well as new applications. The workshop aims at promoting further research in confluence and related properties. The workshop is collocated with the 23rd International Conference on Rewriting Techniques and Applications (RTA 2012). During the workshop the 1st Confluence Competition (CoCo 2012) takes place. IMPORTANT DATES: * submission March 6, 2012 * notification March 20, 2012 * final version April 3, 2012 * workshop May 29, 2012 TOPICS: The workshop solicits short papers/extended abstracts on the following topics: * confluence and related properties (unique normal forms, commutation, ground confluence) * critical pair criteria * decidability issues * complexity issues * system descriptions * certification * applications of confluence ORGANISING COMMITTEE: * Nao Hirokawa JAIST * Aart Middeldorp University of Innsbruck * Naoki Nishida Nagoya University PROGRAM COMMITTEE: * Takahito Aoto Tohoku University * Nao Hirokawa JAIST (co-chair) * Aart Middeldorp University of Innsbruck (co-chair) * Femke van Raamsdonk VU University Amsterdam * Aaron Stump The University of Iowa * Rakesh M. Verma University of Houston SUBMISSION: We solicit short papers or extended abstracts of at most five pages. There will be no formal reviewing. In particular, we welcome short versions of recently published articles and papers submitted elsewhere. The program committee checks relevance and may provide additional feedback. The accepted papers will be made available electronically before the workshop. In addition, we plan to distribute a printed version of the proceedings at the workshop. The page limit for papers is 5 pages in LIPIcs style. Submission will be via EasyChair at https://www.easychair.org/account/signin.cgi?conf=iwc2012 ====================================================================== First Call for Provers CoCo 2012 1st Confluence Competition http://coco.nue.riec.tohoku.ac.jp/2012/ ====================================================================== Recently, several new implementations of confluence proving/disproving tools are reported and interest for proving/disproving confluence "automatically" has been grown. CoCo aims to foster the development of techniques for proving/disproving confluence automatically by setting up a dedicated and fair confluence competition among confluence proving/disproving tools. The 1st Confluence Competition (CoCo 2012) runs during the 1st International Workshop on Confluence (IWC 2012), which is collocated with the 23rd International Conference on Rewriting Techniques and Applications (RTA 2012) at Nagoya University, Japan. In this competition a category for first-order term rewrite systems will be run. Other categories (e.g., higher-order) will be considered if there are tools and problems. IMPORTANT DATES: * registration April 1 - May 15, 2012 * tool submission May 1 - May 15, 2012 * competition May 29, 2012 REGISTRATION/SUBMISSION: Registration and tool submission will be via the email address: coco-sc [AT] jaist.ac.jp Tools must be able to read input files written in the old TPDB format. The output of the tools must contain an answer in the first line followed by some proof argument understandable for human experts. Valid answers are YES (the input is confluent) and NO (the input is not confluent). Every other answer is interpreted as the tool could not determine the status of the input. For more information including competition rules, see http://coco.nue.riec.tohoku.ac.jp/ ORGANISING COMMITTEE: * Takahito Aoto Tohoku University (chair) * Nao Hirokawa JAIST * Harald Zankl University of Innsbruck

1 0

The 46th MLG Meeting: Program
by Takahiro Seki 16 Oct '11

16 Oct '11

第46回 MLG 数理論理学研究集会のご案内 (重複してお受け取りの際はご容赦ください。) 　新潟大学の関です。　2011年度MLG数理論理学研究集会（第46回）を下記の要領で開催します。　講演・宿泊の申し込みは締め切りましたが，参加することは可能です。なお，その場合，事前の申し込みは不要ですが，参加費（会場代）1,500円をいただきます。 ========================================= 　第46回 MLG 数理論理学研究集会開催要領 ========================================= 　日時: 2011 年 10 月 23 日(日) 14:00 ～ 10 月 25 日(火) 11:50 　場所: KKR湯沢ゆきぐに（ＪＲ上越新幹線越後湯沢駅西口より徒歩約8分）　　　　〒949-6101 新潟県南魚沼郡湯沢町湯沢2574 　　　　URL : http://www.kkryuzawa.com/ 　MLG46ホームページ：　http://math2.ed.niigata-u.ac.jp/~seki/MLG46/ 　講演プログラム： ○　10月23日（日）　14:00～14:10　開会・事務連絡　14:10～14:50　松田直祐（千葉大学）　　　Proof-theoretic study of the correspondence of classical logic 　　　and intuitionistic logic 　15:10～15:50　関　隆宏（新潟大学）　　　Some negative translations of non-associative substructural logics 　15:50～16:30　小野寛晰（北陸先端科学技術大学院大学）　　　Substructural aspects of negative translations ○　10月24日（月）　 9:00～ 9:40　岩波　克（東京工業大学）　　　Łukasiewicz論理の公理化について　 9:40～10:20　山川郁加（千葉大学）　　　ラムダ計算と組合せ論理の関係（古森雄一との共同研究）　10:30～11:10　鹿島　亮（東京工業大学）　　　ECTL (Extended Computation Tree Logic) の完全公理化　11:10～11:50　佐々木克巳（南山大学）　　　シークエントと実証明　13:00～13:40　Milan Petrik（北陸先端科学技術大学院大学）　　　Semantics of fuzzy logic 　13:40～14:20　プライニング　ノルベルト（北陸先端科学技術大学院大学）　　　未定　14:30～15:10　大森　仁（神戸大学）　　　An expansion of Belnap-Dunn logic 　　　（Joint work with Katsuhiko Sano）　15:10～15:50　佐野勝彦（北陸先端科学技術大学院大学）　　　Hybrid product of modalized Belnap-Dunn logics 　16:00～16:40　佐藤雅彦（京都大学）　　　A canonical locally named representation of binding ○　10月25日（火）　 9:30～10:10　小島健介（京都大学）　　　Making neighborhood semantics intuitionistic 　10:20～11:00　倉田俊彦（法政大学）　　　On duality between Kripke models and lattice theoretical models 　　　of second order intuitionistic propositional logic 　　　(Joint work with Ken-etsu Fujita) 　11:00～11:40　鈴木信行（静岡大学）　　　Remarks on existence property in super-intuitionistic predicate 　　　logics 　11:40～11:50　事務連絡・閉会 --- 関　隆宏新潟大学企画戦略本部評価センター Tel : 025-262-6088 Fax : 025-262-6248 E-mail : tseki(a)adm.niigata-u.ac.jp

1 0

[CFP] 情報処理学会第87回プログラミング研究会
by Susumu Kanemune 16 Oct '11

16 Oct '11

大阪電気通信大学の兼宗です。＊＊＊＊複数受け取られた方は、ご容赦ください＊＊＊＊この場を借りて、2011年度第4回情報処理学会プログラミング研究会の発表募集のご案内をさせて頂きたく存じます。プログラミング研究会(PRO)は、・プログラミング言語の設計、処理系の実装・プログラミングの理論、基本概念・プログラミング環境、支援システム・プログラミング方法論、パラダイム・これらを応用したシステムの開発事例・その他、プログラミングに関する面白い話題を対象とした研究発表の場で、1998年度から毎年3〜4回のペースで論文誌を発行しています。PRO論文誌は研究会と密接にリンクしており、研究会で発表されたもののうちあらかじめ論文投稿を希望し、論文原稿を提出されているものが査読の対象となっています（論文誌投稿を希望しない発表も歓迎します）。おおむね研究会から3週間で論文の採否が決定されるという迅速さも大きな特徴です。2011年度第4回研究会も多くの発表ならびに論文投稿をお待ちしております。参加費は無料です。申込〆切は11月18日(投稿〆切は12月16日)です。よろしくご検討ください。第87回プログラミング研究会(PRO-2011-4)発表募集日程: 2012年1月23日(月)・24日(火) 会場: 久米島町　イーフ情報プラザ　交流ホール（沖縄県久米島町字比嘉160-57）発表申込締切: 2011年11月18日(金) 投稿論文原稿提出締切: 2011年12月16日(金) 申込先: 兼宗進（大阪電気通信大学） E-mail: kanemune(a)acm.org 案内ページ: http://kanemune.eplang.jp/?pro87 ・申込みに当たっての注意はプログラミング研究会のページ http://www.ipsj.or.jp/sig/pro/ を参照してください。・連絡はE-mailでお願いします。・申込み後返信がない場合はご連絡下さい。 // 兼宗進 (Susumu Kanemune) // 大阪電気通信大学 (Osaka Electro-Communication University)

1 0

PPL2012 論文募集
by Koji Nakazawa 16 Oct '11

16 Oct '11

（重複の場合はご容赦ください．）京都大学の中澤です．来年3月に和歌山県白浜温泉で開催される第14回プログラミングおよびプログラミング言語ワークショップ (PPL2012) のご案内です．詳細な投稿方法などは決定次第，下記ワークショップwebページにてお知らせしますので，ご投稿，ご参加をご検討ください． -------------------------------------------------------------------------- 第14回プログラミングおよびプログラミング言語ワークショップ（PPL2012） http://ppl2012.cs.uec.ac.jp/ 論文募集主催: 日本ソフトウェア科学会プログラミング論研究会日程: 2012年3月8日(木)〜3月10日(土) 会場: 和歌山県西牟婁郡白浜温泉むさし http://www.yado-musashi.co.jp/ PPL2012は，プログラミングおよびプログラミング言語に関する研究者が一堂に会し，最新の研究成果の発表，および新たな研究課題についての討論やアイディア交換等を行うことを目的とした，合宿形式のワークショップです．プログラミングおよびプログラミング言語の理論・設計・実装・処理系などに関する研究発表を，カテゴリ別に幅広く募集します．カテゴリ１: 国内外で未発表の論文の発表カテゴリ２: 国際会議・学術雑誌等で既発表であるが，国内では未発表の研究の紹介カテゴリ３: ポスター・デモ発表（既発表・未発表の別を問いません） ※ショートプレゼンテーションは行いませんカテゴリ１の採択論文の中から，特に独創的なアイディアや顕著な成果を含むものに対して論文賞を授与する予定です．また，ポスター・デモを含む全発表のなかから，聴衆の投票により，最も優秀なプレゼンテーションに発表賞（一般の部，学生の部）を授与する予定です．カテゴリ１（国内外未発表論文） ------------------------------ 完成した理論やシステムの研究発表のみならず，萌芽的なアイディアや問題点の提示等も歓迎します．発展途上の研究内容も積極的に採録する方針です（ただし，PPLでの発表として相応しくないと判断される場合は，この限りではありません）．また，カテゴリ1で発表された研究については，会場での討議や査読コメントをもとにその完成度を高め，将来の学術雑誌・会議等での業績に結び付けることを奨励しています．そのため，予稿集の配布は参加者のみへの限定的なものとする予定です．採録された論文は，PPL2012参加者に配布される予稿集に掲載され，参加者のみがアクセス可能な形でWEB上で公開されます（論文へのリンク集ページを作成し，閲覧に必要なパスワードを参加者に連絡します）．カテゴリ１で発表された研究のうち，PPL2012プログラム委員会として優れていると認めるものは，PPL2012終了後（2012年4月下旬予定），「コンピュータソフトウェア」誌PPL2012推薦論文としての投稿が可能です．推薦論文は，PPL プログラム委員が引き続き査読を行うことによる，迅速な査読プロセスを特長としています．カテゴリ２（国外既発表論文） ---------------------------- 査読付の国際会議または学術雑誌等で既発表であるが，国内では未発表な研究の紹介をする場です．採録決定済みの研究も含みます．PPLへの関連をもとに採録を判定いたします．カテゴリ３（ポスター・デモ発表） ------------------------------------------ ２時間程度のセッション内でのポスター発表またはデモ発表です．既発表・未発表の別を問いません．PPLへの関連をもとに採録を判定いたします．また，申込多数の場合は抽選によって採否を決定する可能性があります．なお，PPL2012 ではポスターやデモによる活発な意見交換を促進したいという観点から，ショートプレゼンテーションのセッションは設けません． ====================================================================== 投稿・発表申込要領３つのカテゴリそれぞれに対して，投稿は以下のように行って下さい．最新の情報は上記Webページでご確認下さい．カテゴリ１（国内外未発表論文） ------------------------------ 投稿手続きは二段階です．発表申込を行った上で論文提出を行って下さい．発表申込締切：2011年12月22日(木) 著者名，所属，論文タイトル，論文概要（日本語300〜400字程度もしくは英語200 words程度）を提出してください．論文提出締切：2012年1月6日(金) 10ページ程度（最大15ページ）の論文（英語もしくは日本語，PostScriptもしくはPDF形式）を提出して下さい．採否通知：2012年1月31日(火) 最終原稿提出締切：2012年2月13日(月) 採録された論文の最終原稿の提出方法は，採否通知にてお知らせいたします． (注) カテゴリ１への投稿論文と類似の論文を，他の会議（予稿集を出版するもの）・論文誌などに同時投稿する場合は，査読の有無に関わらず，その旨を発表申込および論文提出の際に明記して下さい．PPLでは同時投稿の事実のみをもって論文を不採録とすることはありませんが，採否の決定に利用する場合があります（他の会議との重複を避けるため，発表内容についての条件付採録とすることもあります）．カテゴリ２（国外既発表論文） ---------------------------- 昨年同様，カテゴリ2の申込締切が少し早くなっていますのでご注意ください．締切直後（2月初旬頃）に採否が決定する国際会議については，あらかじめ，下記問い合わせ先までご相談ください．発表申込締切：2012年1月23日(月) 原論文（ページ数不問，PostScriptもしくはPDF形式）とabstract（テキスト形式）を，著者名，所属，論文タイトル，原論文の出典（発表会議名，掲載済／予定の別等）と併せて上記申込先宛にお送り下さい．採否通知：2012年1月31日(火) 最終原稿提出締切：2012年2月13日(月) カテゴリ３（ポスター・デモ発表） ------------------------------------------ ポスター・デモの区別を行なわずに募集いたします．デモを行なう場合は，発表概要においてその旨をご説明ください．発表申込締切：2012年2月6日(月) 著者名，所属，発表タイトル，発表概要（200〜300字程度），希望する発表形態（ポスター・デモの別），をテキスト形式で上記申込先宛にお送り下さい．採否通知：2012年2月13日(月) 問い合わせ先：ppl2012-oc(a)kuis.kyoto-u.ac.jp ====================================================================== プログラム委員会青戸等人 (東北大学) 稲葉一浩 (Google) 上野雄大 (東北大学) 小笠原啓 (ITプランニング) 角谷良彦 (東京大学) Jacques Garrigue (名古屋大学) 小宮常康 (電気通信大学) 立堀道昭 (IBM東京基礎研究所) 千代英一郎 (日立製作所) 中澤巧爾 (京都大学) 中田秀基 (産業技術総合研究所) 西村進 (京都大学) 長谷部浩二 (筑波大学) 浜名誠 (群馬大学) 前田敦司 (筑波大学) 八杉昌宏 (京都大学) 横山大作 (東京大学) 渡部卓雄 (東京工業大学) 実行委員会鵜川始陽 (電気通信大学) [実行委員長] 中澤巧爾 (京都大学) [プログラム共同委員長] 前田敦司 (筑波大学) [プログラム共同委員長] --------------------------------------------------------------------------

1 0

Kobe Colloquium on Logic, Statistics and Informatics Oct.18
by Makoto Kikuchi 11 Oct '11

11 Oct '11

皆様渕野昌＠神戸大学システム情報学研究科です． 2011年10月18日（火）の 15：30 から以下ように Barcelona 大学の Joan Bagaria 教授による Omega-logic, the Omega-conjecture, and the Continuum Hypothesis に関する神戸情報数理コロキウムの講演を予定しております．講演者の Joan Bagaria 氏には，集合論の専門の方だけでなくロジック全般の general audience 向けの講演になるよう，お願いしてあります．興味のある方は御参加ください． o なお，同日の 14:00 からは Sam Sanders 氏（東北大学）の同コロキウムでの講演も予定されています． o また，この講演会の前日の 10月17日 (月) の午後には，Slawomir Solecki, S.M. Srivastava, Tamas Matrai 三氏の講演が同じ場所で予定されています (Fri, 7 Oct 2011 10:11:28 +0900 の logic mailing list の Joerg Brendle 氏による案内を参照) . - ---------------------------------------------------------------------------------- 神戸情報数理コロキウム日時：2011年10月18日（火）15:30 ～ 17:00 場所：神戸大学自然科学総合研究棟3号館4階421室（渕野グループ内プレゼンテーション室）講演者： Joan Bagaria (バルセロナ大学) 題目： Omega-logic, the Omega-conjecture, and the Continuum Hypothesis アブストラクト： Abstract: In 1990, W. Hugh Woodin introduced Omega-logic as an approach to truth in the universe of all sets inspired by recent work on large cardinals and determinacy. In Omega-logic statements are valid if, roughly, they hold in every forcing extension of the universe, or its sufficiently rich initial segments. Thus, Omega-logic is the logic of generic absoluteness. In these talks we will describe the basic features of Omega-logic, leading to the formulation of the Omega-conjecture and a discussion of its relevance in current set- theoretic research. In particular I shall focus on Woodin's arguments against the vagueness of the Continuum Hypothesis. - -- best regards Saka\'e Fuchino (渕野昌) - ------------------------------------------------------------------------- Kobe University Graduate School of System Informatics Rokko-dai 1-1, Nada, Kobe 657-8501 e-mail: fuchino(a)diamond.kobe-u.ac.jp web page: http://kurt.scitec.kobe-u.ac.jp/~fuchino/ - -------------------------------------------------------------------------

1 0

RTA 2012: First Call For Papers
by Nao Hirokawa 11 Oct '11

11 Oct '11

RTA 2012 の論文募集をご案内致します。今回の RTA は名古屋で開催されます。ぜひ投稿をご検討下さい。廣川　直（北陸先端科学技術大学院大学） - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - ******************************************************** * First Call For Papers * * RTA 2012 * * Rewriting Techniques and Applications * * 23rd International Conference * * * * May 28 - Jun 2, 2012, Nagoya, Japan * * http://rta2012.trs.cm.is.nagoya-u.ac.jp/ * * * ******************************************************** The 23rd International Conference on Rewriting Techniques and Applications (RTA 2012) is the major forum for the presentation of research on rewriting. IMPORTANT DATES: Abstract: Jan 04, 2012 Paper Submission: Jan 09, 2012 Notification: Mar 02, 2012 Final version: Mar 26, 2012 RTA 2012 seeks original submissions on all aspects of rewriting. Typical areas of interest include (but are not limited to): * Applications: case studies; analysis of cryptographic protocols; rule-based (functional and logic) programming; symbolic and algebraic computation; SMT solving; theorem proving; system synthesis and verification; proof checking; reasoning about programming languages and logics; program transformation; XML queries and transformations; systems biology; * Foundations: equational logic; rewriting logic; rewriting models of programs; matching and unification; narrowing; completion techniques; strategies; rewriting calculi; constraint solving; tree automata; termination; complexity; combination; * Frameworks: string, term, and graph rewriting; lambda-calculus and higher-order rewriting; constrained rewriting/deduction; categorical and infinitary rewriting; stochastic rewriting; net rewriting; binding techniques; Petri nets; * Implementation: implementation techniques; parallel execution; rewrite and completion tools; confluence and termination checking; certification of rewriting properties; abstract machines; explicit substitutions; BEST PAPER AWARD: An award is given to the best paper or papers as decided by the program committee. STUDENT SUPPORT: Limited student support will be available and announced in future versions of this call. PROGRAMME COMMITTEE CHAIR: * Ashish Tiwari SRI International, Menlo Park, CA http://www.csl.sri.com/users/tiwari PROGRAMME COMMITTEE: * Andreas Abel Ludwig-Maximilians-University Munich * Zena Ariola University of Oregon * Paolo Baldan Università degli Studi di Padova * Ahmed Bouajjani University of Paris 7 * Evelyne Contejean LRI Université Paris-Sud-CNRS * Irène Anne Durand LaBRI Université of Bordeaux * Jörg Endrullis Vrije Universiteit Amsterdam * Silvio Ghilardi Università degli Studi di Milano * Guillem Godoy Universidad Politécnica de Cataluña * Nao Hirokawa Japan Advanced Institute of Science and Technology * Deepak Kapur University of New Mexico, Albuquerque, NM * Jordi Levy IIIA - CSIC * Paul-Andre Mellies University of Paris 7 * Pierre-Etienne Moreau Ecole des Mines de Nancy * Joachim Niehren INRIA Lille * Grigore Rosu University of Illinois at Urbana-Champaign * Albert Rubio Universidad Politécnica de Cataluña * Masahiko Sakai Nagoya University * Carolyn Talcott SRI International * René Thiemann University of Innsbruck CONFERENCE CHAIR: * Masahiko Sakai Nagoya University PUBLICATION: RTA proceedings will be published by LIPIcs (Leibniz International Proceedings in Informatics). LIPIcs is open access, meaning that publications will be available online and free of charge, and authors keep the copyright for their papers. LIPIcs publications are indexed in DBLP. STACS, FSTTCS and ICLP proceedings also appear in LIPIcs. See http://www.dagstuhl.de/lipics for more information about LIPIcs. Accepted papers will be considered for publication in a special issue of the journal Logical Methods in Computer Science (LMCS). SUBMISSIONS: Submissions must be original and not submitted for publication elsewhere. Submission categories include regular research papers, applications of rewriting techniques, problem sets, and system descriptions. The page limit for submissions is 10 proceedings pages for system descriptions and 15 proceedings pages for all other categories. Additional material may be provided in an appendix which is not subject to the page limit. However, submissions must be self-contained within the respective page limit; reading the appendix should not be necessary to assess the merits of a submission. Submissions are accepted in either Postscript or PDF format. LaTeX template for LIPIcs is available at: http://drops.dagstuhl.de/styles/lipics/lipics-authors.tgz Abstracts and papers must be submitted electronically through the EasyChair system at: http://www.easychair.org/conferences/?conf=RTA2012 Questions concerning submissions may be addressed to the PC chair, Ashish Tiwari by emailing ashish_dot_tiwari_at_sri_dot_com

1 0

PEPM'12 - DEADLINE EXTENSION
by Kohei SUENAGA 11 Oct '11

11 Oct '11

logic-ml の皆様、 # 複数受け取られた場合はどうぞご容赦ください。京都大学の末永と申します。 PEPM 2012 の締切が延長されました。新しい締切は10月16日の23:59 GMTで、日本時間で10月17日（月）の08:59です。先日お知らせしました通り、ショートペーパーやツールペーパーも絶賛募集中です。また、Journal Special Issue も出る予定です。どうぞ投稿をご検討下さい末永幸平京都大学大学院情報学研究科 ksuenaga(a)sato.kuis.kyoto-u.ac.jp -- PEPM'12 - DEADLINE EXTENSION Due to a number of requests for extensions, the deadline for submission to PEPM'12 has been extended until 23:59 GMT on Sunday 16 October. We would like to remind you about three aspects of PEPM. Journal Special Issue There will be a journal special issue for PEPM'12. PEPM'09 has already appeared in Higher-order and Symbolic Computation (HOSC, online-first edition this year), and the special issue based on PEPM'10 papers has just been delivered to the HOSC editorial team. Short papers We're looking for short papers (up to 4pp) and tool papers as well as full research papers. All categories of papers will appear in the formal ACM proceedings. Tool papers The main purpose of a tool paper is to display other researchers in the PEPM community a completed, robust and well-documented tool; more guidance on the format and expected contact is given on the PEPM 2012 web site. In contrast with regular PEPM submissions, PEPM tool demo papers may include work that has been published elsewhere. In the ideal case, the technical foundations of the tool will have been published previously, and the submitted PEPM tool paper will report on follow-on work that has produced a robust tool that has been applied to interesting examples. The PEPM program committee will consider accepting tool demo papers that describe tools that have been presented at other conferences/ workshops if these conferences/ workshops belong to a different community (the authors should acknowledge the previous demos and justify the benefits of presenting the tool again for the PEPM audience). Call For Papers ACM SIGPLAN 2012 Workshop on Partial Evaluation and Program Manipulation January 23-24, 2012. Philadelphia, Pennsylvania, USA (co-located with POPL'12) http://www.program-transformation.org/PEPM12 Paper submission deadline: Sunday, October 16, 2011, 23:59, GMT The PEPM Symposium/Workshop series aims to bring together researchers and practitioners working in the broad area of program transformation, which spans from refactoring, partial evaluation, supercompilation, fusion and other metaprogramming to model-driven development, program analyses including termination, inductive programming, program generation and applications of machine learning and probabilistic search. PEPM focuses on techniques, supporting theory, tools, and applications of the analysis and manipulation of programs. Each technique or tool of program manipulation should have a clear, although perhaps informal, statement of desired properties, along with an argument how these properties could be achieved. Topics of interest for PEPM'12 include, but are not limited to: - Program and model manipulation techniques such as: supercompilation, partial evaluation, fusion, on-the-fly program adaptation, active libraries, program inversion, slicing, symbolic execution, refactoring, decompilation, and obfuscation. - Program analysis techniques that are used to drive program/model manipulation such as: abstract interpretation, termination checking, binding-time analysis, constraint solving, type systems, automated testing and test case generation. - Techniques that treat programs/models as data objects including metaprogramming, generative programming, embedded domain-specific languages, program synthesis by sketching and inductive programming, staged computation, and model-driven program generation and transformation. - Application of the above techniques including case studies of program manipulation in real-world (industrial, open-source) projects and software development processes, descriptions of robust tools capable of effectively handling realistic applications, benchmarking. Examples of application domains include legacy program understanding and transformation, DSL implementations, visual languages and end-user programming, scientific computing, middleware frameworks and infrastructure needed for distributed and web-based applications, resource-limited computation, and security. To maintain the dynamic and interactive nature of PEPM, we will continue the category of `short papers' for tool demonstrations and for presentations of exciting if not fully polished research, and of interesting academic, industrial and open-source applications that are new or unfamiliar. Student attendants with accepted papers can apply for a SIGPLAN PAC grant to help cover travel expenses and other support. All accepted papers, short papers included, will appear in formal proceedings published by ACM Press and will be included in the ACM Digital Library. Selected papers may later on be invited for a journal special issue dedicated to PEPM'12. Submission Categories and Guidelines Authors are strongly encouraged to consult the advice for authoring research papers and tool papers before submitting. The PC Chairs welcome any inquiries about the authoring advice. Regular research papers must not exceed 10 pages in ACM Proceedings style. Short papers are up to 4 pages in ACM Proceedings style. Authors of tool demonstration proposals are expected to present a live demonstration of the described tool at the workshop (tool papers should include an additional appendix of up to 6 extra pages giving the outline, screenshots, examples, etc. to indicate the content of the proposed live demo at the workshop). Important Dates - Paper submission: Sunday, October 16, 2011, 23:59, GMT - Author notification: Tue, November 8, 2011 - Workshop: Mon-Tue, January 23-24, 2012 Invited Speakers - Markus Pueschel (ETH Zurich, Switzerland) - Martin Berger (University of Sussex, UK) Program Chairs - Oleg Kiselyov (Monterey, CA, USA) - Simon Thompson (University of Kent, UK) Program Committee Members - Emilie Balland (INRIA, France) - Ewen Denney (NASA Ames Research Center, USA) - Martin Erwig (Oregon State University, USA) - Sebastian Fischer (National Institute of Informatics, Japan) - Lidia Fuentes (Universidad de Malaga, Spain) - John Gallagher (Roskilde University, Denmark and IMDEA Software, Spain) - Dave Herman (Mozilla Research, USA) - Stefan Holdermans (Vector Fabrics, the Netherlands) - Christian Kaestner (University of Marburg, Germany) - Emanuel Kitzelmann (International Computer Science Institute, USA) - Andrei Klimov (Keldysh Institute of Applied Mathematics, Russian Academy of Sciences) - Shin-Cheng Mu (Academia Sinica, Taiwan) - Alberto Pardo (Universidad de la Repu'blica, Uruguay) - Kostis Sagonas (Uppsala University, Sweden and National Technical University of Athens, Greece) - Anthony M. Sloane (Macquarie University, Australia) - Armando Solar-Lezama (MIT, USA) - Aaron Stump (The University of Iowa, USA) - Kohei Suenaga (University of Kyoto, Japan) - Eric Van Wyk (University of Minnesota, USA) - Kwangkeun Yi (Seoul National University, Korea)

1 0

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Logic-ml October 2011