Logic-ml

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

1792 discussions

数学基礎論サマースクール2015
by Makoto Kikuchi 18 Jul '15

18 Jul '15

皆様，先日ご案内いたしました数学基礎論サマースクール（8/18〜8/21）において，初日の午前中に，数理論理学の予備知識を全く持たない人を対象とする，数理論理学のチュートリアルを実施します．詳細はホームページ（http://www2.kobe-u.ac.jp/~mkikuchi/ss2015.html）でご確認ください．数学基礎論サマースクール世話人菊池誠 -- 数学基礎論サマースクール2015のご案内参加申込〆切：2015年7月31日（金）以下の要領で数学基礎論サマースクール2015を開催します．ご参加希望の方は下記の要領でお申込下さい．皆様のご参加を心よりお待ちしています．【注意】学部学生，数学基礎論を専門としない大学院生や研究者の参加を歓迎します．　初日の午前中に数理論理学の予備知識を全く持たない人を対象とする，　数理論理学のチュートリアルを実施します．（要申込）【概要】様相論理入門と，証明や真理に関する様相論理の話題についての講義．　また，様相論理と他分野との関係や発展的内容についての特論．【日時】2015年8月18日（火）15:10 ～ 21日（金）15:00 【場所】神戸大学六甲台第2キャンパス内工学部教室棟LR501教室（戎記念ホール）【住所】〒657-8501神戸市灘区六甲台町1-1 【ホームページ】http://www2.kobe-u.ac.jp/~mkikuchi/ss2015.html 【講師】薄葉季路（神戸大），金子守（早稲田大），倉橋太志（木更津高専），　黒川英徳（神戸大），佐藤雅彦（京大名誉教授），佐野勝彦（JAIST），渕野昌（神戸大）【参加費】無料【参加申込】以下の内容を e-mail で件名「ss2015」として，mkikuchi(a)kobe-u.ac.jp 宛にお送りください．・氏名（ふりがな）：・所属：・懇親会出欠：出席／欠席申込〆切：2015年7月31日（金）【内容】〈講義〉（各3コマ） 1. 様相論理入門（佐野）　様相論理の構文論と意味論，正規様相論理，最近の発展と歴史的背景 2. 証明可能性論理（倉橋）　算術と不完全性定理，ゲーデル・レーブ論理と算術的完全性定理，証明可能性論理の拡張 3. 強制法と様相論理（薄葉）　公理的集合論と強制法，ジェネリック拡大と強制関係，強制様相論理 4. 真理と様相（黒川）　タルスキの真理論と知者のパラドックス，クリプキの真理論，真理の改定理論〈特論〉（各1コマ） 1. 認識論理のゲーム論的意思決定への応用（金子） 2. 計算機科学と様相論理（佐藤） 3. 公理的集合論と様相論理（渕野）〈その他〉 1. チュートリアル　時間：10:00-12:30，講師：依岡輝幸（静岡大），場所：LR501教室　内容：数理論理学の予備知識を全く持たない人を対象とする少人数の講義．　受講ご希望の方は参加申込と同時に，または別便で件名「ss2015」として本文中に　「チュートリアル受講希望」と書いて mkikuchi(a)kobe-u.ac.jp までご連絡下さい． 2. 導入　時間：14:00-15:00，担当：菊池誠（神戸大・世話人），場所：LR501教室　内容：今回のサマースクールの背景および企画意図の説明．【懇親会】19日夜に神戸大学内で懇親会を開催します．　日時：2015年8月19日（水）午後7時から　会場：和風レストランさくら http://www.kucoop.jp/info/shop-belbox.html 　場所：神戸大学六甲台第1キャンパス内 BEL BOX 3階　会費：3,500円（予定）【アドバイザ】新井敏康（千葉大），鈴木信行（静岡大），松原洋（名古屋大）【世話人】神戸大学大学院システム情報学研究科菊池誠，酒井拓史【連絡先】菊池誠 mkikuchi(a)kobe-u.ac.jp

1 0

CFP: LENLS12 (Logic and Engineering of Natural Language Semantics 12)
by Koji Mineshima 17 Jul '15

17 Jul '15

（重複して受け取られた場合はご容赦ください）今年の１１月に東京で開催される LENLS 12 国際ワークショップのご案内をお送り致します。皆様のご投稿・ご参加をお待ちしております。峯島宏次（お茶の水女子大学） [Apologies for multiple copies] ================================================================= SECOND CALL FOR PAPERS Logic and Engineering of Natural Language Semantics 12 (LENLS 12) Workshop Site : (15th) Ochanomizu University Room 207-209, Science Building 3, Tokyo, Japan (The bldg. #20 in the "campus map" in the following webpage) http://www.ocha.ac.jp/en/access/index.html (16th,17th) Raiousha Building, Keio University Kanagawa, Japan http://www.keio.ac.jp/en/maps/hiyoshi.html Dates : November 15-17, 2015 Contact Person: Eric McCready (Aoyama Gakuin University) Contact Email : lenls12[[at]]easychair.org Website : http://www.is.ocha.ac.jp/~bekki/lenls/ ================================================================= Chair: Eric McCready (Aoyama Gakuin University) Co-chair: Daisuke Bekki (Ochanomizu University/National Institute of Informatics/JST CREST) Koji Mineshima (Ochanomizu University/JST CREST) Invited Speakers: - Nicholas Asher (CNRS, Institut de Recherche en Informatique de Toulouse/Universit'e Paul Sabatier) - Stefan Kaufmann (University of Connecticut) - Magdalena Kaufmann (University of Connecticut) - Robert Henderson (University of Arizona) - Tomohiro Sakai (Waseda University) LENLS is an annual international workshop on formal syntax, semantics and pragmatics. It will be held as one of the workshops of the 7th JSAI International Symposia on AI (isAI2015) (https://www.ai-gakkai.or.jp/isai/) sponsored by the Japan Society for Artificial Intelligence (JSAI) (http://www.ai-gakkai.or.jp/en). The first day of LENLS will include a half-day workshop on politeness and honorification with talks by Nicholas Asher, Daisuke Bekki and Eric McCready. These talks will consider the lexical semantics of honorifics, syntactic and semantic aspects of composition with honorifics, and strategic aspects of politeness and formality. The workshop is open to the public and is funded by JSPS Kiban C Grant #25370441. Aims and Topics: ================ We invite submissions to this year's workshop on topics in formal syntax, semantics and pragmatics, and related fields, including but in no way limited to the following: - Formal syntax, semantics and pragmatics of natural language - Model-theoretic and/or proof-theoretic semantics of natural language - Computational Semantics - Continuations in natural language - Game-theoretic/Bayesian approaches to pragmatics - Nonclassical Logic and its relation to natural language (especially Substructural/Fuzzy/Categorical/Topological logics) - (Formal) Philosophy of language - Scientific methodology and/or experimental design for linguistics Submissions: ============ Abstracts (anonymous, up to 4 pages, including figures and references, A4 size, with 12 point font) must be submitted electronically in PDF format at: https://www.easychair.org/conferences/?conf=lenls12 When the abstract is accepted, the author is expected to submit a full paper (10-14 pages) before the workshop. The proceedings of the workshop will be available at the conference site for registered persons. Important dates: ================ Abstract submission deadline: August 23, 2015 Notification of acceptance: September 30, 2015 Deadline for camera-ready copy: October, 2015 Half-day workshop on politeness: November 15, 2015 LENLS12: November 15-17, 2015 Sponsor: ======== LENLS is being organized by an alliance of "Establishment of Knowledge-Intensive Structural Natural Language Processing and Construction of Knowledge Infrastructure" (http://nlp.ist.i.kyoto-u.ac.jp/CREST/?en) project, funded by JST CREST Programs "Advanced Core Technologies for Big Data Integration" (http://www.jst.go.jp/kisoken/crest/en/research_area/ongoing/areah25-6.html). Workshop Organizers/Program Committee: ====================================== - Eric McCready (Aoyama Gakuin University) - Daisuke Bekki (Ochanomizu University/National Institute of Informatics/JST CREST) - Koji Mineshima (Ochanomizu University/JST CREST) - Alastair Butler (Tohoku University) - Richard Dietz (University of Tokyo) - Yoshiki Mori (University of Tokyo) - Yasuo Nakayama (Osaka University) - Katsuhiko Sano (Japan Advanced Institute of Science and Technology) - Katsuhiko Yabushita (Naruto University of Education) - Tomoyuki Yamada (Hokkaido University) - Shunsuke Yatabe (West Japan Railway Company) - Kei Yoshimoto (Tohoku University)

1 0

セミナー案内
by KASHIMA Ryo 13 Jul '15

13 Jul '15

数理論理学セミナーのお知らせ日時：7月17日(金)15:10から場所：東京工業大学大岡山西８号館Ｗ棟10階 W1008 【１】話者：横溝恭平（日本大学）題目：中間命題論理の断片に関する保存性の問題について概要： Sを→(ならば)を元にもつ命題論理記号の集合とする。ヒルベルト流の直観主義論理Hに対しその断片論理H_Sは、Hの公理型とその代入をS論理式(論理記号がSの元のみ出現する論理式) に制限した論理H_Sであることが知られている。本発表では、このHに関する性質が中間論理でも成り立つかについて、つまり S論理式の集合Σに対し、中間論理H + ΣがH_S + Σの保存拡大になる条件について、代数的な視点で考察する。参考文献： [1] A. Horn, The separation theorem of intuitionist propositional calculus, J. Symbolic Logic, vol.27, pp391-399 (1962) [2] C. G. McKay, The decidability of certain intermediate propositional logics, J. Symbolic Logic, vol.33, pp.258-264 (1968) [3] V. A. Jankov, Conjunctively indecomposable formulas in propositional calculi, USSR-Izvestiya, vol.3, num.1, pp.17-35 (1969) 【２】話者：梅北拓朗題目：集合論における強制法と様相論理概要：集合論において、強制法とはZFCのモデルを拡大してある命題（例えば連続体仮説）が成立するようなモデルを構成する手法であるが、 Hamkinsは「あるZFCのモデルが別のモデルの強制法による拡大になっている」という関係をKripkeフレームにおける到達可能関係とみなす「様相論理の強制法的解釈」において、様相論理の公理のいくつかが自然にZFCで成立し、また(5)という名前で知られる論理式（◇□φ→□φ）は、それをZFCに加えても無矛盾であることを見出した。これらの結果について紹介する。予備知識は特に仮定しない。 ----- 本セミナーは定期的に東工大で開催しているものです。初めて参加を希望される方はご一報ください。 ----- 鹿島亮東京工業大学大学院情報理工学研究科数理・計算科学専攻 kashima(a)is.titech.ac.jp

1 0

Fwd: Kobe Colloquium on Logic, Statistics and Informatics, July 14 (Olivier Finkel)
by Joerg Brendle 08 Jul '15

08 Jul '15

Kobe Colloquium on Logic, Statistics and Informatics 以下の要領でコロキウムを開催します。日時：2015年7月14日（火）13:30-15:00 講演者：Olivier Finkel （パリ第７大学）場所：神戸大学自然科学総合研究棟3号館4階421室（プレゼンテーション室） ============================================================ 題目： Logic, Complexity and Infinite Computations アブストラクト： The theory of automata reading infinite words, which is closely related to infinite games, is a rich theory which is used for the specification and verification of non-terminating systems. We prove that the Wadge hierarchy of omega-languages accepted by 1-counter Büchi automata (or by 2-tape Büchi automata) is equal to the Wadge hierarchy of omega-languages accepted by Büchi Turing machines, which forms the class of effective analytic sets. Moreover the topological complexity of an omega-language accepted by a 1-counter Büchi automaton, or of an infinitary rational relation accepted by a 2-tape Büchi automaton, is not determined by the axiomatic system ZFC. In particular, there is a 1-counter Büchi automaton A (respectively, a 2-tape Büchi automaton B) and two models V1 and V2 of ZFC such that the omega-language L(A) (respectively, the infinitary rational relation L(B)) is Borel in V1 but not in V2. We prove that the determinacy of Gale-Stewart games whose winning sets are accepted by real-time 1-counter Büchi automata (or by 2-tape Büchi automata) is equivalent to the determinacy of (effective) analytic Gale-Stewart games which is known to be a large cardinal assumption. Using some results of set theory we prove that one can effectively construct a 1-counter Büchi automaton (respectively, a 2-tape Büchi automaton) A such that: (1) There exists a model of ZFC in which Player 1 has a winning strategy in the Gale-Stewart game G(L(A)); but the winning strategies cannot be recursive and not even hyperarithmetical. (2) There exists a model of ZFC in which the Gale-Stewart game is not determined. We also prove that the determinacy of Wadge games between two players in charge of omega-languages accepted by real-time 1-counter Büchi automata (or by 2-tape Büchi automata) is equivalent to the effective analytic determinacy, and thus is not provable in ZFC. ======================================================== 交通：阪急六甲駅またはJR六甲道駅から神戸市バス36系統「鶴甲団地」行きに乗車，「神大本部工学部前」停留所下車，徒歩すぐ． http://www.kobe-u.ac.jp/info/access/rokko/rokkodai-dai2.htm

1 0

数学基礎論サマースクール2015
by Makoto Kikuchi 04 Jul '15

04 Jul '15

数学基礎論サマースクール2015のご案内参加申込〆切：2015年7月31日（金）以下の要領で数学基礎論サマースクール2015を開催します．ご参加希望の方は下記の要領でお申込下さい．皆様のご参加を心よりお待ちしています．【概要】様相論理入門と，証明や真理に関する様相論理の話題についての講義．　また，様相論理と他分野との関係や発展的内容についての特論．【日時】2015年8月18日（火）13:30 ～ 21日（金）15:00 【場所】神戸大学六甲台第2キャンパス内工学部教室棟LR501教室（戎記念ホール）【住所】〒657-8501神戸市灘区六甲台町1-1 【ホームページ】http://www2.kobe-u.ac.jp/~mkikuchi/ss2015.html 【講師】薄葉季路（神戸大），金子守（早稲田大），倉橋太志（木更津高専），　黒川英徳（神戸大），佐藤雅彦（京大名誉教授），佐野勝彦（JAIST），渕野昌（神戸大）【参加費】無料【参加申込】以下の内容を e-mail で件名「ss2015」として，mkikuchi(a)kobe-u.ac.jp 宛にお送りください．・氏名（ふりがな）：・所属：・懇親会出欠：出席／欠席申込〆切：2015年7月31日（金）【内容】〈講義〉（各3コマ） 1. 様相論理入門（佐野） 2. 証明可能性論理（倉橋） 3. 強制法と様相論理（薄葉） 4. 真理と様相（黒川）〈特論〉（各1コマ） 1. 認識論理のゲーム論的意思決定への応用（金子） 2. 計算機科学と様相論理（佐藤） 3. 公理的集合論と様相論理（渕野）【懇親会】19日夜に神戸大学内で懇親会を開催します．　日時：2015年8月19日（水）午後7時から　会場：和風レストランさくら http://www.kucoop.jp/info/shop-belbox.html 　場所：神戸大学六甲台第1キャンパス内 BEL BOX 3階　会費：3,500円（予定）【世話人】神戸大学大学院システム情報学研究科菊池誠，酒井拓史【連絡先】菊池誠 mkikuchi(a)kobe-u.ac.jp

1 0

1st CFP: 4th International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS2015)
by Takashi Kitamura 03 Jul '15

03 Jul '15

皆様、産総研の北村崇師と申します。 11月にパリで開催される国際ワークショップ FTSCS2015 の案内（論文募集）をお送りいたします。よろしくお願いいたします。 --------------------------------------------------------------------- Call for Papers FTSCS 2015 4th International Workshop on Formal Techniques for Safety-Critical Systems Paris, November 6, 2015 (satellite workshop of ICFEM 2015) http://www.ftscs.org --------------------------------------------------------------------- *** Science of Computer Programming special issue *** *** Springer CCIS proceedings *** Aims and Scope: There is an increasing demand for using formal methods to validate and verify safety-critical systems in fields such as power generation and distribution, avionics, automotive systems, and medical systems. In particular, newer standards, such as DO-178C (avionics), ISO 26262 (automotive systems), IEC 62304 (medical devices), and CENELEC EN 50128 (railway systems), emphasize the need for formal methods and model-based development, thereby speeding up the adaptation of such methods in industry. The aim of this workshop is to bring together researchers and engineers who are interested in the application of formal and semi-formal methods to improve the quality of safety-critical computer systems. FTSCS strives to promote research and development of formal methods and tools for industrial applications, and is particularly interested in industrial applications of formal methods. Specific topics include, but are not limited to: * case studies and experience reports on the use of formal methods for analyzing safety-critical systems, including avionics, automotive, medical, railway, and other kinds of safety-critical and QoS-critical systems * methods, techniques and tools to support automated analysis, certification, debugging, etc., of complex safety/QoS-critical systems * analysis methods that address the limitations of formal methods in industry (usability, scalability, etc.) * formal analysis support for modeling languages used in industry, such as AADL, Ptolemy, SysML, SCADE, Modelica, etc. * code generation from validated models. The workshop will provide a platform for discussions and the exchange of innovative ideas, so submissions on work in progress are encouraged. Submission: We solicit submissions reporting on: A- original research contributions (15 pages max, LNCS format); B- applications and experiences (15 pages max, LNCS format); C- surveys, comparisons, and state-of-the-art reports (15 pages max, LNCS); D- tool papers (5 pages max, LNCS format); E- position papers and work in progress (5 pages max, LNCS format) related to the topics mentioned above. All submissions must be original, unpublished, and not submitted concurrently for publication elsewhere. Paper submission is done via EasyChair at https://easychair.org/conferences/?conf=ftscs2015. The final version of the paper must be prepared in LaTeX, adhering to the LNCS format available at http://www.springer.com/computer/lncs?SGWID=0-164-6-793341-0. Publication: All accepted papers will appear in the pre-proceedings of FTSCS 2015. Accepted papers in the categories A-D above will appear in the workshop proceedings that will be published as a volume in Springer's CCIS series. The authors of a selected subset of accepted papers will be invited to submit extended versions of their papers to appear in a special issue of the Science of Computer Programming journal. Important dates: Submission deadline: September 5, 2015 Notification of acceptance: October 5, 2015 Workshop: November 6/7, 2015 Venue: Paris, France (city center!) Program chairs: Cyrille Artho AIST, Japan Peter Olveczky University of Oslo, Norway Program committee: Musab AlTurki King Fahd U. of Petroleum and Minerals, Saudi Arabia Etienne Andre University Paris 13, France Toshiaki Aoki JAIST, Japan Cyrille Artho AIST, Japan Kyungmin Bae Carnegie Mellon University, USA David Broman KTH, Sweden and UC Berkeley, USA Bernd Fischer Stellenbosch University, South Africa Osman Hasan National U. of Sciences & Technology, Pakistan Klaus Havelund NASA JPL, USA Fuyuki Ishikawa National Institute of Informatics, Japan Takashi Kitamura AIST, Japan Alexander Knapp Augsburg University, Germany Brian Larson Kansas State University, USA Wenchao Li SRI International, USA Robi Malik University of Waikato, New Zealand Frederic Mallet INRIA Sophia Antipolis, France Roberto Nardone University of Napoli "Federico II", Italy Thomas Noll RWTH Aachen University, Germany Peter Olveczky University of Oslo, Norway Charles Pecheur Universite catholique de Louvain, Belgium Paul Pettersson Malardalen University, Sweden Camilo Rocha Escuela Colombiana de Ingenieria, Colombia Markus Roggenbach Swansea University, UK Ralf Sasse ETH Zurich, Switzerland Oleg Sokolsky University of Pennsylvania, USA Sofiene Tahar Concordia University, Canada Jean-Pierre Talpin INRIA Rennes, France Jackie Wang McMaster University, Canada Alan Wassyng McMaster University, Canada Michael Whalen University of Minnesota, USA Huibiao Zhu East China Normal University, China Contact: (web) http://www.ftscs.org (email) peterol(a)ifi.uio.no and c.artho(a)aist.go.jp -- Takashi KITAMURA t.kitamura(a)aist.go.jp http://staff.aist.go.jp/t.kitamura/ Nat. Inst. of Advanced Industrial Science and Technology (AIST) Nakoji 3-11-46, Amagasaki, Hyogo 661-0974, Japan Tel: +81-6-6494-8054 Internal Tel: *33-274-71902 Fax: +81-6-6494-8073

1 0

NLCS'15 Program
by Makoto Kanazawa 30 Jun '15

30 Jun '15

*********************** Call for Participation *********************** Third Workshop on Natural Language and Computer Science NLCS '15 July 5, 2015 Kyoto, Japan http://www.indiana.edu/~iulg/nlcs.html Program with abstracts: http://easychair.org/smart-program/NLCS'15/index.html Venue: Kyoto University, Clock Tower Centennial Hall, 2nd Floor, Conference Room 3 http://www.kurims.kyoto-u.ac.jp/icalp-lics2015/workshops.html Schedule: 10:30-11:00 Coffee Break 11:00-12:30 Session 1 11:00 Makoto Kanazawa, Distributional Learning of Formal Languages: A Logic-Based Approach (invited talk) 12:00 Philippe de Groote, On Logical Relations and Conservativity 12:30-14:00 Lunch Break 14:00-15:30 Session 2 14:00 Bruno Mery, Lexical Semantics with Linear Types 14:30 Gabriel Gaudreault, Bidirectional Functional Semantics for Pregroup Grammars 15:00 Glyn Morrill and Oriol Valentín, Computational Coverage of TLG: Nonlinearity 15:30-16:00 Coffee Break 16:00-17:00 Session 3 16:00 Gerard de Melo, Learning to Reason about the World using Big Data (invited talk) 17:00-17:15 Short Break without Coffee 17:15-18:15 Session 4 17:15 Oleg Kiselyov, Applicative Abstract Categorial Grammar 17:45 Sylvain Salvati, Non-linear Second Order Abstract Categorial Grammars and Deletion ------------------------------------- Contact: Makoto Kanazawa

1 0

モデル理論夏の学校（講演申込み締切）
by ikeda＠hosei.ac.jp 27 Jun '15

27 Jun '15

皆様，以前，メールいたしました「モデル理論夏の学校」に関して，講演（および参加）申込み締切を７月１１日に延長しました．講演予定でまだ申込みをされていない方は申込みの手続き，よろしくお願いいたします．池田宏一郎（法政大学） ------------------------------------------------------------------ 皆様，法政大学の池田と申します．今年８月に法政大学で研究集会「モデル理論夏の学校2015」が開催されます．この研究集会は毎年夏に開催されるモデル理論および関連分野に関する研究集会です．モデル理論に興味のある方の参加をお待ちしております．・日程：２０１５年８月２２日（土）- ２４日（月）・会場：法政大学市ヶ谷キャンパス５５年館５５１教室・所在地：〒102-8160東京都千代田区富士見2-17-1 ・世話人：池田宏一郎（法政大学経営学部，ikeda(at)hosei.ac.jp）・Web page：https://sites.google.com/site/modeltheorysummer2015/ 参加を希望される方は，下記のフォームに必要事項を記入の上，池田宛に電子メールでお申し込みください．なお，旅費補助は講演者を優先に考えております． %%%%%%%%%%モデル理論夏の学校・参加申し込みフォーム%%%%%%%%%% ・氏名：・所属機関：・職名／学年：・講演：する／しない・講演題目：・旅費補助の希望：する／しない %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 池田宏一郎（法政大学）

2 1

千葉 logic seminar (2015年7月8日)
by Naohi Eguchi 24 Jun '15

24 Jun '15

千葉 logic seminar の第6回のお知らせです。どなたでも参加できますのでどうぞ気軽にいらっしゃって下さい。問合せ先江口（千葉大学） Naohi Eguchi <neguchi(a)g.math.s.chiba-u.ac.jp> --------------------------------------- 千葉 Logic Seminar https://sites.google.com/site/chibalogicseminar/home/seminar 日時：2015年7月8日(水)15:00-16:00 場所：千葉大学理学部2号館105号室アクセスは http://www.chiba-u.ac.jp/campus_map/nishichiba/index.html の地図の黄色い理学部の中で数字2が付いている建物の1階です。 Speaker: Martin Avanzini (University of Innsbruck) Title: Analysing the Complexity of Functional Programs: Higher-Order Meets First-Order Abstract: In this talk I will outline the content of our recent ICFP paper. Here, we shows how the runtime complexity of higher-order functional programs can be analysed automatically by applying program transformations to a defunctionalized versions of them, and feeding the result to existing tools for the complexity analysis of first-order term rewrite systems. Crucial, all involved transformations are complexity reflecting. As a consequence, a complexity certificate on the first-order system can be relayed back (asymptotically) to the initial higher-order program. Reference: Analysing the Complexity of Functional Programs: Higher-Order Meets First-Order Martin Avanzini, Ugo Dal Lago and Georg Moser Proc. ICFP 2015, to appear. Long version: http://arxiv.org/abs/1506.05043

1 0

Klaus Keime 教授講演会
by Hideki Tsuiki 23 Jun '15

23 Jun '15

京都大学人間・環境学研究科の立木です。 7 月 3 日 (LICS サテライト Workshop の前日) に、Darmstadt 工科大学の Klaus Keimel 先生による講演会を京都大学で行います。どうぞ、お気軽にお越しください。講演会の後に、一緒にお食事に行こうと考えています。人数を把握しておきたいので、お食事に来られる方は、あらかじめメールでご連絡頂けると幸いです。多くの方のご参加をお待ちしております。立木 ------------------------------------------------------------ 講演会のお知らせ日時： 7月3日（金） 16:30 より場所：京都大学総合人間学部棟 1401 教室 (吉田南キャンパスに入って左側の建物の４Fです）講演者： Klaus Keimel (Darmstadt 工科大学名誉教授) 題目： On the equivalence of state transformer semantics and predicate transformer semantics The meaning of a program may be modeled by the input-output behavior, we call it 'state transformer semantics'. Alternatively, for verifying programs one will be interested in properties A of the output and one wants to find conditions on the input that guarantee property A for the output. One will work with the transformation that assigns to property A of the output the weakest precondition p(A) on the input that guarantees property A for the output; let us call it 'predicate transformer semantics'. In the presence of computational effects like nondeterministic or probabilistic choice, a computation will not be modeled by a function that transforms inputs from a input domain X to an output domain Y but by a state transformer t:X --> T(Y), where T is an appropriate computational monad. The corresponding predicate transformer p associates predicates on Y to predicates on X. Not all predicate transformers will correspond to state transformers, and one looks for necessary and, if possible, sufficient conditions for predicate transformers to correspond to state transformers t:X --> T(Y). Such conditions are sometimes called 'healthiness' conditions. Most examples in the literature dealing with the equivalence of the two semantics can be seen to be based on a domain R of 'observations' and a monad T 'subordinate' to the continuation monad [[(-) --> R] --> R]. For the continuation monad predicates on objects X take values in R. For the continuation monad the state transformers t and the predicate transformers p corresponding to another are related by 'swapping arguments': t(x)(A)= p(A)(x) for x in X and predicates A on Y. It is the aim of this paper to describe a framework of an algebraic/order theoretical nature for the monad T so that the equivalence between state and predicate transformer semantics described above for the continuation monad can be carried over. This framework always yields necessary healthiness conditions. The sufficiency criterion has to be verified in each special situation separately. We illustrate our methods by several examples. As semantic domains we use dcpos (directed complete partially ordered sets). But the same methods can be applied to other Cartesian closed categories and beyond, as we indicate in the concluding remarks.

1 0

Jump to page:

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Logic-ml