- 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 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

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 31 Jan '12

31 Jan '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 31 Jan '12

31 Jan '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 29 Jan '12

29 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 28 Jan '12

28 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 27 Jan '12

27 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 18 Jan '12

18 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 11 Jan '12

11 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

Talk by Jean-Yves Girard at RIMS, Kyoto U. (1/12)
by Kazushige TERUI 09 Jan '12

09 Jan '12

みなさま今週木曜日に催されるセミナーのご案内をさせていただきます。どうぞお気軽にお越しください。照井 --- RIMS-CS website http://www.kurims.kyoto-u.ac.jp/~cs/ ===== Speaker: Jean-Yves Girard (IML Marseille & RIMS Kyoto) Title: A SECOND LOOK AT PROOF-NETS Date: 11.00 -, January 12th (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: In logic, we have a reasonable answer to the question : "What is a typable object?" but none so far to the question : "What is a typed object?" By a second look at proof-nets, especially the ones involving quantifiers, we shall propose an answer to the second question. ------------------------------------------ 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

情報処理学会第88回プログラミング研究発表会(2012/03) 発表募集 (再送)
by Keisuke Nakano 06 Jan '12

06 Jan '12

＊＊＊＊複数受け取られた方はご容赦ください＊＊＊＊電気通信大学の中野と申します． 3月に産業技術総合研究所つくばセンターにて開催予定の，情報処理学会第88回プログラミング研究会の発表申込締切（ 1月13日(金) ）が迫ってまいりました．発表募集のご案内を再送いたしますので，投稿・発表についてどうぞご検討ください．申込時点で必要なのはタイトルと概要などです． http://www.ipsj.or.jp/sig/pro/trans-author.html -- 中野圭介 / Keisuke Nakano この場を借りて2011年度第5回情報処理学会プログラミング研究発表会の発表募集のご案内をさせて頂きたく存じます．プログラミング研究会(PRO)は，・プログラミング言語の設計，処理系の実装・プログラミングの理論，基本概念・プログラミング環境，支援システム・プログラミング方法論，パラダイム・これらを応用したシステムの開発事例・その他，プログラミングに関する面白い話題を対象とした研究発表の場で，1998年度から毎年3-4回のペースで論文誌を発行しています．PRO論文誌は研究会と密接にリンクしており，研究会で発表されたもののうちあらかじめ論文投稿を希望し，論文原稿を提出されているものが査読の対象となっています (論文誌投稿を希望しない発表も歓迎します)．おおむね研究会から3週間で論文の採否が決定されるという迅速さも大きな特徴です． 2012年3月の研究会も多くの発表ならびに論文投稿をお待ちしております．参加費は無料です．申込締切は1月13日(投稿締切は2月13日)ですので，よろしくご検討ください．なお，多数の発表申込みがある場合には，発表をお断りすることがございますので，お早めにお申し込みください．また，今回も和文として投稿された論文の英語化を支援する試みを実施します．和文原稿にて採録を判断し，(著者が希望する場合は) 採録決定後に英語化していただいてから掲載致します．この英語化に関する詳細については， http://millsmess.cs.uec.ac.jp/pro/2011-5/english-paper-encouragement.html をご覧ください．第88回プログラミング研究会(PRO-2011-5)発表募集日程: 2012年3月15日(木)・16日(金) 会場: 産業技術総合研究所つくば中央共用講堂中会議室〒305-8561　茨城県つくば市東1-1-1　中央第1 つくばエクスプレス線つくば駅からバス約20分 (交通ガイド: http://www.aist.go.jp/aist_j/guidemap/tsukuba/center/tsukuba_map_c.html) 発表申込締切: 2012年1月13日(金) 投稿論文原稿提出締切: 2012年2月13日(月) 申込先: 中野圭介(電通大) E-mail: ksk [at] cs.uec.ac.jp 案内ページ: http://millsmess.cs.uec.ac.jp/pro/2011-5/ ・申込みに当たっての注意はプログラミング研究会のページ http://www.ipsj.or.jp/sig/pro/ を参照してください．・できるだけE-mailでお願いします．・申込み後返信がない場合はご連絡下さい．

1 0

Prof. Kwangkeun Yi Lecture at NII Logic Seminar
by Makoto Tatsuta 04 Jan '12

04 Jan '12

Prof. Kwangkeun Yi Lecture at NII Logic Seminar Date: January 10, 2012, 15:00--17:00 Place: National Institute of Informatics, Lecture Room 1208 (12th floor) 場所: 国立情報学研究所 12階 1208室 (半蔵門線,都営地下鉄三田線・新宿線神保町駅または東西線竹橋駅より徒歩5分) (地図 http://www.nii.ac.jp/introduce/access1-j.shtml) Speaker: Prof. Kwangkeun Yi (Seoul National University) Title: Static Analysis of Multi-Staged Programs via Unstaging Translation Abstract: Static analysis of multi-staged programs is challenging because the basic assumption of conventional static analysis no longer holds: the program text itself is no longer a fixed static entity, but rather a dynamically constructed value. This article presents a semantic-preserving translation of multi-staged call-by-value programs into unstaged programs and a static analysis framework based on this translation. The translation is semantic-preserving in that every small-step reduction of a multi-staged program is simulated by the evaluation of its unstaged version. Thanks to this translation we can analyze multi-staged programs with existing static analysis techniques that have been developed for conventional unstaged programs: we first apply the unstaging translation, then we apply conventional static analysis to the unstaged version, and finally we cast the analysis results back in terms of the original staged program. Our translation handles staging constructs that have been evolved to be useful in practice (typified in Lisp's quasi-quotation): open code as values, unrestricted operations on references and intentional variable-capturing substitutions. This article omits references for which we refer the reader to our companion technical report. This is a joint work with Wontae Choi, Baris Aktemur, and Makoto Tatsuta. 問合せ先: 龍田真 (国立情報学研究所) e-mail: tatsuta(a)nii.ac.jp http://research.nii.ac.jp/~tatsuta

1 0

Nagoya set theory seminar
by 吉信康夫 21 Dec '11

21 Dec '11

(重複して受け取られた場合はご容赦ください) 名古屋集合論セミナーのご案内：日時：2012年1月11日(水) 午後2時15分～4時(途中15分休憩) 場所：名古屋大学大学院情報科学研究科棟 322号室 (名古屋市地下鉄名城線名古屋大学駅1番出口より徒歩数分、下記のキャンパスマップのA4にある建物です。) http://www.nagoya-u.ac.jp/global-info/access-map/higashiyama/ 講演者：Franklin D. Tall (トロント大学) 題目：A useful model of set theory アブストラクト: I will sketch a method for getting mutually consistent consequences of PFA and V = L. The talks are unavoidably technical, and assume acquaintance with the method of proper forcing with elementary submodels as side conditions. The hope is that although listeners are unlikely to be able to follow all the details presented, they will get enough of the ideas so that they can more easily study the research papers if they are interested. 多数のご参加をお待ちしております。名古屋大学大学院情報科学研究科吉信康夫

1 0

Fwd: [Proof Complexity] Postdoc position in proof complexity at KTH
by Satoru Kuroda 20 Dec '11

20 Dec '11

logic-ml の皆様，黒田＠群馬県立女子大学です． Proof complexity の ML にポスドク募集の案内が流れてきましたので，こちらに流します．すでにご覧になっている場合はご容赦ください． ---------- Forwarded message ---------- From: Jakob Nordstrom <jakobn(a)kth.se> Date: 2011/12/20 Subject: [Proof Complexity] Postdoc position in proof complexity at KTH To: proof-complexity(a)math.cas.cz Dear colleagues, This is just to ask for your help in advertising an open postdoc position in proof complexity at KTH Royal Institute of Technology. The formal deadline is January 31, but candidates are encouraged to apply already now. The intended start date is August-September 2012. I would be very grateful if you could help spread this information. For more details, see the enclosed PDF flyer, which is also available at http://www.csc.kth.se/~jakobn/openings/PostdocAug12Flyer.pdf . The full, formal announcement can be found at http://www.csc.kth.se/~jakobn/openings/D-2011-0603-Eng.php . As advertised before on this list, I am also looking for two PhD students, and here the formal announcement is http://www.csc.kth.se/~jakobn/openings/D-2011-0503-Eng.php . Informal enquiries about the postdoc or PhD positions are welcome. With best regards, Jakob Nordstrom Jakob Nordström, Assistant Professor KTH Royal Institute of Technology Osquars backe 2, SE-100 44 Stockholm, Sweden Phone: +46 8 790 69 19 (office), +46 70 742 21 98 (cell) http://www.csc.kth.se/~jakobn/ _______________________________________________ Proof-Complexity mailing list Proof-Complexity(a)math.cas.cz http://list.math.cas.cz/listinfo/proof-complexity -- Satoru Kuroda Gunma Prefectural Women's University

1 0

Fwd: categories: MSFP 2012 deadline extension
by Ichiro Hasuo 19 Dec '11

19 Dec '11

Dear colleagues, The deadline for MSFP 2012 has been extended by one week to FRIDAY 23 DECEMBER. See details below. Best regards, James Chapman and Paul Blain Levy MSFP 2012 co-chairs -- 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. Important Dates: ================ Submission of papers: 23 December 2011 Notification: 25 January 2012 Final versions due: 6 Feburary 2012 Workshop: 25 March 2012 Invited Speakers: ================= Danko Ilik, Goce Delčev University of Štip, Republic of Macedonia Neil Ghani, University of Strathclyde, UK Submission: =========== Papers must report previously unpublished work and not be submitted concurrently to another conference with refereed proceedings. Accepted papers must be presented at the workshop by one of the authors. There is no specific page limit, but authors should strive for brevity. Accepted regular papers will be published in the Electronic Proceedings in Theoretical Computer Science (EPTCS). After the workshop, there might be an opportunity to publish selected papers in a journal special issue. All submissions must be in PDF format and use the EPTCS style files. Submissions can be made through the EasyChair website, at http://www.easychair.org/conferences/?conf=msfp2012 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. [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

Logic, Algebra, and Truth Degrees 2012 - First Call
by latd12＠jaist.ac.jp 15 Dec '11

15 Dec '11

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

1 0

東北大学ロジックセミナーのご案内(12月26日)
by Naohi Eguchi 09 Dec '11

09 Dec '11

(本案内を重複してお受け取りの際はご容赦ください) Logic-ml の皆様，東北大学の江口と申します．下記の要領で東北大学ロジックセミナー(田中一之研究室)を開催いたします．興味のある方は参加をご検討ください．日時：12月26日(月)，16時から．場所：東北大学北青葉山キャンパス理学総合棟1201号室発表者：新井敏康 (千葉大学大学院理学研究科) タイトル：Searching witnesses of $\Sigma^{0}_{2}$-formulas in proofs アブストラクト： We can find a witness of a PA-provable $\Sigma^{0}_{2}$-formula as limits of an elementary recursive function, whose convergence is ensured by weakly descending chains of ordinals. 東北大学ロジックセミナーの詳細につきましては下記をご参照ください． https://sites.google.com/site/sendailogichomepage/ -- 江口直日東北大学大学院理学研究科数学専攻産学官連携研究員 980-8578 宮城県仙台市青葉区荒巻字青葉6ー3 E-mail: eguchi(a)math.tohoku.ac.jp

1 0

PPL2012論文募集
by Koji Nakazawa 07 Dec '11

07 Dec '11

（重複の場合はご容赦ください．）京都大学の中澤です．来年3月に和歌山県白浜温泉で開催される第14回プログラミングおよびプログラミング言語ワークショップ (PPL2012) のご案内（2回目）です．みなさまのご投稿，ご参加をお待ちしております．論文投稿・発表申込方法の詳細と招待講演者の情報を追加いたしました．カテゴリ1はeasy chairを通して，カテゴリ2, 3は下記投稿用メールアドレスまでお申込ください．最新情報は引き続き下記ワークショップ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ページでご確認下さい．カテゴリ１（国内外未発表論文） ------------------------------ 投稿手続きは二段階です．発表申込を行った上で論文提出を行って下さい． (注) 採録された論文等著作物は，日本ソフトウェア科学会著作権規定 (http://www.jssst.or.jp/files/user/edit/chosakuken-kitei.pdf) にもとづいて利用されますので，予めご確認ください． (注) カテゴリ１への投稿論文と類似の論文を，他の会議（予稿集を出版するもの）・論文誌などに同時投稿する場合は，査読の有無に関わらず，その旨を発表申込および論文提出の際に明記して下さい．PPLでは同時投稿の事実のみをもって論文を不採録とすることはありませんが，採否の決定に利用する場合があります（他の会議との重複を避けるため，発表内容についての条件付採録とすることもあります）．発表申込先：https://www.easychair.org/conferences/?conf=ppl2012 発表申込締切：2011年12月22日(木) 著者名，所属，論文タイトル，論文概要（日本語300〜400字程度もしくは英語200 words程度）を提出してください．上記webページのフォームに入力する日本語の文字コードはすべてUTF-8にしてください． (注) フォームにおいて，change informationをクリックすると文字化けが発生する場合がありますが，情報の登録は正しく行なわれますので問題ありません．論文提出締切：2012年1月6日(金) 10ページ程度（最大15ページ）の論文（英語もしくは日本語，PostScriptもしくはPDF形式）を提出して下さい．採否通知：2012年1月31日(火) 最終原稿提出締切：2012年2月13日(月) 採録された論文の最終原稿の提出方法は，採否通知にてお知らせいたします．カテゴリ２（国外既発表論文） ---------------------------- 昨年同様，カテゴリ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

Kobe Kolloquiun on Logic, Statistics and Informatics
by fuchino＠isc.chubu.ac.jp 05 Dec '11

05 Dec '11

We announce the following talk in Kobe Colloquium on Logic, Statistics and Informatics: ------------------------------------------------------------------------- Date and time: Dec. 12, 2011 (Mon.), 15:10 -- 16:40 Place: Presentation Room of "Fuchino Group" on the 4th Floor of Science and Technology Research Building 3 (Shizenkagakutou Sangokan) (see: http://www.kobe-u.ac.jp/en/access/rokko/campus.htm) Speaker: Professor Dr. Peter Vojtas (Department of Software Engineering of the Charles University in Prague) Title of the talk: Soundness and completeness of fuzzy Prolog/Datalog. ------------------------------------------------------------------------- Abstract: We start with using user preference search as a motivation for a many valued (fuzzy) model of Prolog/Datalog/Querying. We mention problems of classical approach with refutation and clausal rules. We base our semantics on implicative rules and many valued modus ponens. We prove soundness and completeness of our semantics. We discuss also clausal approach and fuzzy resolution. -- best regards Saka\'e Fuchino (渕野昌) ------------------------------------------------------------------------- Kobe University Graduate School of System Informatics Rokko-dai 1-1, Nada, Kobe 657-8501 e-mail: fuchino(a)diamond.kobe-u.ac.jp web page: http://kurt.scitec.kobe-u.ac.jp/~fuchino/ -------------------------------------------------------------------------

1 0

LATD2012
by Hiroakira Ono 02 Dec '11

02 Dec '11

Logic, Algebra and Truth Degrees 2012 http://www.jaist.ac.jp/rcis/latd12/ First Call for Papers The third official meeting of the EUSFLAT Working Group on Mathematical Fuzzy Logic [1] will be held on 10-14 September 2012 in Kanazawa, Japan. The conference is organized by Research Center for Integrated Science [2], Japan Advanced Institute of Science and Technology [3]. Mathematical Fuzzy Logic is a subdiscipline of Mathematical Logic which studies the notion of comparative truth. The assumption that 'truth comes in degrees' has proved to be very useful in many, both theoretical and applied, areas of Mathematics, Computer Science and Philosophy. The main goal of this meeting is to foster collaboration between researchers in the area of Mathematical Fuzzy Logic, and to promote communication and cooperation with members of neighbouring fields. The featured topics included, but are not limited to, the following: . Proof systems for fuzzy logics: Hilbert, Gentzen, natural deduction, tableaux, resolution, computational complexity, etc. . Algebraic semantics: residuated lattices, MTL-algebras, BL-algebras, MV-algebras, Abstract Algebraic Logic, functional representation, etc. . Game-theory: Giles games, Renyi-Ulam games, evaluation games, etc. . First-order fuzzy logics: axiomatizations, arithmetical hierarchy, model theory, etc. . Higher-order fuzzy logical systems: type theories, Fuzzy Class Theory, and formal fuzzy mathematics. . Philosophical issues: connections with vagueness and uncertainty. . Applied fuzzy logical calculi: foundations of logical programming, logic-based reasoning about similarity, description logics, etc. We also welcome contributions on any relevant aspects of related logical systems (such as substructural and quantum logics, and many-valued logics in general). Conference Web Site: http://www.jaist.ac.jp/rcis/latd12/ Important dates: . 22 April 2012: deadline for submissions . 3 June 2012: notifications sent . 10-14 September 2012: conference Programme Committee: . Stefano Aguzzoli (University of Milano, Italy) . Matthias Baaz (Vienna University of Technology, Austria) . Petr Cintula (Academy of Sciences, Czech Republic) . Carles Noguera (CSIS, Spain) . Hiroakira Ono (JAIST, Japan), Chair . James Raftery (University of KwaZulu-Natal, South Africa) . Constantine Tsinakis (Vanderbilt University, USA) Invited Speakers: . Rostislav Horcik (Academy of Sciences, Czech Republic) . Emil Jerabek (Academy of Sciences, Czech Republic) . Daniele Mundici (University of Florence, Italy) . Greg Restall (University of Melbourne, Australia) . Luca Spada (University of Salerno, Italy) Tutorial: . Felix Bou (CICS, Spain) If you are interested in presenting a paper, please submit a 2‚Äì4 pages abstract at http://www.easychair.org/conferences/?conf=latd2012 Your submission will be confirmed automatically on the e-mail address you provide. The accepted abstracts will be available on-line after the final decision of the program committee. If you have any problems to submit an abstract, please contact us at mail to: latd2012(a)jaist.ac.jp The deadline for contributions is 22 April 2012. The notification of acceptance/rejection will be sent until 3 June 2012. Conference dates: The scientific program will start Monday morning (10 September) and finish Friday noon (14 September). Wednesday afternoon we plan an excursion. Venue: The conference will be held in the city of Kanazawa [4,5,6], located in the Ishikawa prefecture of Japan on the Japan Sea. The venue is the Ishikawa Prefectural Museum of Art [7] in the center of Kanazawa. Local Organizing Committee: . Norbert Preining (JAIST, Japan), Chair . Katsuhiko Sano (JAIST, Japan) . Kazushige Terui (Kyoto University, Japan) . Shunsuke Yatabe (AIST, Japan) For further information please contact: latd2012(a)jaist.ac.jp [1] http://www.mathfuzzlog.org/ [2] http://www.jaist.ac.jp/rcis/en/ [3] http://www.jaist.ac.jp/ [4] http://en.wikipedia.org/wiki/Kanazawa,_Ishikawa [5] http://www.kanazawa-tourism.com/ [6] http://wikitravel.org/en/Kanazawa [7] http://www.ishibi.pref.ishikawa.jp/index_j.html

1 0

Kobe Colloquium on Logic, Statistics and Informatics: 1 Dec., 2011
by Hirotaka Kikyo 26 Nov '11

26 Nov '11

皆様桔梗宏孝＠神戸大学システム情報学研究科です． 2011年12月1日（木）の 17：00 から下記のように Lyon 1 大学の Amador Martin-Pizarro 氏によるモデル理論におけるMorleyの定理に関する神戸情報数理コロキウムの講演を予定しております．講演者の Amador Martin-Pizarro 氏には，モデル理論の専門の方だけでなくロジック全般の general audience 向けの講演になるよう，お願いしてあります．興味のある方は御参加ください．なお，この回の次の神戸コロキウムでは，2011年12月12日 15：10 から Professor Peter Vojtas (Charles Univ. (プラハ大学)) による many valued Prolog に関する講演を予定しております．これについては改めてご案内いたします． ---------------------------------------------------------------------------------- 神戸情報数理コロキウム日時：2011年12月1日（木）17:00 〜 18:30 場所：神戸大学自然科学総合研究棟3号館4階421室（渕野グループ内プレゼンテーション室）講演者： Amador Martin-Pizarro (リヨン１大学) 題目： Morley's theorem and Geometric Model Theory アブストラクト：A countable theory is uncountably categorical if it only has a unique model (up to isomorphism) on each uncountable cardinal. Morley proved that a theory is uncountably categorical if it is categorical on cardinality the continuum. His proof uses the fact that every model can be built from basic bricks, called strongly minimal sets (which generalise the concept of an absolutely irreducible algebraic curve). The goal of this talk is to give an overview (to a general audience) of some of the ideas of the proof based on examples. Moreover, we will link the classification of strongly minimal sets to results in other areas of mathematics, specially number theory, such as the existence of infinite Mersenne primes and Schanuel's conjecture. ------------------------------------------- 神戸大学自然科学総合研究棟3号館への行き方： http://kurt.scitec.kobe-u.ac.jp/~kikyo/seminar/scitec3.pdf

1 0

セミナー案内
by KASHIMA Ryo 25 Nov '11

25 Nov '11

数理論理学セミナーのご案内日時：10月27日(木)17時から場所：東京工業大学大岡山キャンパス西８号館Ｗ棟 10階 W1008セミナー室話者：堀畑佳宏（東北大）題目：弱い算術とconcatenationの理論概要：文字列の結合に関する理論（concatenationの理論） TC は、2005年に Grzegorczyk によって導入され、その決定不可能性が示された。一方、2009年にはVisser, Svejdar, Ganea がそれぞれ独立に、TC が Robinson 算術 Q と互いに翻訳可能であることを示した。本発表では、concatenation の理論 WTC を新たに導入し、この理論が Robinson と Tarski によって導入された非常に弱い算術 R と互いに翻訳可能となることを見る。 ---------- 会場までの交通案内はこちらから： http://www.titech.ac.jp/about/campus/index.html ----- 鹿島亮東京工業大学大学院情報理工学研究科数理・計算科学専攻 kashima(a)is.titech.ac.jp ＃＃＃木曜夕方を中心に不定期的にセミナーを開催しています。＃＃＃＃＃＃詳細はお問い合わせください。＃＃＃

1 1

Call for Participation: PEPM 2012
by Kohei SUENAGA 25 Nov '11

25 Nov '11

（重複して受け取られた場合はどうぞご容赦ください。）京都大学の末永と申します。来年1月に POPL 2012 と併設で開催される PEPM 2012 のご案内をお送りいたします。今回も日本からの４本の論文を含む見所満載のプログラムになっております。 Early registration は12月24日までとなっております。 POPL ともども皆様の参加をお待ち申し上げております。京都大学末永幸平 ksuenaga(a)sato.kuis.kyoto-u.ac.jp -- ACM SIGPLAN 2012 Workshop on Partial Evaluation and Program Manipulation http://www.program-transformation.org/PEPM12 January 23-24, 2012. Philadelphia, PA, USA (co-located with POPL'12) Call For Participation Online registration is open at https://regmaster3.com/2012conf/POPL12/register.php Early registration deadline is December 24, 2011 The PEPM Symposium/Workshop series brings together researchers and practitioners working in the broad area of program transformation, which spans from refactoring, partial evaluation, supercompilation, fusion and other metaprogramming to model-driven development, program analyses including termination, inductive programming, program generation and applications of machine learning and probabilistic search. PEPM focuses on techniques, supporting theory, tools, and applications of the analysis and manipulation of programs. In addition to the presentations of regular research papers, the PEPM program includes tool demonstrations and `short paper' presentations of exciting if not fully polished research. PEPM has established a Best Paper award. The winner will be announced at the workshop. INVITED TALKS Compiling Math to High Performance Code Markus Pueschel (ETH Zuerich, Switzerland) http://www.inf.ethz.ch/~markusp/index.html Specification and verification of meta-programs Martin Berger (University of Sussex, UK) http://www.informatics.sussex.ac.uk/users/mfb21/ ACCEPTED PAPERS Regular research papers: Naoki Kobayashi, Kazutaka Matsuda and Ayumi Shinohara. Functional Programs as Compressed Data Kazutaka Matsuda, Kazuhiro Inaba and Keisuke Nakano. Polynomial-Time Inverse Computation for Accumulative Functions with Multiple Data Traversals Dana N. Xu. Hybrid Contract Checking via Symbolic Simplification Susumu Katayama. An Analytical Inductive Functional Programming System that Avoids Unintended Programs Roberto Giacobazzi, Neil Jones and Isabella Mastroeni. Obfuscation by Partial Evaluation of Distorted Interpreters Michael Gorbovitski, Yanhong A. Liu, Scott Stoller and Tom Rothamel. Composing Transformations for Instrumentation and Optimization Elvira Albert, Jesus Correas Fernandez, German Puebla and Guillermo Roman-Diez. Incremental Resource Usage Analysis Takumi Goto and Isao Sasano. An approach to completing variable names for implicitly typed functional languages Martin Hirzel and Bugra Gedik. Streams that Compose using Macros that Oblige Vlad Ureche, Tiark Rompf, Arvind Sujeeth, Hassan Chafi and Martin Odersky. StagedSAC: A Case Study in Performance-Oriented DSL Development Markus Degen, Peter Thiemann and Stefan Wehr. The Interaction of Contracts and Laziness Surinder Kumar Jain, Chenyi Zhang and Bernhard Scholz. Translating Flowcharts to Non-Deterministic Languages Francisco Javier Lopez-Fraguas, Enrique Martin-Martin and Juan Rodriguez-Hortala. Well-typed Narrowing with Extra Variables in Functional-Logic Programming Geoff Hamilton and Neil Jones. Superlinear Speedup by Distillation: A Semantic Basis Short papers: Jacques Carette and Aaron Stump. Towards Typing for Small-Step Direct Reflection Janis Voigtlaender. Ideas for Connecting Inductive Program Synthesis and Bidirectionalization Tool demonstration papers: Edvard K. Karlsen, Einar W. Hoest and Bjarte M. Oestvold. Finding and fixing Java naming bugs with the Lancelot Eclipse plugin Adriaan Moors, Tiark Rompf, Philipp Haller and Martin Odersky. Scala-Virtualized Elvira Albert, Puri Arenas, Samir Genaim, Miguel Gomez-Zamalloa and German Puebla. COSTABS: A Cost and Termination Analyzer for ABS

1 0

Workshop on Juris-informatics (JURISIN 2011)の開催のお知らせ
by Ken Satoh 17 Nov '11

17 Nov '11

各位今年の12/1-2に高松でJSAI-IsAIの一部として開催される法律と情報学のワークショップJURISIN2011 http://research.nii.ac.jp/~ksatoh/jurisin2011.html のプログラムをお送り致します。多数の方のご参加をお待ちしております。登録は、 http://www.ai-gakkai.or.jp/jsai-isai/2011/#registration の情報をご覧ください。 12/1には法言語学(Forensic Linguistics)研究で有名な明治大学法学部の堀田秀吾教授 12/2にはIJCAIでResearch Excellence Awardを受賞したKowaski教授の招待講演があります。どうぞよろしくお願いいたします。佐藤　健国立情報学研究所 =============================================================== JURISIN 2011 Program Dec. 1, 2011 12:45-13:00 Opening Remark: Ken Satoh (National Institute of Informatics and Sokendai) 13:00-14:00 Invited Talk I Implications of Forensic Linguistics for Juris-informatics Syugo Hotta (Meiji University) 14:00-14:30 Document Structure Analysis with Syntactic Model and Parsers: Application to Legal Judgments Hirokazu Igari, Akira Shimazu and Koichiro Ochimizu 14:30-15:00 Recall-Oriented Evaluation Metrics for Consistent Translation of Japanese Legal Sentences Yasuhiro Ogawa, Masaki Mori and Katsuhiko Toyama 15:00-15:30 Using Classification to Support Legal Knowledge Engineers in the Eunomos Legal Document Management System Luigi Di Caro, Llio Humphreys and Guido Boella 15:30-16:00 Coffee Break 16:00-16:30 Prerequisite-Effect Structure on Intuitionistic Kripke Model Katsuhiko Sano, Shingo Hagiwara and Satoshi Tojo 16:30-17:00 The Concept and Definition of Software Accountability in Legal Engineering Ryo Hayasaka and Koichiro Ochimizu Dec. 2, 2011 9:30-10:30 Invited Talk II WUENIC: A Case Study in Rule-based Knowledge Representation and Reasoning Robert Kowalski(Imperial College London) and Anthony Burton 10:30-11:00 Coffee Break 11:00-11:30 A Substance-Field based Argumentation Framework Wachara Fungwacharakorn, Nuanwan Soonthornphisaj and Boonserm Kijsirikul 11:30-12:00 Deliberation Process Support System for Citizen Judge Trial Based on Structure of Factors Takanori Sato, Shogo Okada and Katsumi Nitta 12:00-12:30 A Semantics of Argumentation under Incomplete Information Ken Satoh and Kazuko Takahashi 12:30-12:45 Concluding Remark: Ken Satoh (National Institute of Informatics and Sokendai)

1 0

Call for Participation: LENLS 8 (Logic and Engineering of Natural Language Semantics 8)
by BEKKI Daisuke 16 Nov '11

16 Nov '11

（重複して受け取られた場合はご容赦ください）今年の12/1-3に高松で開催される LENLS8 国際ワークショップのプログラムをお送り致します。多数の方のご参加をお待ちしております。 12/3にはアムステルダム大学のFrank Veltman先生、青山学院大学のEric McCready先生によるチュートリアル講演を予定しています。戸次大介（お茶の水女子大学）照会先：lenls8 [[at]] easychair.org [Apologies for multiple copies] ================================================================= CALL FOR PARTICIPATION Logic and Engineering of Natural Language Semantics 8 (LENLS8) Workshop Site : "Sunport Hall Takamatsu", Takamatsu 2-1, Sunport, Takamatsu-shi, Kagawa-ken, Japan Information/Registration： 5th Floor Conference Rooms： 5th and 6th Floor Dates : December 1-3, 2011 Contact Person: Alastair Butler Contact Email : lenls8(a)easychair.org Website : http://www.is.ocha.ac.jp/‾bekki/lenls/ ================================================================= Chair: Alastair Butler (JST/Tohoku University) Invited Speaker(s): Frank Veltman (University of Amsterdam) Kentaro Inui (Tohoku University) Information on Takamatsu: http://www.takamatsu.or.jp/eng/ http://www.city.takamatsu.kagawa.jp/english/access/ http://www.my-kagawa.jp/eg/ LENLS is an annual international workshop focusing on formal semantics and pragmatics. It will be held as one of the workshops of JSAI isAI 2011, sponsored by The Japan Society for Artificial Intelligence (JSAI). Registration ============ The proceedings of the workshop will be available at the conference site for registered persons. Please follow the link below and register yourself until 24th November 2011. http://www.ai-gakkai.or.jp/jsai-isai/2011/index.html#registration Program ======= December 1st (Thu), 2011 ------------------------- 09:00-10:00: Reception 10:00-10:10: Opening Remarks 10:10-11:40: Session 1 * Yoshiki Mori "Back To the Future, Back From the Future - To and Fro For the Counterfactual Future In the Past -" * Yurie Hara, Yuli Feng and Shigeto Kawahara "Emphatic Stress as Epistemic Conflict: A case study of Mandarin Chinese" * Chungmin Lee "Dynamic Perspective Shifts in Evidentials: Evidence from Korean" 11:40-13:00: Lunch 13:00-15:00: Session 2 * Mauricio Hernandes "Players who don't know how to play. An Haskell implementation of unawareness." * Oleg Prosorov "A Sheaf-Theoretic Framework for Dynamic Semantics" * Margot Colinet and Gre'goire Winterstein "Linking probabilistic accounts: polarity items and discourse markers" * Hiroko Ozaki and Daisuke Bekki "Extractability as Deduction Theorem in Subdirectional Combinatory Logic" 15:00-15:30: Coffee break 15:30-16:30: Session 3 * Gre'goire Winterstein "Ludics and Presupposition Projection" * Nicholas Asher and Jason Quinley "Begging Questions, Getting Answers and Basic Cooperativity" 16:30-17:30: Invited Talk 1 * Frank Veltman (University of Amsterdam) "(TBA)" December 2nd (Fri), 2011 ------------------------- 08:30-09:00: Reception 09:00-10:30: Session 4 * Yo Sato and Wai Lok Tam "Underspecified types and the semantic bootstrapping of common nouns and adjectives: a simulation with a robot's sensory data " * David Yoshikazu Oshima "The Japanese particle yo in declaratives: Relevance, priority, and blaming" * Katsuhiko Yabushita "Japanese NPI Dare-mo as Unrestricted Universal Quantifier" 10:30-11:00: Coffee break 11:00-12:00: Session 5 * J.-R. Hayashishita and Daisuke Bekki "Conjoined nominal expressions in Japanese: Interpretation through monad" * Christina Unger "Dynamic semantics as monadic computation" 12:00-13:30: Lunch 13:30-15:00: Session 6 * Satoru Suzuki "Measurement-Theoretic Foundations of Gradable-Predicate Logic" * Tzu-Keng Fu "Universal Logic and the Logical Many-valuedness" * Alastar Butler and Kei Yoshimoto "Towards a self-selective and self-healing evaluation" 15:00-15:30: Coffee break 15:30-16:30: Invited Talk 2 * Kentaro Inui (Tohoku University) "Toward Deep Processing of Language in the Era of Large-scale Knowledge Resources: Time for Formal Semantics to Meet NLP Again" Alternates ---------- * Eric Mccready "Trust in Evidential Testimony" December 3rd (Sat), 2011 ------------------------- On the 3rd December, there will also be special tutorial lectures at the workshop venue by Frank Veltman (University of Amsterdam) and Eric McCready (Aoyama Gakuin University). Lecturer: - Frank Veltman (University of Amsterdam) - Eric McCready (Aoyama Gakuin University) Location: "Sunport Hall Takamatsu", Takamatsu 2-1, Sunport, Takamatsu-shi, Kagawa-ken, Japan Time Table (Tentative): 10:00-12:00 Session 1: Tutorial Lecture by Eric McCready Title: (TBA) 12:00-13:30 Lunch 13:30-17:30 Session 2: Tutorial Lecture by Frank Veltman Title: "Or else, what?" Abstract: In this talk I will present the theory of imperatives that I have developed in the past five years and apply it to a number of problems involving disjunction. In particular I will use it to analyse pseudo-imperatives and a variant of the Miners Paradox. Organizing Committee ==================== Alastair Butler (Chair) Daisuke Bekki Eric McCready Yoshiki Mori Yasuo Nakayama Katsuhiko Yabushita Tomoyuki Yamada Shunsuke Yatabe Kei Yoshimoto Contact ======= lenls8 [[at]] easychair.org

1 0

Call for papers Special issue of Logic Journal of IGPL *** Non-classical Modal and Predicate Logics ***
by Yuping Shen 16 Nov '11

16 Nov '11

(Apologies for multiple copies) Call for papers *** Non-classical Modal and Predicate Logics *** special issue of Logic Journal of IGPL Modalities and predicates have since ancient time been central notions in logic. In the 20th century, various systems of non-classical logics have emerged, with applications in many disciplines like Computer Science, Linguistics, Mathematics, and Philosophy. This gave rise to the questions of non-classical treatment of quantification and modalities and their accommodation in these non-classical settings. In response, various modal and predicate variants of non-classical logics have been introduced and studied in the past decades. This special issue is solely dedicated to modal and predicate non-classical logics. Its aim is to bring together papers from various branches of non-classical logics, not only to present recent advances in the particular fields, but also to identify common problems and methods and foster the exchange of ideas between researchers from separate fields. Topics of interest: * The study of first- or higher-order variants of non-classical logics, including, but not limited to: - Predicate intuitionistic and superintuitionistic logics - Predicate modal logics - Predicate substructural logics - Predicate many-valued and partial logics - Predicate paraconsistent logics - Predicate non-monotonic logics, etc. * Non-classical theories of quantification over classical logic, such as: - Free logics - Branching quantifiers and IF-logic - Generalized quantifiers * Extensions by modalities of (propositional or predicate) non-classical logics, including: - Modal extensions of (super)intuitionistic, substructural, many-valued, paraconsistent, non-monotonic, etc., logics - Co-algebraic treatment of modalities We encourage to submit papers on the above logics from any branches of mathematical logic (proof-theory, model theory, game theory, complexity, etc.), be it purely theoretical or about applications in the foundation of mathematics, computer science, linguistics, and philosophy. == Deadline == 31 March 2012 == Submissions == Papers should be submitted to ncmpl(a)cs.cas.cz. Please also use this email to express interest in submitting a paper. == A related conference == This special issue is related with the conference Non-classical Modal and Predicate Logics, organized Guangzhou (Canton), China, 5-9 December, 2011. http://logic.sysu.edu.cn/ncmpl2011 Petr Cintula, Rosalie Iemhoff, Shier Ju guest editors

1 0

「論理学と数学の哲学に関する研究会」のお知らせ
by Shunsuke Yatabe 09 Nov '11

09 Nov '11

「論理学と数学の哲学に関する研究会」のお知らせ日本科学哲学会第44回大会のサテライトイベントとして、以下の研究会を開催いたします。奮ってご参加ください。本研究会は、論理学および数学の哲学に関するテクニカルな研究に関する情報交換を行うための研究会です。通常の学会では発表は20分程度であり、テクニカルなテーマについて詳細な突っ込んだ議論を行うことが出来ません。そこで、本研究会では、テクニカルなテーマについての発表を、質疑応答も含め一人あたり一時間半程度おこない、議論を深めよう、ということを目的としています。 * 日時：2011年11/21（月）9:00-18:30 * 会場：星陵会館（永田町・赤坂見附） 1階会議室Ｆ http://www.seiryokai.org/kaikan.html * タイムテーブル： o 午前の部：グレアム・プリースト「存在しないものに向かって」　　　　　　　　　　　翻訳本刊行記念セッション + 9:00-10:30 久木田水生（京都大学）：　　　　　　　　　　　　記述句の多義性 + 10:45-12:15 藤川直也（首都大学東京）：　　　　　　　　　　　『存在しないものに向かって』における内包的他動詞の　　　　　　　　　　　　扱いについて o 午後の部：曖昧性セッション + 13:30-15:00 伊勢田哲治（京都大学）：　　　　　　　　　　　　曖昧述語に関する統計的モデルと主観的確率 + 15:15-16:45 岡本賢吾（首都大学東京）：　　　　　　　　　　　　遷移・文脈的変項・無視可能性 ― 動的ハイブリッド　　　　　　　　　　　　論理から曖昧性を考える + 17:00-18:30 矢田部俊介（産業技術総合研究所）：　　　　　　　　　　　　あいまい性と極限ー構成的素朴集合論における余帰　　　　　　　　　　　　納的対象の定義可能性 * Web site: http://researchmap.jp/joeluyy5c-21098/#_21098 * お問い合わせはこちらまでお願いします（[at]を@にお書き換え下さい） o 矢田部俊介( shunsuke.yatabe[at]aist.go.jp ) o 大西琢朗( takuro.onishi[at]gmail.com ) ********************************************************************************** * 講演要旨*** + 久木田水生（京都大学） # 題目：記述句の多義性 # 要旨：記述句を含む文（以下「記述文」）の評価（意味の決定）には根本的に異なる二つの方法がある。一つは「マイノング的評価」であり、そこでは記述句は名前と同様に対象を指示する項として扱われる。しかしながら記述句の中には「現在のフランス国王」のように、指示対象が存在しないものもあるため、マイノング的評価においては、記述句（あるいは一般に項）によって存在しない対象を指示することが可能でなければならない。もう一つは「ラッセル的評価」であり、そこでは記述句は独立した文法的単位とは見なされず、それ自体では指示対象を持たない。従ってここでは「現在のフランス国王」のような記述句が何か存在しない対象を指示するものと見なされる必要はない。このためにマイノング的評価とラッセル的評価の間には、存在しない対象を真正の対象として認めるか否かという、意味論の根本的な枠組みにおける対立が生じる。この二つのどちらが正しい記述文の評価法であるかを決定することは難しい。記述文のある使用例はマイノングを支持するように思われるし、別の使用例はラッセルを支持するように思われる。私たちは場面に応じて異なる評価法を使い分けている、というのが実情であろう。Towards Non-Being(2005)（邦訳『存在しないものに向かって』）においてグレアム・プリーストはマイノング主義に基づいた意味論を提示しており、その意味論では記述文の評価も当然マイノング的である。しかしその一方、プリーストは記述句が異なる場面で異なる使われ方をしていることを認めている。それは記述句が現実に存在する対象を指示するよう意図されている場面と、そうでない場面である。彼は世界意味論の枠組みに依拠しつつ、話者の意図に応じて記述文を評価する舞台となる世界の選び方が変化する、と説明する。しかし彼の説明は、典型的なラッセル的事例（例えば「水星の軌道の内側の惑星が水星の近日点の歳差を引き起こしている」等の文）を分析する際には、不自然であると言わざるを得ない。本発表で私たちはプリーストの意味論がどのように異なる意図で使用されている記述文を取り扱っているかを検討し、マイノング的にせよラッセル的にせよ、一つの評価方法ですべての事例を取り扱うことが困難であるということを指摘する。その上で私たちは二つの異なる評価方法の基盤となるような一般的な意味論的枠組みを提示することを試みる。その意味論は記述句に対して一つの表示を割り当てるという点ではマイノング主義的だが、存在しないものを真正な対象と見なさないという点では反マイノング主義的である。 + 藤川直也（首都大学東京） # 題目：『存在しないものに向かって』における内包的他動詞の扱いについて # 要旨：`seek'や`worship'などに代表されるいわゆる内包的他動詞は、一般に、次の三つ（のうちの少なくとも一つ）の特徴をもつとされる。 * (1) 目的語の名詞句が存在的コミットメントを欠く、 * (2) 目的語において置換可能性が成り立たない、 * (3) 確定的読みと不確定的読み（あるいはrelationalな読みとnotional な読み）をもつ。『存在しないものに向かって』において、プリーストは、非存在主義という一種のマイノング主義に基づいて、内包的他動詞に意味論を与えている。その基本的なアイデアは、例えば`John seeks a unicorn'をおおよそ`∃x(unicorn'(x) & seek'(John, x))'のように分析した上で、量化子を存在中立的なものと見なす（その量化のドメインには、存在する対象のみならず、非存在対象が含まれる）というものだ。この提案は、内包的他動詞の(1)の特徴を直裁的に説明する。さらにプリーストは、内包的他動詞の残る二つの特徴のそれぞれに対して、(1)に対する説明とは独立の説明を与えている。特徴(2)については、彼は、現象そのものを否定する。すなわち、内包的他動詞の目的語に関して、同一指示表現の置換は常に可能であると主張する。また特徴(3)については、不確定的な読みをもつ事例はすべて、なんらかの補文をとる文にパラフレーズ可能であり、不確定的読みはそのようなパラフレーズによって説明されると主張する。　本発表では、プリーストが内包的他動詞に与える意味論と、内包的他動詞の三つの特徴に対する彼の分析を紹介した上で、特に、(i) プリーストは、内包的他動詞の三つの特徴にそれぞれ独立した説明を与えているが、それらは整合的だろうか、(ii) 彼の意味論は、内包的他動詞を含む文に関して妥当に思われる推論、とりわけ目的語の量化名詞句が重要な役割を果たしていると思われる事例を適切に説明できるだろうか、という点に注目しながら、プリーストの提案を検討する。 + 伊勢田哲治（京都大学） # 題目：曖昧述語に関する統計的モデルと主観的確率 # 要旨：発表要旨　 http://researchmap.jp/mug0ywbe4-21099/?action=multidatabase_action_main_fil… 　（pdfファイル）曖昧述語に関しては単純なものから複雑なものまでさまざまなモデルが存在する。しかし、モデルが精緻になればなるほど、「果たしてこれが本当に日常的に使われている曖昧述語の背後に存在する構造なのだろうか」という疑問がわいてこずにはおかない。本発表でめざすのは、確率や統計の比較的単純なモデルのみで曖昧述語を取り扱うことである。一方で、対象自体の性質として、曖昧な対象が存在するように見える。たとえば「赤」から「黄色」への色のグラデーションにおいて赤と黄色の「唯一の本当の境目」があるというのは非常にありそうにない。他方で、われわれは曖昧な対象に対して二値的な用法を受け入れているように見える。たとえば、「このリンゴは赤い」といった表現は「はい」か「いいえ」で答えられる問いであるように見える。曖昧述語はなんらかの意味で確率と関わるように見えるけれども、上記のような特徴を考えるなら、単純なベイズ主義で曖昧述語を取り扱うのは難しそうに思われる。そこで導入するのが、重付置主義をベースとした統計モデルである。本発表で提示する統計モデルの概要をまず紹介する（このモデルは2011年7月に第14回CLMPSにおいて発表したものである）。曖昧述語の解釈に使われる基本的なモデルは、重付置主義で言うところの「精密化」(precisification)が一定の統計的分布をとるというモデルである。与えられた状況下で、曖昧述語Fの外延と反外延の間の精密な線を引くという決定（精密化決定）を繰り返し行うものとする。この線の場所としてある値は選ばれやすく、別の値は選ばれにくい、という形で精密化決定は一定の分布φを形成すると考えられる。この手続きは「誤差」のある測定に非常に似ている。そのアナロジーを推し進めるなら、「最小二乗法を使って真の境界線を推定する」といった行き方も考えられる。しかしすでに述べたように、曖昧述語はそもそも真の境界線を持たないような述語だと考えられるので、そうした推定は場違いであると思われる。それにかわって本発表で採用するのは、還元主義的戦略、すなわち、曖昧述語の意味の本体はこの精密化決定の分布φそのものであり、曖昧述語の二値的用法も最終的にはこの確率分布に還元される、という考え方である。二値的な用法の導入の仕方として、「重付置主義的解決」と「ベイズ的解決」を考える。重付置主義的解決とは、分布φを元に「許容可能性」に類する区別を導入するという考え方である。この場合、曖昧述語は重付置主義における重真と同じような簡単な様相論理的性質を持つことができる。もう一つのベイズ主義的解決とは、「次の精密化決定は与えられた対象XをＦの外延の側に入れる」という命題の事後確率を考え、その確率が十分に小さければ「ＸはＦではない」を受け入れる、という考え方である。これはベイズの定理を使うという意味でベイズ的とはいえ、分布は統計的分布であり、また統計的検定における有意水準に似たアイデアを使うなど、単なるベイズ主義とはひと味違うものになっている。以上が曖昧述語の統計的モデルの概要であるが、本発表ではこれにさらに主観的確率の要素を付け加える。統計的モデルの基礎となっている精密化決定の分布φは、仮想的なものであり、われわれが曖昧述語を使う際に事前の情報として持っているとは考えにくい。したがって、実際に曖昧述語を使う際には、さらにこの分布についての主観的な確率に基づいて判断する、という、もう一段階の不確実性が持ち込まれていると考えられる。二段階目の不確実性を導入する方法はいくつか考えられるが、上記のベイズ的解決を採用するなら、「次の精密化決定は与えられた対象XをＦの外延の側に入れる」という命題に対する主観的な事後確率を与える形が考えられる。このような手順で考えるならば、曖昧性が対象自体の性質であり、しかもわれわれはそれらについて二値的に語る、という状況において、主観的確率を使った判断が可能となる。 + 岡本賢吾（首都大学東京） # 題目：遷移・文脈的変項・無視可能性――動的ハイブリッド論理から曖昧性を考える # 要旨：発表要旨 http://researchmap.jp/muf24r5dr-21099/?action=multidatabase_action_main_fil… （pdfファイル）（以下は要旨pdfファイル[1]部からの抜粋）本発表は，2011年7月17日に「哲学若手研究者フォーラム」で話した内容の増補改訂版である。例えば、熱力学などのマクロ物理学のうちには，曖昧述語を用いた推論事例（として再構成しうるもの）が、実はごく当たり前に含まれていると考えられる。その典型は、当日述べる通り、「無視しうる（negligible）大きさ」が登場する様々の論証などである。このような熱力学などの論証については、とりわけ次の事実が注目される。すなわちそこでは、曖昧性をめぐる通常の哲学的議論のうちで「toleranceの原理」と呼ばれているもの――曖昧述語の適用基準には許容性がある，すなわち例えば，身長r cmの人が「背が高い」ならばr−10＾-1 cmの人もそうである、等々―― が、一定の仕方で受け入れられており、この原理への（少なくとも暗黙の）アピールがほぼ不可欠に生じていると解される、ということである。ところが他方で、現在、かなりの数の哲学者――通常のsuper-valuation主義者、真理値degree 論者、fuzzy論理支持者、等々のほぼすべて――は、「toleranceの原理」は妥当ではありえないと主張している。だがそうなると、彼らが正しいとする限り、熱力学の論証においては、不当な原理へのアピールという極めて不可解なこと――そのままでは論理的に許容し難いこと――が起こっていることになってしまう。これは看過できない問題である。もちろん、そうは言っても、「toleranceの原理」を受け入れる路線に転向する以外に一切対処策がないということにはならない。例えば、この原理へのアピールを含まない形へ熱力学の論証を書き換えるといったこともおそらく不可能ではないだろう。しかし、そうした書き換えは決して簡単ではないと予想されるし（少なくとも、一様な仕方ですべての論証を書き換える手続きを与えるのは相当に難しいだろう）、それ以前の問題として、既存の科学で受け入れられている論証に対して、そのような大幅な書き換えを要求するとしたら、それはむしろ、要求する側の考えに何か問題がある（当該の科学の論証を分析し損ねている公算が高い）と見るべきであるように思われる。要するに、 super-valuation、真理値degree論、fuzzy論理、等々を持ち出す分析は、もちろんそれぞれに独創的で、論理技術のエキジビションとしては十分興味深く啓発的なのだが、しかし曖昧述語の現実の用法の解明としては、多分に空想的・思弁的であり、あまり的確に的を射ていない疑いがある、ということである。　これに対して、今回、発表者は次のことを試みる。すなわち，以下の［２］で略述するような論理的枠組みを用いれば――この枠組みは，もともとtoleranceの原理を擁護すること（この原理を、他の原理と矛盾することのない仕方で、受け入れ可能なものとして定式化可能にさせること）をその基本的動機としている――、実際に当該の熱力学的論証の妥当な形式化が可能となる、ということである。これにより、(i)発表者の提案が、上記のような多くの哲学者たちのアプローチとは異なり、曖昧性述語の現実の用法に即した十分なリアリティーを備えたもの（とまで言えるかは判らないが，ともかくそうした望みを持ったもの）であること， (ii)もっと基本的な問題として，曖昧性についての通常の哲学的議論において安易に前提されがちなある種の考え、つまり、「曖昧述語は自然言語の特異的な特性である」とか「もっぱら現象的性質を表すものである」といった考えが，単なる誤った思い込みに過ぎないこと、等々の結論を引き出しうるであろう．本発表の目標は、基本的にこうした点にある。 + 矢田部俊介（産業技術総合研究所） # 題目：あいまい性と極限ー構成的素朴集合論における余帰納的対象の定義可能性とその影響について # 要旨：曖昧さを表現できるような弱い論理体系においては、同時に包括原理などの対象の循環的定義を許す原理を仮定しても無矛盾であることが知られている。本発表では、構成的な部分構造論理の一つである Flew∀ （直観主義論理から縮約規則を除去した体系）上の素朴集合論 CONS を例に取り、包括原理を仮定することは、言語を豊かにするだけでなく、一方で文の極限を取る（一見メタな）余帰納的操作さえ可能にしてしまうことを示す。具体的には、CONS 上の算術においては、後者関数に関する不動点を定義することが可能である。そしてこの不動点は、自然数全体の集合ωに関し排中律が成立する（∀x（ｘ∈ω∨¬x∈ω））ことが CONS では証明できないことを保証する。このキーとなる不動点は、余帰納的に定義された対象であり、後者関数を取るという操作の極限であると見なせる。通常、排中律は対象の確定性を表現すると考えられるため、極限操作が排中律に対する反例を提供するという事実は示唆的である。また、この証明を紹介すると同時に、素朴集合論内部における余帰納的な文・対象の定義可能性について議論する。 -- Shunsuke Yatabe <shunsuke.yatabe(a)aist.go.jp> AIST/CRTV (National Institute of Advanced Industrial Science and Technology/ Collaborate Research Team for Verification) tel: +81-6-6494-8047 fax: +81-6-6494-8073

1 0

「ロボットは東大に入れるか」シンポジウムのご案内
by noriko arai 08 Nov '11

08 Nov '11

みなさま、いつもお世話になります。新井紀子＠情報研です。国立情報学研究所では、以下のようなシンポジウムの開催を予定しております。ふるってご参加いただけますようお願いいたします。新井　紀子 **********************************************以下、乞う転載************* 国立情報学研究所（以下NII）では、12月14日（水）、「人工頭脳プロジェクト」キックオフシンポジウムを開催します。　本プロジェクトは、NIIが中心となって1980年以降細分化された人工知能分野を再統合することで新たな地平を切り拓くことを目的に、若い人たちに夢を与えるプロジェクトとして発足しました。日本における学際的な知識・先端技術を集積し、ひいては国際連携を視野に研究活動をスタートさせるため、この度キックオフシンポジウムを開催します。　本プロジェクトの具体的なベンチマークとして、2016年までに大学入試センター試験で高得点をマークすること、また2021年に東京大学入試を突破することを目標に研究活動を進めています。これまで蓄積された人工知能の各要素技術の精度を高め、情報技術分野の未来価値創成につなげるとともに、人間の思考に関する包括的な理解を内外の研究者とともに深めていきたいと考えております。　シンポジウムでは、松原仁氏（公立はこだて未来大学教授）を迎え基調講演を、また、作家の瀬名秀明氏を司会に迎え「知性と知識のはざまで」と題したパネルディスカッションを行います。　国立情報学研究所「人工頭脳プロジェクト」キックオフシンポジウム「ロボットは東大に入れるか」●日時：平成23年12月14日（水）13時20分〜17時30分●会場：学術総合センター一橋記念講堂　　　　〒110-8712 東京都千代田区一ツ橋２−１−２●URL：「ロボットは東大に入れるか」 http://21robot.org/※上記ウェブサイトで参加申込を受け付けています。※入場無料、定員450名（定員に達し次第申込を締め切らせて頂きま… Research、ジェイシー教育研究所プログラム概要：＜第一部＞　講演会基調講演　（松原仁・公立はこだて未来大学）人工知能のグランドチャレンジ　−チェス、サッカー、クイズから東大入試へ− 「ロボットは東大に入れるか」プロジェクト概要説明（新井紀子・NII）「人工知能にとってなぜ大学入試はチャレンジングか」（稲邑哲也・NII）「知識を問う問題にコンピュータはどれだけ答えられるか」（宮尾祐介・NII）＜第二部＞　パネルディスカッション「知性と知識のはざまで」司会　瀬名秀明（作家）安西祐一郎（日本学術振興会）、喜連川優（東京大学）、松原仁、新井紀子 -- --------------------------------------------- Noriko Arai National Institute of Informatics http://researchmap.jp/arai_noriko/

1 0

NIIレクチャーシリーズのお知らせ(Thomas Agotnes)
by Ken Satoh 07 Nov '11

07 Nov '11

NIIレクチャーシリーズのお知らせ国立情報学研究所(NII)では、海外の情報学に関係する著名研究者を招聘し、レクチャーシリーズを行っております。今回は、論理学によるマルチエージェントシステム、ゲーム理論の定式化を研究されているノルウェーのベルゲン大学のThomas Agostnes先生の連続レクチャーのお知らせです。講師:Professor Thomas Agotnes from University of Bergen, Norway. 講義名：Social Laws for Multi-Agent Systems: Logic and Games 　　　　　詳しい講演の内容は、 http://www.nii.ac.jp/en/calendar/2011/121302/ 　をご覧ください。場所：国立情報学研究所 20階 2001 または2010室講義日：2011年 12/13, 20, 27, 2012年1/10, 17, 24, 31 時間: 15:30-17:00 出席は無料で、どなたでも参加できます。なお、CTL(computational tree logic)に興味をお持ちの方に対しては、本講義の中にこの論理の紹介およびマルチエージェントへの応用などが含まれており特に有用であると思います。また、この連続講演の一部は、Ali Mili先生のソフトウェア工学関連の連続講演(http://www.nii.ac.jp/en/calendar/2011/1213/) の後に行われるので、１日で２つの講演を連続して聞くことができます。参加のご検討よろしくお願いします。佐藤　健国立情報学研究所および総研大 ========== - Lecture Series: Social Laws for Multi-Agent Systems: Logic and Games Lecturer: Professor Thomas Agotnes, University of Bergen Thomas Agotnes is a professor at the Department of Information Science and Media Studies at the University of Bergen, Norway. Since his PhD in 2004 form University of Bergen, Agotnes has worked and published extensively in multi-agent systems and related areas. In 2009, he won best paper award at AAMAS 2009 on logical analysis of normative systems. Agotnes is an active member of the international multi-agent systems community. He is a member of the board of directors of the European Association for Multi-Agent Systems (EURAMAS), was the general chair of STAIRS 2010, and has served on the program committees of the main conferences and workshops in his field, including the senior program committees of AAMAS and IJCAI. Schdeule Lecture 1: Specifying and verifying state-transition models for multi-agent Systems Place: National Institute of Informatics, Lecture room 2001, 20F Date: 15:30-17:00, December 13, 2011 Lecture 2: Social laws for coordination Place: National Institute of Informatics, Lecture room 2001, 20F Date: 15:30-17:00, December 20, 2011 Lecture 3: Dealing with non-compliance Place: National Institute of Informatics, Lecture room 2001, 20F Date: 15:30-17:00, December 27, 2011 Lecture 4: Coordinating self-interested agents Place: National Institute of Informatics, Lecture room 2001, 20F Date: 15:30-17:00, January 10, 2012 Lecture 5: Social laws design as an optimisation problem, and as a mechanism design problem Place: National Institute of Informatics, Lecture room 2010, 20F Date: 15:30-17:00, January 17, 2012 Lecture 6: Reasoning about social laws Place: National Institute of Informatics, Lecture room 2010, 20F Date: 15:30-17:00, January 24, 2012 Lecture 7: Strategic reasoning under imperfect information Place: National Institute of Informatics, Lecture room 2010, 20F Date: 15:30-17:00, January 31, 2012

1 0

NII Type Theory Workshop
by Makoto Tatsuta 07 Nov '11

07 Nov '11

Sixth NII Type Theory Workshop Date: November 14, 2011, 11: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: 11:00--11:30 Takayuki Koai (National Institute of Informatics) Title: Verification of Substitution Theorem Using HOL 11:30--12:00 Mauricio Hernandes (The Graduate University for Advanced Studies) Title: Game theory from a logician perspective 12:00--13:40 Lunch Break 13:40--14:10 Takanori Hida (Kyoto University) Title: A computational interpretation of the axiom of determinacy 14:10--14:40 Makoto Tatsuta (National Institute of Informatics) Title: Non-Commutative Infinitary Peano Arithmetic 14:40--15:00 Tea Break 15:00--16:00 Neil D. Jones (University of Copenhagen) Title: Termination Analysis of the Untyped lambda-Calculus 16:00--17:00 Stefano Berardi (Torino University) Title: A Topology over a set of Knowledge States and a Fixed Point Problem Abstracts: ---------------------------------------------------------------------- Takayuki Koai (National Institute of Informatics) Title: Verification of Substitution Theorem Using HOL Abstract: Substitution Theorem is a new theorem in untyped lambda calculus, which was proved in 2006. This theorem states that for a given lambda term and given free variables in it, the term becomes weakly normalizing when we substitute arbitrary weakly normalizing terms for these free variables, if the term becomes weakly normalizing when we substitute a single arbitrary weakly normalizing term for these free variables. This paper formalizes and verifies this theorem by using higher-order theorem prover HOL. A control path, which is the key notion in the proof, explicitly uses names of bound variables in lambda terms, and it is defined only for lambda terms without bound variables renaming. The lambda terms without bound variable renaming are formalized by using the HOL package based on contextual alpha-equivalence. The verification uses 10119 lines of HOL code and 326 lemmas. This is a joint work with Makoto Tatsuta. ---------------------------------------------------------------------- Mauricio Hernandes (The Graduate University for Advanced Studies) Title: Game theory from a logician perspective Abstract: I intend in this talk to introduce a few concepts in game theory like Nash Equilibrium and Backward-Induction, and then express those ideas with some modal logic. ---------------------------------------------------------------------- Takanori Hida (Kyoto University) Title: A computational interpretation of the axiom of determinacy Abstract: Axiom of determinacy(AD) is a central topic in descriptive set theory and there are a number of research on this axiom. In this talk, we approach to the computational content of negative translation of AD using realizability interpretation due to Berardi, Bezem and Coquand (1998). ---------------------------------------------------------------------- Makoto Tatsuta (National Institute of Informatics) Title: Non-Commutative Infinitary Peano Arithmetic Abstract: Does there exist any sequent calculus such that it is a subclassical logic and it becomes classical logic when the exchange rules are added? The first contribution of this paper is answering this question for infinitary Peano arithmetic. This paper defines infinitary Peano arithmetic with non-commutative sequents, called non-commutative infinitary Peano arithmetic, so that the system becomes equivalent to Peano arithmetic with the omega-rule if the the exchange rule is added to this system. This system is unique among other non-commutative systems, since all the logical connectives have standard meaning and specifically the commutativity for conjunction and disjunction is derivable. This paper shows that the provability in non-commutative infinitary Peano arithmetic is equivalent to Heyting arithmetic with the recursive omega rule and the law of excluded middle for Sigma-0-1 formulas. Thus, non-commutative infinitary Peano arithmetic is shown to be a subclassical logic. The cut elimination theorem in this system is also proved. The second contribution of this paper is introducing infinitary Peano arithmetic having antecedent-grouping and no right exchange rules. The first contribution of this paper is achieved through this system. This system is obtained from the positive fragment of infinitary Peano arithmetic without the exchange rules by extending it from a positive fragment to a full system, preserving its 1-backtracking game semantics. This paper shows that this system is equivalent to both non-commutative infinitary Peano arithmetic, and Heyting arithmetic with the recursive omega rule and the Sigma-0-1 excluded middle. This is a joint work with Stefano Berardi and was presented at CSL 2011. ---------------------------------------------------------------------- Neil D. Jones (University of Copenhagen) Title: Termination Analysis of the Untyped lambda-Calculus Abstract: An algorithm is developed that, given an untyped lambda-expression, can certify that its call-by-value evaluation will terminate. It works by an extension of the ``size-change principle'' earlier applied to first-order programs. The algorithm is sound (and proven so) but not complete: some lambda-expressions may in fact terminate under call-by- value evaluation, but not be recognised as terminating. The intensional power of size-change termination is reasonably high: It certifies as terminating all primitive recursive programs, and many interesting and useful general recursive algorithms including programs with mutual recursion and parameter exchanges, and Colson's ``minimum'' algorithm. Further, the approach allows free use of the Y combinator, and so can identify as terminating a substantial subset of PCF. (joint work with Nina Bohr; in Logical Methods in Computer Science, 2008, Issue 1) ---------------------------------------------------------------------- Stefano Berardi (Torino University) Title: A Topology over a set of Knowledge States and a Fixed Point Problem 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. ----------------------------------------------------------------------

1 0

Workshop on Linear Logic (abstracts available)
by Kazushige TERUI 05 Nov '11

05 Nov '11

皆様線型論理関連ワークショップ（１１月７日−１１日、京都大学）について、アブストラクト入りのプログラムが出来上がりましたのでご案内をさせていただきます。 ※１１月９日（水）の懇親会に参加希望の方は７日（月）までにお申し込みください。 -------------------- Workshop on Linear Logic (Geometry of Interaction, Traced Monoidal Categories and Implicit Complexity) * Date: 7th - 11th, November (11th reserved for free discussion) * Location: Room 110, Faculty of Science Building No.3, Kyoto University http://www.kyoto-u.ac.jp/en/access/campus/north.htm 京都大学理学部３号館１１０号室 http://www.kyoto-u.ac.jp/ja/access/campus/map6r_n.htm ※数理解析研究所ではありませんのでご注意ください。 * Workshop Dinner 18:30-, 9th November. Izakaya Anji Fuchomae (Annex) http://www.anji-gr.com/futyoumae/index.html 　Students 3,000yen, Others 5,000yen ※Please inform us by 7th Monday if you would like to participate. * Organizers Michele Basaldella: mbasalde(a)kurims.kyoto-u.ac.jp Kazushige Terui: terui(a)kurims.kyoto-u.ac.jp Claudia Faggian * Program with abstracts http://www.kurims.kyoto-u.ac.jp/~terui/wsprogram.pdf ------------------------------------- Registration Form 1. Your name, affiliation, status 2. You participate in the workshop during ?th - ?th November. 3. You do/do not participate in the social dinnter on 9th. 　 (Inform us if you have any dietary option.) -------------------------------------- ------------------------------------------ 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

WST 2012: First Call For Papers
by Nao Hirokawa 04 Nov '11

04 Nov '11

来年2月に行われます停止性に関するワークショップの論文投稿募集の案内をお送り致します。今年はオーストリアのオーバーグルグルで開催されます。投稿を見当して頂けますと幸いです。廣川　直（北陸先端科学技術大学院大学） ====================================================================== First Call for Papers WST 2012 12th International Workshop on Termination Feb 19 - 23, 2012, Obergurgl, Innsbruck http://cl-informatik.uibk.ac.at/users/georg/events/wst2012/ ====================================================================== The goal of the Workshop on Termination is to be a venue for presentation and discussion of all topics in and around termination. In this way, the workshop tries to bridge the gaps between different communities interested and active in research in and around termination. We will work very hard to attain the same friendly atmosphere as in past workshops, which enabled fruitful exchanges leading to joint research and subsequent publications. IMPORTANT DATES: * submission December 18, 2012 * notification January 15, 2012 * final version January 29, 2012 * workshop February 19 - 23, 2012 TOPICS: The 12th International Workshop on Termination welcomes contributions on all aspects of termination and complexity analysis. Contributions from the imperative, constraint, functional, and logic programming communities, and papers investigating applications of complexity or termination (for example in program transformation or theorem proving) are particularly welcome. Areas of interest to the workshop include, but are not limited to, the following: * Termination of programs * Termination of rewriting * Termination analysis of transition systems * Complexity of programs * Complexity of rewriting * Implicit computational complexity * Implementations of termination and complexity analysis methods * Certification of termination and complexity proofs * Termination orders, well-founded orders, and reduction orders * Termination methods for theorem provers * Strong and weak normalization of lambda calculi * Termination analysis for different language paradigms * Challenging termination problems/proofs * Applications to program transformation and compilation * Other applications of termination methods * Comparisons and classification of termination methods * Non-termination and loop detection * Termination in distributed systems * Proof methods for liveness and fairness * Well-quasi-order theory * Ordinal notations * Subrecursive hierarchies PROGRAM COMMITTEE: * Ugo Dal Lago University of Bologna * Danny De Schreye K.U. Leuven * Samir Genaim The Complutense University * Nao Hirokawa JAIST * Georg Moser University of Innsbruck (chair) * Albert Rubio Universitat Politecnica de Catalunya * Peter Schneider-Kamp University of Southern Denmark * Rene Thiemann University of Innsbruck SUBMISSION: Submissions are short papers/extended abstract which should not exceed 5 pages. There will be no formal reviewing. The accepted papers will be made available electronically before the workshop. Papers should be submitted electronically via the submission page: http://www.easychair.org/conferences/?conf=wst2012 Final versions should be created using LaTeX and the style file LIPIcs (http://drops.dagstuhl.de/styles/lipics/lipics-authors.tgz).

1 0

数学基礎論若手の会 (3rd announcement)
by SAKAI Hiroshi 01 Nov '11

01 Nov '11

皆様：神戸大学の酒井拓史と申します．数学基礎論若手の会のご案内をさせていただきます．今年度の数学基礎論若手の会の申し込み締め切りが 11月6日(日) と迫っていますが，いまのところ参加枠と講演枠にかなりの余裕があります．皆様のふるってのご参加／ご講演をお待ちしています．また，お近くに数学基礎論を勉強している学生さんや，興味をお持ちの方がいらっしゃいましたら，周知していただけると助かります．よろしくお願いします．以下は，以前にも当メーリングリストに配信させていただいた若手の会の案内です：数学基礎論若手の会は，数学基礎論を専攻する学生と若手研究者の交流を目的とした，合宿形式の研究集会です．これから数学基礎論を勉強しようとしている学生さんの参加なども歓迎します．また講演はオリジナルの成果発表の他にも，研究の途中報告や内容紹介など幅広く募集しています．過去の若手の会の記録は以下のページでご覧いただけます： http://www.mi.s.osakafu-u.ac.jp/~kada/wakate/index.html 今年度の若手の会は下記の要領で開催します．ご質問等ありましたら，幹事の酒井までお気軽にご連絡ください．日程： 12月9日(金)午後〜 11日(日)午前場所：大阪府羽衣青少年センター http://www.osaka-yha.com/osakakokusai/ 幹事：酒井拓史 (神戸大学) hsakai(a)people.kobe-u.ac.jp ホームページ： http://www2.kobe-u.ac.jp/~hsakai/wakate2011/ [宿泊・食事] 宿泊と食事は会場併設の大阪国際ユースホステルを利用します．宿泊は12月9日(金)と10日(土)の2晩，食事は9日(金)の夕食から 11日(日)の朝食までの5食を下記料金で利用いただけます：宿泊： 1人1泊 2,800円 (6人部屋利用) 食事：朝食 630円，昼食 630円，夕食 1,050円 ※ 個室などを希望される方は，お早めに酒井までご連絡ください． ※ 夕食後に親睦会を予定しており，会費を別途 1,000円程度いただく予定です． [参加申し込み] 参加を希望される方は，幹事の酒井にメールにてお申し込みください． <申込締切> 11月6日(日) =========== 参加申し込みフォーム ============ 氏名：所属：職名・学年：参加希望日程：全日程参加 or ... 講演希望：希望する or 希望しない or 未定講演タイトル： (未定の場合は "未定" とご記入ください．) 講演時間： 30分程度 or 60分程度 or 未定宿泊： 9日(金)の夜 … ○ or × 10日(土)の夜 … ○ or × 食事： 9日(金)夕食 … ○ or × 10日(土)朝食 … ○ or × 10日(土)昼食 … ○ or × 10日(土)夕食 … ○ or × 11日(日)朝食 … ○ or × 質問・要望等： ============================================== 多くの方のご参加・ご講演をお待ちしております． --------------------------------------------- 酒井拓史神戸大学大学院システム情報学研究科講師 e-mail: hsakai(a)people.kobe-u.ac.jp tel: 078-803-245 address: 〒657-8501 神戸市灘区六甲台町 1-1 神戸大学システム情報学研究科 ---------------------------------------------

1 0

Talk by Michele Basaldella, Tue 1 Nov at RIMS, Kyoto U
by Kenshi Miyabe 25 Oct '11

25 Oct '11

数理解析研究所　特定研究員の宮部です。重複して受け取られた場合はご容赦ください． RIMSでは、2週間に1度、GCOE tea timeを行っています。 http://www.kurims.kyoto-u.ac.jp/~kenkyubu/gcoe/2008teatime.html 来週、2011年11月1日(火)、第48回 GCOE tea timeでは、 Micheleが話をします。時間のご都合がよろしければ是非ご参加ください．講演者： Michele BASALDELLA (数理解析研究所　研究員) タイトル: Dilators: a gentle introduction 講演の概要: We aim to recall some basic aspects of the concept of dilator, a notion which has been introduced in proof-theory (a branch of mathematical logic) by J.-Y. Girard about 30 years ago. Essentially, a dilator is a certain kind of endofunctor of the category of the ordinal　numbers, which can be thought as an abstract counterpart of the more concrete system of ordinal notation which are abundant in proof-theory. In this introductory talk, we recall the notion of denotation system (a kind of generalization of the Cantor normal form representation of the ordinal numbers), the notion of dilator, and show a correspondence between them. なお、この講演は英語で行われます。時間(Time)：15:00-16:00 場所(Place)：数理解析研究所402号室(RIMS, Room 402) -- Kenshi Miyabe email: kmiyabe(a)kurims.kyoto-u.ac.jp Researcher Research Institute for Mathematical Sciences, Kyoto University Kyoto 606-8502 Japan Tel: +81-75-753-7202 / Fax: +81-75-753-7272

1 0

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Logic-ml