Logic-ml

9 participants
1781 discussions

[CFP] 情報処理学会第86回プログラミング研究会
by Kazuyuki Shudo 28 Aug '11

28 Aug '11

皆様、東工大首藤です。発表申込の締切まで一週間を切りました．再度のご案内をさせていただきます．この場を借りて2011年度第3回情報処理学会プログラミング研究発表会の発表募集のご案内をさせて頂きたく存じます．プログラミング研究会(PRO)は，・プログラミング言語の設計，処理系の実装・プログラミングの理論，基本概念・プログラミング環境，支援システム・プログラミング方法論，パラダイム・これらを応用したシステムの開発事例・その他，プログラミングに関する面白い話題を対象とした研究発表の場で，1998年度から毎年3〜4回のペースで論文誌を発行しています．PRO論文誌は研究会と密接にリンクしており，研究会で発表されたもののうちあらかじめ論文投稿を希望し，論文原稿を提出されているものが査読の対象となっています（論文誌投稿を希望しない発表も歓迎します）．おおむね研究会から3週間で論文の採否が決定されるという迅速さも大きな特徴です．2011年度第3回研究会も多くの発表ならびに論文投稿をお待ちしております．参加費は無料です．申込〆切は9月2日(投稿〆切は10月1日)ですので，よろしくご検討ください．なお，多数の発表申込みがある場合には，発表をお断りすることがございますので，お早めにお申し込みください．第86回プログラミング研究会(PRO-2011-3)発表募集日程：　2011年 11月 1日(火)・2日(水) 会場：神奈川近代文学館〒231-0862 横浜市中区山手町110 港の見える丘公園内 http://www.kanabun.or.jp/ 発表申込締切: 2011年 9月 2日(金) 投稿論文原稿提出締切: 2011年 10月 1日(金) 申込先：首藤一幸（東京工業大学）　E-mail: ipsj-pro86 [at] shudo.net 　Tel/Fax: 03-5734-3211 案内ページ: http://www.shudo.net/sigpro/2011-3/ ・申込みに当たっての注意はプログラミング研究会のページ http://www.ipsj.or.jp/sig/pro/ を参照してください．・できるだけE-mailでお願いします．・申込み後返信がない場合はご連絡下さい．

1 0

[参加募集] 日本ソフトウェア科学会第28回大会
by Yukiyoshi Kameyama 25 Aug '11

25 Aug '11

皆様， 9月下旬に沖縄・那覇で開催される日本ソフトウェア科学会第28回大会の参加募集をお送りします．是非御参加ください． -- 亀山幸義 (筑波大学) http://logic.cs.tsukuba.ac.jp/~kam -------------------------------------------------------------------------- 日本ソフトウェア科学会第28回大会日時：2011年9月26日(月) [プレイベント] 2011年9月27日(火)〜29日(木) [大会本体] 会場：沖縄産業支援センター・沖縄県市町村自治会館 (沖縄県那覇市) http://jssst11.kuis.kyoto-u.ac.jp/ -------------------------------------------------------------------------- 熱い企画満載です！ -------------------------------------------------------------------------- 日本ソフトウェア科学会では第28回大会を9月27日(火)から29日(木)まで沖縄県那覇市で開催します．今年の大会は，湊真一先生の招待講演をはじめ，特別講演，研究会セッション，ソフトウェア論文セッション，一般セッション，デモ・ポスターセッション，萌芽セッション，チュートリアル，PPLサマースクールなど盛り沢山の内容で開催します．今年から大会本体の事前参加登録が必要となりましたので，ご注意ください．皆様のご参加をお待ちしております． ■概要招待講演・BDD/ZDDを基盤とする離散構造処理系の技法と最近の展開湊　真一 (北海道大学情報科学研究科 / JST ERATO) 特別講演・あみぐるみのための3次元モデリングと製作支援インタフェース (日本ソフトウェア科学会第15回論文賞受賞論文) 五十嵐悠紀, 五十嵐健夫, 鈴木宏正出典：コンピュータソフトウェア, Vol. 26, No. 1, pp. 51-58, 2009 ・Java言語への変換によるポインタ演算の安全な実装方式 (日本ソフトウェア科学会第15回論文賞受賞論文) 上嶋祐紀, 住井英二郎出典：コンピュータソフトウェア, Vol. 26, No. 1, pp. 139-154, 2009 ・Balanced Trees Inhabiting Functional Parallel Programming (ACM ICFP 2011採択論文) 森畑明昌, 松崎公紀出典：16th ACM SIGPLAN International Conference on Functional Programming (ICFP 2011), 2011 一般の登壇発表・研究会セッション - プログラミング論研究会(PPL) - マルチ・エージェントと協調計算研究会(MACC) 「MACC企画セッション：エージェントシミュレーション」(第一線の研究者による講演) - インタラクティブシステムとソフトウェア研究会(ISS) - ソフトウェア工学の基礎研究会(FOSE) - ディペンダブルシステム研究会(DSW) - ネットワークが創発する知能研究会(EIN) ・ソフトウェア論文セッション・一般セッションデモ・ポスターセッション萌芽セッション(大会と同時開催の併設イベント) プレイベント・チュートリアル「ストリーミングコンピューティングの基礎と実践」 http://www.jssst.or.jp/tutorial/detail/id=131 日時：9月26日(月) 13:00〜18:00 ・PPLサマースクール2011「クラウドのプログラミング」 http://ppl.jssst.or.jp/index.php?ss2011 日時：9月26日(月) 10:00〜17:00 大会の詳細については以下のウェブサイトをご覧ください． http://jssst11.kuis.kyoto-u.ac.jp/ ■参加登録大会本体と萌芽セッションへの参加登録については，日本ソフトウェア科学会事務局が準備する以下の参加登録ページより事前参加登録を行い， 9月20日(火) までに参加費をお振り込みください． https://feb.db-boss.com/asas/seminar/regist.asp?sid=361 当日参加登録は原則として受け付けない予定です．また，プレイベントへの参加方法については各プレイベントのウェブサイトでご確認ください． ■組織大会委員長遠藤聡志 (琉球大学) 運営委員長河野真治 (琉球大学) プログラム委員長八杉昌宏 (京都大学) プログラム委員会八杉昌宏 (委員長, 京都大学) 明石修 (NTT未来ねっと研究所) 五十嵐淳 (京都大学) 伊知地宏 (ラムダ数学教育研究所) 岩崎英哉 (電気通信大学) 馬谷誠二 (京都大学) 大沢英一 (はこだて未来大学) 亀山幸義 (筑波大学) 栗原聡 (大阪大学) 河野健二 (慶應義塾大学) 志築文太郎 (筑波大学) 杉山安洋 (日本大学) 中野圭介 (電気通信大学) 並木美太郎 (東京農工大学) 番原睦則 (神戸大学) 細部博史 (国立情報学研究所) 増原英彦 (東京大学) ■お問合せ研究発表，プログラムについてお問合せの際はプログラム委員長(八杉昌宏)宛てに以下へメールをお送りください． yasugi*ＡＴ*kuis.kyoto-u.ac.jp (*ＡＴ*は@に置き換えてください) その他，大会全般についてのお問合せは以下へお願いします． jssst11q*ＡＴ*kuis.kyoto-u.ac.jp (*ＡＴ*は@に置き換えてください) --------------------------------------------------------------------------

1 0

【講演募集】 RIMS 研究集会「記述集合論の展望」 (10/19 〜 21)
by FUJITA Hiroshi 24 Aug '11

24 Aug '11

愛媛大学の藤田です．残暑厳しき候，みなさまいかがお過ごしでしょうか．集合論分野のRIMS研究集会の講演申し込みの第一次締め切りが近付いてまいりましたので，再度お知らせいたします．今年度の集合論分野のRIMS研究集会は，「記述集合論の展望」 (Aspects of Descriptive Set Theory) という表題のもと，日時: 2011年10月19日(水) 9:00 より同21日(金) 17:00 まで会場: 京都大学数理解析研究所 420号室にて開催される運びとなっております．広い意味で記述集合論に関連する諸分野 (実数の集合論，内部モデル，強制法，巨大基数公理，集合論的実解析学，など) の講演を募ります． **** これまでのところ，講演申し込みが少なくてちょっと困っています．講演していただける方は，お名前と所属と職名 (それぞれ英語表記も) 講演タイトル (ひとまず未定でも結構です) を，できれば8月中を目処に藤田博司 (愛媛大学理学部) fujita.hiroshi.mh(a)ehime-u.ac.jp までお知らせください．タイトル未定の場合，どんな分野の話になりそうか大まかにでもお伝えくだされば，プログラム編成上助かります．旅費の補助が必要な方は，あわせてお知らせください．この研究集会の情報は次のWebサイトでも発信いたします． http://www.math.sci.ehime-u.ac.jp/~fujita/rims2011/index.ja.html (日本語) http://www.math.sci.ehime-u.ac.jp/~fujita/rims2011/index.en.html (英語) をご覧ください．英語版ページには短縮URL http://ehimath.zz.tc/sets2011 もご用意しました．随時更新してまいりますのでご覧ください． -- 藤田博司 <fujita.hiroshi.mh(a)ehime-u.ac.jp> 愛媛大学大学院理工学研究科

1 0

Final Call for Participation: MOL 12
by Makoto Kanazawa 22 Aug '11

22 Aug '11

FINAL CALL FOR PARTICIPATION (Registration closes on August 25, 2011.) 12th Meeting on Mathematics of Language (MOL 12) Nara, Japan, September 6-8, 2011 http://sites.google.com/site/mol12nara/ Invited Speakers Kit Fine, New York University Andreas Maletti, University of Stuttgart Program available at http://sites.google.com/site/mol12nara/program SATELLITE EVENT Second Workshop on Multiple Context-Free Grammars and Related Formalisms (MCFG+2) Information on http://sites.google.com/site/mol12nara/mcfgplus Contact: mol12(a)googlegroups.com

1 0

第二十二回ALGI（代数，論理，幾何と情報科学研究集会）のプログラム（ほぼ決定）と参加募集
by 西澤弘毅 19 Aug '11

19 Aug '11

logic-ml メーリングリストの皆様，鳥取環境大学の西澤弘毅と申します。直前のご連絡になりましたが、第二十二回 ALGI（代数，論理，幾何と情報科学研究集会）のプログラム決定のお知らせと参加の募集をさせていただきます。 ALGI (Algebra, Logic, Geometry and Informatics) は、代数学や論理学、幾何学の情報科学への応用について、および情報科学の代数学や論理学、幾何学への応用についての研究集会で、年一回の頻度で開催されています。 ALGIの趣旨や過去の集会の情報がウェブページ http://sakura.math.kyushu-u.ac.jp/algi/ にありますので、参考までに御覧ください。このたび、第二十二回ALGIを開催することになりました。 **************************************************************** * 第二十二回 ALGI（代数，論理，幾何と情報科学研究集会） * * * * 2011年8月23日（火）13:15 〜24日（水）12:30 * * 東京大学　柏キャンパス第2総合研究棟3階315会議室（千葉県柏市）* * * * 開催のお知らせと参加・講演の募集 * **************************************************************** プログラムの詳細はウェブページ http://sakura.math.kyushu-u.ac.jp/algi/22/ に掲載されております。簡略版は下記の通りです。ただし、今後講演申込みがございましたら、 23日の休憩時間を減らすなどして１件のみ対応することが可能です。８月２３日（火） 13:15 - 13:30 オープニング＋連絡など 13:30 - 14:15 星野直彦（京都大学数理解析研究所）演題： A characterisation of unique decomposition categories 14:15 - 14:45 休憩 14:45 - 16:00 宮部賢志（京都大学数理解析研究所）演題： An optimal semimeasure and its convergence 神志那純，潮俊光（大阪大学大学院基礎工学研究科），木下佳樹（産業技術総合研究所）演題：部分観測Mealyオートマトンのスーパバイザ制御への余代数的アプローチ 16:00 - 16:30 休憩 16:30 - 17:30 末永幸平（京都大学情報学研究科日本学術振興会特別研究員 (PD)）演題： Programming with Infinitesimals: A WHILE-Language for Hybrid System Modeling 夕方：懇親会（柏キャンパス内「お魚倶楽部　はま」）８月２４日（水）10:00 - 10:45 西澤弘毅（鳥取環境大学）演題： Relational Representation Theorem for Algebraic Quantales with respect to Completely Coprime Elements and Atoms 10:45 - 11:00 休憩 11:00 - 12:00 倉永崇（名古屋大学大学院多元数理科学研究科）演題：認知幾何学に向けて木下佳樹（AIST）演題： NBE through Yoneda revisited in Agda 12:00 - 12:30 クロージング＋連絡などできるだけ多くの皆さんのご参加をお待ちしております。懇親会への参加希望は、初日に受け付けます。西澤弘毅（鳥取環境大学）古澤仁（鹿児島大学理学部）会場の手配などは東京大学の松野裕さんと大島聡史さんにお願いしております。 -- 西澤弘毅鳥取環境大学環境情報学部情報システム学科〒689-1111鳥取市若葉台北1-1-1 koki(a)kankyo-u.ac.jp (koki.nishizawa(a)gmail.com に転送) TEL: 0857-38-6786

1 0

Open Position at the RCIS/JAIST
by Norbert Preining 17 Aug '11

17 Aug '11

Open Position for one post doctoral researcher at RCIS/JAIST At the Research Center for Integrated Science [1] at the Japanese Advanced Institute of Science and Technology [2] a post doctoral researcher position is open starting from October. Fields of research: Mathematical Logic, in particular Semantic/Proof-theoretic methods in Nonclassical logics (including substructural logics, intermediate and many-valued logics) and related fields Application: Application should comprise a curriculum vitae, a short statement on research interests, preferrably a recommendation letter, per email to ono(a)jaist.ac.jp, preining(a)jaist.ac.jp (both) Deadline for application: 17 September 2011 Inquiries should be sent to the above adresses, too. ONO Hiroakira PREINING Norbert [1] http://www.jaist.ac.jp/rcis/en [2] http://www.jaist.ac.jp/ ------------------------------------------------------------------------ Norbert Preining preining(a){jaist.ac.jp, logic.at, debian.org} JAIST, Japan TeX Live & Debian Developer DSA: 0x09C5B094 fp: 14DF 2E6C 0307 BE6D AD76 A9C0 D2BF 4AA3 09C5 B094 ------------------------------------------------------------------------

1 0

証明論研究集会のご案内（第２報）
by Suzuki Toshio 16 Aug '11

16 Aug '11

証明論研究集会のご案内（第２報）皆様首都大学東京の鈴木登志雄です。さて、毎年恒例の証明論と関連分野（証明論、逆数学、限定算術、非古典論理、リカージョン、アルゴリズム的ランダムネス、計算量理論、ゲーム理論における論理学的問題など）のワークショップを以下のように開催することになりました。皆様のご講演、ご参加を心よりお待ち申し上げます。 2011年証明論と計算論研究集会（WORKSHOP ON PROOF THEORY AND THEORY OF COMPUTING 2011）９月１２日（月）から１４日（水）東京都八王子市南大沢１−１首都大学東京国際交流会館中会議室集会のウェブサイト http://www.ac.auone-net.jp/~bellp/meeting/proof2011.html アクセス：京王相模原線南大沢駅、徒歩10分新宿から南大沢までは電車で最速約３４分（京王線準特急・京王八王子行に乗り、調布で京王相模原線急行・橋本行に乗り換え）。 http://www.tmu.ac.jp/university/campus_guide/access.html ご講演いただける方は、プログラム作成のため、以下にご記入の上、８月２６日（土）までに鈴木登志雄宛にご連絡お願いします。未定の部分はわかる範囲でご記入ください。宛先 toshio-suzuki(a)tmu.ac.jp --------------------------------------------- お名前：ご所属：参加日程：講演：講演予定(連絡済)/ 講演予定/ 講演はしない講演希望時間： 60分 / （　分を希望）講演タイトル： (未定の場合は未定とご記入ください．) 備考： --------------------------------------------- 発表なしのご参加の場合も、会場確保のため上記の日までにご連絡いただけると助かります。宛先は上記と同じです。それでは、よろしくお願いいたします。関連する最近の集会： Feb. 2011, Workshop on Proof Theory and Computability Theory http://www.jaist.ac.jp/is/labs/ishihara-lab/wptct2011/ Sep. 2010, Formal Systems and Computability Theory http://www.kurims.kyoto-u.ac.jp/~kyodo/kokyuroku/contents/1729.html -- 鈴木登志雄首都大学東京理工学研究科数理情報科学専攻 toshio-suzuki(a)tmu.ac.jp

1 0

SLACS 2011 のご案内および講演募集（再送）
by Kamo Hiroyasu 16 Aug '11

16 Aug '11

login-ml のみなさま（重複して受信された場合はご容赦ください。） SLACS 2011 の世話人をおおせつかっている奈良女子大学の鴨浩靖です。ご案内および講演募集を再送させていただきます。第28回記号論理と情報科学研究集会 (SLACS 2011) は，奈良女子大学で開催の予定です．SLACSは，記号論理学と計算機科学の研究者や学生の相互交流を目的として開催されている研究集会です．完成された研究のみならず，発展途上の話題も大歓迎です． SLACS 2011 のページは http://taurus.ics.nara-wu.ac.jp/slacs2011/ です。 SLACS全般のページは http://www.sato.kuis.kyoto-u.ac.jp/SLACS です。開催要項開催日：2011年9月12日(月)午前〜 9月13日(火)午後（講演が少ない場合は、開始を遅らせます）場所：奈良女子大学G棟G302教室奈良女子大学へは、大阪または京都から近鉄が便利です。近鉄奈良駅から徒歩約5分です。当日は夏期休暇中で南門が閉鎖されているため、正門におまわりください。アクセスマップ http://www.nara-wu.ac.jp/accessmap.html キャンパスマップ http://www.nara-wu.ac.jp/image_c/campusmap2.jpg 懇親会：9月12日夜に懇親会を予定しています．詳細はプログラム確定後、お知らせします。参加費，参加申込はともに不要です．（懇親会につきましては費用を御負担いただきます．）講演を希望される方は、・題目・講演者名・e-mail address ・所属・梗概・講演時間・講演に必要な道具などの情報を slacs2011(a)mensa.ics.nara-wu.ac.jp までお知らせください。とりあえず、「講演したいと思っている」程度の不完全情報でも結構です。多くの皆さんのご講演・ご参加をお待ちしております。奈良女子大学理学部情報科学科鴨浩靖 _______________________________________________ Logic-ml mailing list Logic-ml(a)sato.kuis.kyoto-u.ac.jp http://www.sato.kuis.kyoto-u.ac.jp/cgi-bin/mailman/listinfo/logic-ml

1 0

PEPM 2012: Second Call for Papers
by Kohei SUENAGA 12 Aug '11

12 Aug '11

皆様、（重複して受け取られた場合はどうぞご容赦ください。）京都大学の末永幸平と申します。来年の1月23〜24日にPOPL'12と併設で開催される PEPM'12の2nd CFPをお送りいたします。論文投稿の締切は今年の10月10日です。 Invited speaker が Markus Pueschel氏 (ETH Zurich, Switzerland) と Martin Berger氏 (University of Sussex, UK) に決まりました。 Partial Evaluation と会議名についておりますが、それに限らず広くプログラム変換・解析に関するトピックを扱っております。また、現実のソフトウェアへの適用に関するケーススタディも発表することができます。どうぞ投稿をご検討ください。末永幸平京都大学情報学研究科日本学術振興会特別研究員 (PD) ksuenaga(a)sato.kuis.kyoto-u.ac.jp -- ACM SIGPLAN 2012 Workshop on Partial Evaluation and Program Manipulation January 23-24, 2012. Philadelphia, Pennsylvania, USA (co-located with POPL'12) Call For Papers Paper submission deadline: Mon, October 10, 2011, 23:59, GMT http://www.program-transformation.org/PEPM12 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: Mon, October 10, 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

研究員の募集
by koba 03 Aug '11

03 Aug '11

皆様、＃複数受け取られましたらご容赦ください．東北大学の小林と申します．当研究室では現在，高階モデル検査（高階再帰スキームのモデル検査）とそのプログラム検証などへの応用をテーマとした研究を精力的に進めており，プロジェクトに携わるポストドクの研究員を探しております．身近にご興味のある方がいらっしゃいましたら，8月15日（必着）までに小林 (koba(a)ecei.tohoku.ac.jp) までメールでお知らせいただければ幸いです。その際、できれば略歴および論文リスト（フォーマット自由）もメールに添えるかまたは郵送でお送りください。（後日、さらに詳細な資料をお願いする可能性があります）．募集の条件は概ね以下のとおりです。 ================ 着任時期：2011年10月〜2012年4月の間（さらに数ヵ月の前後は応相談）任期：年度単位の更新で、業績により最長2016年3月まで延長可能給与：月額30〜35万円程度（大学の規定による．細かい条件は応相談）研究テーマ：高階モデル検査（高階再帰スキームのモデル検査）および、そのプログラム検証やデータ圧縮への応用。高階モデル検査については，下記のプロジェクトの概要および，小林らによる最近のPOPL 2009/2010やPLDI 2011, LICS 2009等の論文をご覧ください。条件： - 着任時に博士号を取得していること - 理論計算機科学全般に明るいこと． - 以下の中の２つ以上のトピックに詳しいか、または１つ以上のトピックに詳しくプログラミング能力が特に高いことモデル検査（特にソフトウェアモデル検査）型システムゲーム意味論プログラム解析オートマトンと形式言語理論自動定理証明 (可逆)データ圧縮技術問い合わせ先：小林直樹東北大学大学院情報科学研究科情報基礎科学専攻〒980-8579 仙台市青葉区荒巻字青葉6-3-09 TEL: 022-795-7177 FAX: 022-795-7526 Email: koba(a)ecei.tohoku.ac.jp ====================== 研究プロジェクトの概要 ====================== モデル検査はシステムが与えられた性質を満たすか否か網羅的に検証する手法であり，近年ハードウェアやソフトウェア検証の分野で大きな成功を修めている．高階モデル検査は，検証対象のシステムとして無限木を記述する高階文法を扱うものであり，従来の有限状態モデル検査やプッシュダウンモデル検査の真の拡張になっている．最近になって，我々は，高階モデル検査が高レベルプログラムの自動検証に有用であることを示すとともに，高階モデル検査問題が多重指数関数完全の計算量クラスに属するにもかかわらず，多くの入力に対して現実的な時間で動作するようなモデル検査アルゴリズムを考案し，世界初の高階モデル検査器の実現に成功した．さらに，それに基づいて関数型言語MLの小さなサブセットに対するソフトウェアモデル検査器を実現した．本研究プロジェクトでは，上記の成果をさらに発展させ，（１）高階モデル検査の理論および実装技術の発展による，より高速な高階モデル検査器の実現（２）関数型言語やオブジェクト指向言語に対するソフトウェアモデル検査器（つまり高階モデル検査に基づくプログラム自動検証器）の実現（３）データ圧縮など，高階モデル検査の新たな応用分野の開拓を目指す．

1 1

Jump to page:

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Logic-ml