Logic-ml

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

1792 discussions

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

Second Call for Participation: JAIST Spring School 2012 - Formal Reasoning: Theory and Application - (5 - 9 March, 2012)
by Katsuhiko Sano 14 Feb '12

14 Feb '12

各位、重複して受け取られた場合はどうぞご容赦ください。現在、北陸先端科学技術大学院大学、情報科学研究科では、 JAIST Spring School 2012 - Formal Reasoning: Theory and Application - http://www.jaist.ac.jp/~hirokawa/jss12.html chair 東条敏 (JAIST) を平成24年3月5日から3月9日まで於、金沢県立美術館の日程で開催する予定です。これにあたり、本スプリングスクールへの参加に関心のある、日本国内の大学院生・ポスドク（学部・研究科は問いません）を10名程度募集いたします（なお、参加費（一万円程度、昼食代と懇親会代を含みます）が必要です）。会場のキャパシティに限りがございますので、参加に興味がおありの方は、下記のApplication Form に必要事項を記入の上（日本語可）、 jss2012-oc(a)jaist.ac.jp まで件名 "JSS2012 Domestic Application" でご返信ください。締切は平成24年2月17日(金) と致します。 ************************************************************ *** JAIST Spring School 2012 Application Form *** *** Deadline: 17th February 2012 *** *** Reply to "jss2012-oc(a)jaist.ac.jp" *** *** with subject-line "JSS2012 Domestic Application" *** ************************************************************ 1) Family (last) Name: 2) Middle Name (if any): 3) Given (first) Name: 4) Sexuality: (male/female) 5) Age: 6) Nationality: 7) Affiliation: 8) E-mail address: 9) Home page URL (if you have): 10) Status (choose one): - graduate student (indicate grade) - postdoc (indicate when you became postdoc) - others (indicate your status) 11) Sketch your main motivation (in a few lines) to attend JAIST Spring School 2012, research interests, and past research achievements. If you have already published some research papers, indicate them. 12) If you are a student, indicate the following: Supervisor's name: Supervisor's title and affiliation: Supervisor's e-mail address: 13) Any special dietary requirements or food allergies?: ************************************************************ ********************** end end end ************************* ************************************************************

1 0

ワークショップ「数理論理学の諸科学への発展と展開」のご案内
by Katsuhiko Sano 14 Feb '12

14 Feb '12

皆様、重複して受け取られた場合はどうぞご容赦ください。北陸先端科学技術大学院大学情報科学研究科では、平成２３年度　数学・数理科学と諸科学・産業との連携研究ワークショップ拡がっていく数学　〜期待される　”見えない力”〜 http://www.mext.go.jp/a_menu/math/index.htm （後援：（社）日本数学会、日本応用数理学会、統計関連学会連合、（独）科学技術振興機構）の一環として、文部科学省と共同で以下のワークショップを開催いたします。タイトル：数理論理学の諸科学への発展と展開 http://www.jaist.ac.jp/~hirokawa/ml12.html 日時：　平成２４年３月９日（金）　９：００〜１７：００場所：　石川県立美術館　広坂別館講演者：　佐藤雅彦（京都大学大学院情報学研究科）　下嶋篤（同志社大学文化情報学部）　田中一之（東北大学大学院理学研究科）　東条敏（北陸先端科学技術大学院大学情報科学研究科）　山田友幸（北海道大学大学院文学研究科）また、前日３月８日（木）には、ワークショップの直前３月５日（月）〜３月８日（木）に開催される JAIST Spring School 2012 -- Formal Reasoning: Theory and Application -- http://www.jaist.ac.jp/~hirokawa/jss12.html と合同で懇親会を開催予定です。会費は6，000円を予定しています。会場等の準備の都合もございますので、参加に興味がおありの方は、氏名：所属・職（学生の場合は学年）： 3月8日（木）の懇親会：　参加・不参加　（どちらかをお選びください）を jss2012-oc(a)jaist.ac.jp まで件名 "JSS2012 Workshop" でご返信ください。また、締切は　平成24年2月21日(火) とします。なお、JAIST Spring School 2012に申し込まれた、または、これから申し込まれる方の申し込みは不要です。 -- Katsuhiko Sano School of Information Science Japan Advanced Institute for Science and Technology IS building No.1 7F, 1-1 Asahidai, Nomi, Ishikawa, 923-1292, Japan

1 0

2012LLS
by Toshihiko Kurata 12 Feb '12

12 Feb '12

kisoron-ml，logic-mlの皆様，昨年の夏休み期間に行われました「ラムダと論理の研究会」ですが，春休みにも同様に行うこととなりました．詳しい情報は http://www.i.hosei.ac.jp/~kurata/2012LLS/ にありますので気軽に参加を検討いただけますと幸いです．過去のセミナーと同様に「ラムダ計算と論理およびその周辺分野」に関して，成果発表の場というよりは成果をあげる場となっていまして，講演件数を抑え，残りの時間は個人やグループで柔軟に計画してもらうようになっています．色々な方と交流を持つためにも丁度よいと思います．（こうした形式のセミナーは主に海外で行われているらしく，それを取り入れた古森先生の研究室の下で継続的に実施されています．） ---- Toshihiko Kurata, Hosei University e-mail kurata(a)hosei.ac.jp ---------------------------------------------------------------------- 日時：　2012年3月18日(日)午後5時から3月22日(木)正午まで場所：　国立大学草津セミナーハウス参加申込：　昨夏と同様に事務的なことは倉田（法政大学）が窓口となっています．講演や参加を希望されます方は以下の項目を kurata(a)hosei.ac.jp までメイル下さい．会議室確保の都合がありまして，参加のみ希望されます方も予め御連絡頂けますと幸いです． -------------------------- 参加申込 -------------------------- 氏名：所属：連絡先 (e-mail): 参加期間：講演希望：有・無題目：希望時間：その他： -------------------------------------------------------------- また，セミナーに参加される方の中で特にセミナーハウスでの宿泊を希望される方は 2月20日までに宿泊申込を倉田（上記e-mailアドレス）までメイル下さい．宿泊定員の関係でこちらの締切は早くなっています．（確保した部屋が一杯になったら締切内に申し込んでも部屋が確保できない可能性がありますので御了承下さい．）他の情報は後から送って頂いて構いませんので，よろしくお願いいたします． ------------------- セミナーハウス宿泊申込 ------------------- セミナーハウスの宿泊の申込をします。部屋タイプの希望（教員は選択可，学生は学生部屋となります）：　　　　教員用, 学生用, どちらでもよい宿泊・食事の希望（希望しない部分を消去して下さい）：　　　　18日　　夕食　宿泊　　　　19日　　朝食　夕食　宿泊　　　　20日　　朝食　夕食　宿泊　　　　21日　　朝食　夕食　宿泊　　　　22日　　朝食 --------------------------------------------------------------

1 0

CFP: AiML 2012
by Thomas Bolander 11 Feb '12

11 Feb '12

AiML-2012: FINAL CALL FOR PAPERS 9-TH INTERNATIONAL CONFERENCE ON ADVANCES IN MODAL LOGIC COPENHAGEN, 22-25 AUGUST, 2012 http://hylocore.ruc.dk/aiml2012.html Advances in Modal Logic is an initiative aimed at presenting the state of the art in modal logic and its various applications. The initiative consists of a conference series together with volumes based on the conferences. Information about the AiML series can be obtained at http://www.aiml.net. AiML-2012 is the ninth conference in the series. TOPICS We invite submission on all aspects of modal logic, including: - history of modal logic - philosophy of modal logic - applications of modal logic - computational aspects of modal logic (complexity and decidability of modal and temporal logics, modal and temporal logic programming, model checking, model generation, theorem proving for modal logics) - theoretical aspects of modal logic (algebraic/categorical perspectives on modal logic, coalgebraic modal logic, completeness and canonicity, correspondence and duality theory, many-dimensional modal logics, modal fixed point logics, model theory of modal logic, proof theory of modal logic) - specific instances and variations of modal logic (description logics, modal logics over non-boolean bases, dynamic logics and other process logics, epistemic and deontic logics, modal logics for agent-based systems, modal logic and game theory, modal logic and grammar formalisms, provability and interpretability logics, spatial and temporal logics, hybrid logic, intuitionistic logic, substructural logics, computationally light fragments of all such logics) Papers on related subjects will also be considered. CONFERENCE LOCATION Advances in Modal Logic 2012 will be held at the IDA conference centre in downtown Copenhagen: http://ida.dk/sites/moedecenter/english/Sider/EnglishForside.aspx This is in easy walking distance from Copenhagen Central Station and a number of reasonably priced hotels. PAPER SUBMISSIONS There will be two types of submissions to AiML-2012: (1) Full papers for publication in the proceedings and presentation at the conference. (2) Abstracts for short presentation only. Both types of papers should be submitted electronically using the EasyChair submission page at http://www.easychair.org/conferences/?conf=aiml2012 At least one author of each accepted paper of abstract must register for, and attend, the conference to present his or her work. (1) FULL PAPERS. Authors are invited to submit, for presentation at the conference and publication in the proceedings, full papers reporting on original research and not submitted elsewhere. The proceedings of AiML'2012 will be published by College Publications (http://www.collegepublications.co.uk) in a volume to be made available at the conference. The submissions should be at most 15 pages, with an optional technical appendix of up to 5 pages, together with a plain-text abstract of 100-200 words. The submissions must be typeset in LaTeX, using a style file and template that will be provided on the AiML'2012 website. (2) ABSTRACTS. These should be at most 5 pages. They may describe preliminary results, work in progress etc., and will be subject to light reviewing. The accepted abstracts will be made available at the conference, and the authors will have the opportunity to make short presentations (of up to 15 minutes) on them. SPECIAL SESSION ON HYBRID LOGIC. Hybrid logic is an extension of modal logic allowing to refer explicitly to states of the model in the syntax of formulas. There will be a special session of AiML devoted to papers on hybrid logic. The scope of the special session is standard hybrid-logical machinery like nominals, satisfaction operators, and the downarrow binder, but also other extensions of modal logic can be considered. SPECIAL SESSION IN HONOUR OF LARISA MAKSIMOVA. There will be a special session of AiML devoted to papers and talks in honour of Larisa Maksimova, in recognition of her many outstanding contributions to modal logic. SPECIAL SESSION ON MODALITIES FOR TYPES. Recent years have witnessed significant growth of interest in constructive type-theoretical modalities, in particular modalities ensuring productivity and type safety of (co-)recursive definitions in reactive programming. Some earlier examples include the use of modalities for staged computation, metaprogramming or in computational lambda-calculus. In order to boost interaction between programming, type-theoretical and modal communities, AiML 2012 will host a special session on these topics. Papers for this session should be submitted to the EasyChair site along with others. Papers for the special sessions should be submitted to the EasyChair site along with others. INVITED SPEAKERS Lev Beklemishev (Moscow State University) Johan van Benthem (University of Amsterdam and Stanford University) Lars Birkedal (IT University of Copenhagen, Denmark) Patrick Blackburn (Roskilde University) Balder ten Cate, (UC Santa Cruz) Larisa Maksimova (Novosibirsk State University) PROGRAMME COMMITTEE Carlos Areces (FaMAF, Universitad Nacional de Cordoba, Argentina) Philippe Balbiani (IRIT, Toulouse, France) Lev Beklemishev (Moscow State University, Russia) Guram Bezhanishvili (New Mexico State University, USA) Nick Bezhanishvili (Imperial College London, UK) Patrick Blackburn (Roskilde University, Denmark) Thomas Bolander (Technical University of Denmark) Torben Brauner (Roskilde University, Denmark) Giovanna Corsi (Università di Bologna, Italy) Giovanna D'Agostino (Università di Udine, Italy) Stephane Demri (LSV, ENS Cachan, France) Melvin Fitting (Lehman College, CUNY, USA) Robert Goldblatt (Victoria University of Wellington, New Zealand) Valentin Goranko (Technical University of Denmark) Rajeev Gore (Australian National University, Australia) Andreas Herzig (IRIT, Toulouse, France) Ian Hodkinson (Imperial College London, UK) Wiebe van der Hoek (University of Liverpool, UK) Rosalie Iemhoff (University of Utrecht, The Netherlands) Alexander Kurz (University of Leicester, UK) Tadeusz Litak (University of Leicester, UK) Hiroakira Ono (Japan Advanced Institute of Science and Technology) Martin Otto (Technical University of Darmstadt, Germany) Alessandra Palmigiano (ILLC, University of Amsterdam, The Netherlands) Renate Schmidt (University of Manchester, UK) Lutz Schröder (DFKI GmbH and University of Bremen, Germany) Valentin Shehtman (Moscow State University, Russia) Dimiter Vakarelov (Sofia University, Bulgaria) Yde Venema (ILLC, University of Amsterdam, The Netherlands) Heinrich Wansing (Ruhr University Bochum, Germany) Frank Wolter (University of Liverpool, UK) Michael Zakharyaschev (Birkbeck College, London, UK) PROGRAMME COMMITTEE CO-CHAIRS Silvio Ghilardi (Università degli Studi di Milano, Italy) Lawrence Moss (Indiana University, USA) ORGANIZING COMMITTEE CO-CHAIRS Thomas Bolander (Technical University of Denmark) Torben Brauner (Roskilde University, Denmark) IMPORTANT DATES Full papers submission deadline: 30 March 2012 Full papers acceptance notification: 18 May 2012 Short presentations submission deadline: 1 June, 2012 Short presentations acceptance notification: 18 June, 2012 Final version of full papers and abstracts due: 15 June 2012 Conference: 22-25 August, 2012. FURTHER INFORMATION. Please see http://hylocore.ruc.dk/aiml2012/ ENQUIRIES. E-mail enquiries should be directed respectively to the PC co-chairs, sent to aiml2012(a)easychair.org

1 0

第26回量子情報技術研究会（QIT26）のご案内
by Harumichi Nishimura 10 Feb '12

10 Feb '12

logic-ml$B$N3'MM!$(B $BBh(B26$B2sNL;R>pJs5;=Q8&5f2q!J(BQIT26$B!K$N0FFb$K$D$$$F!$(B $B@$OC?M$+$i$N0MMjEj9F$r$5$;$F$$$?$@$-$^$9!%(B $B$J$*!$=EJ#$7$F$*<u$1<h$j$N@a$O$4MF<O$/$@$5$$!%(B $BBg:eI\N)Bg3XM}3X7O8&5f2J(B $B@>B<<#F;(B http://www.mi.s.osakafu-u.ac.jp/~hnishimura/ =============================================================== $BBh(B26$B2sNL;R>pJs5;=Q8&5f2q$N$40FFb(B $B8&5f2q$NFbMF(B $B>pJs2J3X$HNL;RNO3X$rM;9g$5$;$??7$7$$J,Ln!$NL;R>pJs2J3X$K4X$9(B $B$k8&5f2q$G$9!%>pJs$rC4$&J*M}7O$NNL;RNO3XE*B&LL$r@Q6KE*$K3h$+$7(B $B$??7$7$$>pJs=hM}86M}$N8&5f$H!$$=$3$+$i3+$+$l$k?7$7$$3XLdBN7O$N(B $B9=C[$*$h$S?7$7$$>pJs5;=Q%Q%i%@%$%`$NAO@8$rL\;X$7$F!$>pJs2J3X!$(B $BJ*M}3X!$8w%(%l%/%H%m%K%/%9$r4^$`M}3X!$9)3X!$?tM}2J3X$K7H$o$k8&(B $B5f<T4V$K<+M3$JF$O@$N>l$rDs6!$7!$$3$N8&5fJ,Ln$NH/E8$r?^$k$3$H$r(B $BL\E*$H$7$F$$$^$9!%Bh(B26$B2s8&5f2q$r2<5-$N$h$&$K3+:E$$$?$7$^$9!%8=(B $B:_$3$NJ,Ln$G3hLv$9$k8&5f<T$OL^O@!$<+J,$N8&5f;q;:$,2?$i$+$N7A$G(B $B;H$($=$&$@$HM=46$7$F$$$k8&5f<T!&5;=Q<T$J$I!$9-$/4XO"$9$kJ,Ln$N(B $B8&5f<T!&5;=Q<T$+$i$NH/I=!$D09V$rJg=8CW$7$^$9!%J3$C$F$4;22C$/$@(B $B$5$$!%(B $B4|F|!!(B2012$BG/(B 5$B7n(B21$BF|!J7n!K(B, 22$BF|!J2P!K(B $B2q>l!!J!0fBg3X!!J85~%-%c%s%Q%9!!Am9g8&5fEo-5(B $B!!!J")(B910-8507 $BJ!0f;TJ85~(B3$BCzL\(B9-1$B!K(B $BH/I=Jg=8FbMF(B $BH/I=Jg=8J,Ln!J?=9~>u67$K$h$C$F$O::FI2DG=@-$"$j!K!'(B $BNL;R>pJs!$NL;R7W;;!$NL;R0E9f$J$I9-$/NL;R>pJs5;=Q$K4X$o$kM}O@E*(B $B8&5f!$<B83E*8&5f!$7W;;5!2J3XE*8&5f!$?t3XE*8&5f!$$*$h$S$=$N4XO"(B $BJ,Ln(B $B>7BT9V1i!'L$Dj(B $BDj0w!!(B180$BL>DxEY(B $B;22CHq!!;vA0?69~$_!!0lHL(B5,000$B1_(B, $B3X@8(B2,000$B1_(B ($BEvF|2q>lJ'$$$O0lHL(B6,000$B1_(B, $B3X@8(B3,000$B1_(B) ($B:)?F2q$OJLES!K(B $B8&5f2q;22C?=9~MWNN(B $B9V1i(B($B8}F,!&%]%9%?!<(B)$B?=9~!$D09V?=9~$O2<5-(BURL$B$K$F<uIU$r9T$$$^$9(B http://staff.aist.go.jp/s-kawabata/qit/ $B!Z9V1i?=9~Dy@Z![(B $B!!(B2012$BG/(B4$B7n(B10$BF|!J2P!K8}F,(B $B!!(B2012$BG/(B4$B7n(B20$BF|!J6b!K%]%9%?!<(B $B!Z;22C?=9~Dy@Z![(B 2012$BG/(B4$B7n(B30$BF|(B($B7n!K(B $B!Z@$OC?M![(B $B:d8}J8B'!JJ!0fBg3X!!9)3X8&5f2J!!EE5$!&EE;R9)3X@l96!K(B $B66K\5.L@!JJ!0fBg3X!!9)3X8&5f2J!!J*M}9)3X@l96!K(B $BNSL@5W!JJ!0fBg3X!!9)3X8&5f2J!!J*M}9)3X@l96!K(B $BKYn4L-!JJ!0fBg3X!!9)3X8&5f2J!!J*M}9)3X@l96!K(B e-mail: qit26(a)serv.apphy.u-fukui.ac.jp $B<g:E!!NL;R>pJs5;=Q;~8B8&5f@lLg0Q0w2q(B $B!!!!!!!!(B($B0Q0wD9!!KL@n>!9@(B($BBg:eBg3X(B)) $B6&:E!!1~MQJ*M}3X2q(B $BNL;R%(%l%/%H%m%K%/%98&5f2q(B

1 0

DICE 2012 - Call for Extended Abstracts
by Nao Hirokawa 09 Feb '12

09 Feb '12

皆様 ETAPS 2012 で非明示計算量に関するワークショップ DICE 2012 が行われます。その extended abstract 募集をご案内致します。このカテゴリは既発表の内容も投稿可能です。ETAPS 参加の方はぜひ投稿をご検討下さい。廣川 =============================================================== CALL FOR EXTENDED ABSTRACTS DICE 2012 3rd Workshop on Developments in Implicit Complexity Tallinn (Estonia), March 31st and April 1st, 2012 (Affiliated with ETAPS 2012) http://dice2012.cs.unibo.it/ =============================================================== SCOPE The area of Implicit Computational Complexity (ICC) has grown out from several proposals to use logic and formal methods to provide languages for complexity-bounded computation (e.g. polytime or logspace computation). It aims at studying computational complexity without referring to external measuring conditions or a particular machine model, but only by considering language restrictions or logical principles implying complexity properties. This workshop focuses on ICC methods related to programs (rather than descriptive methods). In this approach one relates complexity classes to restrictions on programming paradigms (functional programs, lambda calculi, rewriting systems), such as ramified recurrence, weak polymorphic types, linear logic and linear types, and interpretative measures. The two main objectives of this area are: * to find natural implicit characterizations of various complexity classes of functions, thereby illuminating their nature and importance; * to design methods suitable for static verification of program complexity. Therefore ICC is related on the one hand to the study of complexity classes, and on the other hand to static program analysis. The workshop will be open to contributions on various aspects of ICC including (but not exclusively): * types for controlling complexity, * logical systems for implicit computational complexity, * linear logic, * semantics of complexity-bounded computation, * rewriting and termination orderings, * interpretation-based methods for implicit complexity, * programming languages for complexity-bounded computation, * certification of complexity properties of programs, * application of implicit complexity to other programming paradigms (e.g. imperative or object-oriented languages). The first two DICE workshops were held in 2010 in Cyprus and in 2011 in Germany, both as part of ETAPS conferences. Before that, several meetings on this topic had already been held with success in Paris (WICC 2008), and Marseille (GEOCAL 2006 workshop on Implicit computational complexity). _______________________________________________________________ INVITED TALKS * Ulrich Schoepp (LMU Munich) Computation by Interaction for Structuring Resource Bounded Computation * Neelakantan R. Krishnaswami (MPI) tba _______________________________________________________________ SUBMISSION * Submission (extended abstracts): February 18th, 2012 * Notification (extended abstracts): February 28th, 2012 Extended abstracts for short presentations (not included in the proceedings) are of up to 3 pages and authors have to add "(Extended Abstract)" to the title. Papers must be submitted electronically, as pdf files, at the following page: https://www.easychair.org/conferences/?conf=dice2012. We welcome short versions of recently published articles and papers submitted elsewhere. _______________________________________________________________ PROGRAM COMMITTEE * Guillaume Bonfante (Nancy) * Ugo Dal Lago (Bologna, chair) * Marco Gaboardi (Bologna and UPenn) * Nao Hirokawa (JAIST) * Martin Hofmann (Munchen) * Olivier Laurent (ENS Lyon) * Jean-Yves Moyen (Paris Nord) * Isabel Oitavem (Lisboa) * German Puebla (Madrid) * Simona Ronchi Della Rocca (Torino) _______________________________________________________________

2 1

JAIST Verification Seminar on Complexity Theory by Prof. Yijia Chen (Feb 9, 13:00)
by Nao Hirokawa 08 Feb '12

08 Feb '12

皆様明日2月9日(木)に JAIST で行われます Yijia Chen 教授の計算量理論に関する講演をご案内致します。どうぞお気軽にお越しください。 http://www.ldl.jaist.ac.jp/svrcenter/event.html#20120209 廣川　直（北陸先端科学技術大学院大学） - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - Seminars of Research Center for Software Verification, JAIST - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - Date: 9th Feb (Thu) 13:00-15:00 Place: JAIST IS school collaboration room 7 (5F) Speaker: Prof.Yijia Chen (Shanghai Jiao Tong University) Title: A Logic for PTIME and a Parameterized Halting Problem Abstract: Whether there is a logic for polynomial time (PTIME) is the central problem in finite model theory. When formalizing this problem, Gurevich (1988), together with Blass, actually proposed a logic LFP_inv, which is a version of least fixed-point logic plus some additional invariance condition. Although they don't believe that LFP_inv captures PTIME, no proof was given. Later, in a work of Nash, Remmel, and Vianu (2005), it was shown that whether LFP_inv captures PTIME is equivalent to the parameterized complexity of a halting problem: input: A nondeterministic Turing machine M and a natural number n in unary. parameter: |M|, i.e., the size of M question: does M accept the empty input in at most n steps? Our recent work (2010-11) reveals that it is even equivalent to an open problem in proof complexity, i.e., whether there is a polynomial optimal proof system for the set TAUT of tautologies of propositional logic. In this talk, I will discuss all these equivalences and their extensions to some other complexity classes beside PTIME. It turns out that Levin's optimal inverters (1973) play a central role in the proofs. This is joint work with Joerg Flum.

1 0

Advances in Modal Logic IX
by Hiroakira Ono 08 Feb '12

08 Feb '12

AiML-2012: FINAL CALL FOR PAPERS ADVANCES IN MODAL LOGIC IX COPENHAGEN, 22-25 AUGUST, 2012 http://hylocore.ruc.dk/aiml2012 Advances in Modal Logic is an initiative aimed at presenting the state of the art in modal logic and its various applications. The initiative consists of a conference series together with volumes based on the conferences. Information about the AiML series can be obtained at http: //www.aiml.net. AiML-2012 is the ninth conference in the series. TOPICS. We invite submission on all aspects of modal logic, including: - history and philosophy of modal logic; - applications of modal logic; - computational aspects of modal logic (complexity and decidability of modal and temporal logics, modal and temporal logic programming, model checking, model generation, theorem proving for modal logics); - theoretical aspects of modal logic (algebraic/categorical perspectives on modal logic, coalgebraic modal logic, completeness and canonicity, correspondence and duality theory, manydimensional modal logics, modal xed point logics, model theory of modal logic, proof theory of modal logic); - specific instances and variations of modal logic (description logics, modal logics over non-boolean bases, dynamic logics and other process logics, epistemic and deontic logics, modal logics for agent-based systems, modal logic and game theory, modal logic and grammar formalisms, provability and interpretability logics, spatial and temporal logics, hybrid logic, intuitionistic logic, substructural logics, computationally light fragments). Papers on related subjects will also be considered. CONFERENCE LOCATION. Advances in Modal Logic 2012 will be held at the IDA conference center in downtown Copenhagen: http://ida.dk/sites/moedecenter/english/Sider/ EnglishForside.aspx This is in walking distance from Copenhagen Central Station and many reasonably priced hotels. PAPER SUBMISSIONS. There will be two types of submissions to AiML-2012: (1) Full papers for publication in the proceedings and presentation at the conference. (2) Abstracts for short presentation only. Both types of papers should be submitted electronically using the EasyChair submission page at http://www.easychair.org/conferences/? conf=aiml2012. At least one author of each accepted paper or abstract must register for, and attend, the conference to present his or her work. (1) FULL PAPERS. Authors are invited to submit, for presentation at the conference and publication in the proceedings, full papers reporting on original research and not submitted elsewhere. The proceedings of AiML'2012 will be published (in a volume to be made available at the conference) by College Publications http://www.collegepublications.co.uk. The submissions should be at most 15 pages, with an optional technical appendix of up to 5 pages, together with a plain-text abstract of 100-200 words. The submissions must be typeset in LaTex, using a style file and template that will be provided on the AiML'2012 website. (2) ABSTRACTS. These should be at most 5 pages. They may describe preliminary results, work in progress etc., and will be subject to light reviewing. The accepted abstracts will be made available at the conference, and the authors will make short (up to 15 min) presentations on them. SPECIAL SESSION ON HYBRID LOGIC. Hybrid logic is an extension of modal logic allowing to refer explicitly to states of the model in the syntax of formulas. There will be a special session of AiML devoted to papers on hybrid logic. The scope of the special session is standard hybrid-logical machinery like nominals, satisfaction operators, and the downarrow binder, but also other extensions of modal logic can be considered. Papers for this session should be submitted the same way as others. SPECIAL SESSION IN HONOUR OF LARISA MAKSIMOVA. There will also be a special session of AiML devoted to papers and talks in honour of Larisa Maksimova, in recognition of her many outstanding contributions to modal logic. SPECIAL SESSION ON MODALITES FOR TYPES. Recent years have witnessed significant growth of interest in constructive type-theoretical modalities, in particular modalities ensuring productivity and type safety of (co-)recursive definitions in reactive programming. Some earlier examples include the use of modalities for staged computation, metaprogramming or in computational lambda-calculus. In order to boost interaction between programming, type-theoretical and modal communities, AiML 2012 will host a special session on these topics. Papers for this session should be submitted to the EasyChair site along with others. INVITED SPEAKERS Lev Beklemishev (Moscow State University) Johan van Benthem (University of Amsterdam and Stanford University) Patrick Blackburn (Roskilde University) Balder ten Cate (UC Santa Cruz) Larisa Maksimova (Novosibirsk State University) PROGRAMME COMMITTEE Carlos Areces (FaMAF, Univ. Nac. de Cordoba, Argentina) Philippe Balbiani (IRIT, Toulouse, France) Lev Beklemishev (Moscow State University, Russia) Guram Bezhanishvili (New Mexico State University, USA) Nick Bezhanishvili (Imperial College London, UK) Patrick Blackburn (Roskilde University, Denmark) Thomas Bolander (Technical University of Denmark) Torben Brauner (Roskilde University, Denmark) Giovanna Corsi (Universit a di Bologna, Italy) Giovanna D'Agostino (Universit a di Udine, Italy) Stephane Demri (LSV, ENS Cachan, France) Melvin Fitting (Lehman College, CUNY, USA) Silvio Ghilardi (Universit a di Milano, Italy) Robert Goldblatt (Victoria Univ. of Wellington, New Zealand) Valentin Goranko (Technical University of Denmark) Rajeev Gore (Australian National University, Australia) Andreas Herzig (IRIT, Toulouse, France) Ian Hodkinson (Imperial College London, UK) Wiebe van der Hoek (University of Liverpool, UK) Alexander Kurz (University of Leicester, UK) Tadeusz Litak (University of Leicester, UK) Lawrence Moss (Indiana University, USA) Hiroakira Ono (Japan Adv. Inst. of Science and Technology) Martin Otto (Technical University of Darmstadt, Germany) Alessandra Palmigiano (ILLC, Univ. of Amsterdam, The Netherlands) Renate Schmidt (University of Manchester, UK) Lutz Schroder (DFKI GmbH & Univ. of Bremen, Germany) Valentin Shehtman (Moscow State University, Russia) Dimiter Vakarelov (So a University, Bulgaria) Yde Venema (ILLC, Univ. of Amsterdam, The Netherlands) Heinrich Wansing (Ruhr University Bochum, Germany) Frank Wolter (University of Liverpool, UK) Michael Zakharyaschev (Birkbeck College, London, UK) PROGRAMME COMMITTEE CO-CHAIRS Silvio Ghilardi (Universit degli Studi di Milano, Italy) Lawrence Moss (Indiana University, USA) ORGANIZING COMMITTEE CO-CHAIRS Thomas Bolander (Technical University of Denmark) Torben Brauner (Roskilde University, Denmark) IMPORTANT DATES Full papers submission deadline: 30 March 2012 Full papers acceptance noti cation: 18 May 2012 Abstracts submission deadline: 1 June, 2012 Abstracts acceptance noti cation: 7 June, 2012 Final version of full papers and abstracts due: 15 June 2012 Conference: 22-25 August, 2012. FURTHER INFORMATION. See the AiML 2012 website hylocore.ruc.dk/aiml2012 ENQUIRIES. E-mail enquiries should be directed respectively to the PC co-chairs, sent to aiml2012(a)easychair.org

1 0

lectures by Prof. Marta Kwiatkowska
by hagiya＠is.s.u-tokyo.ac.jp 07 Feb '12

07 Feb '12

確率モデル検査で著名な Marta Kwiatkowska先生(University of Oxford)のご講演の案内です。(2件あります。) === 日時: 2月15日(水) 15:30〜場所: 東京大学理学部7号館007 A Framework for Verification of Software with Time and Probabilities Marta Kwiatkowska, University of Oxford (joint work with Gethin Norman and David Parker) Quantitative verification techniques are able to establish system properties such as "the probability of an airbag failing to deploy on demand'' or "the expected time for a network protocol to successfully send a message packet''. In this paper, we describe a framework for quantitative verification of software that exhibits both real-time and probabilistic behaviour. The complexity of real software, combined with the need to capture precise timing information, necessitates the use of abstraction techniques. We outline a quantitative abstraction refinement approach, which can be used to automatically construct and analyse abstractions of probabilistic, real-time programs. As a concrete example of the potential applicability of our framework, we discuss the challenges involved in applying it to the quantitative verification of SystemC, an increasingly popular system-level modelling language. === 日時: 2月17日(金) 15:30〜場所: 東京大学理学部7号館007 Design and Analysis of DNA Strand Displacement Devices using Probabilistic Model Checking Marta Kwiatkowska, University of Oxford (joint work with Matthew Lakin, David Parker, Luca Cardelli and Andrew Phillips, to appear in Journal of the Royal Society Interface) Designing correct, robust DNA devices is difficult because of the many possibilities for unwanted interference between molecules in the system. DNA strand displacement has been proposed as a design paradigm for DNA devices, and the DSD programming language has been developed as a means of formally programming and analysing these devices to check for unwanted interference. We demonstrate, for the first time, the use of formal verification techniques, in particular model checking and probabilistic model checking, to analyse the correctness, reliability and performance of DNA devices during the design phase. We use the probabilistic model checker PRISM, in combination with the DSD language, to design and debug DNA strand displacement components and to investigate their kinetics. We show how our techniques can be used to identify design flaws and to evaluate the merits of contrasting design decisions, even on devices comprising relatively few inputs. We then demonstrate the use of these components to construct a DNA strand displacement device for approximate majority voting. Finally, we discuss some of the challenges and possible directions for applying these methods to more complex designs.

1 0

Jump to page:

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Logic-ml