Logic-ml

9 participants
1781 discussions

CFP: HOR 2012
by Makoto Hamana 01 Mar '12

01 Mar '12

皆様、高階書換え系のワークショップ HOR'12 のご案内です。 6月のRTA'12に併設開催予定で、今年で6回目となります。バリバリの書換え研究から、証明支援系やプログラミング言語への応用まで、高階書換えに関係する論文を広く募集いたします。今年はさらにすでに発表された論文の発表枠も設け、盛上げたく思っておりますので、ぜひ投稿をご検討ください。なおポストプロシーディングスは、EPTCSから出版予定です。 -- 浜名誠/群馬大学 ===================================================================== Call for papers 6th International Workshop on Higher-Order Rewriting HOR 2012 June 2, 2012, Nagoya, Japan Colocated with RTA'12 http://www.cs.gunma-u.ac.jp/events/hor/ ====================================================================== HOR is a forum to present work concerning all aspects of higher-order rewriting. The aim is to provide an informal and friendly setting to discuss recent work and work in progress concerning higher-order rewriting. The following is a non-exhaustive list of topics for the workshop: * Applications: proof checking, type checking, theorem proving, functional programming, declarative programming, program transformation, using some notions of higher-order rewriting. * Foundations: pattern matching, unification, strategies, termination, syntactic properties, type theory, for higher-order rewriting. * Frameworks: graph rewriting, net rewriting, comparisons of different formats. * Implementation: explicit substitution, rewriting tools, compilation techniques. * Semantics: semantics of higher-order rewriting, higher-order abstract syntax, categorical rewriting. Important dates --------------- Paper submission: March 19, 2012 Notification: April 20, 2012 Final version: May 10, 2012 Workshop: June 2, 2012 Submissions ----------- Two categories of papers are solicited: - Category A: Extended abstracts of new results, describing work in progress, or problems in higher-order rewriting. - Category B: Short versions of recently published or submitted elsewhere articles on higher-order rewriting. Papers in this category are for presentation only, and not considered as candidates for the post-workshop proceedings. Papers in both categories should be between 2 and 5 pages, and should note the category (either A or B). Papers are formatted according to EPTCS style, and submitted electronically via the EasyChair submission website. Papers will be judged on relevance, originality, correctness and usefulness. Please address your questions to the PC chair: hamana at cs.gunma-u.ac.jp. Proceedings ----------- The proceedings of HOR 2012 will be made available on the HOR 2012 web page, and a printed version will be distributed at the workshop. Post-workshop proceedings of extended abstracts of selected contributions is planned to be published as a volume of EPTCS. Program Committee ------------------- Andreas Abel (Ludwig-Maximilians-University Munich, Germany) Frederic Blanqui (INRIA, France) Makoto Hamana (Gunma University, Japan) (chair) Stefan Kahrs (University of Kent, UK) Fer-Jan de Vries (University of Leicester, UK) Program and Organizing Chair ---------------------------- Makoto Hamana (Gunma University, Japan)

1 0

2012LLS
by Toshihiko Kurata 29 Feb '12

29 Feb '12

kisoron-ml，logic-mlの皆様，以前ご案内させて頂きました「ラムダと論理の研究会」ですが，セミナーハウスでの宿泊について学生部屋に限りまだ余裕があるとのことです．折角の機会ですので，再度ご案内させて頂きます．関心のあります学生さんは倉田（法政大学，kurata(a)hosei.ac.jp) まで遠慮なく御問合わせ下さい．なお，セミナー自体の参加希望は直前まで可能です．詳細情報は http://www.i.hosei.ac.jp/~kurata/2012LLS/ にありますので，よろしくお願いいたします． ---- Toshihiko Kurata, Hosei University e-mail kurata(a)hosei.ac.jp

1 0

JAIST Advanced Lecture Series (6)
by Hiroakira Ono 28 Feb '12

28 Feb '12

　　　JAIST先端レクチャー・シリーズ（第6回）の開催について　来る3月13日（火）に，下記の講演会を開催します。ホットなトピックスについての分かりやすい講演ですので，多数の皆様（特に学生の方）に参加いただきたく，ご案内申し上げます。　　　　　　　　　　　　　　　記　１．日　　時　平成24年3月13日（火）15:00〜17:00 　２．場　　所　JAIST　知識科学研究科　中講義室　３．講演題目　“Ontology-Based Data Access and Constraint 　　　　　　　　　Satisfaction” http://www.jaist.ac.jp/rcis/seminar/advanced/6 　４．講演者　Frank Wolter 客員教授　　　　　　　（リヴァプール大学　教授）　５．担当教員　小野寛晰 JAIST 先端融合領域研究院: http://www.jaist.ac.jp/rcis/l ogic-activities ------------------------------------------------------------------------- We would like to inform you of the JAIST Advanced Lecture Series 6 by a guest professor of JAIST as follows. DATE：March 13, 2012 15:00-17:00 PLACE：JAIST KS Lecture Hall TITLE：“Ontology-Based Data Access and Constraint Satisfaction” SPEAKER：Prof. Frank Wolter (Univ. of Liverpool, Guest Professor of JAIST) ABSTRACT： In recent years, the use of ontologies to access instance data has become increasingly popular. The general idea is that an ontology provides a vocabulary or conceptual model for the application domain, which can then be used as an interface for querying instance data and to derive additional facts. In this presentation, I will first introduce ontology-based data access (OBDA). I will focus on ontologies given in description logics or, equivalently, the web ontology language OWL. I will then establish a very close link between OBDA and constraint satisfaction problems with finite templates (CSP). Rather surprisingly, for the basic description logic ALC (=modal logic) OBDA and CSP turn out to be essentially equivalent. This result has a large number of consequences for ALC and OBDA in general. I will focus on the following non-uniform complexity problem: what is the complexity of query answering for a fixed ontology? I will present general conditions under which this problem is in PTime and, respectively, coNP-hard. Using the CSP connection is shown that for ALC there is a P/coNP dichotomy for conjunctive query answering if, and only if, the famous, and still open, Feder/Vardi dichotomy conjecture for CSP holds. The talk is based on joint work with Carsten Lutz.

1 0

The second「論数哲」(PhilLogMath) workshop
by Shunsuke Yatabe 21 Feb '12

21 Feb '12

The second「論数哲」"Ron-Suu-Tetsu" (PhilLogMath) workshop We will hold the 2nd 「論数哲」(PhilLogMath) workshop. Our aim is to provide opportunities of detailed discussions among philosophers, logicians and mathematicians. Everyone is welcome. website url: http://researchmap.jp/jovzjd6b4-21098/#_21098 Date : March 14 (Wed) Place: Seiryo Kaikan (Nagata-cho, Tokyo) Room 4A and 4B (floor 4) http://metropolis.co.jp/listings/venues/type/stage-venue/seiryo-kaikan/ Time table 9:00-10:30 Takuro Onishi (Kyoto University) "BHK-interpretation and Bilateralism" 10:30-12:00 Katsuhiko Sano (JAIST) "An `Impossibility' Theorem in Radical Inquisitive Semantics" 13:30-15:00 Masahiko Sato (Kyoto University) "Bootstrapping Mathematics" 15:15-16:45 Richard Dietz (The University of Tokyo) "Comparative Concepts" 17:00-18:30 Conrad Asmus (JAIST) " Vagueness and Revision Sequences" Any slot consists of 60 minutes talk and 30 minutes discussion basically. All talks are in English. Abstracts: * Takuro Onishi "BHK-interpretation and Bilateralism" In this talk, H.Wansing's inferentialist semantics for Bi-intuitionist logic is examined.Bi-intuitionist Logic (a.k.a. Heyting-Brouwer logic) is an extension of Intuitionist Logic with a connective dual to implication. It is sort of an amalgamation of intuitionist and dual-intuitionist logic. Accordingly, BHK-like, inferentialist, or proof-theoretic semantics for the logic would be a bilateralist one appealing to not only "proof" but also"dual proof (disproof)" as primitive notions. In his "Proofs,disproofs and their duals" (2010),Wansing gives a correctness (soundness) proof of a display system for bi-intuitionist logic in terms of the bilateralist semantics. I point out that his proof involves controversial assumptions concerning the relation between proofs and dual proofs and present an alternative view on how they get together. (Although Wansing discuss a BHK-like interpretation for strong negation and its dual as well, I will concentrate on logics without them in this talk.) *Katsuhiko Sano "An `Impossibility' Theorem in Radical Inquisitive Semantics" An aim of this talk is to show that it is impossible to provide a `natural' Kripke semantics with radical inquisitive semantics, recently proposed by Jeroen Groenendijk and Floris Roelofsen. Inquisitive semantics is a new formal framework for the semantics of both declarative and interrogative sentences. One of the main features of this semantics is that we assume there is no type distinction between the declarative and the interrogative, but we provide both classical and inquisitive meanings with each sentence. For example, the declarative sentence `Taro will drink tea or coffee.' proposes two alternatives `Taro will drink tea' and `Taro will drink coffee'. Inquisitive meaning captures such information of the alternatives. In conservative (non-radical) inquisitive semantics (Groenendijk and Roelofsen 2009), intuitionistic Kripke semantics captures how our group knowledge increases though a conversation, and also allows us to derive the inquisitive meaning of a sentence from the classical meaning. In the example above, we could give a reply `Taro won't drink tea or coffee' to the speaker. In conservative inquisitive semantics, however, we cannot cover such a negative reaction. Radical inquisitive semantics is an extension of conservative one such that we can provide with each sentence the positive and negative inquisitive meanings as well as the classical meaning. My contribution of this talk is to establish that *any* `natural' Kripke semantics fails to capture a link between the classical meaning and the negative inquisitive meaning. *Masahiko Sato "Bootstrapping Mathematics" It is well-known that any formal mathematical system can be faithfully encoded within PRA (Primitive Recursive Arithmetic). It is also commonly accepted that any well-established part of mathematics can be presented as a formal system. Thus, it seems that we can bootstrap mathematics, within a computer, simply by implementing PRA in it. However, we will show that this view is too naiive both from computer science point of view and from foundational point of view. We also discuss an alternative approach to this problem by giving an overview of a proof assistant system we are developing. *Richard Dietz "Comparative Concepts" Comparative concepts (such as ‘greener than’ or ‘higher than’)are fundamental to our grasp of associated categorical concepts (‘green’, ‘high’, respectively). Some comparative concepts seem natural, whereas other ones seem rather gerrymandered---e.g., compare ‘x is greener than y’ and ‘x and y are such that either (i) x and y are inspected before midday and x is greener than y, or (ii) x and y are inspected after midday and x is bluer than y’. What kind of cognitive structures under your ability to order objects? And why do we order objects the way we do,and not in other ways? The aim of this talk is to outline an account of comparative concepts within a conceptual spaces framework. The account bears for one on the account of naturalness for comparative concepts.For another, it bears on the theory of gradable concepts, i.e., the type of categorical concepts expressed by gradable terms in natural language.The approach is novel in that it carries some basic assumptions from Peter Gärdenfors' conceptual spaces account of categorical concepts over to comparative concepts (in his monograph ‘Conceptual Spaces’ [2000]).The offered approach is more general both (i) in that it supplies a framework for motivating various types of categorisation rules for gradable concepts, and (ii) in that it gives a model that subsumes ungraded categorisation as a limiting case. *Conrad Asmus "Vagueness and Revision Sequences" Theories of truth and vagueness are closely connected; in this article, I draw another connection between these areas of research. Gupta and Belnap’s Revision Theory of Truth is converted into an approach to vagueness. I show how revision sequences from a general theory of definitions can be used to understand the nature of vague predicates. The revision sequences show how the meaning of vague predicates are interconnected with each other. The approach is contrasted with the similar supervaluationist approach. *Workshop organizer (please replace [at] to @): Yuko Murakami Shunsuke Yatabe ( shunsuke.yatabe[at]aist.go.jp ) Takuro Onishi ( takuro.onishi[at]gmail.com ) -- Shunsuke Yatabe <shunsuke.yatabe(a)aist.go.jp> AIST/CVS (National Institute of Advanced Industrial Science and Technology / Research Center for Verification and Semantics) tel: +81-6-4863-5031 fax: +81-6-4863-5052

1 0

PPL2012 プログラム決定＆参加案内
by Koji Nakazawa 20 Feb '12

20 Feb '12

（重複の場合はご容赦ください．）京都大学の中澤です． 3月に和歌山県白浜温泉で開催される　第14回プログラミングおよびプログラミング言語ワークショップ (PPL2012) につきまして，プログラムが決定いたしましたのでお知らせします．参加登録の締切り（2月24日）が近づいております．　参加登録要領 http://ppl2012.cs.uec.ac.jp/registration.html をご参照の上，日本旅行の専用ページからご登録ください．皆様のご参加をお待ちしております．最新情報は引き続き下記webページにてお知らせします． -------------------------------------------------------------------------- 第14回プログラミングおよびプログラミング言語ワークショップ（PPL2012） http://ppl2012.cs.uec.ac.jp/ 主催: 日本ソフトウェア科学会プログラミング論研究会日程: 2012年3月8日(木)〜3月10日(土) 会場: 和歌山県西牟婁郡白浜温泉むさし http://www.yado-musashi.co.jp/ PPL2012は，プログラミングおよびプログラミング言語に関する研究者が一堂に会し，最新の研究成果の発表，および新たな研究課題についての討論やアイディア交換等を行うことを目的とした，合宿形式のワークショップです．プログラミングおよびプログラミング言語の理論・設計・実装・処理系などに関する研究発表が以下のカテゴリ別に行なわれます．カテゴリ１: 国内外で未発表の論文の発表カテゴリ２: 国際会議・学術雑誌等で既発表であるが，国内では未発表の研究の紹介カテゴリ３: ポスター・デモ発表 −−−−−−−−−− 3月8日(木) −−−−−−−−−− 14:15--14:20 オープニング 14:20--15:20 セッション1 (C1) Query-based RDF-object mapping with graph pattern matching Shunichi Amano, Futoshi Iwama, Hideki Tai, Hisashi Miyashita (IBM Research) (C1) XQueryプログラムに対するMacro Forest Transducersを用いた型検査機構白田靜哉(1), 中野圭介(2), 岩崎英哉(1) ((1)電気通信大学大学院情報理工学研究科, (2)電気通信大学先端領域研究センター) 15:40--16:40 セッション2 (招待講演) プログラム意味論・テンソル圏・量子トポロジー長谷川真人 (京都大学) 17:00--18:30 セッション3 (C2) A Modified GoI Interpretation for a Linear Functional Programming Language and its Adequacy 出典: 14th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2011), LNCS6604, pp.320--334, 2011. Naohiko Hoshino (Research Institute for Mathematical Sciences, Kyoto University) (C2) Constructing Correct Looping Arrows from Cyclic Terms: Traced Categorical Interpretation in Haskell 出典: 11th International Symposium on Functional and Logic Programming (FLOPS 2012), to appear. Makoto Hamana (Department of Computer Science, Gunma University) (C1) 顕在的契約計算におけるアップキャスト除去関山太朗, 五十嵐淳 (京都大学大学院情報学研究科) 20:00--22:00 セッション4 (ポスター・デモ1) A Higher-order Distributed Calculus with Name Creation (ポスター) Adrien Pi\'{e}rard, Eijiro Sumii (Tohoku University) 対応表明つきプロトコル記述からSpiCAへの変換と真正性検証 (ポスター・デモ) 佐藤悠史, 住井英二郎 (東北大学) HTML5構文解析のプッシュダウンオートマトンを用いた検証 (ポスター) 森俊介, 南出靖彦 (筑波大学) 抽象DPLLのIsabelle/HOLによる形式化と検証 (ポスター) 武井裕也 (筑波大学) 文字列解析によるクロスサイトスクリプティング脆弱性検査の改良 (ポスター) 木村将人, 南出靖彦 (筑波大学) A Practical Generate-Test-and-Aggregate Framework on Hadoop (ポスター) 劉雨(1), 江本健斗(2), 胡振江(3) ((1)総合研究大学院大学, (2)東京大学, (3)国立情報学研究所) メタラムダ計算の定式化 (ポスター) 岩井亜里紗, 浅井健一 (お茶の水女子大学) 高階依存型理論を用いた自然言語の意味論構築に向けて (ポスター) 中野悠紀, 戸次大介 (お茶の水女子大学) 対称ラムダ計算の定式化 (ポスター) 新井祐美, 浅井健一 (お茶の水女子大学) js_of_ocamlによるMikiβの実装に向けて (ポスター・デモ) 中野祥, 浅井健一 (お茶の水女子大学) 豊穣圏によるメタラムダ計算の意味論 (ポスター) 増子萌, 戸次大介 (お茶の水女子大学) LMNtal コンパイラにおけるアトム再利用最適化の再設計と実装 (ポスター) 信夫裕貴, 上田和紀 (早稲田大学) ハイブリッドシステムモデリング言語HydLaにおける統合開発環境HIDEの構築 (ポスター・デモ) 櫻庭翔, 上田和紀 (早稲田大学) LMNtal処理系における自由リンク確認機能の実現手法 (ポスター) 谷口直輝, 目黒学, 上田和紀 (早稲田大学) ハイブリッド制約言語HydLaへの入出力機能の導入とその応用例 (ポスター・デモ) 和田亮, 竹口輝, 上田和紀 (早稲田大学) JavaScriptアプリケーションの対話的実行時開発環境 (ポスター) 吉永卓矢, 脇田建 (東京工業大学) 遅延スイープ法における局所性の改善 (ポスター) 金野千顕, 小宮常康 (電気通信大学) イベント駆動型プログラミングのためのストリームを導入したJavaScript拡張言語の設計 (ポスター) 雪本修一, 小宮常康 (電気通信大学) 例外処理を用いた継続導入におけるオーバーヘッドの軽減 (ポスター) 片桐国建, 小宮常康 (電気通信大学) 部分コンパクションの実行頻度と Evacuation Area 選択法の改良 (ポスター) 加藤瞬, 鵜川始陽, 岩崎英哉 (電気通信大学) サーバサイドJavaScript処理系の開発について (ポスター・デモ) 高田祥, 鵜川始陽, 中野圭介, 岩崎英哉 (電気通信大学) FMMへの木スケルトンの適用 (ポスター) 佐藤重幸, 岩崎英哉 (電気通信大学) X-PCF --- {0,1,⊥}-無限列を表現とした実数上の形式計算体系 (ポスター) 寺山慧, 立木秀樹 (京都大学) ジョブ並列スクリプト言語Xcryptの他言語対応に向けて (ポスター・デモ) 上野優, 平石拓, 岩下武史, 中島浩 (京都大学) Azucar: コンパクト順序符号化を用いたSAT型制約ソルバー (デモ) 丹生智也, 田村直之, 番原睦則 (神戸大学) 相互再帰的なクラス定義の型推論に関する一考察 (ポスター) 樗木辰哉, 廣瀬貴裕, 木山真人, 芦原評 (熊本大学) −−−−−−−−−− 3月9日(金) −−−−−−−−−− 9:00--10:00 セッション5 (招待講演) 大脳皮質の計算論細谷晴夫 (理化学研究所脳科学総合研究センター，科学技術振興機構さきがけ) 10:20--11:50 セッション6 (C2) Extractability as Deduction Theorem in Subdirectional Combinatory Logic 出典: 8th International Workshop on Logic and Engineering of Natural Language Semantics (LENLS8), pp.80-93, 2011. Hiroko Ozaki, Daisuke Bekki (Ochanomizu University) (C1) Illative Combinatory Logic を用いた前提の定式化に向けて石下裕里, 戸次大介 (お茶の水女子大学大学院人間文化創成科学研究科) (C1) 一階述語条件論理とそのタブローシステム尾崎有梨, 戸次大介 (お茶の水女子大学) 13:30--14:30 セッション7 (C2) Predicate abstraction and CEGAR for higher-order model checking 出典: 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2011), pp.222-233, 2011. Naoki Kobayashi, Ryosuke Sato, Hiroshi Unno (Tohoku University) (C2) Programming with Infinitesimals: A WHILE-Language for Hybrid System Modeling 出典: 38th International Colloquium on Automata, languages and Programming (ICALP 2011), Volume Part II, pp. 392--403, 2011. Kohei Suenaga(1), Ichiro Hasuo(2) ((1)JSPS Research Fellow, Kyoto University, (2)University of Tokyo) 14:50--16:20 セッション8 (C2) Generate, Test, and Aggregate --- A Calculation-based Framework for Systematic Parallel Programming with MapReduce 出典: 22nd European Symposium on Programming (ESOP 2012), to appear. Kento Emoto(1), Sebastian Ficsher(2), Zhenjiang Hu(2) ((1)University of Tokyo, (2)National Institute of Informatics) (C1) 並列木縮約による並列データフロー解析森畑明昌 (東北大学電気通信研究所) (C1) Coqを使用したMapReduceアプリケーションの検証とScalaコードの抽出姜帆(1,2), 田辺良則(2), 本位田真一(1,2) ((1)東京大学大学院情報理工学系研究科, (2)国立情報学研究所) 16:40-18:10 セッション9 (C1) コードシェーカ: コード配置効果を考慮した適正な性能評価システム松田友希(1), 八杉昌宏(1), 鵜川始陽(2) ((1)京都大学大学院情報学研究科, (2)電気通信大学情報理工学研究科) (C2) Do We Really Need to Extend Syntax for Advanced Modularity? 出典: Modularity Visions track, 11th International Conference on Aspect-Oriented Software Development (AOSD 12), to appear. Shigeru Chiba, Michihiro Horie, Kei Kanazawa, Fuminobu Takeyama, Yuuki Teramoto (Tokyo Institute of Technology) (C1) コンパイラの型推論を利用した型デバッグ手法の提案対馬かなえ, 浅井健一 (お茶の水女子大学) 20:00--22:00 セッション10 (ポスター・デモ2) 型付き関数型言語からシェルスクリプトへの外部関数インタフェース (ポスター・デモ) 菊池大志, 上野雄大, 森畑明昌, 大堀淳 (東北大学) 定理証明系Coqを用いたSibling Propertyとハフマン木との同値性の形式的証明 (ポスター) 須田啓司, 山本光晴 (千葉大学) Standard ML用エラー回復機能を持つ変数名補完の実装 (ポスター・デモ) 諏訪覚, 篠埜功 (芝浦工業大学) 仮想的なタグを用いた共用体入りプログラムの事前条件推定 (ポスター) 今井健男(1,2), 酒井政裕(1), 遠藤侑介(1), 萩谷昌己(2) ((1)東芝, (2)東京大学) プログラミング言語Egison (ポスター・デモ) 江木聡志 (東京大学) Coqによる関係データベースの形式化とHaskellへのプログラム抽出の可能性 (デモ) 中村宇佑 (東京大学) 3次元量子エンタングルメントのグラフによる分類 (ポスター) 本多健太郎 (東京大学) コード推薦システムの既存プログラムを用いた最適化 (ポスター) 村上直也, 増原英彦 (東京大学) GPU向けプログラムをRubyで記述できる言語処理系Ikra (ポスター・デモ) 西口裕介, 増原英彦 (東京大学) Webアプリケーション開発のための分散JavaScriptとそのアプリケーション (デモ) 加藤真人 (東京工業大学) 同期可能なコピー＆ペーストによるコード再利用のためのモジュール化 (ポスター) 寺本裕基, 武山文信, 千葉滋 (東京工業大学) モジュール機構Simplified Method Sheltersの提案とその効率の良い実装方法 (ポスター) 竹下若菜, 千葉滋 (東京工業大学) 同期を考慮したメソッドの自動的配置が可能な言語とそのHPCへの応用 (ポスター) 宗桜子, 千葉滋 (東京工業大学) ブロック単位のコードの再利用を可能とするメソッド内メソッド (ポスター) 平松俊樹 (東京工業大学) HPC向け実行時言語変換器WootinJの実装と可能性 (ポスター) 穂積俊平, 伊尾木将之, 千葉滋 (東京工業大学) ユーザ定義N項演算子により内部DSLを実現する言語ProteaJ (ポスター) 市川和央, 千葉滋 (東京工業大学) 家族継承の機能指向プログラミングへの導入 (ポスター) 武山文信, 千葉滋 (東京工業大学) Integrating events with methods by a single language construct (ポスター) YungYu Zhuan, Shigeru Chiba (Tokyo Institute of Technology) 述語論理計算を実現するデータフロー・ネットワーク (ポスター) 鈴木秀明(1), 吉田幹(2), 澤井秀文(1) ((1)（独）情報通信研究機構, (2)株式会社ビービーアール) KonohaScriptからJavaScriptへのソースコード変換機の設計 (ポスター) 志田駿介, 井出真広, 倉光君郎 (横浜国立大学) KonohaScriptを用いたJavaアプリケーションの実行時動作変更 (ポスター) 若松悠樹, 井出真広, 倉光君郎 (横浜国立大学) JSON形式を用いた大規模ライブラリのFFI作成フレームワークの提案 (ポスター) 小野田武朗, 五嶋壮晃, 倉光君郎 (横浜国立大学) D-Script フレームワーク：分散システムを統一的に管理，運用するためのフレームワーク (ポスター・デモ) 中田晋平(1), 菅谷みどり(1,2), 倉光君郎(1,2) ((1)横浜国立大学, (2)JST/CREST) Coqによる集合論と数学の実装 (ポスター・デモ) 佐藤雅大 (名古屋大学) エフェクトシステムの述語意味論 (ポスター) 勝股審也 (京都大学) Type-Based Safe Resource Deallocation for Shared-Memory Concurrency (ポスター) Ryota Fukuda, Kohei Suenaga, Atsushi Igarashi (Kyoto University) −−−−−−−−−− 3月10日(土) −−−−−−−−−− 9:00--10:00 セッション11 (C1) 永続性にもとづく項書き換えシステムの合流性証明鈴木翼, 青戸等人, 外山芳人 (東北大学電気通信研究所) (C1) 片側減少ダイアグラム法による項書き換えシステムの可換性証明法的場正樹, 青戸等人, 外山芳人 (東北大学電気通信研究所) 10:20--11:20 セッション12 (C2) Functional Programs as Compressed Data 出典: ACM SIGPLAN 2012 Workshop on Partial Evaluation and Program Manipulation (PEPM 2012), pp.121--130, 2012. Naoki Kobayashi, Kazutaka Matsuda, Ayumi Shinohara (Tohoku University) (C2) Polynomial-Time Inverse Computation for Accumulative Functions with Multiple Data Traversals 出典: ACM SIGPLAN 2012 Workshop on Partial Evaluation and Program Manipulation (PEPM 2012), pp.5--14, 2012. Kazutaka Matsuda(1), Kazuhiro Inaba(2), Keisuke Nakano(3) ((1)Tohoku University, (2)National Institute of Infomatics, (3)The University of Electro-Communications (The second author has moved to Google)) 11:20--12:00 クロージング

1 0

「論理・数学的論証と認知のダイナミクス」国際研究会（２月２５日慶応大三田キャンパス）のご案内
by Mitsu Okada 19 Feb '12

19 Feb '12

------------------------------------------------------------------------- 「論理・数学的論証と認知のダイナミクス」研究集会のご案内（２月２５日土曜日） ("Logical-Mathematical Proofs and Cognition" Meeting, 25th feb 2012) 慶應義塾大学三田キャンパス　Mita Campus, Keio University ************************************************************************** ２月２３日２４日の学際オントロジー国際集会の後の２月２５日に次のような会合を予定しています。参加自由です.　（topics: 論証のSurveyability, 幾何学的認知プロセスのｆMRI脳研究、図形推論の証明論、プラトン・テアイテトスとlogic of relativism） Up-dated information は次のURLに掲示いたします。 http://abelard.flet.keio.ac.jp/dolc12/ （重複して受け取られた方にお詫び申し上げます。慶応大哲学岡田光弘） PLACE ROOM 323 (2nd Floor) of the Graduate School Building, Mita Campus of Keio University (5 minutes walk from JR-Tamachi Station or Subway-Mita Station or Subway-Akabanebashi Station) 場所慶應義塾大学三田キャンパス　「大学院棟」２階３２３番教室 JR田町駅、地下鉄三田駅、地下鉄赤羽橋駅から徒歩約５分キャンパスマップ（Campus Map） http://www.keio.ac.jp/en/maps/mita.html ２３−２４日オントロジー会議と２５日論理学研究会の会場建物が異なりますのでご注意ください。 (Associated to the Interdisciplinary Ontology Meeting (23rd-34th Feb), an international Logic Meeting on demontrations/proofs (logical and mathematical) and cognition is scheduled, including the topics of surveyability of proofs, fMRI-brain study on geometrical processing、the logic of relativism and Theaetetus, diagrammatic proofs). また、２月２３日２４日に（分析形而上学、医学生命情報学、AI,　情報科学を含む）学際オントロジー会議を予定しています。（学際オントロジー会議のURL：、For the 23rd-24th Interdisciplinary Ontology, see http://abelard.flet.keio.ac.jp/ontology/index.php?InterOntology12）２０１２年２月２５日土曜日午前１０時から午後５時まで慶應義塾大学第３校舎（大学院棟）３階３２３番教室慶應義塾大学論理学とフォーマルオントロジーオープンリサーチセンター論理学部門主催 *****論理:数学的論証と認知のダイナミズム******* 数学の哲学、分析哲学、実験哲学、現象学、認知心理学、分析形而上学系、数学基礎論系を含むDiscussants,Main participantsをゲストにお招きしてインフォーマルな形で提題講演及びディスカッションを行います。提題者、参加者は次の方たちを含みます。 Berit Brogaard (Departments of Philosophy and Psychology, Center for Neurodynamics, University of Missouri, USA, Phenomenplogy, Cogmitive Science,) Mathieu Marion (Department of Philosophy, Universite de Quebec a Montreal, Logical Philosophy) Maureen Donnelly (Department of Philosophy, The University at Buffalo, Analytic metaphysics, Logic) Mark Ressler (Department of Philosophy, The University at Buffalo, Analytic metaphysics, Logic, others) Sam Sanders (currently visiting Department of Mathematics, Tohoku university, Foundations of mathematics, Non-standard analysis, etc) Hiroyuki Miyoshi (Department of Computer science, Kyoto Sangyo University, Informatics, Logic) and others Discussion-Coordinator　岡田光弘　（Mitsu Okada) 10:00AM 　Mathieu Marion （department of Philosophy, Universite de Quebec a Montreal, Canada) による提題、Surverability of mathematical proofs in Wittgenstein,） 12;30 PM-14:00PM Meeting Lunch 14:00PM Mark Ressler (Department of Philosophy, University of buffalo, USA) 　Logic of relativism １5:30PM Berit Brogaard (Berit Brogaard (Departments of Philosophy and Psychology, Center for Neurodynamics, University of Missouri, USA) Seeing mathematics: perceptual experience and brain activity in acquired synesthesia --------------------------------------------------------------------- ２月２５日のこの研究会の Up-dated information は次のURLに掲示しています。 http://abelard.flet.keio.ac.jp/dolc12/ 主催：　Open Research Centre for Logic and Formal Ontology, Keio University 責任者　岡田光弘 ------------------------------------------------------------------------- また２３日２４日のオントロジー学際会議のupdated情報はhttp://abelard.flet.keio.ac.jp/ontology/index.php?InterOntology12にあります。 ---------------------------------------------------------------------

1 0

Call for Papers: ICE 2012, Interaction and Concurrency Experiences
by Ichiro Hasuo 19 Feb '12

19 Feb '12

みなさま，東京大学の蓮尾です．ワークショップ ICE 2012 のご案内です．若手が集まってやっている印象です．また，査読の過程で「Wiki による，PC，査読者，筆者による議論」があります．どうか投稿・参加をご検討ください．それでは！蓮尾一郎 http://www-mmm.is.s.u-tokyo.ac.jp/~ichiro/ ------------------------------------------------------------------------------------- [- Apologies for multiple copies -] ICE 2012 5th Interaction and Concurrency Experience June 16, 2012, Stockholm, Sweden http://www.artist-embedded.org/artist/-ICE-2012-.html Satellite workshop of DisCoTec 2012 http://discotec.ict.kth.se/ === Highlights === - Invited talks: Marcello Bonsangue Ichiro Hasuo - Innovative selection procedure - Special issue of Scientific Annals of Computer Science (http://www.info.uaic.ro/bin/Annals/) === Important Dates === 30 March 2012................Abstract submission 04 April 2012................Full paper submission 18 April - 12 May 2012.......Reviews, rebuttal and PC discussion 16 May 2012..................Notification to authors 30 May 2012..................Camera-ready for pre-proceedings 16 June 2012.................ICE in Stockholm 15 Sept 2012.................Camera-ready for post-proceedings === Scope === Interaction and Concurrency Experiences (ICEs) is a series of international scientific meetings oriented to theoretical computer science researchers with special interest in models, verification, tools and programming primitives for complex interactions. The general scope of the venue includes theoretical and applied aspects of interactions and the synchronization mechanisms used among components of concurrent/distributed systems, but every experience focuses on a different specific topic (see "Previous Editions" at the end of this call) related to several areas of computer science in the broad spectrum ranging from formal specification and analysis to studies inspired by emerging computational models. The theme of ICE 2012 is ***Distributed coordination, execution models, and resilient interaction***. Topics of interest include, but are not limited to: - Process algebra and coordination: transformation, analysis and implementation - Models for distributed coordination and semantics - Techniques and tools for specification, analysis, verification of resilient interaction - Languages, protocols and mechanisms for sound distributed coordination - Logics and types for interactions - Comparison among different coordination and/or execution models - Expressive power of coordination languages and execution models - Formal semantics of coordination languages - Formal verification of distributed coordinated architectures - Relating different semantic models for coordination languages === Selection Procedure === Since its 1st edition in 2008, the distinguishing feature of ICE has been an innovative paper selection mechanism based on an interactive discussion amongst authors and PC members. During the review phase, each submitted paper is published on a Wiki and associated with a discussion forum whose access will be restricted to the authors and all the PC members who do not have a conflict of interests with the paper. The PC members post comments/questions that the authors shall reply to. As witnessed by the past four editions of ICE, this procedure considerably improves the accuracy of the feedback from reviews, the fairness of the selection, the quality of camera-ready papers, and the discussion during the workshop. === The Public Wiki === After the notification, the accepted papers will be published on a public forum, in order to initiate public discussions that will trigger and stimulate the scientific debate at the workshop. We believe that this will drive the workshop discussions and let prospective participants interact with each other much earlier than in more traditional events. === Submission Guidelines === Papers must report previously unpublished work and not be simultaneously submitted to other conferences/workshops with refereed proceedings. The ICE 2012 post-proceedings will be published in Electronic Proceedings in Theoretical Computer Science (http://eptcs.org/). Submissions must be made electronically in PDF format via EasyChair (http://www.easychair.org/conferences/?conf=ice2012) and should not exceed 15 pages with the EPTCS style (http://style.eptcs.org/). Accepted papers must be presented at the workshop by one of the authors. === Special Issue === Full versions of the best papers selected by the PC will be invited to appear in a special issue of the journal of Scientific Annals of Computer Science (http://www.info.uaic.ro/bin/Annals/). Such contributions will be regularly peer-reviewed according to the standard journal policy, but they will be handled in a shorter time than regular submissions. === Program Committee === Lucia Acciai (University of Firenze, Italy) Luca Aceto (Reykjavik University, Iceland) Massimo Bartoletti (University of Cagliari, Italy) Simon Bliudze (EPFL, Switzerland) Laura Bocchi (University of Leicester, United Kingdom) Filippo Bonchi (CNRS, France) Roberto Bruni (University of Pisa, Italy) Marco Carbone (co-chair) Vincenzo Ciancia (University of Amsterdam, The Netherlands) Pierre-Malo Denielou (Imperial College, United Kingdom) Cinzia Di Giusto (CEA, France) Tobias Heindel (CEA, France) Tom Hirschowitz (CNRS, France) Bartek Klin (Warsaw University, Poland) Ivan Lanese (University of Bologna/INRIA, Italy) Alberto Lluch Lafuente (IMT Lucca, Italy) Bas Luttik (Technische Universiteit Eindhoven, The Netherlands) Manuel Mazzara (Newcastle University, United Kingdom) Mohammadreza Mousavi (Technische Universiteit Eindhoven, The Netherlands) Damien Pous (CNRS, France) Jens-Wolfhard Schicke-Uffmann (TU Braunschweig, Germany ) Alexandra Silva (co-chair) Ana Sokolova (University of Salzburg, Austria) Francesco Tiezzi (IMT Lucca, Italy) Emilio Tuosto (University of Leicester, United Kingdom) Erik de Vink (Technische Universiteit Eindhoven, The Netherlands) === ICEcreamers === - Marco Carbone (IT University of Copenhagen, Denmark; co-chair) - Ivan Lanese (University of Bologna/INRIA, Italy) - Alexandra Silva (Radboud University Nijmegen & CWI, The Netherlands; HasLab / INESC TEC, Portugal; co-chair) - Ana Sokolova (University of Salzburg, Austria) === Contact === ice2012(a)easychair.org === Previous editions === The previous four editions of ICE have been held on * July 6th, 2008 in Reykjavik, Iceland with focus on Synchronous and Asynchronous Interactions in Concurrent/ Distributed Systems, co-located with ICALP'08. The post-proceedings were published in ENTCS (vol.229-3). * August 31st, 2009 in Bologna, Italy with focus on Structured Interactions, co-located with CONCUR'09. The post-proceedings were published in EPTCS (vol.12) and a special issue of MSCS is in preparation. * June 10th, 2010 in Amsterdam, The Netherlands with focus on Guaranteed Interactions, co-located with DisCoTec'10. The post-proceedings were published in EPTCS (vol.38) and selected papers appeared in a joint special issue of SACS (with CAMPUS'10 and CS2BIO'10, Vol. XXI). * June 9th, 2011 in Reykjavik, Iceland with focus on Reliable and Contract-based Interactions, co-located with DisCoTec'11. The post-proceedings were published in EPTCS (vol.59) and a special issue of SACS is now in preparation.

1 0

佐藤雅彦先生最終講義の御案内
by Koji Nakazawa 16 Feb '12

16 Feb '12

logic-mlのみなさま，（重複の場合はご容赦ください）京都大学の中澤です．この3月をもって定年を迎えられる佐藤雅彦先生の最終講義が下記のとおり行なわれますので，この場をお借りしまして，お知らせいたします．最終講義および懇親会に関するお問合せ，登録のお申込は final-lec(a)sato.kuis.kyoto-u.ac.jp までお願いいたします． ---------------------------------------------------------------------- 各位小林茂夫教授・佐藤雅彦教授・後藤修教授最終講義および懇親会のご案内拝啓時下ますますご健勝のこととお喜び申し上げます。さてこの度、知能情報学専攻小林茂夫教授，佐藤雅彦教授，後藤修教授におかれましては、本年３月 31日をもって定年を迎えられ京都大学を退職されることとなりました。つきましては、三教授による最終講義および懇親会が行われますので、下記の通りご案内申し上げます。敬具記 1. 最終講義日時: 平成 24 年 3 月 16 日 (金) 午後 13:00 〜 18:00 会場: 京都大学百周年時計台記念館国際交流ホールI http://www.kyoto-u.ac.jp/ja/access/campus/map6r_y.htm (3番の建物) 13:00〜14:30 佐藤雅彦教授「情報学の内と外〜世界と言語の関係〜」 14:45〜16:15 後藤修教授「ＤＮＡ＝高分子＋情報」 16:30〜18:00 小林茂夫教授「物理世界と感覚世界」 2. 懇親会日時: 平成 24 年 3 月 16 日 (金) 午後 18:45 〜 20:45 (受付: 18:15 〜) 会場: 京都大学百周年時計台記念館国際交流ホールIII http://www.kyoto-u.ac.jp/ja/access/campus/map6r_y.htm (3番の建物) 会費: 一般 8,000円，学生 4,000円 [事前登録] final-lec(a)sato.kuis.kyoto-u.ac.jp までお名前: ご所属: 佐藤教授最終講義 (ご出席・ご欠席) 後藤教授最終講義 (ご出席・ご欠席) 小林教授最終講義 (ご出席・ご欠席) 懇親会 (ご出席・ご欠席) をお知らせください． (事前登録は必須ではありませんが、特に懇親会に関しまして参加者数を把握するため、事前登録にご協力をお願い致します。) 平成24年1月吉日京都大学大学院情報学研究科知能情報学専攻長黒橋禎夫小林教授・佐藤教授・後藤教授最終講義および懇親会準備会 final-lec(a)sato.kuis.kyoto-u.ac.jp

1 0

CFP: 8th Scandinavian Logic Symposium
by Thomas Bolander 16 Feb '12

16 Feb '12

8th SCANDINAVIAN LOGIC SYMPOSIUM 20-21 August 2012 at Roskilde University, DENMARK First Announcement and Call for Papers The 8th Scandinavian Logic Symposium will be held at Roskilde University, Trekroner, Denmark, 20-21 August 2012. After a gap of fifteen years, the Scandinavian Logic Symposium is back. The Symposium is the first major initiative of the newly revived Scandinavian Logic Society (SLS, http://scandinavianlogic.org/) and will be held at Roskilde University (RUC), Denmark. As with previous editions of this conference, the aim of the programme is to reflect current activity in logic in our part of the world. So we hope that participants from Scandinavia, the Baltic countries and Northwestern Russia will take the opportunity to contribute a talk and to meet with fellow logicians from the area. But needless to say, we also extend a warm welcome to logicians from further afield and plan to present a varied and interesting collection of invited and contributed talks. Related events: A post-SLS tutorial day will be organized on August 22 Also note that Advances in Modal Logic (AiML) will be held on 22-25 August 2012, Copenhagen, Denmark. URL: http://hylocore.ruc.dk/aiml2012/ . TOPICS The scope of SLS 2012 is broad, ranging over the whole area of mathematical and philosophical logic, and logical methods in computer science. Suitable topics include (but are not limited to) Proof Theory and Constructivism, Model Theory (including Finite Model Theory), Set Theory, Computability Theory, Categorical Logic, Logic and Provability, Logic and Computer Science, Logic and Linguistics, Modal, Hybrid, Temporal and Description Logic, Logics of Games, Dynamics and Interaction, and Philosophical Logic. PREVIOUS SCANDINAVIAN LOGIC SYMPOSIA: 7th Scandinavian Logic Symposium: Uppsala in 1996 6th Scandinavian Logic Symposium: Telemark in 1982 5th Scandinavian Logic Symposium: Aalborg in 1979 4th Scandinavian Logic Symposium: Jyväskylä in 1976 3rd Scandinavian Logic Symposium: Uppsala in 1973 2nd Scandinavian Logic Symposium: Oslo in 1971 1st Scandinavian Logic Symposium: Åbo in 1968 The proceedings of several of these meetings have been published in book form. INVITED SPEAKERS To be announced PROGRAM COMMITTEE Co-chairs: Neil Jones (Copenhagen) and Erik Palmgren (Stockholm) Members: Torben Brauner (Roskilde) Peter Dybjer (Chalmers) Lars Kristiansen (Oslo) Øystein Linnebo (Birkbeck) Sara Negri (Helsinki) Dag Normann (Oslo) Asger Törnquist (Vienna) Jouko Väänänen (Helsinki) ORGANISING COMMITTEE Patrick Blackburn (RUC), Klaus Frovin Jørgensen (RUC), Stig Andur Petersen (RUC) SUBMISSIONS Abstracts of talks should be submitted by May 1, 2012 using the EasyChair system https://www.easychair.org/conferences/?conf=sls2012 The abstracts may not exceed 3 pages (including bibliography) and should be in PDF format. LOCATION Roskilde University (RUC) is situated at Trekroner, a small town 20 minutes by train from Central Copenhagen, and five minutes by train from Roskilde. ACCOMMODATION Most people who work at RUC and almost all the RUC students live in Copenhagen. Getting to RUC is an easy train journey from the centre of Copenhagen. We anticipate that most conference attendees will book hotels in central Copenhagen, where there are many hotels in many price ranges. Hotel accommodation can also be found in Roskilde, though there the options are more limited. REGISTRATION The conference website will be found at: http://scandinavianlogic.weebly.com/ Details concerning registration will be posted there in due course.

1 0

ICFEM 2012: Call for Papers
by Yuki Chiba 16 Feb '12

16 Feb '12

(重複の場合はご容赦ください．) 皆様，北陸先端科学技術大学院大学の千葉です． 11月に京都で開催されるICFEM 2012の案内を送らせて頂きます． http://www.jaist.ac.jp/icfem2012 ICFEMは形式手法とその実用的応用に関する国際会議です．ぜひ投稿をご検討下さい．よろしくお願いします． ************************************************************ ICFEM 2012: 14th International Conference on Formal Engineering Methods CALL FOR PAPERs 12th-16th, November, 2012 Kyoto Research Park, Kyoto, Japan URL: http://www.jaist.ac.jp/icfem2012 ************************************************************ ICFEM will come back to Japan in 2012 again! Since 1997, ICFEM has been serving as an international forum for researchers and practitioners who have been seriously applying formal methods to practical applications. Researchers and practitioners, from industry, academia, and government, are encouraged to attend, and to help advance the state of the art. We are interested in work that has been incorporated into real production systems, and in theoretical work that promises to bring practical and tangible benefit. ICFEM 2012 will be hosted by National Institute of Advanced Industrial Science and Technology (AIST) and Japan Advanced Institute of Science and Technology (JAIST), which will be held in Kyoto, JAPAN. Kyoto is the ancient capital of JAPAN, where you can find many historical sites which have been designated as World Heritage there. We are looking forward to your submissions. AREA AND TOPICS Submissions related to the following principal themes are encouraged, but any topics relevant to the field of formal methods and their practical applications will also be considered: * Abstraction and refinement * Formal specification and modelling * Software verification * Program analysis * Software model checking * Formal approaches to software testing * Formal methods for object and component systems * Formal methods for cloud computing/robotics/cyber-physical systems/ medical devices/aeronautics/railway * Formal methods for self-* systems * Formal methods for software safety, security, reliability and dependability * Experiments involving verified systems * Formal methods used in certifying products under international standards (ISO 26262, IEC 61508, etc) * Formal model-based development and code generation SUBMISSION AND PUBLICATION Submissions to the conference 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, and relevance to the conference. The proceedings will be published in the Springer Lecture Notes in Computer Science series. Papers should be written in English and not exceed 16 pages in LNCS format (see http://www.springer.de/comp/lncs/authors.html for details). Submission should be done through the ICFEM 2012 submission page (https://www.easychair.org/conferences/?conf=icfem2012), handled by the EasyChair conference system. IMPORTANT DATES Abstract Submission Deadline: 9th April, 2012 Full Paper Submission Deadline: 16th April, 2012 Acceptance/Rejection Notification: 18th June, 2012 Camera Ready Copy Due: 16th July, 2012 Conference: 12th-16th, November, 2012. ORGANIZATION COMMITTEE Conference Chair: Hitoshi Ohsaki (AIST, Japan) Program Chairs: Kenji Taguchi (AIST, Japan) Toshiaki Aoki (JAIST, Japan) General Chairs: Kokichi Futatsugi (JAIST, Japan) Shaoying Liu (Hosei Uni., Japan) Steering Committee Keijiro Araki, Japan Jin Song Dong, Singapore Jifeng He, China Shaoying Liu (Chair), Japan Program Committee (TBD) ----------------------------------- Yuki Chiba Japan Advanced Institute of Science and Technology (JAIST) http://www.jaist.ac.jp/~chiba/index.html chiba(a)jaist.ac.jp

1 0

Jump to page:

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Logic-ml