- Logic-ml - fos.kuis.kyoto-u.ac.jp

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 15 Feb '12

15 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 15 Feb '12

15 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 12 Feb '12

12 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

Asian Workshop on Philosophical Logic
by Hiroakira Ono 03 Feb '12

03 Feb '12

Asian Workshop on Philosophical Logic "Asian Workshop on Philosophical Logic" will be organized by Research Center for Integrated Science (RCIS), Japan Advanced Institute of Science and Technology (JAIST) and held at the Ishikawa Hightech Ceter near JAIST from 15th to 17th February, 2012. Our aim is to promote mutual understandings among researchers on logic working in Asian countries, and to establish closer collaborations in future. The scope of the Workshop will cover: philosophical logic, non-classical logics, algebraic logic, and their applications in computer science and cognitive science During the Workshop, we will have a special session of discussions on future collaborations, in particular on research, education and exchange of researchers in our region. We welcome your participation in both talks and special session. For the details, see http://www.jaist.ac.jp/rcis/awpl/ =============== Organizers Hiroakira Ono Norbert Preining Research Center for Integrated Science http://www.jaist.ac.jp/rcis/ Japan Advanced Institute of Science and Technology Nomi, Ishikawa, 923-1292 Japan ===============

1 0

NII Type Theory Workshop
by Makoto Tatsuta 01 Feb '12

01 Feb '12

Seventh NII Type Theory Workshop Date: February 6, 2012, 13:00--17:00 Place: National Institute of Informatics, Room 2005 (20th floor) 場所: 国立情報学研究所 20階 2005室 (半蔵門線,都営地下鉄三田線・新宿線神保町駅または東西線竹橋駅より徒歩5分) (地図 http://www.nii.ac.jp/introduce/access1-j.shtml) Program: 13:00--13:30 Daisuke Kimura (National Institute of Informatics) Title: A generalized modal lambda calculus 13:30--14:00 Kazuyuki Asada (National Institute of Informatics) Title: Semantics of Multi-rooted Graph with Ordered Branch 14:00--14:20 Tea Break 14:20--15:00 Makoto Tatsuta (National Institute of Informatics) Title: Type Inference for Bimorphic Recursion 15:00--15:40 Yukiyoshi Kameyama (University of Tsukuba) Title: Pseudo-Classical Modal Logic for Staged Computation 15:40--16:00 Tea Break 16:00--17:00 Stefano Berardi (Torino University) Title: A Game Semantic for various Subclassical Logics Abstracts: ---------------------------------------------------------------------- Daisuke Kimura (National Institute of Informatics) Title: A generalized modal lambda calculus Abstract: In this talk, we introduce a lambda calculus with modal types. The types of this system contain information of possible worlds explicitly. This information can be considered as a position which is an abstraction of time or place. The feature of our calculus is that we can change the property of modalities by changing information about the relationship between positions. The aim of our research is the following: (1) To clarify the computational meaning of necessity and possibility modal operators. (2) To give a uniform framework that can treat several calculi with modal types. ---------------------------------------------------------------------- Kazuyuki Asada (National Institute of Informatics) Title: Semantics of Multi-rooted Graph with Ordered Branch Abstract: Buneman et al. introduced a graph transformation language UnCAL, where graph has bisimilarity semantics. There structural recursion plays an important role, and in order to define it, they introduced multi-rooted graph and its algebraic representation. In this talk we give coalgebraic semantics for multi-rooted graph, and see that such final coalgebras has some call-by-value structure. Then we introduce a CBV equational theory. Next we modify the results of graph with un-ordered branch to that with ordered branch, which is important for application to XML. For this ordered graphs, bisimilarity is defined in some subtle way, but we can use the ordered version of above CBV equational theory for reasoning of the bisimilarity between ordered graphs. ---------------------------------------------------------------------- Makoto Tatsuta (National Institute of Informatics) Title: Type Inference for Bimorphic Recursion Abstract: This talk proposes bimorphic recursion, which is restricted polymorphic recursion such that every recursive call in the body of a function definition has the same type. Bimorphic recursion allows us to assign two different types to a recursively defined function: one is for its recursive calls and the other is for its calls outside its definition. Bimorphic recursion in this talk can be nested. This talk shows bimorphic recursion has principal types and decidable type inference. Hence bimorphic recursion gives us flexible typing for recursion with decidable type inference. This talk also shows that its typability becomes undecidable because of nesting of recursions when one removes the instantiation property from the bimorphic recursion. This is a joint work with Ferruccio Damiani. ---------------------------------------------------------------------- Yukiyoshi Kameyama (University of Tsukuba) Title: Pseudo-Classical Modal Logic for Staged Computation Abstract: In this talk, we study a pseudo-classical modal logic, which corresponds to the staged calculus with control operators introduced by our earlier work. Staged computation is a means for run-time code generation, and has been proved useful in improving efficiency and maintainability of software. We are interested in the use of control operators in staged computation, since they play an essential role to avoid the code duplication problem. Combining a staged calculus with control operators in a naive way results in an unsound calculus, and we need a restriction on the typing rule for lambda. We show that this restriction has a logical counterpart similar to Nakano's catch/throw calculus. ---------------------------------------------------------------------- Stefano Berardi (Torino University) Title: A Game Semantic for various Subclassical Logics Abstract: In this talk we describe the state of the art of game semantics for Logic and lambda-calculus, and the motivations for having a game semantics. Then we define a game semantic for Intuitionism extending both Coquands and Hyland-Ongs game semantics. The semantics refines a paper of TLCA 2007. We have two kind of results: (1) (Soundness and Completeness) The recursive winning strategy of our game semantics are isomorphic to the cut-free proofs of some variant of HA-omega (Infinitary Intuitionistic Arithmetic) (2) (Cut Elimination) Any debate between two terminating strategies terminates. This is an ongoing joint work with M. Tatsuta. ---------------------------------------------------------------------- 連絡先龍田真 (国立情報学研究所)

1 0

PPL2012 参加募集＆カテゴリ3発表募集
by Koji Nakazawa 01 Feb '12

01 Feb '12

logic-mlのみなさま，（重複の場合はご容赦ください．）京都大学の中澤です． 3月に和歌山県白浜温泉で開催される　第14回プログラミングおよびプログラミング言語ワークショップ (PPL2012) につきまして，参加登録を開始いたしましたのでお知らせします．参加登録要領 http://ppl2012.cs.uec.ac.jp/registration.html をご参照の上，日本旅行の専用ページからご登録ください．また，カテゴリ3（ポスター・デモ発表）の発表申込締切は　カテゴリ3 発表申込締切：2月6日(月) ですのであわせてお知らせいたします．必要事項をテキスト形式にて投稿用メールアドレス　ppl2012-submit(a)kuis.kyoto-u.ac.jp までお申込ください．皆様のご参加，ご発表をお待ちしております．最新情報は引き続き下記webページにてお知らせします． -------------------------------------------------------------------------- 第14回プログラミングおよびプログラミング言語ワークショップ（PPL2012） http://ppl2012.cs.uec.ac.jp/ 論文募集主催: 日本ソフトウェア科学会プログラミング論研究会日程: 2012年3月8日(木)〜3月10日(土) 会場: 和歌山県西牟婁郡白浜温泉むさし http://www.yado-musashi.co.jp/ PPL2012は，プログラミングおよびプログラミング言語に関する研究者が一堂に会し，最新の研究成果の発表，および新たな研究課題についての討論やアイディア交換等を行うことを目的とした，合宿形式のワークショップです．プログラミングおよびプログラミング言語の理論・設計・実装・処理系などに関する研究発表を，カテゴリ別に幅広く募集します．カテゴリ１: 国内外で未発表の論文の発表カテゴリ２: 国際会議・学術雑誌等で既発表であるが，国内では未発表の研究の紹介カテゴリ３: ポスター・デモ発表（既発表・未発表の別を問いません） ※ショートプレゼンテーションは行いませんカテゴリ１の採択論文の中から，特に独創的なアイディアや顕著な成果を含むものに対して論文賞を授与する予定です．また，ポスター・デモを含む全発表のなかから，聴衆の投票により，最も優秀なプレゼンテーションに発表賞（一般の部，学生の部）を授与する予定です．カテゴリ１（国内外未発表論文） ------------------------------ （投稿受付は終了しました）カテゴリ２（国外既発表論文） ---------------------------- （投稿受付は終了しました）カテゴリ３（ポスター・デモ発表） ------------------------------------------ ２時間程度のセッション内でのポスター発表またはデモ発表です．既発表・未発表の別を問いません．PPLへの関連をもとに採録を判定いたします．また，申込多数の場合は抽選によって採否を決定する可能性があります．なお，PPL2012 ではポスターやデモによる活発な意見交換を促進したいという観点から，ショートプレゼンテーションのセッションは設けません．招待講演 -------- 長谷川真人（京都大学）タイトル（予定）「プログラム意味論・テンソル圏・量子トポロジー - 意味論の「量子化」は可能か？」細谷晴夫（理化学研究所脳科学総合研究センター・科学技術振興機構さきがけ）タイトル（予定）「大脳皮質の計算論」以上のお二方の招待講演を予定しています． ====================================================================== 投稿・発表申込要領３つのカテゴリそれぞれに対して，投稿は以下のように行って下さい．最新の情報は上記Webページでご確認下さい．カテゴリ１（国内外未発表論文） ------------------------------ （投稿受付は終了しました）カテゴリ２（国外既発表論文） ---------------------------- （投稿受付は終了しました）カテゴリ３（ポスター・デモ発表） ------------------------------------------ ポスター・デモの区別を行なわずに募集いたします．デモを行なう場合は，発表概要においてその旨をご説明ください．発表申込先：ppl2012-submit(a)kuis.kyoto-u.ac.jp 発表申込締切：2012年2月6日(月) 著者名，所属，発表タイトル，発表概要（200〜300字程度），希望する発表形態（ポスター・デモの別），をテキスト形式で上記申込先宛にお送り下さい．採否通知：2012年2月13日(月) ワークショップ全般に関する問い合わせ先：ppl2012-oc(a)kuis.kyoto-u.ac.jp ====================================================================== プログラム委員会青戸等人 (東北大学) 稲葉一浩 (Google) 上野雄大 (東北大学) 小笠原啓 (ITプランニング) 角谷良彦 (東京大学) Jacques Garrigue (名古屋大学) 小宮常康 (電気通信大学) 立堀道昭 (IBM東京基礎研究所) 千代英一郎 (日立製作所) 中澤巧爾 (京都大学) 中田秀基 (産業技術総合研究所) 西村進 (京都大学) 長谷部浩二 (筑波大学) 浜名誠 (群馬大学) 前田敦司 (筑波大学) 八杉昌宏 (京都大学) 横山大作 (東京大学) 渡部卓雄 (東京工業大学) 実行委員会鵜川始陽 (電気通信大学) [実行委員長] 中澤巧爾 (京都大学) [プログラム共同委員長] 前田敦司 (筑波大学) [プログラム共同委員長] --------------------------------------------------------------------------

1 0

MSFP 2012 call for participation
by Ichiro Hasuo 31 Jan '12

31 Jan '12

みなさま， ETAPS 2012 附設ワークショップ MATHEMATICALLY STRUCTURED FUNCTIONAL PROGRAMMING のご案内です．ワークショップですが，歴史を持つトピックだけあり，選りすぐりでかっちりした論文が揃っています．せっかくタリンにおいでならば，ぜひご出席ください！蓮尾一郎（東大情報理工） https://www-mmm.is.s.u-tokyo.ac.jp/~ichiro/ ---------- Forwarded message ---------- From: Paul Levy <P.B.Levy(a)cs.bham.ac.uk> Date: Thu, Jan 26, 2012 at 11:38 PM Subject: categories: MSFP 2012 call for participation To: categories list <categories(a)mta.ca> Please note the deadline for early registration, including discounted hotel bookings: *Sunday 29 January* =========================== Fourth Workshop on MATHEMATICALLY STRUCTURED FUNCTIONAL PROGRAMMING 25 March, Tallinn, Estonia A satellite workshop of ETAPS 2012 http://cs.ioc.ee/msfp/msfp2012/ The fourth workshop on Mathematically Structured Functional Programming is devoted to the derivation of functionality from structure. It is a celebration of the direct impact of Theoretical Computer Science on programs as we write them today. Modern programming languages, and in particular functional languages, support the direct expression of mathematical structures, equipping programmers with tools of remarkable power and abstraction. Where would Haskell be without monads? Functional reactive programming without arrows? Call-by-push-value without adjunctions? Type theory without universes? The list goes on. This workshop is a forum for researchers who seek to reflect mathematical phenomena in data and control. The first MSFP workshop was held in Kuressaare, Estonia, in July 2006, affiliated with MPC 2006 and AMAST 2006. The second MSFP workshop was held in Reykjavik, Iceland as part of ICALP 2008. The third MSFP workshop was held in Baltimore, USA, as part of ICFP 2010. Invited Talks: ================= Dependently typed continuation monads as models in Logic Danko Ilik, Goce Delčev University of Štip, Republic of Macedonia Fibred Data Types Neil Ghani, University of Strathclyde, UK Accepted Papers ================== • A Formal Comparison of Approaches to Datatype-Generic Programming José Pedro Magalhães and Andres Löh • An Investigation of the Laws of Traversals Mauro Jaskelioff and Ondrej Rypacek • Evaluation strategies for monadic computations Tomas Petricek • From Mathematics to Abstract Machine: A formal derivation of an executable Krivine machine Wouter Swierstra • Irrelevance, Heterogenous Equality, and Call-by-value Dependent Type Systems Vilhelm Sjöberg, Chris Casinghino, Ki Yung Ahn, Nathan Collins, Harley D. Eades III, Peng Fu, Garrin Kimmell, Tim Sheard, Aaron Stump and Stephanie Weirich • Parametric Compositional Data Types Tom Hvitved and Patrick Bahr • Step-Indexed Normalization for a Language with General Recursion Chris Casinghino, Vilhelm Sjöberg and Stephanie Weirich • Tracing monadic computations and representing effects Maciej Piróg and Jeremy Gibbons ETAPS: ====== European Joint Conferences on Theory and Practice of Software (ETAPS) is the primary European forum for academic and industrial researchers working on topics relating to software science. ETAPS, established in 1998, is a confederation of six main annual conferences (one of them, POST, being new in 2012), accompanied by satellite workshops. ETAPS 2012 is the fifteenth event in the series. http://www.etaps.org/2012 Host City: ========== Tallinn, a city of 412,000 people, is the capital and largest city of Estonia, a small EU member country in Northern Europe, bordering Russia to the East and Latvia to the south. Located in the north of the country, on the southern shores of the Gulf of Finland, opposite Helsinki in Finland, Tallinn is most well known for its picturesque medieval Old Town, a UNESCO World Heritage site. But it also has a vivid cultural scene, outperforming most European centres of similar size. In 2011, Tallinn, along with Turku in Finland, is the Cultural Capital of Europe. Tallinn is easy to travel to. Estonia is part of Schengen and the Eurozone. The Lennart Meri International Airport of Tallinn /TLL) is only 4km from the city centre. Programme Committee: ==================== * James Chapman (co-chair), Institute of Cybernetics, Tallinn, Estonia * Paul Blain Levy (co-chair), University of Birmingham, UK * Thorsten Altenkirch, University of Nottingham, UK * Robert Atkey, University of Strathclyde, Glasgow, UK * Nils Anders Danielsson, Chalmers University and University of Gothenburg, Sweden * Martin Escardo, University of Birmingham, UK * Ichiro Hasuo, University of Tokyo, Japan * Ralf Hinze, University of Oxford, UK * Neelakantan Krishnaswami, Microsoft Research, Cambridge, UK * Daniel R. Licata, Carnegie Mellon University, Pittsburgh, PA * Ulrich Schoepp, LMU Munich, Germany * Alex Simpson, University of Edinburgh, UK * Matthieu Sozeau, INRIA, Paris, France * Sam Staton, University of Cambridge, UK Further Information: ==================== For more information about the workshop, go to: http://cs.ioc.ee/msfp/msfp2012/ With any other questions please do not hesitate to contact the co-chairs at msfp2012(a)easychair.org.

1 0

Philosophy, Mathematics, Linguistics: Aspects of Interaction 2012
by BEKKI Daisuke 30 Jan '12

30 Jan '12

------------------------------------------------------------------ The International Interdisciplinary Conference Philosophy, Mathematics, Linguistics: Aspects of Interaction 2012 (PhML 2012) St. Petersburg, Russia, May 22-25, 2012 http://www.pdmi.ras.ru/EIMI/2012/PhML/index.htm ------------------------------------------------------------------ AIM and SCOPE ============= The PhML 2012 is a sequel in the series of conferences "Philosophy, Mathematics, Linguistics: Aspects of Interaction" intended to provide a forum for presentation of current researches, and to stimulate a dialogue between mathematicians, logicians, philosophers, linguists and computer scientists who share an interest in cross-disciplinary research. The conference will have plenary sessions to present the latest researches. In addition to plenary sessions, the conference will feature a panel discussion entitled "The Heritage of Kant and Contemporary Formal Logic". Apart from plenary sessions, there will also be parallel sessions of thematic sections to present contributed papers. The PhML 2012 will be held on May 22$BK(J5, 2012, at the Euler International Mathematical Institute (EIMI), which is a part of the St. Petersburg Department of Steklov Mathematical Institute (PDMI). PLENARY SPEAKERS ================ Theodora Achourioti (University of Amsterdam, the Netherlands) Michel De Glas (CNRS - University Paris$BK%(Jiderot, France) Dmitry Grigoriev (CNRS - University Lille 1, France) Gerhard Heinzmann (Archives Henri-Poincare (UMR 7117) University of Lorraine/CNRS, France) Jaakko Hintikka (Boston University, USA) Edward Karavaev (St. Petersburg State University, Russia) Michiel van Lambalgen (University of Amsterdam, the Netherlands) Yuri Manin (Max Planck Institute for Mathematics, Germany)- to be confirmed Grigori Mints (Stanford University, USA) Andrey Patkul (St. Petersburg State University, Russia) Jeff Pelletier (University of Alberta, Canada) Graham Priest (City University of New York, USA, University of Melbourne, Australia) Oleg Prosorov (PDMI, St. Petersburg, Russia) Andrei Rodin (University Paris$BK%(Jiderot, France) Gabriel Sandu (University of Helsinki, Finland) Anatol Slissenko (University Paris$BK&(Jst Cr$BqU(Jeil, LACL, France) CALL for PAPERS =============== The PhML 2012 invites to submit papers relating to the interplay between philosophy, mathematics and linguistics for presentation at thematic sections. Each presentation of a contributed paper will be allotted 25 min, including 5 min for discussion. Presentations should be given in English. Papers from any tradition and from a wide variety of perspectives are welcome, including but in no way limited to the following topics: - New trends in the foundations of mathematics today; - Ontology of mathematics and the nature of mathematical truth; - The problem of abstract entities in mathematics, philosophy and linguistics; - Formalization of Kant's logic and theory of judgments; - The mathematical concept of a function: from the notions of mapping, transformation towards the notion of an algorithm; - Complexity of finite objects: limited possibilities of man and computer; - Novel computational models and paradigms; - Philosophical and mathematical aspects of informatics; - Philosophical aspects of the use of natural language in mathematics; - Mathematical investigation of natural language structures; - Mathematical models in the study of language. PAPER SUBMISSION ================ Papers should be prepared in LaTeX or MS Word using style files of PhML format and be submitted electronically as pdf and source files via e-mail: PhML_2012(a)pdmi.ras.ru IMPORTANT DATES: ================ - Submission deadline for contributed papers: March 1st, 2012 - Notification of acceptance: March 15th, 2012 - Final date for camera-ready copy: April 22nd, 2012 - Conference: May 22-25, 2012 - Panel discussion: May 23, 2012 PROCEEDINGS =========== The proceedings of PhML 2012 will be published by PDMI in the local series with ISBN no. ORGANIZING / PROGRAM COMMITTEE ============================== Edward Karavaev (St. Petersburg State University, Russia), Elena Lisanyuk (St. Petersburg State University, Russia), Ivan Mikirtumov (St. Petersburg State University, Russia), Yuri Nechitajlov (St. Petersburg State University, Russia), Vladimir Orevkov (PDMI, St. Petersburg, Russia), co-chair, Oleg Prosorov (PDMI, St. Petersburg, Russia), co-chair, Anatol Slissenko (University Paris$BK&(Jst Cr$BqU(Jeil, LACL, France). PARTICIPATION ============= For registration and further practical information, see: http://www.pdmi.ras.ru/EIMI/2012/PhML/index.htm

1 0

Talk by Stefano Berardi at RIMS, Kyoto U. (2/2)
by Kazushige TERUI 29 Jan '12

29 Jan '12

みなさま今週木曜日に催されるセミナーのご案内をさせていただきます。どうぞお気軽にお越しください。照井 --- RIMS-CS website http://www.kurims.kyoto-u.ac.jp/~cs/ ===== Speaker: Stefano Berardi (University of Torino) Title: A Topology over a set of Knowledge States and a Fixed Point Problem Date: 11.00 -, February 2nd (Thu) Place: Room 478, "Research Bldg. No. 2 (Sougou Kenkyu 2-Goukan)" http://www.kyoto-u.ac.jp/en/access/campus/main.htm (Next to our CS Lab) 総合研究2号館 478号室 (CS室のとなりです) http://www.kyoto-u.ac.jp/ja/access/campus/map6r_y.htm Abstract: We give an abstract formulation of the termination problem for realizer of Heyting Arithmetic plus various subsystem of classical logic. This termination problem is expressed as the existence of a fixed point for a class of continuous maps in a suitable topology. ------------------------------------------ Kazushige TERUI Research Institute for Mathematical Sciences, Kyoto University. Kitashirakawa Oiwakecho, Sakyo-ku, Kyoto 606-8502, JAPAN. Phone: +81-75-753-7235 Fax: +81-75-753-7276 terui(a)kurims.kyoto-u.ac.jp http://www.kurims.kyoto-u.ac.jp/~terui/

1 0

ポスドクの募集案内(Postdoc position in Quantum Information)
by Harumichi Nishimura 29 Jan '12

29 Jan '12

logic-mlの皆様，量子情報のポスドク募集に関する代理投稿をさせていただきます．大阪府立大学理学系研究科西村治道 ------------------------------------------------------------------------------- 立命館の山下茂と申します． Masaryk University, Brno, Czech Republik での以下のポスドクの募集案内を日本国内の量子情報関連MLへの配布を依頼されましたので、MLへ通して下記の案内をさせてください。複数お受け取りになったらご容赦ください。 Postdoc position in Quantum Information at Faculty of Informatics, Masaryk University, Brno, Czech Republik A 2-year (with possible extension to 3 years) postdoctoral position in Quantum Information Processing Theory is opening in Faculty of Informatics, Masaryk University, starting with September 2012, in the group of prof. Jozef Gruska (http://www.fi.muni.cz/quantum). Possible research areas includes - but are not restricted to - models of quantum computations, quantum algorithms, quantum cryptography, quantum entanglement, quantum (pseudo-telepathic) games. The successful candidate will be member of the Quantum information processing and cryptography laboratory that has currently 8 members including two postdocs. The group has close and intensive contacts with quantum groups in Bratislava and Vienna, Faculty of Informatics has more than 2500 students (http://www.fi.muni.cz) and close contacts with Departments of mathematics and Physics of the Faculty of Natural sciences. Applicants must hold a PhD - or be about to obtain one - in informatics, physics or mathematics and should be able to demonstrate very good English and strong research track record. Once application is successful, position should be taken during the period August 15 - September 1, 2012. The following information should be provided in an application: * CV * PhD diploma * A proof of good English (outcomes of TOEFL, CAE or an equivalent test). * Statement of research interest * Lists of publications and presentations * Two representative publications * Two letters of recommendations Electronic publications are preferred. They should be sent via email to gruska(a)fi.muni.cz or via postal mail to Prof. Jozef Gruska Faculty of Informatics Masaryk University Botanicka 68a 60200 Brno, Czech Republic For the official web side of the whole postdocs programs and conditions see http://www.mu.cz/research/postdoctoral ` An applicant will receive 55000 Kc per month (what corresponds concerning exchange rate to about 2200 EUR (and with respect to the living costs to about 3000-3300 EUR in Western Europe). In addition, he/she will receive standard health care insurance for himself/herself) Reasonable traveling and office money are also available

1 0

Workshop on Proof Theory and Computability Theory 2012
by Naohi Eguchi 28 Jan '12

28 Jan '12

Logic-ml の皆様，下記の要領で証明論及び計算可能性理論に関するワークショップを開催いたします． =========================================================== Workshop on Proof Theory and Computability Theory 2012 - Philosophical Frontiers in Reverse Mathematics 日時：2012年2月20日〜23日場所：晴海グランドホテル　(東京都中央区) ワークショップホームページ： http://www.math.tohoku.ac.jp/~eguchi/Workshop2012/Workshop_on_Proof_Theory_… =========================================================== 参加・講演申し込み締め切り： 2月3日(金)　（会場準備のため，早めにお申し込みください．）参加費(宿泊する場合)：一般：32,000円，学生：25,000円　(三泊＋参加費) (21日朝昼食，21日懇親会，22日朝昼夕食，23日朝食が含まれます． 20日の夕食は含まれません．) 宿泊短縮については，個別に相談に応じます．部屋はツインもしくはトリプルの相部屋になります．シングルはかなり高額になりますが，ご希望の方はご相談ください．参加費(宿泊しない場合)：一般：2,000円，学生：1,000円　(全日程で) (お茶代・資料印刷代等に利用させていただきます．食事は含まれません．) 懇親会(21日夜，晴海グランドホテル)：一般：5,000円，学生：3,000円程度参加をご希望の方は本文末のフォームにご記入いただき下記宛てにご返送ください．（★　講演しない場合にも，事前申し込みが必要です．）江口直日: eguchi(a)math.tohoku.ac.jp 皆様のご参加をお待ちいたしております． Kazuyuki Tanaka, Andreas Weiermann, Toshiyasu Arai, Naohi Eguchi, Hajime Ishihara, Sam Sanders, and Takeshi Yamazaki. ------------------- ここから ------------------------------------ 氏名(日本語)：氏名(英語)：所属(日本語)：所属(英語)：身分：　学生・一般　(どちらかをお選びください)　参加日程：宿泊：　有・無　(どちらかをお選びください) 2月21日(火)の懇親会：　参加・不参加　(どちらかをお選びください) 講演：　有・無　(どちらかをお選びください) 講演題目(英語)：講演要旨(英語)： (ごく標準的な Latex コマンド，Latex 環境はご使用いただけます) ------------------- ここまで ------------------------------------

1 0

計算機言語談話会（＠産総研尼崎）開催【2012/2/1】のお知らせ
by Takashi KITAMURA 25 Jan '12

25 Jan '12

皆様、こんにちは！産総研の北村崇師です。下記の通り、産総研組み込みシステム技術連携体（＠尼崎）は、計算機言語談話会（CLC:Computer Language Colloquium）を開催します。どなたでも無料で参加できます。皆様のご参加お待ちしております。また参加の際は、事前に北村（ t.kitamura(a)aist.go.jp ）までメールによるご連絡をお願いいたします。 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 日時：平成 24 年 2 月 1 日（水） 16：00--17: 30 場所：（独）産総研関西センター尼崎事業所 E 棟 2 階セミナー室 http://cfv.jp/cvs/access/index.html 演題：Automatic Specification-Based Program Testing 講演者：Prof. Shaoying Liu (Hosei University, Tokyo, Japan) 梗概： Automatic specification-based testing (ASBT) is a potentially effective and efficient technique for detecting errors in programs and attractive to industry due to its potential in saving time and cost. In this talk, after presenting the goals of the testing technique I will introduce a decompositional functional scenario-based testing technique, a specific ASBT, by explaining the strategy and criteria for test set generation, test oracle for test result analysis, and test process for tool support. I will also discuss the challenges and future research directions. Bio.: Shaoying Liu is Professor at Hosei University, Japan. He received a Ph.D in Computer Science from the University of Manchester, U.K in 1992. His research interests include Formal Engineering Methods, Specification-based Inspection and Testing, and Intelligent Software Engineering Environments. He has published a book titled "Formal Engineering for Industrial Software Development" with Springer-Verlag, four edited conference proceedings, and over 120 academic papers in refereed journals and international conferences. He is the chair of Steering Committee for ICFEM conference, and on the editorial board for the Journal of Software Testing, Verification and Reliability (STVR) and for ISRN Software Engineering Journal. He is a Fellow of British Computer Society, Senior member of IEEE Computer Society, and member of Japan Society for Software Science and Technology. ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 以上よろしくお願いいたします。 -------------------------- 北村崇師 PhD <t.kitamura(a)aist.go.jp> 特別研究員（独）産業技術総合研究所組込みシステム技術連携研究体〒661-0974 兵庫県尼崎市若王寺3-11-46 Tel: 06-6494-8054 Fax: 06-6494-8073

1 0

JAIST Verification Seminars by Yijia Chen and Yohji Akama (Jan 31, Feb 9)
by Nao Hirokawa 24 Jan '12

24 Jan '12

みなさま 1月31日(火)と2月9日(木)にJAISTで行われます、計算量・組合せ理論についての２つセミナーをご案内致します。どうぞお気軽にお越しください。 http://www.jaist.ac.jp/is/labs/ogawa-lab/vs12.html 廣川 - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - Seminars of Research Center for Software Verification, JAIST - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - == Seminar I == Date: 31st Jan (Tue) 13:00-17:00 (closing time is flexible) Place: JAIST IS school collaboration room 7 (5F) 1. Prof.Yijia Chen (Shanghai Jiao Tong University) "Parameterized complexity of SAT" Many natural computational problems are NP-hard, hence they have no polynomial time algorithms assuming NP \ne P. The traditional approaches for coping with such problems are heuristic and approximation algorithms. Nevertheless, the heuristic algorithms often lack a rigorous analysis, while the approximation algorithms cannot guarantee exact solutions. Parameterized algorithms offer another approach which achieves both criteria. The key observation is that many natural problem instances come with some parameters which can be expected to be small, e.g., the size of a vertex cover, the length of a database query, and the tree width of a graph. If an exponential time algorithm has its superpolynomial behavior restricted by the parameters, it might well be efficient in practice. As an example, there is an algorithm for SAT which is exponential in the tree width tw(\alpha) of a given instance \alpha and at the same time linear in the size of \alpha. Therefore, if there is a constant upper bound on tw(\alpha), we can solve the corresponding SAT in linear time. In this talk I will survey some major tools for designing parameterized algorithms, including bounded search tree, kernelization, tree width method, and algorithmic meta-theorems, etc, with a focus on applications to SAT. In passing, I will also discuss some corresponding lower bound results. 2. Dr. Yohji Akama (Tohoku University) "A new order theory of set systems, WQO and BQO" A set system over a set $T$, a subfamily of the power set $P(T)$, is a topic of (extremal) combinatorics, as well as a target of an algorithm to learn in computational learning theory of languages. A well quasi-ordering (WQO for short) is introduced by Higman and employed in algebra, combinatorics, formal language theory, and so on. A better quasi-ordering (BQO for short) is introduced by Nash-Williams and employed in infinitary combinatorics and verification of infinite-state systems. We generalize WQOs and BQOs by using set systems, define the order type of a set system from game-theoretic viewpoint and study nondeterministic, combinatorial operations on set systems, such as monotone (continuous) image and unbounded unions of set systems. The motivating examples are the union of two colored arithmetical progressions, and the discolorization, and new useful examples are shuffle-product and shuffle-closure from formal language theory Furthermore, we provide a neat correspondence : quasi-orderings vs finitely branching simulations, and set systems vs linear, monotone, continuous functions. Next, we introduce a set system that has order type and corresponds to a BQO. We prove that the class of set systems corresponding to BQOs is closed by any monotone function. In (Shinohara and Arimura. ``Inductive inference of unbounded unions of pattern languages from positive data.'', Theoretical Computer Science, pp.191-209, 2000), for any set system $L$, they considered the class of arbitrary (finite) unions of members of $L$. From viewpoint of WQOs and BQOs, we characterize the set systems $L$ such that the class of arbitrary (finite) unions of members of $L$ has order type. == Seminar II == Date: 9th Feb (Thu) 13:00-15:00 (closing time is flexible) Place: JAIST IS school collaboration room 7 (5F) * Prof.Yijia Chen (Shanghai Jiao Tong University) "A Logic for PTIME and a Parameterized Halting Problem" 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

Talk by Thomas Agotnes (1/23)
by Koji Hasebe 19 Jan '12

19 Jan '12

皆様、 1月23日（月）に開催されるセミナーのご案内をさせて頂きます。どうぞお気軽にお越し下さい。長谷部浩二＠筑波大学 --------------------------------------------- Date：14:00-15:00, Jan 23, 2012 Place: Room SB-911-1 (Laboratory of Advanced Research-B, 9th floor), Tsukuba-campus, University of Tsukuba http://www.tsukuba.ac.jp/english/access/tsukuba_access.html http://www.tsukuba.ac.jp/english/access/map_central.html （筑波大学筑波キャンパス，総合研究棟B，9階，911-1号室） http://www.tsukuba.ac.jp/access/tsukuba_access.html http://www.tsukuba.ac.jp/access/map_central.html Speaker: Thomas Ågotnes, Department of Information Science and Media Studies, University of Bergen Title: Group Announcement Logic Abstract: Public announcement logic is used to reason about the epistemic pre- and post-conditions of actions in the form of public announcements. In the talk I will present Group Announcement Logic (GAL), an extension of public announcement logic with constructs (well known from coalition logic) of the form <G>phi, where G is a group of agents. In GAL, the meaning of <G>phi is that there exists an announcement that the members of G can jointly and truthfully make, and after that announcement is made public phi will be true. After introducing GAL I will discuss how it can be used to express properties such as "there is a sequence of truthful public announcements by agents in G, after which phi is true"; the distinction between "agent i knows *that* phi can be achieved by a public announcement" and "agent i knows *how* phi can be achieved by a public announcement"; and meta-logical properties such as axiomatization, expressivity and the complexity of the model checking problem. The talk is based on joint work with Philippe Balbiani, Hans van Ditmarsch and Pablo Seban. ---------------------------------------------

1 1

Asian Workshop on Philosophical Logic (the 1st announcement)
by Hiroakira Ono 17 Jan '12

17 Jan '12

Asian Workshop on Philosophical Logic http://www.jaist.ac.jp/rcis/awpl/ "Asian Workshop on Philosophical Logic" will be organized by Research Center for Integrated Science (RCIS), Japan Advanced Institute of Science and Technology (JAIST) and held at the Ishikawa Hightech Ceter near JAIST from 15th to 17th February, 2012. Originally, the Workshop was planned to be held in March of the last year. Our aim is to promote mutual understandings among researchers on logic working in Asian countries, and to establish closer collaborations in future. The scope of the Workshop will cover: philosophical logic, non-classical logics, algebraic logic, and their applications in computer science and cognitive science The following is a preliminary list of speakers: Phan Minh Dung (Asian Institute of Technology, Bangkok) Shier Ju (Sun Yat-sen University, Guangzhou) Xin Li (JAIST, Ishikawa) Fenrong Liu (Tsinghua University, Beijing) Hu Liu (Sun Yat-sen University, Guangzhou) Yutaka Miyazaki (Osaka University of Economics and Law, Osaka) Katsuhiko Sano (JAIST, Ishikawa) Takahiro Seki (Niigata University, Niigata) Kaile Su (Griffith University, Queensland) Wen-fang Wang (National Yang Ming University, Taipei) Chin-mu Yang (National Taiwan University, Taipei) Xishun Zhao (Sun Yat-sen University, Guangzhou) During the Workshop, we will have a special session of discussions on future collaborations, in particular on research, education and exchange of researchers in our region. The workshop will start from the morning of 15th February and will end in the afternoon of 17th. We welcome your participation in both talks and discussions from all areas and all levels, but ask to inform us if possible in advance of your participation. =============== Organizing Committee Hiroakira Ono ono(a)jaist.ac.jp Norbert Preining preining(a)jaist.ac.jp Research Center for Integrated Science Japan Advanced Institute of Science and Technology Nomi, Ishikawa, 923-1292 Japan ===============

1 0

PPL2012 発表募集（カテゴリ2, ３締切が間近です）
by Koji Nakazawa 16 Jan '12

16 Jan '12

（重複の場合はご容赦ください．）京都大学の中澤です． 3月に和歌山県白浜温泉で開催される　第14回プログラミングおよびプログラミング言語ワークショップ (PPL2012) につきまして，カテゴリ2（国外既発表論文），カテゴリ3（ポスター・デモ発表）の発表申込締切が近づいて参りましたのでお知らせします．  締切は，　カテゴリ2 発表申込締切：1月23日(月) 　カテゴリ3 発表申込締切：2月6日(月) です．いずれも，必要事項をテキスト形式にて投稿用メールアドレス　ppl2012-submit(a)kuis.kyoto-u.ac.jp までお申込ください．皆様のお申込をお待ちしております．なお，参加登録ページにつきましては現在準備中ですので今しばらくお待ちください．最新情報は引き続き下記webページにてお知らせします． -------------------------------------------------------------------------- 第14回プログラミングおよびプログラミング言語ワークショップ（PPL2012） http://ppl2012.cs.uec.ac.jp/ 論文募集主催: 日本ソフトウェア科学会プログラミング論研究会日程: 2012年3月8日(木)～3月10日(土) 会場: 和歌山県西牟婁郡白浜温泉むさし http://www.yado-musashi.co.jp/ PPL2012は，プログラミングおよびプログラミング言語に関する研究者が一堂に会し，最新の研究成果の発表，および新たな研究課題についての討論やアイディア交換等を行うことを目的とした，合宿形式のワークショップです．プログラミングおよびプログラミング言語の理論・設計・実装・処理系などに関する研究発表を，カテゴリ別に幅広く募集します．カテゴリ１: 国内外で未発表の論文の発表カテゴリ２: 国際会議・学術雑誌等で既発表であるが，国内では未発表の研究の紹介カテゴリ３: ポスター・デモ発表（既発表・未発表の別を問いません） ※ショートプレゼンテーションは行いませんカテゴリ１の採択論文の中から，特に独創的なアイディアや顕著な成果を含むものに対して論文賞を授与する予定です．また，ポスター・デモを含む全発表のなかから，聴衆の投票により，最も優秀なプレゼンテーションに発表賞（一般の部，学生の部）を授与する予定です．カテゴリ１（国内外未発表論文） ------------------------------ 完成した理論やシステムの研究発表のみならず，萌芽的なアイディアや問題点の提示等も歓迎します．発展途上の研究内容も積極的に採録する方針です（ただし，PPLでの発表として相応しくないと判断される場合は，この限りではありません）．また，カテゴリ1で発表された研究については，会場での討議や査読コメントをもとにその完成度を高め，将来の学術雑誌・会議等での業績に結び付けることを奨励しています．そのため，予稿集の配布は参加者のみへの限定的なものとする予定です．採録された論文は，PPL2012参加者に配布される予稿集に掲載され，参加者のみがアクセス可能な形でWEB上で公開されます（論文へのリンク集ページを作成し，閲覧に必要なパスワードを参加者に連絡します）．カテゴリ１で発表された研究のうち，PPL2012プログラム委員会として優れていると認めるものは，PPL2012終了後（2012年4月下旬予定），「コンピュータソフトウェア」誌PPL2012推薦論文としての投稿が可能です．推薦論文は，PPL プログラム委員が引き続き査読を行うことによる，迅速な査読プロセスを特長としています．カテゴリ２（国外既発表論文） ---------------------------- 査読付の国際会議または学術雑誌等で既発表であるが，国内では未発表な研究の紹介をする場です．採録決定済みの研究も含みます．PPLへの関連をもとに採録を判定いたします．カテゴリ３（ポスター・デモ発表） ------------------------------------------ ２時間程度のセッション内でのポスター発表またはデモ発表です．既発表・未発表の別を問いません．PPLへの関連をもとに採録を判定いたします．また，申込多数の場合は抽選によって採否を決定する可能性があります．なお，PPL2012 ではポスターやデモによる活発な意見交換を促進したいという観点から，ショートプレゼンテーションのセッションは設けません．招待講演 -------- 長谷川真人（京都大学）タイトル（予定）「プログラム意味論・テンソル圏・量子トポロジー - 意味論の「量子化」は可能か？」細谷晴夫（理化学研究所脳科学総合研究センター・科学技術振興機構さきがけ）タイトル（予定）「大脳皮質の計算論」以上のお二方の招待講演を予定しています． ====================================================================== 投稿・発表申込要領３つのカテゴリそれぞれに対して，投稿は以下のように行って下さい．最新の情報は上記Webページでご確認下さい．カテゴリ１（国内外未発表論文） ------------------------------ （投稿受付は終了しました）カテゴリ２（国外既発表論文） ---------------------------- 昨年同様，カテゴリ2の申込締切が少し早くなっていますのでご注意ください．締切直後（2月初旬頃）に採否が決定する国際会議については，あらかじめ，下記問い合わせ先までご相談ください． (注) 申込時はabstractをテキスト形式でお送りください．最終原稿は，下記のスタイルファイルを利用したpdfにてお送りください．発表申込先：ppl2012-submit(a)kuis.kyoto-u.ac.jp 発表申込締切：2012年1月23日(月) 原論文（ページ数不問，PostScriptもしくはPDF形式）とabstract（テキスト形式）を，著者名，所属，論文タイトル，原論文の出典（発表会議名，掲載済／予定の別等）と併せて上記申込先宛にお送り下さい．採否通知：2012年1月31日(火) 最終原稿提出締切：2012年2月13日(月) カテゴリ３（ポスター・デモ発表） ------------------------------------------ ポスター・デモの区別を行なわずに募集いたします．デモを行なう場合は，発表概要においてその旨をご説明ください．発表申込先：ppl2012-submit(a)kuis.kyoto-u.ac.jp 発表申込締切：2012年2月6日(月) 著者名，所属，発表タイトル，発表概要（200～300字程度），希望する発表形態（ポスター・デモの別），をテキスト形式で上記申込先宛にお送り下さい．採否通知：2012年2月13日(月) ワークショップ全般に関する問い合わせ先：ppl2012-oc(a)kuis.kyoto-u.ac.jp ====================================================================== プログラム委員会青戸等人 (東北大学) 稲葉一浩 (Google) 上野雄大 (東北大学) 小笠原啓 (ITプランニング) 角谷良彦 (東京大学) Jacques Garrigue (名古屋大学) 小宮常康 (電気通信大学) 立堀道昭 (IBM東京基礎研究所) 千代英一郎 (日立製作所) 中澤巧爾 (京都大学) 中田秀基 (産業技術総合研究所) 西村進 (京都大学) 長谷部浩二 (筑波大学) 浜名誠 (群馬大学) 前田敦司 (筑波大学) 八杉昌宏 (京都大学) 横山大作 (東京大学) 渡部卓雄 (東京工業大学) 実行委員会鵜川始陽 (電気通信大学) [実行委員長] 中澤巧爾 (京都大学) [プログラム共同委員長] 前田敦司 (筑波大学) [プログラム共同委員長] --------------------------------------------------------------------------

1 0

Re: [logic-ml] Kobe Colloquium on Logic, Statistics and Informatics Jan. 16, Jan. 18, and Jan. 19
by Joerg Brendle 13 Jan '12

13 Jan '12

Kobe Colloquium on Logic, Statistics and Informatics 以下の要領でセミナー（３つの発表）を開催します。日時：2012年1月16日（月）13:20-14:50 2012年1月18日（水）13:20-14:50 2012年1月19日（木）15:10-16:40 場所：神戸大学自然科学総合研究棟3号館4階421室（プレゼンテーション室）講演者：Frank Tall (University of Toronto, Canada) ======================================================================== 題目：Classic Lindelöf problems and selection principles (talk 1 and 2) 時間：16日（月）と18日（水）1:20-2:50 アブストラクト： There are many connections between classical topological problems concerning Lindelöf spaces and selection principles, such as (generalizations of) Rothberger, Menger, and Hurewicz properties. In the first talk, we will discuss these connections. In the second talk, we will pursue further some of the topics introduced in the first talk, but it is not necessary to have gone to the first talk in order to understand the second. ======================================================================== 題目：PFA(S)[S]: a useful model (talk 3) 時間：19日（木）3:10-4:40 アブストラクト： We introduce a model in which important consequences of PFA hold but also some combinatorics that follow from V=L. This talk is quite technical and assumes familiarity with proper forcing with elementary submodels as side conditions. ======================================================================== 交通：阪急六甲駅またはJR六甲道駅から神戸市バス36系統「鶴甲団地」行きに乗車，「神大本部工学部前」停留所下車，徒歩すぐ． http://www.kobe-u.ac.jp/info/access/rokko/rokkodai-dai2.htm 連絡先：ブレンドレヨーグ brendle(a)kurt.scitec.kobe-u.ac.jp

1 0

JAIST Spring School 2012 - Formal Reasoning: Theory and Application - (5-9 March, 2012)
by Katsuhiko Sano 12 Jan '12

12 Jan '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日(金) と致します。また、本スプリングスクールの最終日に数理論理学の諸科学への発展と展開平成24年3月9日石川県立美術館広坂別館主催：文部科学省・北陸先端科学技術大学院大学情報科学研究科後援：日本数学会・日本応用数理学会・統計関連学会連合・科学技術振興機構 http://www.jaist.ac.jp/~hirokawa/ml12.html chair 石原哉 (JAIST) を開催いたします。招待講演者等、詳細が決まり次第、再度アナウンスをお送りいたしますが、こちらのワークショップにはどなた様もご参加いただけます。 ************************************************************ *** JAIST Spring School 2012 Application Form *** *** 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

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Logic-ml