Logic-ml

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

7 participants
1772 discussions

Deadline Extended: ICFEM 2012 - 14th International Conference on Formal Engineering Methods (ICFEM 2012)
by Yuki Chiba 24 Apr '12

24 Apr '12

(重複の場合はご容赦ください．) 皆様，北陸先端科学技術大学院大学の千葉です． ICFEM 2012の投稿締め切りが再度延長されましたのでお知らせいたしします．アブストラクトの締め切りは過ぎておりますが新たな投稿も受付中です．是非投稿をご検討下さい．よろしくお願いします． ---------- The deadlines of full paper submissions to ICFEM 2012 have been extended again as follows. Full Paper Submission Deadline (Extended): 30th April, 2012 We are looking forward to your submissions. ************************************************************ 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 Full Paper Submission Deadline (Extended): 30th April, 2012 Acceptance/Rejection Notification: 18th June, 2012 Camera Ready Copy Due: 16th July, 2012 Conference: 12th-16th, November, 2012. ORGANIZATION COMMITTEE General Chairs: Kokichi Futatsugi, JAIST, Japan Shaoying Liu, Hosei Uni., Japan Conference Chair: Hitoshi Ohsaki, AIST, Japan Program Chairs: Kenji Taguchi, AIST, Japan Toshiaki Aoki, JAIST, Japan Steering Committee: Keijiro Araki, Kyushu University, Japan Michael Butler, University of Southampton, UK Jin Song Dong, National University of Singapore, Singapore He Jifeng, East China Normal University, China Shaoying Liu (Chair), Hosei University, Japan Jeff Offutt, George Mason University, USA Shengchao Qin, University of Teesside, UK Program Committee: Bernhard K. Aichernig (Graz University of Technology, Austria) Cyrille Artho (AIST, Japan) Richard Banach (University of Manchester, UK) Nikolaj Bjorner(Microsoft Research Redmond, USA) Jonathan P. Bowen (University of Westminster, UK) Michael Butler (University of Southampton, UK) Sagar Chaki (CMU/SEI, USA) Rance Cleaveland (University of Maryland/Reactive Systems, USA) Jim Davies (Oxford University, UK) Zhenhua Duan (Xidian University, China) Joaquim Gabarro (Universitat Politecnica de Catalunya, Spain) Andy Galloway (University of York, UK) Stefania Gnesi (ISTI-CNR, Italy) Wolfgang Grieskamp (Google, USA) Klaus Havelund (NASA JPL, USA) Daniel Jackson (MIT, USA) Thierry Jeron (INRIA, France) Gerwin Klein (NICTA, Australia) Weiqiang Kong (Kyushu University, Japan) Kim G. Larsen (Aalborg University, Denmark) Peter Gorm Larsen (Engineering College of Aarhus, Denmark) Insup Lee (University of Pennsylvania, USA) Michael Leuschel (Heinrich-Heine Universitat Dusseldorf, Germany) Xuandong Li (Nanjing University, China) Yuan-Fang Li (Monash University, Australia) Zhiming Liu (UNU/IIST, Macau) Dominique Mery (Nancy University and LORIA, France) Stephan Merz (INRIA Nancy & LORIA, France) Huaikou Miao (Shanghai University, China) Alexandre Mota (CIn-UFPE, Brasil) Shin Nakajima (NII, Japan) Kazuhiro Ogata (JAIST, Japan) Jose Nuno Oliveira (Universidade do Minho, Portugal) Jun Pang (University of Luxembourg, Luxembourg) Shengchao Qin (Teesside University, UK) Zongyan Qiu (Peking University, China) S. Ramesh (General Motors India, India) Alexander Romanovsky (Newcastle University, UK) Wuwei Shen (Western Michigan University, USA) Marjan Sirjani (Reykjavik University, Iceland) Greame Smith (The University of Queensland, Australia) Jing Sun (University of Auckland, New Zealand) Jun Sun (Singapore University of Technology and Design, Singapore) Yih-Kuen Tsay (National Taiwan University, Taiwan) Viktor Vafeiadis (MPI-SWS, Germany) Hai H. Wang (Aston University, UK) Ji Wang (National University of Defense Technology, China) Wang Yi (Uppsala University, Sweden) Jian Zhang (Chinese Academy of Sciences, China) Huibiao Zhu (East China Normal University, China) ----------------------------------- 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

Extended Deadline: Call for Papers - LfSA'12 - Logics for System Analysis
by Ichiro Hasuo 21 Apr '12

21 Apr '12

みなさま，こんにちは！東京大学の蓮尾です． 7月のバークレー，CAV 併設ワークショップ LfSA のご案内です． - (***New!***) 締切りが延長されて， Abstract submission: April 27 Paper submission: May 4 となりました． - トピックは（広い意味での）論理を用いたシステム検証で， - まだ新しいワークショップ（2回目）で正式なプロシーディングスもありませんが，専門家が集うので「出席して役に立つ」会合であると考えます．ぜひ投稿をご検討ください．（3カテゴリあります）それでは！蓮尾一郎東京大学大学院情報理工学系研究科コンピュータ科学専攻 http://www-mmm.is.s.u-tokyo.ac.jp/~ichiro/ ================================================ Call for Papers -------------------------------------------------- LfSA'12 -- Logics for System Analysis http://www.ls.cs.cmu.edu/LfSA12 -------------------------------------------------- Workshop Affiliated with CAV 2012 July 7th, 2012, Berkeley, USA Safety-critical systems frequently occur as real-time systems, embedded systems, hybrid systems, distributed systems, and cyber-physical systems. They are also becoming more and more important in many application domains, including aviation, automotive, railway, robotic, or medical applications, where both safety and security are relevant aspects. To ensure the correct functioning of safety-critical systems it is necessary to model and reason about hardware, software, communication aspects, physical properties, and the system environment. LfSA’12 is the second workshop on Logics for System Analysis, devoted to the systematic theoretical study, practical development, and applied use of logics for system analysis. The purpose of the LfSA workshop is to bring together researchers and practitioners interested in studying practically relevant systems or in developing the logical foundations and analysis tools for their study. Topics include * Logics for safety-critical systems (real-time, embedded, hybrid, distributed, stochastic, cyber-physical) * Logic-based methods for development of safety-critical systems * Logics to study security aspects of systems or protocols * System representations using logics, automata, modeling languages, state charts, Petri nets, dataflow models * Theories, decision procedures, and calculi for system analysis * Model checking, theorem proving, and systematic testing * Case studies for logical system analysis * Applications of system analysis to industrial problems In particular, we invite contributions that bridge the gap between theory and practice or that combine different application domains. Submission Categories --------------------- * Regular papers (up to 15 pages), which should present previously unpublished work (completed or in progress), including descriptions of research, tools, and applications. * Short papers (up to 5 pages), which describe work in progress or aim at initiating discussions. * Presentation-only papers, i.e., papers already submitted or presented at a conference or another workshop; such papers will not be included in the LfSA proceedings but will be presented during the workshop. In addition to informal and electronic workshop proceedings, we consider the option of a special issue in a journal after the workshop Workshop/Programme Chairs ------------------------- Andre Platzer Carnegie Mellon University Philipp Ruemmer Uppsala University Programme Committee ------------------- A. Banerjee (IMDEA Madrid) R. Barbosa (U. Coimbra) F. S. de Boer (CWI Amsterdam) A. Cimatti (IRST Trento) M. Dam (KTH Stockholm) S. Demri (CNRS Cachan) M. Giese (U. of Oslo) I. Hasuo (U. Tokyo) F. Ivancic (NEC Lab. Princeton) E. B. Johnsen (U. of Oslo) V. Sofronie-Stokkermans (U. Koblenz) U. Waldmann (MPI Saarbrücken) Important Dates/Deadlines ------------------------- Abstract submission: April 27 Paper submission: May 4 Notification: June 8, 2012 Final version: June 29, 2012 Workshop: July 7, 2012 Workshop Webpage ---------------- http://www.ls.cs.cmu.edu/LfSA12 Submission via Easychair ------------------------ https://www.easychair.org/conferences/?conf=lfsa12

1 0

Announcement of a talk by Kenshi Miyabe (4/26 11:00-)
by Shinya Katsumata 21 Apr '12

21 Apr '12

京都大学数理解析研究所の勝股です。 4月26日（木）11:00から当研究所の宮部　賢志氏が以下の講演を行いますので、ご連絡いたします。どうぞお気軽にお越しください。 ========== Time: 11:00-12:00, 26 Apr, 2012 Place: Rm 478, Research Building 2, Main Campus, Kyoto University http://www.kyoto-u.ac.jp/en/access/campus/main.htm (See 34) 京都大学本部構内総合研究2号館 4階478号室 http://www.kyoto-u.ac.jp/ja/access/campus/map6r_y.htm (34番の建物) Speaker: Kenshi Miyabe (Research Institute for Mathematical Sciences, Kyoto University) Title: 予測限界とランダムネス Abstract: 前半では微分可能性とランダムネスの関連について話をする．最近になって，ランダムネスの諸概念が微分可能性により特徴付けられる事が分かってきた．計算可能ランダムネスよりも強いランダムネスでは，「計算可能＋古典的性質」という形で表されるのに対し，計算可能ランダムネスよりも弱いランダムネスでは，より強い計算可能性が必要になる．講演者は微分定理が成り立つ点の集合がランダムネスの諸概念に一致するような関数族が，積分テストから自然に導かれる事を示した．この関係から上記の理由は自然に説明できる事を示す．後半はアルゴリズム的確率について話す．最初に，Solomonoffのアルゴリズム的確率がなぜ重要なのか話す．そして上記の微分定理によるランダムネスの概念の特徴付けを使って，アルゴリズム的確率がより自然な形に拡張される事を示す．その他，今後行いたい拡張についても列挙する．今回の発表は日本語で行います．現段階でのスライドを以下のページにアップしましたので，興味のある方は予めご覧ください． http://kenshi.miyabe.name/wordpress/?p=677&lang=ja

1 0

Extension of submission deadline, grants: LATD 2012
by Hiroakira Ono 20 Apr '12

20 Apr '12

Logic, Algebra and Truth Degrees 2012 http://www.jaist.ac.jp/rcis/latd12/ Extension of deadline === EXTENDED Deadline for contributed talks: 29 April 2012 === === Grants for travel available - please apply! === The deadline for submissions to LATD 2012 has been extended to 29 April 2012 Please hurry to submit your abstract (2-4 pages) at http://www.easychair.org/conferences/?conf=latd2012 Travel/Participation grants =========================== If there are economical reasons *not* to submit a contribution to the conference, please consider applying for a grant with the following information to latd12(a)jaist.ac.jp: - name, affilitation - amount of money needed - title of your contribution (no grant without presentation) - reason/explanation of need for grant We will let you know the result of our decision on grant support soon after the decision on the contributions. ========== Original Call for Contributions follows ============== The third official meeting of the EUSFLAT Working Group on Mathematical Fuzzy Logic [1] will be held on 10-14 September 2012 in Kanazawa, Japan. The conference is organized by Research Center for Integrated Science [2], Japan Advanced Institute of Science and Technology [3]. Mathematical Fuzzy Logic is a subdiscipline of Mathematical Logic which studies the notion of comparative truth. The assumption that 'truth comes in degrees' has proved to be very useful in many, both theoretical and applied, areas of Mathematics, Computer Science and Philosophy. The main goal of this meeting is to foster collaboration between researchers in the area of Mathematical Fuzzy Logic, and to promote communication and cooperation with members of neighbouring fields. The featured topics include, but are not limited to, the following: . Proof systems for fuzzy logics: Hilbert, Gentzen, natural deduction, tableaux, resolution, computational complexity, etc. . Algebraic semantics: residuated lattices, MTL-algebras, BL-algebras, MV-algebras, Abstract Algebraic Logic, functional representation, etc. . Game-theory: Giles games, Rényi-Ulam games, evaluation games, etc. . First-order fuzzy logics: axiomatizations, arithmetical hierarchy, model theory, etc. . Higher-order fuzzy logical systems: type theories, Fuzzy Class Theory, and formal fuzzy mathematics. . Philosophical issues: connections with vagueness and uncertainty. . Applied fuzzy logical calculi: foundations of logical programming, logic-based reasoning about similarity, description logics, etc. We also welcome contributions on any relevant aspects of related logical systems (such as substructural and quantum logics, and many-valued logics in general). Conference Web Site: http://www.jaist.ac.jp/rcis/latd12/ Important dates: . 22 April 2012: deadline for submissions . 3 June 2012: notifications sent . 10-14 September 2012: conference Programme Committee: . Stefano Aguzzoli (University of Milano, Italy) . Matthias Baaz (Vienna University of Technology, Austria) . Petr Cintula (Academy of Sciences, Czech Republic) . Carles Noguera (CSIC, Spain) . Hiroakira Ono (JAIST, Japan), Chair . James Raftery (University of KwaZulu-Natal, South Africa) . Constantine Tsinakis (Vanderbilt University, USA) Invited Speakers: . Rostislav Horčík (Academy of Sciences, Czech Republic) . Emil Jeřábek (Academy of Sciences, Czech Republic) . Daniele Mundici (University of Florence, Italy) . Greg Restall (University of Melbourne, Australia) . Luca Spada (University of Salerno, Italy) Tutorial: . Felix Bou (University of Barcelona, Spain) If you are interested in presenting a paper, please submit a 2-4 pages abstract at http://www.easychair.org/conferences/?conf=latd2012 Your submission will be confirmed automatically on the e-mail address you provide. The accepted abstracts will be available on-line after the final decision of the program committee. If you have any problems to submit an abstract, please contact us at mail to: latd2012(a)jaist.ac.jp The deadline for contributions is 22 April 2012. The notification of acceptance/rejection will be sent until 3 June 2012. Registration: Registration has not started by now, but we appreciate your email informing us on your participation plans. Registration fee is likewise not determined by now. Grants: There is a limited amount of grants available for participants. Please contact us as soon as possible including the following information: - name, affilitation - amount of money needed - title of your contribution (no grant without presentation) - reason/explanation of need for grant Conference dates: The scientific program will start Monday morning (10 September) and finish Friday noon (14 September). Wednesday afternoon we plan an excursion. Venue: The conference will be held in the city of Kanazawa [4,5,6], located in the Ishikawa prefecture of Japan on the Japan Sea. The venue is the Ishikawa Prefectural Museum of Art [7] in the center of Kanazawa. Local Organizing Committee: . Norbert Preining (JAIST, Japan), Chair . Katsuhiko Sano (JAIST, Japan) . Kazushige Terui (Kyoto University, Japan) . Shunsuke Yatabe (AIST, Japan) For further information please contact: latd2012(a)jaist.ac.jp [1] http://www.mathfuzzlog.org/ [2] http://www.jaist.ac.jp/rcis/en/ [3] http://www.jaist.ac.jp/ [4] http://en.wikipedia.org/wiki/Kanazawa,_Ishikawa [5] http://www.kanazawa-tourism.com/ [6] http://wikitravel.org/en/Kanazawa [7] http://www.ishibi.pref.ishikawa.jp/index_j.html

1 0

The 3rd 「論数哲」(PhilLogMath) workshop
by Shunsuke Yatabe 19 Apr '12

19 Apr '12

The third「論数哲」"Ron-Suu-Tetsu" (PhilLogMath) workshop We will hold the 3rd 「論数哲」(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. Date : May 17 (Thu) Place: Seiryo Kaikan (Nagata-cho, Tokyo) http://metropolis.co.jp/listings/venues/type/stage-venue/seiryo-kaikan/ Speaker: *Daisuke Bekki (Ochanomizu University) and Hiroko Ozaki (Ochanomizu University), *Chung-chieh Shan (Cornell Unversity/ Tsukuba University) Two afternoon slots consists of 60 minutes talk and 30 minutes discussion basically. Author meets Critics meeting is in Japanese, and two afternoon talks are in English. The details will be updated at our website url: http://researchmap.jp/jopmokbbr-21098/#_21098 Workshop organizer (please replace [at] to @): * Yuko Murakami * Shunsuke Yatabe ( shunsuke.yatabe[at]aist.go.jp ) * Takuro Onishi ( takuro.onishi[at]gmail.com )

1 0

IWC 2012 & CoCo 2012: Call for Participation and Provers
by Nao Hirokawa 19 Apr '12

19 Apr '12

皆様合流性 (チャーチ・ロッサ性) に関するワークショップ IWC 2012 の参加者募集と合流性自動証明ツールのコンペティション CoCo 2012 の参加ツール募集の案内をお知らせ致します。IWCの早期参加申し込み締切りは4月25日になっております。廣川　直（北陸先端科学技術大学院大学） ====================================================================== Call for Participation IWC 2012 1st International Workshop on Confluence 29 May 2012, Nagoya, Japan, collocated with RTA 2012 http://cl-informatik.uibk.ac.at/events/iwc-2012/ ====================================================================== Recently there is a renewed interest in confluence research, resulting in new techniques, tool support as well as new applications. The workshop aims at promoting further research in confluence and related properties. The workshop is collocated with the 23rd International Conference on Rewriting Techniques and Applications (RTA 2012). During the workshop the 1st Confluence Competition (CoCo 2012) takes place (see below). IMPORTANT DATES: * early registration April 25, 2012 JST (GMT+9) * registration May 9, 2012 JST (GMT+9) * workshop May 29, 2012 JST (GMT+9) Please register at: https://apollon.nta.co.jp/rta2012/ INVITED SPEAKERS: * Vincent van Oostrom Utrecht University * Yoshihito Toyama Tohoku University ACCEPTED PAPERS: * Bertram Felgenhauer: A Proof Order for Decreasing Diagrams * Dominik Klein and Nao Hirokawa: Confluence of Non-Left-Linear TRSs via Relative Termination (Extended Abstract) * Christian Nemeth, Harald Zankl and Nao Hirokawa: IaCOP - Interface for the Administration of COPS * Kristoffer Rose: A Case for Completion Modulo Equivalence * Thomas Sternagel, René Thiemann, Harald Zankl and Christian Sternagel: Recording Completion for Finding and Certifying Proofs in Equational Logic * Hans Zantema: Automatically Finding Non-Confluent Examples in Abstract Rewriting ORGANISING COMMITTEE: * Nao Hirokawa JAIST * Aart Middeldorp University of Innsbruck * Naoki Nishida Nagoya University ====================================================================== Second Call for Provers CoCo 2012 1st Confluence Competition http://coco.nue.riec.tohoku.ac.jp/2012/ ====================================================================== Recently, several new implementations of confluence proving/disproving tools are reported and interest for proving/disproving confluence "automatically" has been grown. CoCo aims to foster the development of techniques for proving/disproving confluence automatically by setting up a dedicated and fair confluence competition among confluence proving/disproving tools. The 1st Confluence Competition (CoCo 2012) runs during the 1st International Workshop on Confluence (IWC 2012), which is collocated with the 23rd International Conference on Rewriting Techniques and Applications (RTA 2012) at Nagoya University, Japan. In this competition a category for first-order term rewrite systems will be run. Other categories (e.g., higher-order) will be considered if there are tools and problems. IMPORTANT DATES: * registration April 1, 2012 - May 15, 2012 * system description April 15, 2012 - May 15, 2012 * tool submission May 1, 2012 - May 15, 2012 * competition May 29, 2012 REGISTRATION/SUBMISSION: Registration and tool submission will be via the email address: coco-sc [AT] jaist.ac.jp Tools must be able to read input files written in the old TPDB format. The output of the tools must contain an answer in the first line followed by some proof argument understandable for human experts. Valid answers are YES (the input is confluent) and NO (the input is not confluent). Every other answer is interpreted as the tool could not determine the status of the input. For more information including competition rules, see http://coco.nue.riec.tohoku.ac.jp/ All registered tool authors are asked to submit a one-page system description paper in EasyChair style. Submission is via EasyChair at https://www.easychair.org/account/signin.cgi?conf=iwc2012 These papers will appear in the proceedings of IWC 2012. ORGANISING COMMITTEE: * Takahito Aoto Tohoku University (chair) * Nao Hirokawa JAIST * Harald Zankl University of Innsbruck

1 0

European PhD Program in Computational Logic (EPCL): Call for Applications
by Bertram Fronhöfer 18 Apr '12

18 Apr '12

Please distribute this call to everybody you think intrested in. ====================================================== European PhD Program in Computational Logic (EPCL) ====================================================== http://www.epcl-study.eu/ CALL FOR APPLICATIONS The European PhD Program in Computational Logic (EPCL) is run jointly by four of the leading European universities in the field: - Free University of Bozen-Bolzano (Italy), - Technische Universität Dresden (Germany), - Technische Universität Wien (Austria), and - Universidade Nova de Lisboa (Portugal). Further international universities, research organizations and enterprises which contribute to Computational Logic or apply results from it are involved as associated partners: The Simon Fraser University (Canada), the Universidad de Chile, the National ICT Australia Limited (NICTA), and several companies. The program involves three years of PhD study in at least two of the European partner universities. It leads to a joint doctoral degree of the partner universities at which the studies have been physically performed. The language of the program is English. Financial support is available in the form of positions and scholarships. Necessary requirements for participation in EPCL are a Master's degree in Computer Science or Mathematics, or an equivalent degree; the proof of adequate knowledge of English; and substantial knowledge in the areas Foundations of Logics, Foundations of Artificial Intelligence and Declarative Programming. The program starts annually in the winter term. Applications for 2012 have to be electronically submitted on the Webpage http://www.epcl-study.eu/, before the ======================================= Application Deadline on 15 May 2012 ======================================= If you have enquiries, please do not hesitate to contact the coordinator of the program Prof. Steffen Hölldobler Technische Universität Dresden Fakultät Informatik International Center for Computational Logic Email: sh(a)iccl.tu-dresden.de Phone: +49 (351) 463 38340 EPCL is supported by the German Federal Ministry of Education and Research (BMBF) within the German Academic Exchange Service (DAAD) program International Doctorates in Germany (IPID). -- Dr.rer.nat.habil. Bertram Fronhöfer TU Dresden Department of Computer Science International Center for Computational Logic 01062 Dresden, Germany Tel.: +49 (0)351 463 39095

1 0

セミナー案内
by KASHIMA Ryo 17 Apr '12

17 Apr '12

セミナーのご案内日時：4月19日(木)16:30から場所：東京工業大学大岡山西８号館W棟11階 W1101セミナー室会場までの交通案内はこちらから： http://www.titech.ac.jp/about/campus/index.html 話者：蓮尾一郎（東京大学コンピュータ科学専攻） http://www-mmm.is.s.u-tokyo.ac.jp/~ichiro/ 題目：Programming with Infinitesimals: A While-Language for Hybrid System Modeling (Joint Work with Kohei Suenaga, Kyoto University) 概要： 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. 参考文献： 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. Ichiro Hasuo and Kohei Suenaga. Exercises in Nonstandard Static Analysis of Hybrid Systems. To appear in Proc. CAV 2012. 問い合わせ先：鹿島亮（東京工業大学数理・計算科学専攻） kashima(a)is.titech.ac.jp

1 0

神戸大集中講義のお知らせ　非線形科学特論II (6/14, 21, 28)
by Taichi Haruna 17 Apr '12

17 Apr '12

メーリングリストの皆様（重複して受け取られた方はどうかご容赦ください）神戸大学の春名と申します。集中講義のご案内をさせて頂きます。皆様のご参加を歓迎致します。 ============================================================ 授業科目名：非線形科学特論II （副題：不定性を保ったまま無限を扱う方法）講師：辻下徹　先生　（立命館大学）場所：神戸大学大学院理学研究科Z棟101 （理学研究科への交通アクセス：http://www.kobe-u.ac.jp/guid/access/rokko /rokkodai- dai2.html Z棟の場所：http://www.sci.kobe-u.ac.jp/images/map.jpg）日時： 2012年6月14日（木）13：20-17：45（3限+4限+5限の半分） 2012年6月21日（木）13：20-18：30（3限+4限+5限） 2012年6月28日（木）13：20-16：40（3限+4限）講義概要：数学は「限りがないコト」を無限集合というモノにより捉える戦略を２０世紀初頭に採択し大発展しました。その中で、無限の本質にある不定さが、当初はネガティブな雰囲気を伴って姿をあらわしたのですが、その積極的な意義を明らかにしたのが超準解析でした。その誕生から半世紀が経過し、無限集合というモノには頼らずに多くの分野の実質的部分が、厳密かつ直観的議論で簡潔に展開できることがわかってきています。しかし、いまなお超準解析は現代数学の補助手段としてしか認識されていないため不自然な制約があり、新しい数学としての面目躍如というところには至っていません。この講義では、超準数学を「現代数学」とは独立した新しい数学と位置づけ、「限りがないコト」を不定性を保ちつつとらえることが「数学をする」日常においてどのように可能となるかを例示したいと思います。講義関連資料を以下に置く予定です： http://ac-net.org/tjst/12/koube-2012.html ============================================================ -- 春名太一神戸大学大学院・理学研究科・地球惑星科学専攻 Taichi Haruna Department of Earth and Planetary Sciences Graduate School of Science, Kobe University E-Mail: tharuna[at]penguin.kobe-u.ac.jp Tel & Fax: +81-(0)78-803-5739

1 0

Talk by Paul-Andre Mellies in Kyoto (19 April 2012)
by Hasegawa Masahito 16 Apr '12

16 Apr '12

$B3'MM!"(B $B:#=5$NLZMK$K5~Bg$G(BPaul-Andre Mellies$B$5$s$N9V1i$rM=Dj$7$F$$$^$9!#(B $B4X?4$r$*;}$A$NJ}$O$I$&$>$*5$7Z$K$4;22C$/$@$5$$!#(B $BD9C+@n???M(B $B5~ETBg3X?tM}2r@O8&5f=j(B ------ $BF|;~(B: 19 April 2012 (Thursday) 11:00-12:00 $B>l=j(B: $B5~ETBg3XAm9g8&5f(B2$B9f4[(B478$B9f<<(B 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 ) $B9V1i<T(B: Paul-Andre Mellies (CNRS, Paris VII) $BBj(B: Braided notions of dialogue categories $B35MW(B: A dialogue category is a monoidal category equipped with an exponentiating object. In this talk, I will introduce a notion of braided dialogue category, and explain how this notion provides a functorial bridge between proof theory and knot theory. ($BLd$$9g$o$;(B: $BD9C+@n(B <hassei(a)kurims.kyoto-u.ac.jp>) -- Masahito Hasegawa Research Institute for Mathematical Sciences, Kyoto University

1 0

Jump to page:

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Logic-ml