- Logic-ml - fos.kuis.kyoto-u.ac.jp

論理哲学ワークショップ 2月27日(金) / Workshop on Philosophy of Logic, Feb 27th (Fri)
by Yuta Takahashi 25 Feb '15

25 Feb '15

みなさま、こんにちは、慶応大学の高橋優太と申します。この場をお借りして、次のワークショップをお知らせさせていただきます。重複して受け取られた場合はどうかご容赦ください。 ---- 論理哲学ワークショップ 2月27日(金) / Workshop on Philosophy of Logic, Feb 27th (Fri) 次のような「論理哲学ワークショップ」を予定しております。今回は特に、現代論理の歴史的背景についても議論します。参加自由です。 The following Workshop on Philosophy of Logic is scheduled. The historical background of some modern logic will be discussed among others. 日時/Date&Time: 2015年2月27日(金) 14:00-17:00, Feb 27 (Fri), 2015 場所: 慶應大学三田キャンパス南館地下4階ディスタンスラーニングルーム Place: Distance Learning Room (Basement 4F), South Building, Mita campus of Keio University. ( http://www.keio.ac.jp/en/maps/mita.html 13番の建物です。/ Building #13 on this map. ) ---- 1. Speaker: Juan Luis Gastaldi (IRePH, Université Paris Ouest Nanterre La Défense) Title: The relation between logical content and arithmetic in the semiotic constitution of Boolean logic 2. Speaker: Yuta Takahashi (Keio University) Title: The Intuitionistic Background of Gentzen's 1935/36 Consistency Proofs --------------------------------------------------------------------- 問合せ先: Mita Logic Seminar 思考と行動判断の研究拠点事務局 logic(a)abelard.flet.keio.ac.jp ABSTRACTS ENCLOSED BELOW: 1. Speaker: Juan Luis Gastaldi (IRePH, Université Paris Ouest Nanterre La Défense) Title: The relation between logical content and arithmetic in the semiotic constitution of Boolean logic Abstract: After the publication of his Begriffsschrift, Frege distanced himself from the Booleans by insistently opposing the content that his logic was able to express to the abstraction of Boolean logic. Frege’s commitment to the notion of content would last until the end of his work, becoming in particular the source of his famous distinction between sense and denotation. But what did Frege exactly mean by this opposition between “contentual” (inhaltlich) and abstract, as a properties of logical systems? A semiotic perspective on the constitution of Boolean logic shows that this distinction can be associated with the one between Arithmetic and Algebra, considered as different mathematical practices on signs respectively underpinning the constitution of these two logical systems. Moreover, a particular attention paid to Boole's own voluntary deviations from what would soon become the standard Boolean system permits to identify different figures of what can be seen as a content dimension arising as a logical effect of the semiotic properties of Arithmetic. 2. Speaker: Yuta Takahashi (Keio University) Title: The Intuitionistic Background of Gentzen's 1935/36 Consistency Proofs Abstract: Gerhald Gentzen gave three consistency proofs for number theory. These consistency proofs have a common aim that originates from Hilbert's Program. Hilbert, in his program, aimed to justify the use of ideal propositions in mathematics, by showing that no contradiction can be derived in a formal system of the ideal parts of mathematics. Gentzen aimed to justify the use of ideal propositions in number theory, and this aim is prominent especially in Gentzen's 1938 consistency proof. In Gentzen's 1935/36 consistency proofs, there is another aim that is not found in Hilbert's Program. The aim is to formulate a ``finitary'' interpretation that gives a meaning to every ideal proposition of number theory and makes the theory sound. In this talk, first we argue that what motivated Gentzen to give such an interpretation is an intuitionists' objection against the significance of consistency proofs. Second, we show that his way of the interpretation appealed to a notion being very close to the notion of spreads, which was introduced in intuitionistic mathematics. As a consequence, we claim that intuitionism was deeply related to both Gentzen's motivation and method for the interpretation. END OF ANNOUNCEMENT------------------------------------------------

1 0

KusatsuSeminar3/16--20: just a reminder
by Fujita Kenetsu 24 Feb '15

24 Feb '15

皆様，『ラムダ計算と論理の早春セミナー』のご案内　（再送）日程：2015年3月16日(月) 午後5時から3月20日(金) 正午まで場所：国立大学草津セミナーハウス　　　〒377-1711 群馬県吾妻郡草津町大字草津字白根737 詳細：http://www.cs.gunma-u.ac.jp/~fujita/2015.03LLSinKusatsu.htm 申込・質問などは藤田（群馬大学）までご連絡をお願いします．興味をお持ちのみなさまのご参加をお待ちしております． ----------- 群馬大学　藤田憲悦

1 0

論理哲学ワークショップ 2月27日(金) / Workshop on Philosophy of Logic, Feb 27th (Fri)
by Yuta Takahashi 24 Feb '15

24 Feb '15

みなさま、こんにちは、慶応大学の高橋優太と申します。この場をお借りして、次のワークショップのご案内をさせていただきます。重複して受け取られた場合はご容赦ください。 ---- 論理哲学ワークショップ 2月27日(金) / Workshop on Philosophy of Logic, Feb 27th (Fri) 次のような「論理哲学ワークショップ」を予定しております。今回は特に、現代論理の歴史的背景についても議論します。参加自由です。 The following Workshop on Philosophy of Logic is scheduled. The historical background of some modern logic will be discussed among others. 日時/Date&Time: 2015年2月27日(金) 14:00-17:00, Feb 27 (Fri), 2015 場所: 慶應大学三田キャンパス南館地下4階ディスタンスラーニングルーム Place: Distance Learning Room (B4F), South Building, Mita campus of Keio University. ---- 1. Speaker: Juan Luis Gastaldi (IRePH, Université Paris Ouest Nanterre La Défense) Title: The relation between logical content and arithmetic in the semiotic constitution of Boolean logic 2. Speaker: Yuta Takahashi (Keio University) Title: The Intuitionistic Background of Gentzen's 1935/36 Consistency Proofs --------------------------------------------------------------------- 問合せ先: Mita Logic Seminar 思考と行動判断の研究拠点事務局 logic(a)abelard.flet.keio.ac.jp ABSTRACTS ENCLOSED BELOW: 1. Speaker: Juan Luis Gastaldi (IRePH, Université Paris Ouest Nanterre La Défense) Title: The relation between logical content and arithmetic in the semiotic constitution of Boolean logic Abstract: After the publication of his Begriffsschrift, Frege distanced himself from the Booleans by insistently opposing the content that his logic was able to express to the abstraction of Boolean logic. Frege’s commitment to the notion of content would last until the end of his work, becoming in particular the source of his famous distinction between sense and denotation. But what did Frege exactly mean by this opposition between “contentual” (inhaltlich) and abstract, as a properties of logical systems? A semiotic perspective on the constitution of Boolean logic shows that this distinction can be associated with the one between Arithmetic and Algebra, considered as different mathematical practices on signs respectively underpinning the constitution of these two logical systems. Moreover, a particular attention paid to Boole's own voluntary deviations from what would soon become the standard Boolean system permits to identify different figures of what can be seen as a content dimension arising as a logical effect of the semiotic properties of Arithmetic. 2. Speaker: Yuta Takahashi (Keio University) Title: The Intuitionistic Background of Gentzen's 1935/36 Consistency Proofs Abstract: Gerhald Gentzen gave three consistency proofs for number theory. These consistency proofs have a common aim that originates from Hilbert's Program. Hilbert, in his program, aimed to justify the use of ideal propositions in mathematics, by showing that no contradiction can be derived in a formal system of the ideal parts of mathematics. Gentzen aimed to justify the use of ideal propositions in number theory, and this aim is prominent especially in Gentzen's 1938 consistency proof. In Gentzen's 1935/36 consistency proofs, there is another aim that is not found in Hilbert's Program. The aim is to formulate a ``finitary'' interpretation that gives a meaning to every ideal proposition of number theory and makes the theory sound. In this talk, first we argue that what motivated Gentzen to give such an interpretation is an intuitionists' objection against the significance of consistency proofs. Second, we show that his way of the interpretation appealed to a notion being very close to the notion of spreads, which was introduced in intuitionistic mathematics. As a consequence, we claim that intuitionism was deeply related to both Gentzen's motivation and method for the interpretation. END OF ANNOUNCEMENT------------------------------------------------

1 0

千葉 logic seminar
by arai toshiyasu 23 Feb '15

23 Feb '15

みなさま新井@千葉大学です。千葉 logic seminar の第5回のお知らせです。どなたでも参加できますのでどうぞ気軽にいらっしゃって下さい。問合せ先新井敏康（千葉大学） tosarai(a)faculty.chiba-u.jp ------------------------------------------ 日時：3月13日(金)13:30-15:00 場所：千葉大学理学部2号館105号室アクセスは http://www.chiba-u.ac.jp/campus_map/nishichiba/index.html の地図の黄色い理学部の中で数字2が付いている建物の1階です。 Speaker: Stan Wainer (Leeds UK) Title: A miniaturized predicativity Abstract: This talk attempts to characterize those recursive functions which are "predictably terminating" according to a finitistic point of view. The basis of the work is Leivant's (1995) theory of ramified induction over N, which has elementary recursive strength. It has been redeveloped and extended in various ways by many people. Eg. Spoors & W. (2012) built a hierarchy of ramified "input-output" theories whose strengths correspond to the levels of the Grzegorczyk hierarchy. Here, a further extension of this hierarchy is developed, with one additional input level on top (level omega). The underlying logic is an autonomously generated infinitary calculus with arbitrary finitely-many stratification levels of numerical inputs and a ramified Repetition Rule. The autonomous control on allowable ordinals is based on a weak (finitistic) notion of "pointwise transfinite induction". It turns out that the ordinal of this theory is then Gamma-0; the provably computable functions are those which are resource-bounded by the slow growing hierarchy; and these are the functions elementary recursive in the Ackermann function. ------------------------------------------------------------------------------------------

1 0

鈴木右京のセミナー (名古屋大学にて)
by Jacques Garrigue 20 Feb '15

20 Feb '15

logic-mlの皆さん、名古屋大学多元数理科学研究科のJacques Garrigueです。突然ですが、以下のセミナーを開催しますので、ご案内申し上げます。講演者:　鈴木佑京（東京大学大学院広域科学科）日時:　　2月24日（火）　10:30--12:00と13:00--14:30 会場:　　名古屋大学　理学A館　A328号室タイトル:　可述算術の世界アブストラクト: エドワード・ネルソンは、古典的算術に対するオルタナティブでありながら、直観主義的算術や有限主義的算術とも異なる――より徹底した構成主義の立場に立つ ――自然数論として、「可述算術」と呼ばれる理論を提案した。彼の理論は、後の限定算術の研究に影響をあたえるとともに、数学的帰納法に関する独特な分析を含んでおり、極めて興味深い。この講演では、１）まずネルソンの構成主義的な思想を説明した後、２）可述算術の数学的展開を解説することで、まず可述算術に対するイントロダクションを行う。そののち、３）ネルソンのような改訂主義とは異なる、講演者自身の観点から、可述算術の持つ概念的な興味を解説する。ここでは、可述算術が、ウィトゲンシュタインなどが展開した「概念形成としての数学」という描像をモデル化したものであることが主張される。

1 0

鈴木右京のセミナー (名古屋大学にて)
by Jacques Garrigue 20 Feb '15

20 Feb '15

1 0

Call for Papers: Hilbert’s Epsilon and Tau in Logic, Informatics and Linguistics
by Makoto Kanazawa 18 Feb '15

18 Feb '15

Call for Papers Hilbert’s Epsilon and Tau in Logic, Informatics and Linguistics Dates: June 10-12, 2015 Location: Montpellier, France Workshop Webpage: https://sites.google.com/site/epsilon2015workshop/ Contact email: Epsilon2015(a)easychair.org Submission deadline: April 1st, 2015 Submission webpage: https://easychair.org/conferences/?conf=epsilon2015 Organizers / workshop co-chairs: Stergios Chatzikyriakidis, LIRMM-CNRS, University of Montpellier Fabio Pasquali, University of Marseille Christian Retoré, University of Montpellier & LIRMM-CNRS Host: I2M-CNRS and University of Montpellier Workshop information: This workshop aims at promoting work on Hilbert’s epsilon calculus in a number of relevant fields ranging from Philosophy and Mathematics to Linguistics and Informatics. The Epsilon and Tau operators were introduced by David Hilbert, inspired by Russell's Iota operator for definite descriptions, as binding operators that form terms from formulae. One of their main features is that substitution with Epsilon and Tau terms expresses quantification. This leads to a calculus which is a strict and conservative extension of First Order Predicate Logic. The calculus was developed for studying first order logic in view of the program of providing a rigorous foundation of mathematics via syntactic consistency proofs. The first relevant outcomes that certainly deserve a mention are the two "Epsilon Theorems" (similar to quantifiers elimination), the first correct proof of Herbrand’s theorem or the use of the Epsilon operator in Bourbaki’s Éléments de Mathématique. Nowadays the interest in the Epsilon substitution method has spread in a variety of fields: Mathematics, Logic, Philosophy, History of Mathematics, Linguistic, Type Theory, Computer science, Category Theory and others. Submission The workshop welcomes submissions of up to 4 (but not less than 2) pages. Usual spacing, font and margin should be used (single-spaced, 11pt or larger, and 1 inch margin on A4 or letter size paper). Abstracts should be submitted by April 1st, 2015 as pdf files through the EasyChair conference system ( https://easychair.org/conferences/?conf=epsilon2015). An indicative list of themes that are of particular interest to the conference are (non-exhaustive): - History of Logic - Philosophy - Proof theory - Model theory - Category theory - Type theory - Quantification in Natural language - Noun-Phrases Semantics - Proof Assistants (e.g. Coq, Isabelle, ... ) - Other subnectors (e.g. Russell's iota, μ-operator, ... ) Reviewing: Abstracts will be reviewed by members of the program committee, and, where appropriate, outside reviewers. The organizers will be responsible for making decisions partly in consultation with the program committee. Notifications will be made by May 1st, 2015. Post-Proceedings: Selected papers from the workshop will appear as a special volume in Journal of Logics and their Applications Important dates: April 1st, 2015: Submission deadline May 1st,2015: Notification of acceptance June 10-12, 2015: Workshop Invited speakers: Claus-Peter Wirth (University of Saarland): The descriptive operators iota, tau and epsilon - on their origin, partial and complete specification, model- theoretic semantics, practical applicability (with the support of the Hilbert Bernays Project (sponsored by IFCoLog)). Vito Michele Abrusci (University of Roma Tre): Hilbert's tau and epsilon in proof theory. Hartley Slater (University of Western Australia): Linguistic and philosophical ramifications of the epsilon calculus. Program Committee: Daisuke Bekki (Ochanomizu University) Stergios Chatzikyriakidis (LIRMM-CNRS & University of Montpellier) Francis Corblin (University of Paris-Sorbonne & Institut Jean Nicod CNRS) Michael Gabbay (University of Cambridge) Makoto Kanazawa (National Institute of Informatics of Tokyo) Ruth Kempson (King's College, London) Alda Mari (CNRS Institut Jean Nicod & ENS & EHESS) Georg Moser (University of Innsbruck) Bruno Woltzenlogel Paleo (Vienna University of Technology) Michel Parigot (CNRS-PPS & University of Paris Diderot 7) Fabio Pasquali (University of Aix-Marseille & I2M CNRS) Christian Retoré (University of Montpellier & LIRMM-CNRS) Mark Steedman (University of Edimburgh) Richard Zach (University of Calgary)

1 0

PPL2015最終参加募集：第17回プログラミングおよびプログラミング言語ワークショップ
by Kazutaka Matsuda 16 Feb '15

16 Feb '15

logic-ml関係者の皆様，東京大学の松田です．複数受け取られた場合はご容赦ください． 3月4日（水）から3月6日（金）に道後温泉で開催される第17回プログラミングおよびプログラミング言語ワークショップ (PPL2015) の参加募集の締切が2/17とせまっておりますので，再度の参加募集のご案内をお届けいたします．今回は， * 橋本和幸 (NVIDIA. 元日本シンボリックス株式会社) 「1980年代のLispマシンSymbolicsとその開発環境Genera 付属：NVIDIA GPUによる超並列コンピューティング」 * Chung-Kil Hur (Seoul National University) 「Formal C semantics and LLVM compiler validation」の二件の招待講演を予定しております．暫定プログラムを公開いたしました． http://www-kb.is.s.u-tokyo.ac.jp/ppl2015/programme/tentative.txt カテゴリ1，2，4の採択論文・発表のリストも http://www-kb.is.s.u-tokyo.ac.jp/ppl2015/accepted.html ご参考ください．参加登録の案内ページは http://www-kb.is.s.u-tokyo.ac.jp/ppl2015/registration/ です．参加登録の締切は2月17日（火）です．どうぞお早めのご登録をお願い致します．多くの方々のご参加をお待ちしております． -------------------------------------------------------------------------- 第17回プログラミングおよびプログラミング言語ワークショップ（PPL2015） http://www-kb.is.s.u-tokyo.ac.jp/ppl2015/ 参加登録のご案内主催: 日本ソフトウェア科学会プログラミング論研究会日程: 2015年3月4日(水)～3月6日(金) 会場: 愛媛県松山市道後温泉「道後プリンスホテル」 http://www.dogoprince.co.jp/ PPL2015は、プログラミングおよびプログラミング言語に関する研究者が一堂に会し、最新の研究成果の発表、および新たな研究課題についての討論やアイディア交換等を行うことを目的とした、合宿形式のワークショップです． ====================================================================== 参加登録ならびに宿泊予約を2月17日(火)まで日本旅行のWebサービスにて受け付けております． http://www-kb.is.s.u-tokyo.ac.jp/ppl2015/registration/ をご参照いただき，ご登録ください．問い合わせ先：ppl2015-oc [at] kb.is.s.u-tokyo.ac.jp （[at]を@に置き換えてください） ====================================================================== プログラム委員会青戸等人東北大学浅田和之東京大学岩崎英哉電気通信大学鵜川始陽高知工科大学馬谷誠二京都大学 [プログラム共同委員長] 大岩寛産業技術総合研究所亀山幸義筑波大学河内谷清久仁日本IBM 久野靖筑波大学木村大輔国立情報学研究所宋剛秀神戸大学塚田武志 University of Oxford 中田景子 FireEye DresDen 浜名誠群馬大学 [プログラム共同委員長] 平井洋一 FireEye Dresden 平石拓京都大学藤田憲悦群馬大学星野直彦京都大学増原英彦東京工業大学渡部卓雄東京工業大学組織委員会松田一孝東京大学 [組織委員長] 浜名誠群馬大学 [プログラム共同委員長] 馬谷誠二京都大学 [プログラム共同委員長] 末永幸平京都大学上野雄大東北大学海野広志筑波大学木村大輔国立情報学研究所 [ポスターセッション幹事] --------------------------------------------------------------------------

1 0

PPL2015参加募集：第17回プログラミングおよびプログラミング言語ワークショップ
by Kazutaka Matsuda 13 Feb '15

13 Feb '15

logic-mlの皆様，東京大学の松田です．複数受け取られた場合はご容赦ください． 3月4日（水）から3月6日（金）に道後温泉で開催される第17回プログラミングおよびプログラミング言語ワークショップ (PPL2015) の参加募集のご案内をお届けいたします．今回は， * 橋本和幸 (NVIDIA. 元日本シンボリックス株式会社) 「1980年代のLispマシンSymbolicsとその開発環境Genera 付属：NVIDIA GPUによる超並列コンピューティング」 * Chung-Kil Hur (Seoul National University) 「Formal C semantics and LLVM compiler validation」の二件の招待講演を予定しております．また，カテゴリ1，2，4の採択論文・発表のリストは http://www-kb.is.s.u-tokyo.ac.jp/ppl2015/accepted.html からご欄になれます．多くの方々のご参加をお待ちしております．参加登録の案内ページは http://www-kb.is.s.u-tokyo.ac.jp/ppl2015/registration/ です．参加登録の締切は2月17日（火）です．どうぞお早めのご登録をお願い致します．今年は昨年と異なり，*三日目は15:30終了予定*となります．ご注意ください． -------------------------------------------------------------------------- 第17回プログラミングおよびプログラミング言語ワークショップ（PPL2015） http://www-kb.is.s.u-tokyo.ac.jp/ppl2015/ 参加登録のご案内主催: 日本ソフトウェア科学会プログラミング論研究会日程: 2015年3月4日(水)～3月6日(金) 会場: 愛媛県松山市道後温泉「道後プリンスホテル」 http://www.dogoprince.co.jp/ PPL2015は、プログラミングおよびプログラミング言語に関する研究者が一堂に会し、最新の研究成果の発表、および新たな研究課題についての討論やアイディア交換等を行うことを目的とした、合宿形式のワークショップです． ====================================================================== 参加登録ならびに宿泊予約を2月17日(火)まで日本旅行のWebサービスにて受け付けております． http://www-kb.is.s.u-tokyo.ac.jp/ppl2015/registration/ をご参照いただき，ご登録ください．問い合わせ先：ppl2015-oc [at] kb.is.s.u-tokyo.ac.jp （[at]を@に置き換えてください） ====================================================================== プログラム委員会青戸等人東北大学浅田和之東京大学岩崎英哉電気通信大学鵜川始陽高知工科大学馬谷誠二京都大学 [プログラム共同委員長] 大岩寛産業技術総合研究所亀山幸義筑波大学河内谷清久仁日本IBM 久野靖筑波大学木村大輔国立情報学研究所宋剛秀神戸大学塚田武志 University of Oxford 中田景子 FireEye DresDen 浜名誠群馬大学 [プログラム共同委員長] 平井洋一 FireEye Dresden 平石拓京都大学藤田憲悦群馬大学星野直彦京都大学増原英彦東京工業大学渡部卓雄東京工業大学組織委員会松田一孝東京大学 [組織委員長] 浜名誠群馬大学 [プログラム共同委員長] 馬谷誠二京都大学 [プログラム共同委員長] 末永幸平京都大学上野雄大東北大学海野広志筑波大学木村大輔国立情報学研究所 [ポスターセッション幹事] --------------------------------------------------------------------------

1 0

講演会(Pawel Parys氏）
by koba 10 Feb '15

10 Feb '15

東京大学の小林と申します。以下のように、ワルシャワ大学のPawel Parys氏を招いて講演会を開催しますので、ふるってご参加ください。 Parysさんは、ここ数年、高階文法、高階プッシュダウンオートマトンなどについて未解決問題を解いたりしてよい仕事をされている方です小林直樹東京大学大学院情報理工学系研究科コンピュータ科学専攻〒113-0033 東京都文京区本郷7-3-1 Phone: 03-5841-4124 Fax: 03-5841-4124 email: koba(a)is.s.u-tokyo.ac.jp ---------------------------------- Time: 2月18日（水） 15:00〜 Place: 理学部7号館 214号室 Title: A Characterization of Lambda-terms Transforming Numbers Speaker: Pawel Parys (Warsaw University) Abstract: It is well known, that simply-typed lambda-terms can be used to represent numbers, as well as some other data types. We show that lambda-terms of each fixed (but possibly very complicated) type can be described by a finite piece of information (a set of appropriately defined intersection types) and by a vector of natural numbers. On one hand the description is compositional: having only the finite piece of information for two closed lambda-terms M and N, we can determine its counterpart for MN, and a linear transformation that applied to the vectors of numbers for M and N gives us the vector for MN. On the other hand, when a lambda-term represents a natural number, then this number is approximated by a number in the vector corresponding to this lambda-term. As a consequence, we prove that in a lambda-term of a fixed type we can store only a fixed number of natural numbers, in such a way that they can be extracted using lambda-terms. More precisely, while representing k numbers in a closed lambda-term of some type we only require that there are k closed lambda-terms M1,...,Mk such that Mi takes as argument the lambda-term representing the k-tuple, and returns the i-th number in the tuple (we do not require that, using lambda-calculus, one can construct the representation of the k-tuple out of the k numbers in the tuple). Moreover, the same result holds when we allow that the numbers can be extracted approximately, up to some error (even when we only want to know whether a set is bounded or not). All the results remain true when we allow the Y combinator (recursion) in our lambda-terms, as well as uninterpreted constants.

1 0

Prof. Georg Moser at NII Logic Seminar
by Makoto Tatsuta 07 Feb '15

07 Feb '15

Prof. Georg Moser at NII Logic Seminar Date: February 13, 2015, 14:00--16:00 Place: National Institute of Informatics, Room 1208 (12th floor) 場所: 国立情報学研究所 12階 1208室 (半蔵門線,都営地下鉄三田線・新宿線神保町駅または東西線竹橋駅より徒歩5分) (地図 http://www.nii.ac.jp/about/access/) Speaker: Prof. Georg Moser (University of Innsbruck) Title: Amortised Cost Analysis and Term Rewrite Systems Abstract: I will present a univariate resource analysis for typed term rewrite systems based on a potential-based type system. This type system gives rise to polynomial bounds on the innermost runtime complexity. The thus obtained amortised resource analysis relates to polynomial interpretations and we obtain the perhaps surprising result that whenever a rewrite system can be well-typed, then there exists a polynomial interpretation that orients the system. If time permits I'll speak about very recent generalisations to a multivariate analysis. This is a joint work with Martin Hofmann. 問合せ先: 龍田真 (国立情報学研究所) e-mail: tatsuta(a)nii.ac.jp http://research.nii.ac.jp/~tatsuta

1 0

Fwd: [PVS] Topics in Theoretical Computer Science 205 (Tehran, Iran) -- Call for Papers
by Ichiro Hasuo 04 Feb '15

04 Feb '15

みなさま，東京大学の蓮尾です．8月にテヘランで行われる国際会議 TTCS の案内をお送りします．ICALP や TCS のように track A/B に分かれていて，スコープの広い会議です．ぜひ投稿をご検討ください．また，お近くの研究者のみなさん（特にこのメールが届かない，アルゴリズム系のみなさま）にこのメールを転送いただけると助かります．どうかよろしくお願いいたします．蓮尾一郎 http://www-mmm.is.s.u-tokyo.ac.jp/ (apologies if you receive multiple copies) ========================================= Topics in Theoretical Computer Science (TTCS 2015) http://www.ttcs.ir/ Institute for Research in Fundamental Sciences (IPM), Tehran, Iran August 26-28, 2015 ========================================= Scope ________________________________ TTCS is a new bi-annual conference series, intending to serve as a forum for novel and high-quality research in all areas of Theoretical Computer Science. The conference is held in cooperation with the European Association for Theoretical Computer Science. There will be a number of satellite events at TTCS, These will feature presentation of early research results, and position papers. There will also be a forum for Ph.D. students to receive comments about their ongoing research projects. Topics of interest include but are not limited to: algebra and co-algebra in computer science, algorithms and data structures, algorithmic coding theory, algorithmic graph theory and combinatorics, approximation algorithms, computational complexity, computational geometry, computational learning theory, concurrency theory, coordination languages, economics and algorithmic game theory, fixed parameter algorithms, formal verification and model-based testing, logic in computer science, machine learning methods, models of computation and reasoning for embedded, hybrid, and cyber-physical systems, optimization, parallel and distributed algorithms, quantum computing, randomness in computing, stochastic and probabilistic specification and reasoning theoretical aspects of other CS-related research areas, e.g., computational science, databases, information retrieval, and networking, theoretical cryptography, theory of programming languages, and type theory and its application in program verification. Keynote Speakers ________________________________ Anuj Dawar, Cambridge University, UK Michael Fellows, Charles Darwin University, Australia Mehrnoosh Sadrezadeh, Queen Mary University of London, UK Submission ________________________________ For the main conference, we solicit research papers in all areas of theoretical computer science. All papers will undergo a rigorous review process and will be judged based on their originality, soundness, significance of the results, and relevance to the theme of the conference. Papers should be written in English. Research papers should not exceed 15 pages in the LNCS style format. Multiple and/or concurrent submission to other scientific venues is not allowed and will result in rejection as well as notification to the other venue. Any case of plagiarism (including self-plagiarism from earlier publications) will result in rejection as well as notification to the the authors' institutions. Papers should be submitted through our EasyChair submission website: https://www.easychair.org/conferences/?conf=ttcs2015 . The web site is open for submissions. Important Dates ________________________________ Paper Submission: May 15, 2015 (Anywhwere on Earth) Author notification: June 26, 2015 Camera ready paper due: July 10, 2015 Conference: August 26-28, 2015 Program Committee ________________________________ Track A: Algorithms and Complexity Mohammad Ali Abam, Sharif University of Technology, Iran Saeed Akbari, Sharif University of Technology, Iran Saeed Alaei, Cornell University, USA Mohammad Hossein Bateni, Google Research, USA Salman Beigi, IPM, Iran Amir Daneshgar, Sharif University of Technology, Iran Fedor Fomin, University of Bergen, Norway Ali Ghodsi, University of Waterloo, Canada Mohammad Ghodsi, Sharif University of Technology, Iran Mohammad T. Hajiaghayi, University of Maryland, USA (Chair) Amin Karbasi, Yale University, USA Nicole Immorlica, Microsoft Research, USA Amit Kumar, IIT Delhi, India Mohammad Mahdian, Google Research, USA Hamid Mahini, University of Maryland, USA Bojan Mohar, Simon Fraser University, Canada Mohammad Mahmoody, University of Virginia, USA Vahab Mirrokni, Google Research, USA Morteza Monemizadeh, Frankfurt University, Germany Shayan Oveisgharan, UC Berkeley and University of Washington, USA Debmalya Panigrahi, Duke University, USA Jorg Sack, Carleton University, Canada Mohit Singh, Microsoft Research, USA Dimitrios M. Thilikos, CNRS, France and University of Athens, Greece Suresh Venkatasubramanian, University of Utah, USA Jan Vondrak, IBM Almaden Research Center, USA Track B: Logic, Semantics, and Programming Theory Farhad Arbab, CWI and Leiden University, The Netherlands S. Arun-Kumar, IIT Delhi, India Ilaria Castellani, INRIA Sophia Antipolis, France Dave Clarke, Uppsala University, Sweden and KU Leuven, Belgium Pieter Cuijpers, Eindhoven University of Technology, The Netherlands Fatemeh Ghassemi, Tehran University, Iran Matthew Hennessy, Trinity College Dublin, Ireland Ichiro Hasuo, University of Tokyo, Japan Mahdi Jaghoori, AMC University of Amsterdam, The Netherlands Jeroen Keiren, Vrije Universiteit Amsterdam, The Netherlands Bas Luttik, Eindhoven University of Technology, The Netherlands Jose Meseguer, University of Illinois at Urbana, USA Lary Moss, Indiana University, USA Mohammad Mousavi, Halmstad University, Sweden (Chair) Jun Pang, University of Luxembourg, Luxembourg Gerardo Schneider, Chalmers University of Technology, Sweden Marjan Sirjani, Reykjavik University, Iceland Walter Vogler, Augsburg University, Germany Tim Willemse, Eindhoven University of Technology, The Netherlands

1 0

ICTAC 2015 First call for papers
by Kohei SUENAGA 04 Feb '15

04 Feb '15

（複数お受け取りの場合はご容赦ください．）皆様，京都大学の末永です．今年10月にコロンビアで開かれる国際会議 ICTAC の論文募集をお送りします．ご投稿をお待ちしております．末永幸平 -- ********************************************************************** CALL FOR PAPERS -- ICTAC 2015 12th International Colloquium on Theoretical Aspects of Computing 29-31 October 2015, Cali, Colombia http://www.ictac2015.co DEADLINE FOR SUBMISSIONS: JUNE 5, 2015. ********************************************************************** ICTAC 2015 will take place at the campus of Universidad Javeriana, Cali, Colombia during October 29-31, 2015. The ICTAC conference series aims at bringing together practitioners and researchers to exchange ideas and experiences addressing challenges in theoretical aspects of computing as well as in exploiting theory through methods and tools for system development. ICTAC also aims to promote cooperation between participants and institutions from developing and industrial countries in research and education. THEMES AND TOPICS OF PAPERS Topics of interest include theories of computation and programming, foundations of software engineering and formal techniques in software design and verification, as well as tools that support formal techniques for software modeling, system design and verification. The topical areas of the conference include, but are not limited to * Automata theory and formal languages; * Principles and semantics of programming languages; * Theories of concurrency, mobility and reconfiguration; * Logics and their applications; * Software architectures, their models, refinement and verification; * Relationship between software requirements, models and code; * Program static and dynamic analysis and verification; * Software specification, refinement, verification and testing; * Model checking and theorem proving; * Models of object and component systems; * Coordination and feature interaction; * Integration of theories, formal methods and tools for engineering computing systems; * Service-oriented architectures: models and development methods; * Models of concurrency, security, and mobility; * Theory of distributed, grid and cloud computing; * Real-time, embedded, hybrid and cyber-physical systems; * Type and category theory in computer science. INVITED SPEAKERS * Jean-Raymond Abrial * Volker Diekert * César Muñoz * Catuscia Palamidessi * Davide Sangiorgi * Moshe Vardi * Glynn Winskel ASSOCIATED EVENTS * ICTAC Summer School on Formal Methods (October 25-27) * DCM 2015: 11th International Workshop on Developments in Computational Models (October 28) PAPER SUBMISSION == Important Dates * Abstract submission: Monday, June 1, 2015. * Paper submission: Friday, June 5, 2015. * Author notification: Monday, July 20, 2015. * Camera ready: Monday, August 3, 2015. == Paper Categories and Format We call for submissions, related to the above areas and topics, according to the following three categories: * Regular papers, with original research contributions; * Short papers, on recent work or proposals of emerging challenges; * Tool papers, on tools that support formal techniques for software modeling, system design and verification. Submissions should adhere to the LNCS format (see http://www.springer.de/comp/lncs/authors.html for details). Regular papers should not exceed 18 pages. Short and tool papers should not exceed 10 pages. Submissions to the colloquium must not have been published or be concurrently considered for publication elsewhere. All submissions will be judged on the basis of originality, contribution to the field, technical and presentation quality, as well as their relevance to the conference. ==Submission Link Papers must be submitted by using www.easychair.org/conferences/?conf=ictac2015. ==Proceedings As for the past editions, the proceedings of ICTAC 2015 will be published by Springer in the series Lecture Notes in Computer Science (LNCS). ==Special Issue Extended versions of selected papers from ICTAC 2015 will be invited to a special issue of Mathematical Structures in Computer Science (http://journals.cambridge.org/action/displayJournal?jid=MSC). GENERAL CHAIRS * Martin Leucker, University of Luebeck (DE). * Camilo Rueda, Pontificia Universidad Javeriana - Cali (CO). * Frank Valencia, CNRS and LIX, Ecole Polytechnique (FR). CONTACT CHAIR * Frank D. Valencia (frank.valencia(a)gmail.com). PROGRAM COMMITTEE * Nazareno Aguirre (AR) * Gerard Assayag (FR) * Mauricio Ayala-Rincón (BR) * Pablo Barceló (CL) * Gustavo Betarte (UY) * Filippo Bonchi (FR) * Marco Carbone (DK) * Ilaria Castellani (FR) * Néstor Cataño (CO) * Gabriel Ciobanu (RO) * Silvia Crafa (IT) * Pedro R. D'Argenio (AR) * Nicolas D'Ippolito (AR) * Stefan Dantchev (UK) * Rocco De Nicola (IT) * Yuxin Deng (CN) * Gilles Dowek (FR) * Moreno Falaschi (IT) * José Luiz Fiadeiro (UK) * Wan Fokkink (NL) * Fabio Gadducci (IT) * Julian Gutierrez (UK) * Stefan Haar (FR) * Thomas Hildebrandt (DK) * Einar Broch Johnsen (NO) * Bartek Klin (PL) * Marta Kwiatkowska (UK) * Kim G. Larsen (DK) * Martin Leucker (DE) (co-chair) * Etienne Lozes (FR) * Larissa Meinicke (AU) * Hernan Melgratti (AR) * Dominique Mery (FR) * Matteo Mio (FR) * Andrzej Murawski (UK) * Vivek Nigam (BR) * Mauricio Osorio (MX) * Prakash Panangaden (CA) * Jorge A. Pérez (NL) * Elaine Pimentel (BR) * António Ravara (PT) * Camilo Rocha (CO) * Camilo Rueda (CO) (co-chair) * Augusto Sampaio (BR) * Vijay Saraswat (US) * Vladimiro Sassone (UK) * Gerardo Schneider (SE) * Alexandra Silva (NL) * Jiri Srba (DK) * Jean-Bernard Stefani (FR) * Perdita Stevens (UK) * Kohei Suenaga (JP) * Alwen Tiu (SG) * Kazunori Ueda (JP) * Frank Valencia (FR) (co-chair) * Vasco T. Vasconcelos (PT) * Kapil Vaswani (IN) * Björn Victor (SE) * Igor Walukiewicz (FR) * Farn Wang (TW) * Alan Wassyng (CA) * Gianluigi Zavattaro (IT) -- Kohei Suenaga (末永幸平), Ph.D Associate professor (准教授) Graduate School of Informatics, Kyoto University (京都大学情報学研究科) ksuenaga(a)gmail.com http://www.fos.kuis.kyoto-u.ac.jp/~ksuenaga/

1 0

JAIST Logic Workshop Series 2015
by Hajime Ishihara 03 Feb '15

03 Feb '15

皆様来年3月に金沢で開催されるJAIST Logic Workshop Series 2015のお知らせです。ふるってご投稿・ご参加ください。問合せ先：石原　哉・木原貴行・根元多佳子・横山啓太北陸先端科学技術大学院大学情報科学研究科 e-mail: jlws2015(a)jaist.ac.jp -------------------------------------------------------- *Call for Abstracts* JAIST LOGIC WORKSHOP SERIES 2015 Constructivism and Computability 2 March 2015 – 6 March 2015 Shiinoki Cultural Complex, Kanazawa, Japan http://www.jaist.ac.jp/is/labs/ishihara-lab/jlws2015/ -------------------------------------------------------- IMPORTANT DATES November 30 - deadline for abstract submissions December 25 - notification of accepted contributions February 15 - deadline for registrations March 2-6 - Constructivism and Computability workshop TUTORIALS * Giovanni Sambin (University of Padova) * Hideki Tsuiki (Kyoto University) * Stanley Wainer (University of Leeds) INVITED SPEAKERS * Ulrich Berger (Swansea University) * Takayuki Kihara (JAIST) * Graham Leigh (Vienna University of Technology) * Michael Rathjen (University of Leeds) * Masahiko Sato (Kyoto University) * Makoto Tatsuta (National Institute of Informatics) PROGRAM COMMITTEE * Toshiyasu Arai (Chiba University) * Andrej Bauer (University of Ljubljana) * Ulrich Berger (Swansea University) * Hajime Ishihara (co-chair, JAIST) * Masahiro Kumabe (Open University of Japan) * Erik Palmgren (Stockholm University) * Peter Schuster (University of Leeds) * Helmut Schwichtenberg (co-chair, LMU Munich) * Dieter Spreen (University of Siegen, UNISA Pretoria) * Kazuyuki Tanaka (Tohoku University) SUBMISSIONS Submissions of short abstracts (1 page in PDF format) are accepted through easychair.org, see https://easychair.org/conferences/?conf=jlws2015 DESCRIPTION JAIST Logic Workshop Series is a workshop series bringing together researchers from mathematical logic and its application, especially to artificial intelligence and software science. Each workshop has its own focus on a specific area of research in mathematical logic and its application. Previous workshops have been held in Kanazawa 2013, 2014 and 2014: http://www.jaist.ac.jp/~hirokawa/pr2013/ http://www.jaist.ac.jp/~preining/wpp/ http://www.jaist.ac.jp/~v-sano/jw2014/index.html In 2015, JAIST Logic Workshop Series focuses on “Constructivism and Computability” aiming at interaction and knowledge transfer between constructive mathematics and computability theory. The workshop is held being affiliated with EU FP7 Marie Curie Actions IRSES projects COMPUTAL (http://computal.uni-trier.de/) and CORCON (http://corcon.net/), but is open to all researchers in the areas. SCOPE Constructive mathematics and computability, and related areas including but not limited to: intuitionistic logic and type theory, proof theory, constructive analysis and topology, program extraction from proofs, recursion theory, computable analysis and topology, classical/constructive reverse mathematics, algorithmic randomness, real number computation etc. LOCAL ORGANIZERS * Hajime Ishihara (JAIST) * Takayuki Kihara (JAIST) * Takako Nemoto (JAIST) * Keita Yokoyama (JAIST) The workshop is supported by: * Japan Advanced Institute of Science and Technology (JAIST) CO-LOCATED WORKSHOP * JSPS-NUS Joint Workshop in Mathematica Logic and Foundations of Mathematics (6-7 March 2015, at the same venue)

1 2

ICALP 2015 CfP
by Shinya Katsumata 28 Jan '15

28 Jan '15

京都大学の勝股です。投稿締切まで３週間となりましたICALP2015のご案内です。 ---------- ICALP 2015 http://www.kurims.kyoto-u.ac.jp/icalp2015/ Second Call for Papers ====================== The 42nd International Colloquium on Automata, Languages, and Programming (ICALP) will take place in the period 6-10 July 2015 in Kyoto, Japan. The conference will co-locate with LICS 2015, the 30th ACM/IEEE Symposium on Logic in Computer Science. The ICALP 2015 conference chair is Kazuo Iwama (Kyoto University). ICALP is the main conference and annual meeting of the European Association for Theoretical Computer Science (EATCS). As usual, the main conference will be preceded and/or followed by a series of workshops. Important dates --------------- Submission deadline: Tuesday, 17 February 2015, 23:59 PST (Pacific Standard Time, UTC-8) Author notification: 15 April 2015 Final manuscript due: 30 April 2015 Deadlines are firm; late submissions will not be considered. Proceedings ----------- ICALP proceedings are published in the Springer-Verlag ARCoSS (Advanced Research in Computing and Software Science) subseries of LNCS (Lecture Notes in Computer Science). Invited Speakers ================= Ken Kawarabayashi, NII, Japan Valerie King, University of Victoria, Canada Thomas Moscibroda, MSR Asia, China Anca Muscholl, Universite Bordeaux, France (Joint with LICS) Peter O'Hearn, Facebook, UK (Joint with LICS) Invited Tutorial Speakers (Joint with LICS) ------------------------------------------- Piotr Indyk, MIT, USA Andrew Pitts, University of Cambridge, UK Geoffrey Smith, Florida International University, USA Masterclass speaker ------------------- Ryuhei Uehara, JAIST, Japan Topics ====== Papers presenting original research on all aspects of theoretical computer science are sought. Typical but not exclusive topics of interest are: Track A: Algorithms, Complexity and Games ----------------------------------------- * Algorithmic Game Theory * Approximation Algorithms * Combinatorial Optimization * Combinatorics in Computer Science * Computational Biology * Computational Complexity * Computational Geometry * Cryptography * Data Structures * Design and Analysis of Algorithms * Machine Learning * Parallel, Distributed and External Memory Computing * Randomness in Computation * Quantum Computing Track B: Logic, Semantics, Automata and Theory of Programming ------------------------------------------------------------- * Algebraic and Categorical Models * Automata, Games, and Formal Languages * Emerging and Non-standard Models of Computation * Databases, Semi-Structured Data and Finite Model Theory * Principles and Semantics of Programming Languages * Logic in Computer Science, Theorem Proving and Model Checking * Models of Concurrent, Distributed, and Mobile Systems * Models of Reactive, Hybrid and Stochastic Systems * Program Analysis and Transformation * Specification, Refinement, Verification and Synthesis * Type Systems and Theory, Typed Calculi Track C: Foundations of Networked Computation: Models, Algorithms and Information Management ------------------------------------------------------ * Algorithmic Aspects of Networks and Networking * Formal Methods for Network Information Management * Foundations of Privacy, Trust and Reputation in Networks * Mobile and Wireless Networks and Communication * Network Economics and Incentive-Based Computing Related to Networks * Networks of Low Capability Devices * Network Mining and Analysis * Overlay Networks and P2P Systems * Specification, Semantics, Synchronization of Networked Systems * Theory of Security in Networks Submission Guidelines -------------------- Authors are invited to submit an extended abstract of no more than 12 pages, including references, in LNCS style presenting original research on the theory of Computer Science. All submissions will be electronic via the EasyChair page for the conference, with three tracks (A, B and C): https://easychair.org/conferences/?conf=icalp2015 Submissions should be made to the appropriate track of the conference. No prior publication or simultaneous submission to other publication outlets (either a conference or a journal) is allowed. Submissions must adhere to the specified format and length. Submissions that are too long or formatted incorrectly may be rejected immediately. All the technical details that are necessary for a proper scientific evaluation of a submission must be included in a clearly-labelled appendix, to be consulted at the discretion of program committee members. This includes, in particular, the proofs of all the key theorems in a paper. Should I submit my paper to Track A or Track C? ------------------------------------------------ While the scope of Tracks A and B are generally well understood given their long history, the situation for Track C may be less obvious. In particular, some clarifications may be helpful regarding areas of potential overlap, especially between Tracks A and C. The aim for Track C is to be the leading venue for theory papers truly motivated by networking applications, and/or proposing theoretical results relevant to real networking, certified analytically, but not necessarily tested practically. The motivation for the track was the lack of good venues for theory papers motivated by applications in networking. On the one hand, the good networking conferences typically ask for extended experiments and/or simulations, while the TCS community is hardly able to do such experiments or simulations. On the other hand, the good conferences on algorithms tend to judge a paper based only on its technical difficulty and on its significance from an algorithmic perspective, which may not be the same as when judging the paper from the perspective of impact on networks. Several areas of algorithmic study of interest to track C have a broad overlap with track A. Graph algorithmics can belong in either, though if the work is not linked to networking, it is more appropriate in track A. Algorithmic game theory is another area of major overlap. Aspects involving complexity, the computation of equilibria and approximations, belong more in Track A, while results with applications in auctions, networks and some aspects of mechanism design belong in Track C. Finally, it should be noted that algorithms and complexity of message-passing based distributed computing belong squarely in track C, while certain other aspects of distributed computing do not fall under its scope. Best Paper Awards ----------------- As in previous editions of ICALP, there will be best paper and best student paper awards for each track of the conference. In order to be eligible for a best student paper award, a paper should be authored only by students and should be marked as such upon submission. Committees ========== Track A: Algorithms, complexity, and games ------------------------------------------ Peyman Afshani, Aarhus University, Denmark Hee-Kap Ahn, POSTECH, South Korea Hans Bodlaender Utrecht University, The Netherlands Karl Bringmann, Max-Planck Institut für Informatik, Germany Sergio Cabello, University of Ljubljana, Slovenia Ken Clarkson, IBM Almaden Research Center, USA Eric Colin de Verdiere, École Normale Supérieure Paris, France Stefan Dziembowski, University of Warsaw, Poland David Eppstein, University of California at Irvine, USA Dimitris Fotakis, National Technical University of Athens, Greece Paul Goldberg, University of Oxford, UK MohammadTaghi Hajiaghayi, University of Maryland at College Park, USA Jesper Jansson, Kyoto University, Japan Andrei Krokhin, Durham University, UK Asaf Levin, Technion, Israel Inge Li Gortz, Technical University of Denmark, Denmark Pinyan Lu, Microsoft Research Asia, China Frederic Magniez, Universite Paris Diderot, France Kazuhisa Makino, Kyoto University, Japan Elvira Mayordomo, Universidad de Zaragoza, Spain Ulrich Meyer, Goethe University Frankfurt am Main, Germany Wolfgang Mulzer, Free University Berlin, Germany Viswanath Nagarajan, University of Michigan, USA Vicky Papadopoulou, European University Cyprus, Cyprus Michal Pilipczuk, University of Bergen, Norway Liam Roditty, Bar-Ilan University, Israel Ignaz Rutter, Karlsruhe Institute of Technology, Germany Rocco Servedio, Columbia University, USA Jens Schmidt, TU Ilmenau, Germany Bettina Speckmann (chair), TU Eindhoven, The Netherlands Csaba D. Toth, California State University Northridge, USA Takeaki Uno, National Institute of Informatics, Japan Erik Jan van Leeuwen, Max-Planck Institut für Informatik, Germany Rob van Stee, University of Leicester, UK Ivan Visconti, University of Salerno, Italy Track B: Logic, semantics, automata and theory of Programming ------------------------------------------------------------- Andreas Abel, Chalmers and Gothenburg University, Sweden Albert Atserias, Universitat Politècnica de Catalunya, Spain Christel Baier, TU Dresden, Germany Lars Birkedal, Aarhus University, Denmark, Luis Caires, Universidade Nova de Lisboa, Portugal James Cheney, University of Edinburgh, UK Wei Ngan Chin, National University of Singapore, Singapore Ugo Dal Lago, University of Bologna, Italy Thomas Ehrhard, CNRS, Université Paris Diderot, France Zoltan Esik, University of Szeged, Hungary Xinyu Feng, University of Science and Technology of China, China Wan Fokkink, VU University Amsterdam, The Netherlands Shin-ya Katsumata, Kyoto University, Japan Naoki Kobayashi (chair), The University of Tokyo, Japan Eric Koskinen, New York University, USA Antonín Kucera, Masaryk University, Czech Republic Orna Kupferman, Hebrew University, Israel Annabelle Mclver, Macquarie University, Australia Dale Miller, INRIA Saclay, France Markus Mueller-Olm, University of Münster, Germany Andrzej Murawski, Univeristy of Warwick, UK Joel Ouaknine, Univeristy of Oxford, UK Prakash Panangaden, McGill University, Canada Pawel Parys, University. of Warsaw, Poland Reinhard Pichler, TU Vienna, Austria Simona Ronchi Della Rocca, University of Torino, Italy Jeremy Siek, Indiana University, USA Track C: Foundations of networked computation: Models, algorithms and information management ------------------------------------------------------ Ioannis Caragiannis, Univ. Patras, Greece Katarina Cechlarova, Pavol Jozef Safarik Univ., Slovakia Shiri Chechik, Tel Aviv Univ., Israel Yuval Emek, Technion, Israel Sandor Fekete, TU Braunschweig, Germany Pierre Fraigniaud, CNRS and Paris Diderot, France Leszek Gasieniec, Univ. Liverpool, UK Aristides Gionis, Aalto Univ., Finland Magnus M. Halldorsson (chair), Reykjavik Univ, Iceland Monika Henzinger, Univ. Wien, Austria Bhaskar Krishnamachari, USC, USAL Fabian Kuhn, Freiburg, Germany Michael Mitzenmacher, Harvard Univ, USA Massimo Merro, Univ. Verona, Italy Gopal Pandurangan, Univ. Houston, USA Pino Persiano, Salerno, Italy R. Ravi, CMU, USA Ymir Vigfusson, Emory Univ., USA Roger Wattenhofer, ETH Zurich, Switzerland Masafumi Yamashita, Kyushu Univ., Japan

1 0

Kobe Colloquium on Logic, Statistics and Informatics, January 27 (Monroe Eskew)
by Joerg Brendle 26 Jan '15

26 Jan '15

Kobe Colloquium on Logic, Statistics and Informatics 以下の要領でコロキウムを開催します。日時：2014年1月27日（火）13:20-14:50 講演者：Monroe Eskew （筑波大学）場所：神戸大学自然科学総合研究棟3号館4階421室（プレゼンテーション室） ============================================================ 題目： A global version of Chang’s conjecture アブストラクト： In the 80s, Foreman showed the consistency of (aleph_{n+1},aleph_n) —>> (aleph_{m+1},aleph_m) holding simultaneously for all natural numbers n > m, starting from a 2-huge cardinal. He asked whether a global version of Chang’s conjecture is consistent. We answer this, showing that it is consistent from the same hypothesis that for all pairs of regular cardinals mu < kappa, (kappa^+,kappa) —>> (mu^+,mu). The method uses a relatively simple forcing iteration, and it answers some technical questions raised by Shioya. We also discuss some related issues about singular cardinals. ============================================================ 交通：阪急六甲駅またはJR六甲道駅から神戸市バス36系統「鶴甲団地」行きに乗車，「神大本部工学部前」停留所下車，徒歩すぐ． http://www.kobe-u.ac.jp/info/access/rokko/rokkodai-dai2.htm

1 0

JSPS-NUS Joint Workshop in Logic
by Tanaka Kazuyuki 26 Jan '15

26 Jan '15

JSPS-NUS二国間共同研究のロジック・ワークショップのご案内シンガポールとの二国間交流事業（代表：田中、Chong）の一環として下記の研究会を開催致します。 Workshop in Mathematical Logic and Foundations of Mathematics 日程：2015年3月6日(金) から3月8日(日) まで場所：金沢しいのき迎賓館および金沢東急ホテルこのワークショップは主に共同研究のメンバーによって行われるものですが、ご関心のある方は一般からもご参加いただけます。但し、会場準備の都合上事前登録者に限りますので参加希望の方は SendaiLogic[at]math.tohoku.ac.jp （締切２月８日）までご連絡ください。下記のページで＜英語＞でもご案内しております。 http://www.math.tohoku.ac.jp/~tanaka/kanazawa2015.html よろしくお願いします。　東北大学　田中一之コンタクト：　SendaiLogic[at]math.tohoku.ac.jp

1 0

『第２回山陰基礎論・解析学研究集会』の御案内
by Horihata Yoshihiro 23 Jan '15

23 Jan '15

皆様米子高専の堀畑です．明日と明後日に米子で件名の研究会を開きます．ホームページ https://sites.google.com/site/yonagonctmath/slas2015 参加自由です．よろしくお願いいたします．参加者リスト阿部吉弘（神奈川大学）池上大祐（神戸大学）薄葉季路（神戸大学）嘉田勝（大阪府立大学）木原貴行（ＪＡＩＳＴ）熊本真一郎（金沢大学）倉橋太志（木更津高専）古清水大直（米子高専）小林玉青（米子高専）小浪吉史（島根大学）静間荘司（大阪府立大学）柴田孝祐（米子高専，建築学科５年）高木啓行（信州大学）竹内耕太（筑波大学）根元多佳子（ＪＡＩＳＴ）濱田裕康（佐世保高専）樋口幸治郎（千葉大学）吉居啓輔（沖縄高専）吉田聡（鳥取環境大学）米子高専・数学同好会学生３人世話人：堀畑佳宏 -- 米子工業高等専門学校教養教育科・数学〒683-8502 鳥取県米子市彦名町4448 Tel: 0859-24-5075 E-mail: horihata(a)yonago-k.ac.jp

1 0

Re: [logic-ml] メーリングリストへの配信願い
by Atsushi Igarashi 22 Jan '15

22 Jan '15

logic-ml のみなさま，五十嵐＠logic-ml管理人です．成蹊大学・理工学部・情報科学科の山本様からの依頼での代理投稿です． ---------------------------------------------------------- logic-ml の皆様，成蹊大学・理工学部・情報科学科の山本と申すものです．以下のように，当学科で助教の公募を行っています．募集期間が短く申し訳ありませんが，ご関心のある方々の応募をお待ちしております． 1. 募集人員：助教１名 (任期付き) 2. 所属：理工学部情報科学科 3. 専門分野：計算機科学・情報科学における理論分野全般 4. 着任時期：２０１５年５月１日（金） 5. 応募締切：２０１５年２月１４日（土）（必着）詳細は，下記 URL をご参照下さい． http://www.seikei.ac.jp/gakuen/recruit/teacher/university.html 以上．

1 0

PPL2015参加登録開始がご案内：第17回プログラミングおよびプログラミング言語ワークショップ
by Kazutaka Matsuda 16 Jan '15

16 Jan '15

logic-ml関係者の皆様，東京大学の松田です．複数受け取られた場合はご容赦ください． 3月4日（水）から3月6日（金）に道後温泉で開催される第17回プログラミングおよびプログラミング言語ワークショップ (PPL2015) の参加登録を開始いたしましたで，そのご案内をお届けいたします．今回は， * 橋本和幸 (NVIDIA. 元日本シンボリックス株式会社) 「1980年代のLispマシンSymbolicsとその開発環境Genera 付属：NVIDIA GPUによる超並列コンピューティング」 * Chung-Kil Hur (Seoul National University) 「Formal C semantics and LLVM compiler validation」の二件の招待講演を予定しております．多くの方々のご参加をお待ちしております．参加登録の案内ページは http://www-kb.is.s.u-tokyo.ac.jp/ppl2015/registration/ です．参加登録の締切は2月17日（火）です．どうぞお早めのご登録をお願い致します．今年は昨年と異なり，*三日目は全日開催*となります．ご注意ください．また，カテゴリ2（国外既発表論文），4（サーベイ・チュートリアル）の申し込みは 2015年1月23日(金) 17:00 (JST) まで，カテゴリ3（ポスター・デモ発表）の申し込みは 2015年2月6日(金) 17:00 (JST) まで受け付けております．こちらも http://www-kb.is.s.u-tokyo.ac.jp/ppl2015/ をご参照の上，投稿をご検討いただけますと幸いです． -------------------------------------------------------------------------- 第17回プログラミングおよびプログラミング言語ワークショップ（PPL2015） http://www-kb.is.s.u-tokyo.ac.jp/ppl2015/ 参加登録のご案内主催: 日本ソフトウェア科学会プログラミング論研究会日程: 2015年3月4日(水)～3月6日(金) 会場: 愛媛県松山市道後温泉「道後プリンスホテル」 http://www.dogoprince.co.jp/ PPL2015は、プログラミングおよびプログラミング言語に関する研究者が一堂に会し、最新の研究成果の発表、および新たな研究課題についての討論やアイディア交換等を行うことを目的とした、合宿形式のワークショップです． ====================================================================== 参加登録ならびに宿泊予約を2月17日(火)まで日本旅行のWebサービスにて受け付けております． http://www-kb.is.s.u-tokyo.ac.jp/ppl2015/registration/ をご参照いただき，ご登録ください．問い合わせ先：ppl2015-oc [at] kb.is.s.u-tokyo.ac.jp （[at]を@に置き換えてください） ====================================================================== プログラム委員会青戸等人東北大学浅田和之東京大学岩崎英哉電気通信大学鵜川始陽高知工科大学馬谷誠二京都大学 [プログラム共同委員長] 大岩寛産業技術総合研究所亀山幸義筑波大学河内谷清久仁日本IBM 久野靖筑波大学木村大輔国立情報学研究所宋剛秀神戸大学塚田武志 University of Oxford 中田景子 FireEye DresDen 浜名誠群馬大学 [プログラム共同委員長] 平井洋一 FireEye Dresden 平石拓京都大学藤田憲悦群馬大学星野直彦京都大学増原英彦東京工業大学渡部卓雄東京工業大学組織委員会松田一孝東京大学 [組織委員長] 浜名誠群馬大学 [プログラム共同委員長] 馬谷誠二京都大学 [プログラム共同委員長] 末永幸平京都大学上野雄大東北大学海野広志筑波大学木村大輔国立情報学研究所 [ポスターセッション幹事] --------------------------------------------------------------------------

1 0

Gilles Dowek教授講演会　１月１６日金曜日　三田ロジックセミナー
by Mitsuhiro Okada 15 Jan '15

15 Jan '15

次のようなセミナートークを予定しておりますのでご案内させていただきます。参加自由です。(日時が次のように変更しています。Please note that　the date/time changed as follows.) 　　　　　　　　慶應義塾大学文学部哲学専攻岡田光弘 ------------------------------ Mita Logic Seminar Jan.16th (Fri) 13:00-14:30 Place: Basement B1 , Meeting Room #3, North Building, Mita campus, Keio University　(Campus Map http://www.keio.ac.jp/en/maps/mita.html) １月１６日金曜日　１３時ー１４時半, 慶應義塾大学三田キャンパス北館地下一階第３会議室　(キャンパスマップhttp://www.keio.ac.jp/ja/access/mita.html） Speaker; Gilles Dowek, INRIA, France Title: Real numbers, chaos, and the principle of a bounded density of information Abstract: Two definitions of the notion of a chaotic transformation are compared: sensitivity to initial conditions and sensitivity to perturbations. Only the later is compatible with the idea that information has a finite density. 連絡先：思考と行動判断の研究拠点事務局（logic(a)abelard.flet.keio.ac.jp) ------------

1 0

PPL2015 ポスター発表申込み締切日訂正
by Makoto Hamana 14 Jan '15

14 Jan '15

皆様、すみませんです、先ほどご案内したPPL2015の案内メールのポスター・デモ発表申込み締切り日に間違いありましたので訂正させていただきます。 [訂正] カテゴリ3（ポスター・デモ発表）締切は 2015年2月6日(金) 17:00 (JST) です。カテゴリ4(サーベイ・チュートリアル)の方は1月23日〆で正しいです。 PPL 2015 Webページ http://www-kb.is.s.u-tokyo.ac.jp/ppl2015/ にあるものが正式な情報です。お騒がせして申し訳ありません。どうぞよろしくお願いいたします。 -- 浜名　誠群馬大学理工学府電子情報部門 http://www.cs.gunma-u.ac.jp/~hamana/

1 0

CFP: PPL2015 サーベイ・チュートリアル、ポスター発表募集
by Makoto Hamana 13 Jan '15

13 Jan '15

皆様、群馬大学の浜名です。来年3月に愛媛県松山市道後温泉で開催される第17回プログラミングおよびプログラミング言語ワークショップ PPL'15 2015年3月4日(水)〜3月6日(金) http://www-kb.is.s.u-tokyo.ac.jp/ppl2015/ のサーベイ・チュートリアル、ポスター発表申込みの案内をさせていただきます。 * サーベイ・チュートリアル発表 (カテゴリ4）は、今年のPPLからの試みで、プログラミング言語分野の学生、研究者に役立つようなサーベイ・チュートリアル発表を広く募集します。プログラミング言語理論も実装も歴史が深くなってきて、自分の特定専門分野の事は知っていても、なかなか他の小分野の事はよく知らないという事が多くなってきました。そこでプログラミング言語に関わる様々な理論、応用の小分野間の相互理解と全体の底上げとなる事を目指し、設置しました。既発表・未発表の別を問いません(申込みは簡単なアウトラインの提出のみ)。既存発表の解説論文、教科書、セミナーや講義での資料、経験などお持ちの方はそれを用いていただくのも便利かと思います。 - ある専門分野の事を皆にもっと知ってもらいたい！ - 難しい分野と言われているがアイデアはそんなことないから解説したい。 - 現在隆盛を誇っている分野はこんな風に発展してきた。あまり知られていないが自分の専門性から解説したい。 - 解説論文を出版したけど、これを発表で話したことはないな… - 自分もやってる活発な〇〇分野の研究動向をまとめたいけどなかなかきっかけがない。これを機にまとめようか。などいろいろパターン、動機はあるかと思います。上記どれか当てはまるような方、もちろんそれに限らず、ぜひ申込みいただければと思います。通常発表と同様の30分での発表を予定していますが、採択件数によっては発表者との相談で少し時間延長もできるかもしれません。通常研究発表とは違い、ある程度確立した分野の話、専門家の方にお願いできればと思っております。PPLへの関連および関連研究への言及をもとに採録を判定いたします。 * ポスター・デモ発表 (カテゴリ3)は例年盛況な2時間程度のセッション内でのポスター発表またはデモ発表です。既発表・未発表の別を問いません。今年はポスター賞も設置しました。申込み多数の場合はプログラム委員会での選考により採否を決定します。締切はどちら(カテゴリ3,4)も、来週末 2015年1月23日(金) 17:00 (JST) ですので、ぜひ申込みをご検討ください。詳しい申込み方法などは http://www-kb.is.s.u-tokyo.ac.jp/ppl2015/ ご参照ください。 -- 浜名　誠群馬大学理工学府電子情報部門 http://www.cs.gunma-u.ac.jp/~hamana/

1 0

KusatsuSeminar3/16--20
by Fujita Kenetsu 13 Jan '15

13 Jan '15

皆様，『ラムダ計算と論理の早春セミナー』のご案内日程：2015年3月16日(月) 午後5時から3月20日(金) 正午まで場所：国立大学草津セミナーハウス　　　〒377-1711 群馬県吾妻郡草津町大字草津字白根737 詳細：http://www.cs.gunma-u.ac.jp/~fujita/2015.03LLSinKusatsu.htm 申込・質問などは藤田（群馬大学）までご連絡をお願いします．興味をお持ちのみなさまのご参加をお待ちしております． ----------- 群馬大学　藤田憲悦

1 0

Ninth NII Type Theory Workshop
by Makoto Tatsuta 12 Jan '15

12 Jan '15

Ninth NII Type Theory Workshop Date: January 15, 2015, 10:20--17:30 Place: National Institute of Informatics, Room 1208 (12th floor) 場所: 国立情報学研究所 12階 1208室 (半蔵門線,都営地下鉄三田線・新宿線神保町駅または東西線竹橋駅より徒歩5分) (地図 http://www.nii.ac.jp/about/access/) Program: 10:20--11:00 Daisuke Kimura (National Institute of Informatics) Title: A framework of models of functional PTSs 11:00--11:40 Josh Ko (National Institute of Informatics) Title: Relational algebraic ornamentation 11:40--13:10 Lunch Break 13:10--13:50 Makoto Fujiwara (Tohoku University) Title: On the strength of ¥Delta^0_1-LEM over Intuitionistic Analysis 13:50--14:30 Koji Nakazawa (Kyoto University) Title: Confluence of lambda-calculi with permutative conversion 14:30--14:50 Break 14:50--15:30 Mahmudul Faisal Al Ameen (The Graduate University for Advanced Studies) Title: Completeness of Separation Logic with Recursive Procedures 15:30--16:10 Makoto Tatsuta (National Institute of Informatics) Title: Decidability of Separation Logic with Monadic Inductive Definitions 16:10--16:30 Break 16:30--17:30 Stefano Berardi (Torino University) Title: Realizability and Strong Normalization for Heyting Arithmetic with EM1 Abstracts: ---------------------------------------------------------------------- Daisuke Kimura (National Institute of Informatics) Title: A framework of models of functional PTSs Abstract: This talk presents a framework of models of functional PTSs. The class of functional PTSs is a class of PTS which contains well-known type theories such as the simply typed lambda calculus, System F, lambda P (dependent type system), and Calculus of Constructions. This framework of models is obtained by using Cousineau and Dowek's embedding from a functional PTS into a lambda P modulo. As a result of this talk, a semantical condition for a functional PTS to be a strongly normalizing system is given. This result is expected to give a semantical approach to Barendregt-Geuvers-Klop conjecture. ---------------------------------------------------------------------- Josh Ko (National Institute of Informatics) Title: Relational algebraic ornamentation Abstract: Type theory makes it possible to treat programs and proofs uniformly as the same entities. Dependently typed programmers aim to design programs that carry their own correctness proofs, exploiting the coincidence of programs and proofs to the full extent. A generic construction that can help to achieve this is relational algebraic ornamentation, with which we can synthesise datatypes satisfying properties that can be expressed in terms of folds. In this talk I will show how relational algebraic ornamentation can help with designing a dependently typed program for solving the well-known minimum coin change problem. ---------------------------------------------------------------------- Makoto Fujiwara (Tohoku University) Title: On the strength of ¥Delta^0_1-LEM over Intuitionistic Analysis Abstract: Ishihara [2] showed over intuitionistic analysis EL that Markov’s principle MP is equivalent to WMP+¥Pi^0_1-DML(under the name of MP^v). On the other hand, Akama et al. [1] showed that ¥Delta^0_1-LEM is implied from both of MP(under the name of ¥Sigma^0_1-DNE) and ¥Sigma^0_1-DML(under the name of ¥Sigma^0_1-LLPO). In this talk, we show over EL that ¥Delta^0_1-LEM is implied from ¥Pi^0_1-DML and equivalent to ¥Delta^0_1 comprehension axiom, which is from reverse mathematics. In addition, some separation results are also presented. This is a joint work with Hajime Ishihara and Takako Nemoto. References: [1] Y. Akama, S. Berardi, S. Hayashi and U. Kohlenbach, An arithmetical hierarchy of the law of excluded middle and related principles. Proc. of the 19th Annual IEEE Symposium on Logic in Computer Science (LICS'04), pp. 192--201, IEEE Press (2004). [2] H. Ishihara, Markov's principle, Church's thesis and Lindel¥"of theorem, Indag. Math. (N.S.) 4 (1993), pp. 321--325. ---------------------------------------------------------------------- Koji Nakazawa (Kyoto University) Title: Confluence of lambda-calculi with permutative conversion Abstract: We give a new proof of confluence for the lambda and the lambda-mu calculi with permutative conversion for case branching. For such calculi, naive approaches with parallel reductions do not work, and we adopt a proof technique with generalized notions of complete development with the Z property, introduced by Dehornoy and van Oostrom. Our idea also gives a simpler proof for confluence of the first-order classical natural deduction, which has been proved by Ando with more complicated notions. ---------------------------------------------------------------------- Mahmudul Faisal Al Ameen (The Graduate University for Advanced Studies) Title: Completeness of Separation Logic with Recursive Procedures Abstract: This talk proves the completeness of Hoare's Logic extended by separation logic for verification of while programs with pointers and recursive procedures. ---------------------------------------------------------------------- Makoto Tatsuta (National Institute of Informatics) Title: Decidability of Separation Logic with Monadic Inductive Definitions Abstract: This talk shows the decidability of entailments of symbolic heaps in separation logic with monadic inductive definitions under certain conditions. ---------------------------------------------------------------------- Stefano Berardi (Torino University) Title: Realizability and Strong Normalization for Heyting Arithmetic with EM1 Abstract: We present a new Curry-Howard correspondence for HA+EM1, first order constructive Heyting Arithmetic with the excluded middle on Sigma-0-1-formulas. We add to the lambda calculus an operator k_a which represents, from the viewpoint of programming, an exception operator with a delimited scope, and from the viewpoint of logic, a restricted version of the excluded middle. We motivate the restriction of the excluded middle by its use in proof mining; we introduce new techniques to prove strong normalization for HA + EM1 and the witness property for simply existential statements. One may consider our results as an application of the ideas of Interactive realizability, which we have adapted to the new setting and used to prove our main theorems. This technique has been recently extended by F. Aschieri to the entire excluded middle for First Order Arithmetic. This is a joint work with F. Aschieri and G. Birolo. ---------------------------------------------------------------------- 問合せ先　龍田 (tatsuta(a)nii.ac.jp)

1 0

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Logic-ml