Logic-ml

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

1792 discussions

Kobe Colloquium on Logic, Statistics and Informatics June 28, 2012
by Joerg Brendle 26 Jun '12

26 Jun '12

Kobe Colloquium on Logic, Statistics and Informatics 以下の要領でコロキウムを開催します。日時：2012年6月28日（木）15:10-16:40 場所：神戸大学自然科学総合研究棟3号館4階421室（プレゼンテーション室）講演者：Paul Larson (Miami University, Oxford, Ohio) ======================================================================== 題目：Models of size aleph_1 in abstract elementary classes アブストラクト： We will present some applications of set theoretic techniques to the study of models of cardinality aleph_1 in various abstract elementary classes. The impetus for this work was the still-open question of absoluteness of aleph_1-categoricity for the class of models of a fixed sentence of L_{omega_1, omega}. Most of our results apply to the class of analytically presented AEC's, those whose restriction to countable models is analytic. These classes have been studied for many years under various names. Time permitting, connections with Vaught's Conjecture will also be discussed. This is joint work with Baldwin and Shelah. ======================================================================== 交通：阪急六甲駅またはJR六甲道駅から神戸市バス36系統「鶴甲団地」行きに乗車，「神大本部工学部前」停留所下車，徒歩すぐ． http://www.kobe-u.ac.jp/info/access/rokko/rokkodai-dai2.htm 連絡先：ブレンドレヨーグ brendle(a)kurt.scitec.kobe-u.ac.jp

1 0

「範疇文法と証明論」シンポジウム (7/21) のご案内
by BEKKI Daisuke 25 Jun '12

25 Jun '12

（重複して受け取られた場合はご容赦ください） ============================================== 第二回「範疇文法と証明論」シンポジウムのご案内 ============================================== 　「範疇文法と証明論」は、理論言語学、数理論理学、自然言語処理の学際シンポジウムです。範疇文法(Categorial Grammar)と証明論的意味論 (Proof Theoretic Semantics)を中心テーマとして、言語学者、論理学者、自然言語処理研究者が、それぞれの立場から研究発表を行います。　どなたでも、お気軽にご参加下さい。日時：2012/7/21(土) 10:00-17:00（予定）場所：お茶の水女子大学理学部3号館209（以下の地図の建物20） http://www.ocha.ac.jp/access/campusmap_l.html 東京都文京区大塚2-1-1 丸ノ内線茗荷谷駅徒歩7分、または有楽町線護国寺駅徒歩7分）備考：お茶の水女子大学に入構する際に、守衛所にて身分証明書の提示を求められます。使用言語：日本語（質疑は英語可）参加費：無料講演予定： ------------------------------------------------------------------ 宮尾祐介・松崎拓也（国立情報学研究所）「大学入試における「論理」とは？」峯島宏次（慶應義塾大学）「Syllogistic logics and categorial grammar」佐野勝彦（北陸先端科学技術大学院大学）「Inquisitive semantics and inquisitive logic」上垣渉（MIT) 「選言を含む知識帰属とinquisitive logic」窪田悠介（東京大学・JSPS）「Hybrid Type-Logical Categorial Grammar」矢田部俊介（産業技術総合研究所）「範疇文法と証明論的意味論」戸次大介（お茶の水女子大学）「範疇文法とモナド」 ------------------------------------------------------------------

1 0

AiML-2012: Call for Participation
by Thomas Bolander 20 Jun '12

20 Jun '12

AiML-2012: CALL FOR PARTICIPATION 9-TH INTERNATIONAL CONFERENCE ON ADVANCES IN MODAL LOGIC COPENHAGEN, 22-25 AUGUST, 2012 http://hylocore.ruc.dk/aiml2012.html Advances in Modal Logic is an initiative aimed at presenting the state of the art in modal logic and its various applications. The initiative consists of a conference series together with volumes based on the conferences. Information about the AiML series can be obtained at http://www.aiml.net. AiML-2012 is the ninth conference in the series. REGISTRATION: Please see http://hylocore.ruc.dk/aiml2012/registration.php NOTE THAT THE DEADLINE FOR EARLY REGISTRATION IS JUNE 29. ACCEPTED PAPERS: Please see http://hylocore.ruc.dk/aiml2012/accepted.php CONFERENCE LOCATION Advances in Modal Logic 2012 will be held at the IDA conference centre in downtown Copenhagen: http://ida.dk/sites/moedecenter/english/Sider/EnglishForside.aspx This is in easy walking distance from Copenhagen Central Station and a number of reasonably priced hotels. INVITED SPEAKERS Lev Beklemishev (Moscow State University) Johan van Benthem (University of Amsterdam and Stanford University) Lars Birkedal (IT University of Copenhagen, Denmark) Patrick Blackburn (Roskilde University) Balder ten Cate (UC Santa Cruz) Larisa Maksimova (Novosibirsk State University) SPECIAL SESSION ON HYBRID LOGIC. Hybrid logic is an extension of modal logic allowing to refer explicitly to states of the model in the syntax of formulas. There will be a special session of AiML devoted to papers on hybrid logic. The scope of the special session is standard hybrid-logical machinery like nominals, satisfaction operators, and the downarrow binder, but also other extensions of modal logic can be considered. SPECIAL SESSION IN HONOUR OF LARISA MAKSIMOVA. There will be a special session of AiML devoted to papers and talks in honour of Larisa Maksimova, in recognition of her many outstanding contributions to modal logic. PROGRAMME COMMITTEE Carlos Areces (FaMAF, Universitad Nacional de Cordoba, Argentina) Philippe Balbiani (IRIT, Toulouse, France) Lev Beklemishev (Moscow State University, Russia) Guram Bezhanishvili (New Mexico State University, USA) Nick Bezhanishvili (Imperial College London, UK) Patrick Blackburn (Roskilde University, Denmark) Thomas Bolander (Technical University of Denmark) Torben Brauner (Roskilde University, Denmark) Giovanna Corsi (Università di Bologna, Italy) Giovanna D'Agostino (Università di Udine, Italy) Stephane Demri (LSV, ENS Cachan, France) Melvin Fitting (Lehman College, CUNY, USA) Robert Goldblatt (Victoria University of Wellington, New Zealand) Valentin Goranko (Technical University of Denmark) Rajeev Gore (Australian National University, Australia) Andreas Herzig (IRIT, Toulouse, France) Ian Hodkinson (Imperial College London, UK) Wiebe van der Hoek (University of Liverpool, UK) Rosalie Iemhoff (University of Utrecht, The Netherlands) Alexander Kurz (University of Leicester, UK) Tadeusz Litak (University of Leicester, UK) Hiroakira Ono (Japan Advanced Institute of Science and Technology) Martin Otto (Technical University of Darmstadt, Germany) Alessandra Palmigiano (ILLC, University of Amsterdam, The Netherlands) Renate Schmidt (University of Manchester, UK) Lutz Schröder (Friedrich-Alexander-Universität Erlangen-Nürnberg) Valentin Shehtman (Moscow State University, Russia) Dimiter Vakarelov (Sofia University, Bulgaria) Yde Venema (ILLC, University of Amsterdam, The Netherlands) Heinrich Wansing (Ruhr University Bochum, Germany) Frank Wolter (University of Liverpool, UK) Michael Zakharyaschev (Birkbeck College, London, UK) PROGRAMME COMMITTEE CO-CHAIRS Silvio Ghilardi (Università degli Studi di Milano, Italy) Lawrence Moss (Indiana University, USA) ORGANIZING COMMITTEE CO-CHAIRS Thomas Bolander (Technical University of Denmark) Torben Braüner (Roskilde University, Denmark) FURTHER INFORMATION. Please see http://hylocore.ruc.dk/aiml2012/ ENQUIRIES. E-mail enquiries should be directed to aiml2012(a)easychair.org

1 0

セミナー案内
by KASHIMA Ryo 18 Jun '12

18 Jun '12

セミナーのご案内日時：6月21日(木)16:30から場所：東京工業大学大岡山西８号館W棟11階 W1101セミナー室会場までの交通案内はこちらから： http://www.titech.ac.jp/about/campus/index.html 話者：松田直祐（千葉大学修士課程）題目：Charch-Rosser Theorem 概要： [1]を参考にしながらも、よりシンプルな概念のみを用いて Church-Rosser Theorem の証明を与える。 [1]：M.Takahashi, Parallel Reductions in Lambda-calculus, J.Symbolic Comput. Vol.7 (1989), pp.113-123. ----- 問い合わせ先：鹿島亮（東京工業大学） kashima(a)is.titech.ac.jp

1 0

第四回「論数哲」研究会のお知らせ
by 矢田部俊介 18 Jun '12

18 Jun '12

We will hold the 4th 「論数哲」(PhilLogMath) workshop. Our aim is to provide opportunities of detailed discussions among philosophers, logicians, mathematicians and linguists. We focus on theoretical and computational linguistics this time. Everyone is welcome. website url: http://researchmap.jp/jopyjeyia-21098/#_21098 Date : July 16 (Mon) National holiday （海の日） Place: Seiryo Kaikan (Nagata-cho, Tokyo) http://metropolis.co.jp/listings/venues/type/stage-venue/seiryo-kaikan/ Time table 10:00-12:00 上垣渉（MIT）　　尺度推意（scalar implicature）、その材料とレシピ 13:30-15:00 八木沢敬（カルフォルニア州立大学）　　可能世界を超える可能性 15:30-17:00 上出哲広（サイバー大学）　　 An embedding-based method for non-classical logics Every slots consists of 60 minutes talk and 30 minutes discussion basically. Abstracts: 上垣渉　尺度推意（scalar implicature）、その材料とレシピ自然言語の文は、ときに、それに含まれる語彙を「字義通り」に解釈した意味よりも強い（取り消し可能な）解釈を生み出すことがある。例えば、日本語母語話者は、日本語において選言に対応するとされる「pまたはq」は、「pかつq、ではない」（あるいは「pかつqであるとは話者は知らない」）という解釈をもつという直観をもつ。Grice(1975) 以降、このような事実は、文が表す意味を「字義通りの意味（literal meaning）」と「推意（implicature）」に分け、前者は言語に固有の文法的メカニズムによって生み出され、後者は言語に限らないコミュニケーション一般における推論によって字義通りの意味から導きだされるとする考えが言語学においては一般的である。ただ、後者の推意を生み出すメカニズムがどのようなものであるかに関しては、近年まで理論的な精緻化は比較的乏しく、推意は伝統的な意味論的分析を守るために分析と事実の齟齬を放り込んでおくためのある種のブラックボックス（あるいは「語用論的ゴミ箱（pragmatic wastebasket）」）として機能していた傾向がある。ところが、推意とくに尺度推意（scalar implicature）の近年の研究の展開において、字義通りの意味から推意が導かれる具体的なメカニズムの理論が精緻化されてきている（例えば、Jäger(2011), Franke (2009) によるゲーム理論的モデル、Goodman & Stuhlmuller (2012)によるベイズ理論を用いたモデル、Chierchia (2004), Chierchia, Fox & Spector (2011)による尺度推意を文法自体に組み込むモデルなど）。本発表では、この理論的展開において重要な意義をもつ二つの問題、すなわち (i)推意を生み出すのは「文法外」のメカニズムに限られるのか、(ii)推意の導出の際に用いられる代替発話（alternative utterances）の集合はいかにして規定されるのか、についての最近の研究を紹介する。そして、(i)の問題については、推意を文法に組み込む仮説がその主要な証拠としてきた「埋め込まれた尺度推意（embedded scalar implicature）」が、必ずしも推意に関する語用論的な見方と矛盾しないこと、(ii)の問題については、談話における「議題となる疑問（Question under Discussion）」が代替発話を規定するのに重要な役割を果たすことを議論したい。八木沢敬　可能世界を超える可能性標準的な可能世界の枠組みでは、すべての可能性は何らかの可能世界での実現として理解される。本論では、この理解を批判する。まず、標準的な可能世界の枠組みによる様相の理解の根底にあるアイデアを「別域の方法」（method of alternatives）として同定し、次に、それを可能世界を擁する論理空間そのものに関する様相言明に適用することによって、可能世界での実現としては理解できない可能性の概念を明らかにする。それにあたって、現実世界についての様相、信念の様相、背理法の使用、思考の様相などを考察する。上出哲広　An embedding-based method for non-classical logics An embedding-based proof method for some non-classical logics is presented. This method can uniformly prove the cut-elimination,completeness, decidability and Craig interpolation theorems for some non-classical logics including some paraconsistent and temporal logics. This method is based on two theorems for syntactically and semantically embedding the required non-classical logic into its negation-less or time-less fragment. Firstly in this talk, some results on Nelson's paraconsistent logic and its neighbors, which have recently been obtained by Kamide and Wansing, are presented. Secondly, some results on linear-time temporal logic and its neighbors are presented. Workshop organizer: Yuko Murakami Shunsuke Yatabe ( shunsuke.yatabe(a)aist.go.jp ) Takuro Onishi ( takuro.onishi(a)gmail.com )

1 0

ＲＩＭＳ研究集会「証明論と複雑性」
by Suzuki Toshio 11 Jun '12

11 Jun '12

　研究集会案内・講演募集　（複数お受け取りの場合はご容赦ください）首都大学東京の鈴木登志雄です。さて、以下のように研究集会を開催いたします。皆様の参加・講演申込みをお待ちしております。 ------------------------------------------------------------------ 参加・講演募集ＲＩＭＳ研究集会「証明論と複雑性（Proof theory and complexity）」期間　２０１２年９月１２日（水）午後から１４日（金）午後場所　数理解析研究所４２０号室（収容人数１５０名）しめきり７月１３日（金）、返信先 toshio-suzuki[ATMARK]tmu.ac.jp http://www.ac.auone-net.jp/~bellp/meeting/proof2012.html ------------------------------------------------------------------ 目的と範囲 ============= 形式体系の研究には古典論理の証明論，非古典論理，逆数学をはじめとして様々な分野があり，それぞれの分野において，形式体系と複雑性との関係が活溌に研究されています。ここでいう複雑性とは計算に必要な資源の最小量として導入される各種の量であり，時間計算量だけでなく，とくに証明の長さ，コルモゴロフ記述量，および問い合わせの回数を含みます。これら各種の複雑性は，互いに関連性をもっています。また，形式体系と複雑性を結びつける概念・手法としては，たとえばextended Frege system，計算可能関数のfunction algebra による特徴づけ，two-sorted predicate calculus ，資源限定マルティンゲール，ブール関数のゲーム木としての表現，質問記号付き命題論理などがあります。本研究集会では，形式体系の様々な分野の研究者が集まって最新の研究のアイデアを交換することにより，形式体系と複雑性の関係について研究を推進します。基調講演者（敬称略、題未定） ========================== 垂井　淳（電気通信大学　大学院情報理工学研究科）黒田　覚（群馬県立女子大学　文学部）一般講演募集 ============= 形式体系と複雑性に関する一般講演を募集します。発表は日本語または英語でお願いします。想定する話題の例として以下をあげますが、これらに限定するわけではありません。古典論理の証明論非古典論理（線形論理ほか）証明の長さ逆数学限定算術ラムダ計算アルゴリズム的情報理論命題論理の計算量（ブール決定木を含む）リカージョン・セオリー計算量理論における論理学的な手法・概念参加・講演申込み ============= お名前　　　　：所属　　　　　：身分（学年）　：メールアドレス：参加日程　　　：講演していただける場合は以下もご記入ください。講演タイトル　：講演希望時間　：長め（４５分）・短め（２５分）［どちらかをお選びください］講演希望日時　：［もし強いご希望があればお書きください］予稿の事前提出：あり・なし［どちらかをお選びください。詳細は下記］　この研究集会について２０１１年１１月以降に首都大の鈴木とメールのやりとりをなさった方のうち、前回と所属・身分・メールアドレスに変更のない方は、該当項目の記入を適宜省略していただいてかまいません。　（ＲＩＭＳからの旅費援助を受けない方は）飛び入り参加も可能ですが、講演を予定せず参加される方も含めて、参加日程をお知らせいただけると助かります。７月下旬に、研究代表者からＲＩＭＳへ、あらためて参加者リストを送ることになっています。　研究集会当日に配布したい予稿（Ａ４用紙１から２ページ程度）をあらかじめＲＩＭＳに提出しておき、ＲＩＭＳに予稿集を作成しておいてもらうこともできます。希望の場合は講演申込時におしらせください。予稿の提出は申込み後、ＲＩＭＳと相談の後にしていただきます。　講演時間には５分の質疑応答時間を含みます。お一人あたりの発表時間について、募集締め切り後に調整する可能性があります。申込み宛先 ============= toshio-suzuki[ATMARK]tmu.ac.jp [ATMARK]は@に変更してください。（首都大・理工　鈴木登志雄）以下の締め切り日より早く申し込んでいただけるとなおありがたいです。今回は短期共同研究ではなくＲＩＭＳ研究集会という形式です。研究計画提案書提出時の参加予定者に限定せず、講演を募集いたします。日程の要点 ============= 講演申込み締め切り　２０１２年７月１３日（金）研究集会　９月１２日（水）午後から１４日（金）午後講究録原稿締め切り　未定（研究集会終了後しばらくしてから）会場設備 ============= 液晶プロジェクター、書画カメラ、黒板、スクリーン、レーザーポインター、指示棒詳細は以下ＵＲＩ（トップページ->共同利用掛->共同利用掛から） http://www.kurims.kyoto-u.ac.jp/~kyodo/kyodotop-ja.html 発表用のパソコン（MiniD-sub15ピンに対応）は各自でご持参ください。研究代表者はマックブック（OS: Snow Leopard）を持参する予定です。報告集 ============= 集会の後、通常の数理解析研究所講究録を刊行予定です。講究録別冊（査読付き）の刊行はしません。代表者 ============= 鈴木登志雄（首都大学東京）１９２−０３９７　東京都八王子市　南大沢１−１首都大学東京　理工学研究科　数理情報科学専攻 toshio-suzuki[ATMARK]tmu.ac.jp 集会ウェブサイト ============= http://www.ac.auone-net.jp/~bellp/meeting/proof2012.html それでは、よろしくお願いいたします。

1 0

Talk by Takeshi Tsukada (Tohoku U.), Monday Next Week
by Ichiro Hasuo 05 Jun '12

05 Jun '12

みなさま，東京大学の蓮尾です．来週の月曜日，東北大の塚田武志さんをお迎えしてご講演いただきます．ハードコアなゲーム意味論のお話のようです :-) 事前の登録等不要です．ぜひお越しください！蓮尾一郎東京大学コンピュータ科学専攻 http://www-mmm.is.s.u-tokyo.ac.jp/ ======================================================== Mon 11 June 2012, 16:40-18:10 Takeshi Tsukada (Tohoku U, http://www.kb.ecei.tohoku.ac.jp/~tsukada/) ２レベルゲーム意味論による共通型の解釈場所：東京大学本郷キャンパス理学部7号館1階 102教室（アクセス： http://www-mmm.is.s.u-tokyo.ac.jp/ の一番下を見てください）本発表では２レベルゲーム意味論という新しいゲーム意味論を導入し、これを用いることで共通型システムのゲーム的解釈が与えられることを示す。ゲーム意味論と共通型理論は近年の高階モデル検査（＝高階再帰スキームという文法が生成する木のモデル検査）の理論において重要な役割を果たしており、これらの間の関係を明らかにすることは高階モデル検査の理論の進展のための重要な課題であると認識されてきた。これまでも直感的な対応関係は知られていたが、形式的な対応関係は本発表で導入する２レベルゲーム意味論によるものがはじめてである。２レベルゲームは、その名が示す通り、上層のゲームと下層のゲームの２つ（とそれらの間の関係）から成る。下層のゲームは項の計算を表し、上層のゲームは項の性質の証明を表す。このふたつのゲームは密接に関係しており、その関係は上層のゲームから下層のゲームへの写像として表現される。本発表では、２レベルゲームに関する次の結果について述べる。 (A) （単純型システムの詳細化であるような）共通型システムにおける型導出は２レベルゲームの勝利戦略として解釈することができる。さらに、２レベルゲーム意味論は共通型システムに対して fully complete である。つまり、すべての（２レベルゲームにおける）勝利戦略はある（共通型システムの）型導出の解釈となっている。 (B) 共通型システムの重要な性質に主拡張補題というものがある。これに対応する性質を、２レベルゲームも満たすことを示す。この証明は純粋にゲーム意味論的手法で行うことができる。また最後に、２レベルゲーム意味論の高階モデル検査への応用と今後の展開についてに述べる。参考文献： [1] C.-H. Luke Ong and Tsukada Takeshi. Two-Level Game Semantics, Intersection Types, and Recursion Schemes. ICALP 2012 (to appear).

1 0

Sendai Logic Workshop のご案内
by higurashi3873＠yahoo.co.jp 26 May '12

26 May '12

Logic-ml $B$N3'MM!$(B $B$3$s$P$s$O!$ElKLBg3X$NKYH*2B9($G$9!%(B $B2<5-$NMWNN$G!$ElKLBg3X!JEDCf0lG78&!K$K$F8&5f2q$r9T$$$^$9$N$G!$6=L#$N$"$kJ}$O$<$R$4;22C$/$@$5$$!%(B $B;09V1i$4$6$$$^$9!%(B ************************************************************************* Sendai Logic Workshop $BF|;~!'(B6$B7n(B1$BF|!J6b!K(B14:00$B!A(B17:30 $B>l=j!'ElKLBg3X(B $BKL@DMU;3%-%c%s%Q%9(B $BM}3X9gF1Eo(B 1201$B9f<<(B $B-!(B14:00$B!A(B15:00 $B9V1i<T!'</Eg(B $BN<(B $B!JEl5~9)6HBg3XBg3X1!(B $B>pJsM}9)3X8&5f2J!K(B $B%?%$%H%k!'(BCTL$B$H<~JU$NO@M}$N8xM}2=$K$D$$$F(B $B%"%V%9%H%i%/%H!'(B Computation Tree Logic (CTL) $B$O!$;~4V$N?d0\$KH<$C$F>uBV$,JQ2=$9$k%7%9%F%`$N5-=R$KMQ$$$i$l$kMMAjO@M}!J;~AjO@M}!K$NBeI=$G$"$k!#(B $BK\9V1i$NL\E*$O!$(BCTL$B$H$=$N<~JU$NO@M}$KBP$9$k%R%k%Y%k%HN.8xM}2=$H40A4@-$K$D$$$F=iJb$+$i2r@b$7!$9V1i<T$N:G6a$N;E;v!J(BECTL$B$N8xM}2=!K$d<h$jAH$_$?$$LdBj!JMMAj&L7W;;$N40A4@-$NJL>ZL@!K$K$D$$$F@bL@$9$k$3$H$G$"$k!#(B $BM=HwCN<1$O8EE5L?BjO@M}$N40A4@-DjM}DxEY$G==J,$NM=Dj!#(B $B-"(B15:15$B!A(B16:15 $B9V1i<T!':,85(B $BB?2B;R(B $B!JKLN&@hC<2J3X5;=QBg3X1!Bg3X(B $B>pJs2J3X8&5f2J!K(B $B%?%$%H%k!'(BWadge $B%2!<%`$N%P%j%(!<%7%g%s$H(B Wadge $B3,AX(B $B%"%V%9%H%i%/%H!'(B Wadge [3] $B$K$h$jDj5A$5$l$?(B Wadge $B3,AX$OO"B34X?t$K$h$k5UA|$K$D$$$FJD$8$?%/%i%9$N@.$93,AX$G!"(BBorel $B3,AX$d(B Hausdorff $B$N=89g:9$K$h$k3,AX$h$j$b$h$j:Y$+$$=89g$N3,AX$rM?$($k!#(B $B$3$N3,AX$N3F%/%i%9$N=89gA`:n$K$h$k5-=R$O(B Louveau [2] $B$K$h$jM?$($i$l$?$,!"(B $BHs>o$KHQ;($G$"$k!#(B Wadge $B3,AX$G??$KF1$8<!?t$r$b$D=89g$O(B Wadge $B%2!<%`$K$h$jFCD'$E$1$i$l$k$,!"(BDuparc [1] $B$G$O$3$N%2!<%`$N%P%j%(!<%7%g%s$K$h$j(B Wadge $B%/%i%9$N<!?t$N5-=R$N4JN,2=$rM?$((B $B$F$$$k!#(B $BK\9V1i$G$O(B [1] $B$NFbMF$rCf?4$K!"(BWadge $B%2!<%`$H(B Wadge $B3,AX$K4X$9$k8&5f$r>R2p$9$k!#(B $B;29MJ88%!'(B [1] J. Duparc, Wadge Hierarchy and Veblen Hierarchy. Part I: Borel Sets of Finite Rank. Journal of Symbolic Logic 66(1), pp. 56-86, 2001 [2] A. Louveau, Some results in the Wadge hierarchy of Borel sets, Cabal seminar 79-81, Lecture Notes in Mathematics, vol. 1019, Springer Verlag, 1983, pp. 28-55. [3] W.W. Wadge, Reducibility and determinateness on the Baire space., Ph.D. thesis, Berkeley, 1984. $B-#(B16:30$B!A(B17:30 $B9V1i<T!'O!Hx(B $B0lO:(B $B!JEl5~Bg3XBg3X1!(B $B>pJsM}9)3X7O8&5f2J!K(B $B%?%$%H%k!'(BProgramming with Infinitesimals: A While-Language for Hybrid System Modeling (Joint Work with Kohei Suenaga, Kyoto University) $B%"%V%9%H%i%/%H!'(B We add, to the common combination of a WHILE-language and a Hoare-style program logic, a constant dt that represents an infinitesimal (i.e. infinitely small) value. The outcome is a framework for modeling and verification of hybrid systems: hybrid systems exhibit both continuous and discrete dynamics and getting them right is a pressing challenge. We rigorously define the semantics of programs in the language of nonstandard analysis, on the basis of which the program logic is shown to be sound and relatively complete. If the time allows, our recent prototype automatic prover will also be demonstrated. $B;29MJ88%!'(B Kohei Suenaga and Ichiro Hasuo. Programming with Infinitesimals: A While-Language for Hybrid System Modeling. Proc. ICALP 2011, Track B. LNCS 6756, p. 392-403. Springer-Verlag. ************************************************************************* $B0J>e$G$9!%(B $B%;%_%J!<>pJs$O2<5-@gBf%m%8%C%/$N%[!<%`%Z!<%8$+$i$b$4Mw$$$?$@$1$^$9!%(B https://sites.google.com/site/sendailogichomepage/ $BKYH*!!2B9((B -- -- $BElKLBg3XBg3X1!!!M}3X8&5f2J(B $B?t3X@l96!!;:3X41O"7H8&5f0w(B E-mail: higurashi3873(a)yahoo.co.jp

1 0

talks by Vivek Nigam and Hugo Herbelin in Kyoto (28th May 2012)
by Hasegawa Masahito 24 May '12

24 May '12

$B3'MM!"(B $B0J2<$NFbMF$G#2#8F|!J7n!K$K9V1i$rFs7oM=Dj$7$F$$$^$9!#(B Herbelin$B$5$s$N9V1i$O(BFLOPS2012$B$N$*OC$N3HD%HG$G$9!#(B $B$I$&$>$4MhD0$/$@$5$$!#(B $BD9C+@n???M(B <hassei(a)kurims.kyoto-u.ac.jp> $B5~ETBg3X?tM}2r@O8&5f=j(B ==================================================== Date: 28 May 2012 (Monday) 14:30-17:00 14:30-15:30 talk by Vivek Nigam 16:00-17:00 talk by Hugo Herbelin Venue: Room 478, General Research Building No.2, Kyoto University (Access information & map: http://www.kyoto-u.ac.jp/en/access http://www.kurims.kyoto-u.ac.jp/~hassei/map-2.jpg) $BCm!'?tM}2r@O8&5f=jK\4[$G$O$"$j$^$;$s!#(B $BI4K|JW$N$=$P$NAm9g8&5fFs9f4[$N(B4$B3,$G$9!#(B ==================================================== Speaker: Vivek Nigam (Ludwig Maximilian University of Munich) Title: An Extended Framework for Specifying and Reasoning about Proof Systems Abstract: It has been shown that linear logic can be successfully used as a framework for both specifying proof systems for a number of logics, as well as proving fundamental properties about the specified systems. In this paper, we show how to extend the framework with subexponentials in order to be able to declaratively encode a wider range of proof systems, including a number of non-trivial proof systems such as a multi-conclusion intuitionistic logic, classical modal logic S4, and intuitionistic Lax logic. Moreover, we propose methods for checking whether an encoded proof system has important properties, such as if it admits cut-elimination, the completeness of atomic identity rules, and the invertibility of its inference rules. Finally, we present a tool implementing some of these specification/verification methods. This is a joint work with Giselle Reis and Elaine Pimentel. ==================================================== Speaker: Hugo Herbelin (Laboratoire PPS, CNRS, INRIA & Universite Paris Diderot) Title: Classical call-by-need sequent calculi: The unity of semantic artifacts Abstract: We systematically derive a classical call-by-need sequent calculus, which does not require an unbounded search for the standard redex, by using the unity of semantic artifacts proposed by Danvy et al. The calculus serves as an intermediate step toward the generation of an environment-based abstract machine. The resulting abstract machine is context-free, so that each step is parametric in all but one component. The context-free machine elegantly leads to an environment-based CPS transformation. This transformation is observationally different from a natural classical extension of the transformation of Okasaki et al., due to duplication of un-evaluated bindings. We further demonstrate the usefulness of a systematic approach by deriving an abstract machine and CPS for an alternative classical call-by-need calculus. (Joint work with Zena M. Ariola, Paul Downen, Keiko Nakata & Alexis Saurin) ====================================================

1 0

第89回プログラミング研究会開催案内
by Takahito Aoto 22 May '12

22 May '12

＊＊＊＊複数受け取られた方はご容赦ください＊＊＊＊情報処理学会第89回プログラミング研究発表会開催のご案内をさせて頂きます． 6月21日(木)・22日(金)に小樽にて開催されます．皆様のご参加をお待ちしております．また，第1日目の夜に懇親会を予定しています．懇親会への参加をご希望の方は 6月14日(木)までに下記の要領で花井までお申し込みください．(発表会への参加自体については事前の申し込みは不要です．) ------------------------------------ To: ryo.hanai [at] aist.go.jp Subject: PRO89-party 6月21日(木)の懇親会に参加します．御名前: 御所属: 区別: 学生・一般 (6月14日(木)までにお知らせ下さい．) ------------------------------------ なお，下記のプログラムで，発表の順番につきましては今後変更される可能性がございますのでご了承ください．最新情報は以下のWEBページに掲載致します． http://www.jsk.t.u-tokyo.ac.jp/pro-2012-1/ --- 担当: 花井亮(産総研)，青戸等人(東北大学) ================================================================= 情報処理学会第89回プログラミング研究発表会プログラム ================================================================= 日程： 2012年6月21日（木)・22日（金）場所：小樽市民センター 3階研修室〒047-0031 小樽市色内2丁目13番5号 JR小樽駅より徒歩5分 ※ 1件あたり45分 (発表25分，質疑・討論20分) ※ 発表の順番につきましてはまだ確定ではありませんのでご了承ください． 6月21日(木) セッション１：14:15-15:45 2012-1-(1)：14:15-15:00 「ビットマップマーキングを利用したマークコンパクトごみ集めのJikes RVM への実装」 ○森川和哉, 鵜川始陽, 岩崎英哉（電気通信大） 2012-1-(2)：15:00-15:45 「マイコン制御学習用プログラミング言語の設計と実装」 ○谷岡政宏（北海道職業能力開発大学校） 15:45-16:00 休憩セッション２：16:00-17:30 2012-1-(3)：16:00-16:45 「文脈指向言語EventCJへの合成層の導入」 ○紙名哲生（東京大）, 青谷知幸（北陸先端大）, 増原英彦（東京大） 2012-1-(4)：16:45-17:30 「文脈指向プログラムの資源利用解析に基づく層活性解析法」 ○青谷知幸（北陸先端大）, 紙名哲生, 増原英彦（東京大） 19:00-21:00 懇親会 6月22日(金) セッション３：10:00-11:30 2012-1-(5)：10:00-10:45 「スクリプト言語KonohaScriptにおけるLLVMを用いたJust-in-timeコンパイラの実装と評価」 ○井出真広, 志田駿介, 倉光君郎（横浜国立大） 2012-1-(6)：10:45-11:30 「アトミックグループで拡張された正規表現のオートマトンへの変換」 ○杉山聡, 南出靖彦（筑波大） =================================================================

1 0

Jump to page:

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Logic-ml