Logic-ml May 2012

11 participants
13 discussions

セミナー案内
by KASHIMA Ryo 12 Oct '12

12 Oct '12

数理論理学セミナーのご案内日時：12月22日(木)17時から場所：東京工業大学大岡山西８号館W棟11階 W1101セミナー室会場までの交通案内はこちらから： http://www.titech.ac.jp/about/campus/index.html 話者：藤原誠（東北大学）題目：結婚定理の逆数学概要： 1972年にManasterとRosensteinは可算版結婚定理を再帰理論的に分析し、通常の可算版結婚定理は計算可能には成立しないことを示した。一方、1983年にKiersteadは拡張Hall条件を導入し、計算可能に成立する結婚定理を得た。本発表では、拡張Hall条件を用いて考え得るあらゆる結婚定理の複雑さを逆数学的に分析する。また、Kiersteadとは別の観点から、計算可能に成立する結婚定理について考察する。 ----- 鹿島亮東京工業大学大学院情報理工学研究科数理・計算科学専攻 kashima(a)is.titech.ac.jp ＃＃＃木曜夕方を中心に不定期的にセミナーを開催しています＃＃＃＃＃＃詳細はお問い合わせください＃＃＃

1 1

Sendai Logic Workshop のご案内
by higurashi3873＠yahoo.co.jp 25 May '12

25 May '12

Logic-ml $B$N3'MM!$(B $B$3$s$P$s$O!$ElKLBg3X$NKYH*2B9($G$9!%(B $B2<5-$NMWNN$G!$ElKLBg3X!JEDCf0lG78&!K$K$F8&5f2q$r9T$$$^$9$N$G!$6=L#$N$"$kJ}$O$<$R$4;22C$/$@$5$$!%(B $B;09V1i$4$6$$$^$9!%(B ************************************************************************* Sendai Logic Workshop $BF|;~!'(B6$B7n(B1$BF|!J6b!K(B14:00$B!A(B17:30 $B>l=j!'ElKLBg3X(B $BKL@DMU;3%-%c%s%Q%9(B $BM}3X9gF1Eo(B 1201$B9f<<(B $B-!(B14:00$B!A(B15:00 $B9V1i<T!'</Eg(B $BN<(B $B!JEl5~9)6HBg3XBg3X1!(B $B>pJsM}9)3X8&5f2J!K(B $B%?%$%H%k!'(BCTL$B$H<~JU$NO@M}$N8xM}2=$K$D$$$F(B $B%"%V%9%H%i%/%H!'(B Computation Tree Logic (CTL) $B$O!$;~4V$N?d0\$KH<$C$F>uBV$,JQ2=$9$k%7%9%F%`$N5-=R$KMQ$$$i$l$kMMAjO@M}!J;~AjO@M}!K$NBeI=$G$"$k!#(B $BK\9V1i$NL\E*$O!$(BCTL$B$H$=$N<~JU$NO@M}$KBP$9$k%R%k%Y%k%HN.8xM}2=$H40A4@-$K$D$$$F=iJb$+$i2r@b$7!$9V1i<T$N:G6a$N;E;v!J(BECTL$B$N8xM}2=!K$d<h$jAH$_$?$$LdBj!JMMAj&L7W;;$N40A4@-$NJL>ZL@!K$K$D$$$F@bL@$9$k$3$H$G$"$k!#(B $BM=HwCN<1$O8EE5L?BjO@M}$N40A4@-DjM}DxEY$G==J,$NM=Dj!#(B $B-"(B15:15$B!A(B16:15 $B9V1i<T!':,85(B $BB?2B;R(B $B!JKLN&@hC<2J3X5;=QBg3X1!Bg3X(B $B>pJs2J3X8&5f2J!K(B $B%?%$%H%k!'(BWadge $B%2!<%`$N%P%j%(!<%7%g%s$H(B Wadge $B3,AX(B $B%"%V%9%H%i%/%H!'(B Wadge [3] $B$K$h$jDj5A$5$l$?(B Wadge $B3,AX$OO"B34X?t$K$h$k5UA|$K$D$$$FJD$8$?%/%i%9$N@.$93,AX$G!"(BBorel $B3,AX$d(B Hausdorff $B$N=89g:9$K$h$k3,AX$h$j$b$h$j:Y$+$$=89g$N3,AX$rM?$($k!#(B $B$3$N3,AX$N3F%/%i%9$N=89gA`:n$K$h$k5-=R$O(B Louveau [2] $B$K$h$jM?$($i$l$?$,!"(B $BHs>o$KHQ;($G$"$k!#(B Wadge $B3,AX$G??$KF1$8<!?t$r$b$D=89g$O(B Wadge $B%2!<%`$K$h$jFCD'$E$1$i$l$k$,!"(BDuparc [1] $B$G$O$3$N%2!<%`$N%P%j%(!<%7%g%s$K$h$j(B Wadge $B%/%i%9$N<!?t$N5-=R$N4JN,2=$rM?$((B $B$F$$$k!#(B $BK\9V1i$G$O(B [1] $B$NFbMF$rCf?4$K!"(BWadge $B%2!<%`$H(B Wadge $B3,AX$K4X$9$k8&5f$r>R2p$9$k!#(B $B;29MJ88%!'(B [1] J. Duparc, Wadge Hierarchy and Veblen Hierarchy. Part I: Borel Sets of Finite Rank. Journal of Symbolic Logic 66(1), pp. 56-86, 2001 [2] A. Louveau, Some results in the Wadge hierarchy of Borel sets, Cabal seminar 79-81, Lecture Notes in Mathematics, vol. 1019, Springer Verlag, 1983, pp. 28-55. [3] W.W. Wadge, Reducibility and determinateness on the Baire space., Ph.D. thesis, Berkeley, 1984. $B-#(B16:30$B!A(B17:30 $B9V1i<T!'O!Hx(B $B0lO:(B $B!JEl5~Bg3XBg3X1!(B $B>pJsM}9)3X7O8&5f2J!K(B $B%?%$%H%k!'(BProgramming with Infinitesimals: A While-Language for Hybrid System Modeling (Joint Work with Kohei Suenaga, Kyoto University) $B%"%V%9%H%i%/%H!'(B We add, to the common combination of a WHILE-language and a Hoare-style program logic, a constant dt that represents an infinitesimal (i.e. infinitely small) value. The outcome is a framework for modeling and verification of hybrid systems: hybrid systems exhibit both continuous and discrete dynamics and getting them right is a pressing challenge. We rigorously define the semantics of programs in the language of nonstandard analysis, on the basis of which the program logic is shown to be sound and relatively complete. If the time allows, our recent prototype automatic prover will also be demonstrated. $B;29MJ88%!'(B Kohei Suenaga and Ichiro Hasuo. Programming with Infinitesimals: A While-Language for Hybrid System Modeling. Proc. ICALP 2011, Track B. LNCS 6756, p. 392-403. Springer-Verlag. ************************************************************************* $B0J>e$G$9!%(B $B%;%_%J!<>pJs$O2<5-@gBf%m%8%C%/$N%[!<%`%Z!<%8$+$i$b$4Mw$$$?$@$1$^$9!%(B https://sites.google.com/site/sendailogichomepage/ $BKYH*!!2B9((B -- -- $BElKLBg3XBg3X1!!!M}3X8&5f2J(B $B?t3X@l96!!;:3X41O"7H8&5f0w(B E-mail: higurashi3873(a)yahoo.co.jp

1 0

talks by Vivek Nigam and Hugo Herbelin in Kyoto (28th May 2012)
by Hasegawa Masahito 24 May '12

24 May '12

$B3'MM!"(B $B0J2<$NFbMF$G#2#8F|!J7n!K$K9V1i$rFs7oM=Dj$7$F$$$^$9!#(B Herbelin$B$5$s$N9V1i$O(BFLOPS2012$B$N$*OC$N3HD%HG$G$9!#(B $B$I$&$>$4MhD0$/$@$5$$!#(B $BD9C+@n???M(B <hassei(a)kurims.kyoto-u.ac.jp> $B5~ETBg3X?tM}2r@O8&5f=j(B ==================================================== Date: 28 May 2012 (Monday) 14:30-17:00 14:30-15:30 talk by Vivek Nigam 16:00-17:00 talk by Hugo Herbelin Venue: Room 478, General Research Building No.2, Kyoto University (Access information & map: http://www.kyoto-u.ac.jp/en/access http://www.kurims.kyoto-u.ac.jp/~hassei/map-2.jpg) $BCm!'?tM}2r@O8&5f=jK\4[$G$O$"$j$^$;$s!#(B $BI4K|JW$N$=$P$NAm9g8&5fFs9f4[$N(B4$B3,$G$9!#(B ==================================================== Speaker: Vivek Nigam (Ludwig Maximilian University of Munich) Title: An Extended Framework for Specifying and Reasoning about Proof Systems Abstract: It has been shown that linear logic can be successfully used as a framework for both specifying proof systems for a number of logics, as well as proving fundamental properties about the specified systems. In this paper, we show how to extend the framework with subexponentials in order to be able to declaratively encode a wider range of proof systems, including a number of non-trivial proof systems such as a multi-conclusion intuitionistic logic, classical modal logic S4, and intuitionistic Lax logic. Moreover, we propose methods for checking whether an encoded proof system has important properties, such as if it admits cut-elimination, the completeness of atomic identity rules, and the invertibility of its inference rules. Finally, we present a tool implementing some of these specification/verification methods. This is a joint work with Giselle Reis and Elaine Pimentel. ==================================================== Speaker: Hugo Herbelin (Laboratoire PPS, CNRS, INRIA & Universite Paris Diderot) Title: Classical call-by-need sequent calculi: The unity of semantic artifacts Abstract: We systematically derive a classical call-by-need sequent calculus, which does not require an unbounded search for the standard redex, by using the unity of semantic artifacts proposed by Danvy et al. The calculus serves as an intermediate step toward the generation of an environment-based abstract machine. The resulting abstract machine is context-free, so that each step is parametric in all but one component. The context-free machine elegantly leads to an environment-based CPS transformation. This transformation is observationally different from a natural classical extension of the transformation of Okasaki et al., due to duplication of un-evaluated bindings. We further demonstrate the usefulness of a systematic approach by deriving an abstract machine and CPS for an alternative classical call-by-need calculus. (Joint work with Zena M. Ariola, Paul Downen, Keiko Nakata & Alexis Saurin) ====================================================

1 0

第89回プログラミング研究会開催案内
by Takahito Aoto 22 May '12

22 May '12

＊＊＊＊複数受け取られた方はご容赦ください＊＊＊＊情報処理学会第89回プログラミング研究発表会開催のご案内をさせて頂きます． 6月21日(木)・22日(金)に小樽にて開催されます．皆様のご参加をお待ちしております．また，第1日目の夜に懇親会を予定しています．懇親会への参加をご希望の方は 6月14日(木)までに下記の要領で花井までお申し込みください．(発表会への参加自体については事前の申し込みは不要です．) ------------------------------------ To: ryo.hanai [at] aist.go.jp Subject: PRO89-party 6月21日(木)の懇親会に参加します．御名前: 御所属: 区別: 学生・一般 (6月14日(木)までにお知らせ下さい．) ------------------------------------ なお，下記のプログラムで，発表の順番につきましては今後変更される可能性がございますのでご了承ください．最新情報は以下のWEBページに掲載致します． http://www.jsk.t.u-tokyo.ac.jp/pro-2012-1/ --- 担当: 花井亮(産総研)，青戸等人(東北大学) ================================================================= 情報処理学会第89回プログラミング研究発表会プログラム ================================================================= 日程： 2012年6月21日（木)・22日（金）場所：小樽市民センター 3階研修室〒047-0031 小樽市色内2丁目13番5号 JR小樽駅より徒歩5分 ※ 1件あたり45分 (発表25分，質疑・討論20分) ※ 発表の順番につきましてはまだ確定ではありませんのでご了承ください． 6月21日(木) セッション１：14:15-15:45 2012-1-(1)：14:15-15:00 「ビットマップマーキングを利用したマークコンパクトごみ集めのJikes RVM への実装」 ○森川和哉, 鵜川始陽, 岩崎英哉（電気通信大） 2012-1-(2)：15:00-15:45 「マイコン制御学習用プログラミング言語の設計と実装」 ○谷岡政宏（北海道職業能力開発大学校） 15:45-16:00 休憩セッション２：16:00-17:30 2012-1-(3)：16:00-16:45 「文脈指向言語EventCJへの合成層の導入」 ○紙名哲生（東京大）, 青谷知幸（北陸先端大）, 増原英彦（東京大） 2012-1-(4)：16:45-17:30 「文脈指向プログラムの資源利用解析に基づく層活性解析法」 ○青谷知幸（北陸先端大）, 紙名哲生, 増原英彦（東京大） 19:00-21:00 懇親会 6月22日(金) セッション３：10:00-11:30 2012-1-(5)：10:00-10:45 「スクリプト言語KonohaScriptにおけるLLVMを用いたJust-in-timeコンパイラの実装と評価」 ○井出真広, 志田駿介, 倉光君郎（横浜国立大） 2012-1-(6)：10:45-11:30 「アトミックグループで拡張された正規表現のオートマトンへの変換」 ○杉山聡, 南出靖彦（筑波大） =================================================================

1 0

CFP: LENLS 9 (Logic and Engineering of Natural Language Semantics 9)
by BEKKI Daisuke 22 May '12

22 May '12

（重複して受け取られた場合はご容赦ください）今年の１２月に宮崎で開催される LENLS 9 国際ワークショップのCFPをお送り致します。多数のご投稿をお待ちしております。戸次大介（お茶の水女子大学） [Apologies for multiple copies] ================================================================= FIRST CALL FOR PAPERS Logic and Engineering of Natural Language Semantics 9 (LENLS 9) Workshop Site : "Amusement Zone Miyazaki (The JA-AZM Hall)" Kirishima 1-1-1, Miyazaki, Japan. http://www.jaazm.jp/access/english.html Dates : December 1-3, 2012 Contact Person: Alastair Butler (PRESTO JST/Tohoku University) Contact Email : lenls9[[at]]easychair.org Website : http://www.is.ocha.ac.jp/‾bekki/lenls/ ================================================================= Chair: Alastair Butler (PRESTO JST/Tohoku University) Co-chair: Daisuke Bekki (Ochanomizu University) Eric McCready (Aoyama Gakuin University) Invited Speaker(s): - Hans Kamp (University of Stuttgart) Call For Papers: ================ LENLS is an annual international workshop focusing on formal semantics and pragmatics. It will be held as one of the workshops of the third JSAI International Symposia on AI (isAI2012) (http://www.ai-gakkai.or.jp/jsai-isai/2012/) sponsored by the Japan Society for Artificial Intelligence (JSAI) (http://www.ai-gakkai.or.jp/jsai/english.html). We invite submissions to this year's workshop on topics in formal semantics and pragmatics, and related fields, including but in no way limited to the following: - Dynamic syntax/semantics/pragmatics of natural language - Categorical/topological/coalgebraic approaches for natural language syntax/semantics/pragmatics - Logic and its relation to natural language and linguistic reasoning (especially dynamic logics) - Type-theoretic approaches to natural language - Formal Philosophy of language - Formal pragmatics (especially game-theoretic and utility-theoretic approaches) - Substructural expansion of Lambek Lambda Calculi - Many-valued/Fuzzy and other non-classical logics and natural language Submissions: ============ Abstracts (up to 4 pages, including figures, bibliography, apendices) must be submitted electronically in PDF format at: https://www.easychair.org/conferences/?conf=lenls9 When his/her abstract is accepted, the author is expected to submit a full paper (10-14 pages) before the workshop. The proceedings of the workshop will be available at the conference site for registered persons. Important dates: ================ Abstract submission deadline: September 1, 2012 Notification of acceptance: October 10, 2012 Deadline for camera-ready copy: October 31, 2012 Deadline for onsite registration: November 24, 2012 LENLS 9: December 01-02, 2012 Tutorial Lecture (by Hans Kamp): December 03, 2012 Workshop Organizers/Program Committee: ====================================== - Alastair Butler (PRESTO JST/Tohoku University) - Daisuke Bekki (Ochanomizu University) - Eric McCready (Aoyama Gakuin University) - Koji Mineshima (Keio University) - Yoshiki Mori (University of Tokyo) - Yasuo Nakayama (Osaka University) - Katsuhiko Sano (Japan Advanced Institute of Science and Technology) - Katsuhiko Yabushita (Naruto University of Education) - Tomoyuki Yamada (Hokkaido University) - Shunsuke Yatabe (National Institute of Advanced Industrial Science and Technology) - Kei Yoshimoto (Tohoku University)

1 0

RIMS研究集会（集合論関連）
by Yo Matsubara 21 May '12

21 May '12

南山大学の宮元さんのご依頼で代理投稿させていただきます．　　　　　　　　　　　　　　　　　松原洋 ----------------------------------------------------- 各位研究集会のお知らせを申し上げます。 RIMS研究集会:　強制法による拡大と巨大基数日程：2012年12月4日（火）午後〜12月7日（金）午前会場：京都大学数理解析研究所 111号室予定されるゲストスピーカー: David Aspero (ウィーン大学、オーストリア) Boban Velickovic(パリ大学、フランス）また、詳細は以下にお願いし、更新する予定です。 http://www2.kobe-u.ac.jp/~hsakai/RIMS2012/index_ja.html 世話人: 宮元　忠敏 (南山大学経営学部) 電子メール: miyamoto(a)nanzan-u.ac.jp

1 0

2nd CFP: CPP 2012 - 2nd International Conference on Certified Programs and Proofs
by Jacques Garrigue 18 May '12

18 May '12

The deadline for submitting to CPP 2012 is June 8, 2012. The Second International Conference on Certified Programs and Proofs (CPP 2012) CALL FOR PAPERS Kyoto, Japan December 13-15 2012 http://cpp12.kuis.kyoto-u.ac.jp/ co-located with APLAS 2012 http://aplas12.kuis.kyoto-u.ac.jp/ CPP is a new international forum on theoretical and practical topics in all areas, including computer science, mathematics, and education, that consider certification as an essential paradigm for their work. Certification here means formal, mechanized verification of some sort, preferably with production of independently checkable certificates. We invite submissions on topics that fit under this rubric. The first CPP conference was held in Kenting, Taiwan during December 7-9, 2011. As with the first meeting, the proceedings will be published in Springer-Verlag's Lecture Notes in Computer Science series. Suggested, but not exclusive, specific topics of interest for submissions include: certified or certifying programming, compilation, linking, OS kernels, runtime systems, and security monitors; program logics, type systems, and semantics for certified code; certified decision procedures, mathematical libraries, and mathematical theorems; proof assistants and proof theory; new languages and tools for certified programming; program analysis, program verification, and proof-carrying code; certified secure protocols and transactions; certificates for decision procedures, including linear algebra, polynomial systems, SAT, SMT, and unification in algebras of interest; certificates for semi-decision procedures, including equality, first-order logic, and higher-order unification; certificates for program termination; logics for certifying concurrent and distributed programs; higher-order logics, logical systems, separation logics, and logics for security; teaching mathematics and computer science with proof assistants; and "Proof Pearls" (elegant, concise, and instructive examples). IMPORTANT DATES: Authors are required to submit a paper title and a short abstract before submitting the full paper. The submission should include when necessary a url where to find the formal development assessing the essential aspects of the work. All submissions will be electronic. All deadlines are at midnight (GMT). Abstract Deadline: Friday, June 8, 2012 Paper Submission Deadline: Friday, June 15, 2012 Author Notification: Monday, August 27, 2012 Camera Ready: Monday, September 17, 2012 Conference: December 13-15, 2012 PROGRAM CO-CHAIRS: Chris Hawblitzel (Microsoft Research Redmond) Dale Miller (INRIA Saclay and LIX, Ecole Polytechnique) GENERAL CHAIR: Jacques Garrigue (Nagoya University) PROGRAM COMMITTEE: Stefan Berghofer (secunet Security Networks AG) Wei-Ngan Chin (National University of Singapore) Adam Chlipala (MIT) Mike Dodds (University of Cambridge) Amy Felty (University of Ottawa) Xinyu Feng (University of Science and Technology of China) Herman Geuvers (Radboud University, Nijmegen) Robert Harper (Carnegie Mellon University) Chris Hawblitzel (Microsoft Research Redmond) Gerwin Klein (NICTA) Laura Kovacs (Vienna University of Technology) Dale Miller (INRIA Saclay and LIX, Ecole Polytechnique) Rupak Majumdar (UCLA, Max Planck Institute for Software Systems) Lawrence Paulson (University of Cambridge) Frank Piessens (KU Leuven) Randy Pollack (Harvard and Edinburgh University) Bow-Yaw Wang (Academia Sinica) Santiago Zanella Béguelin (IMDEA Software Institute) ORGANIZING COMMITTEE: Jacques Garrigue and Atsushi Igarashi Email: cpp2012oc(a)math.nagoya-u.ac.jp CPP STEERING COMMITTEE: Andrew Appel (Princeton University) Nikolaj Bjørner (Microsoft Research Redmond) Georges Gonthier (Microsoft Research Cambridge) John Harrison (Intel Corporation) Jean-Pierre Jouannaud (co-Chair) (INRIA and Tsinghua University) Gerwin Klein (NICTA) Tobias Nipkow (Technische Universität München) Zhong Shao (co-Chair) (Yale University) SUBMISSION INSTRUCTIONS: Papers should be submitted electronically online via the conference submission web page at URL: http://www.easychair.org/conferences/?conf=cpp2012 Acceptable formats are PostScript or PDF, viewable by Ghostview or Acrobat Reader. Submissions should not exceed 16 pages in LNCS format, including bibliography and figures. Submitted papers will be judged on the basis of significance, relevance, correctness, originality, and clarity. They should clearly identify what has been accomplished and why it is significant. The proceedings of the symposium will be published as a volume in Springer-Verlag’s Lecture Notes in Computer Science series. Each submission must be written in English and provide sufficient detail to allow the program committee to assess the merits of the paper. It should begin with a succinct statement of the issues, a summary of the main results, and a brief explanation of their significance and relevance to the conference, all phrased for the non-specialist. Technical and formal developments directed to the specialist should follow. Whenever appropriate, the submission should come along with a formal development, using whatever prover, e.g., Agda, Coq, Elf, HOL, HOL-Light, Isabelle, Matita, Mizar, NQTHM, PVS, Vampire, etc. References and comparisons with related work should be included. Papers not conforming to the above requirements concerning format and length may be rejected without further consideration. The results must be unpublished and not submitted for publication elsewhere, including the proceedings of other published conferences or workshops. The PC chairs should be informed of closely related work submitted to a conference or journal in advance of submission. Original formal proofs of known results in mathematics or computer science are among the targets. One author of each accepted paper is expected to present it at the conference.

1 0

EASLLC 2012
by Hiroakira Ono 17 May '12

17 May '12

East-Asian School on Logic, Language, and Computation (EASLLC 2012) Southwest University, Chongqing, China, August 27-31, 2012 http://home.hib.no/prosjekter/easllc2012/ This is a school for graduate students and postdoctoral scholars, similar in spirit to the annual ESSLLI summer schools in Europe and also to the Sino-European Summer School on Logic, Language, and Computation, which took place in Guangzhou, China in December 2010. - The program of EASLLC 2012 will consist of nine courses in three different tracks: logic, language, and computation. · Logic Track: Fenrong Liu (Tsinghua University), Rohit Parikh (Brooklyn College of CUNY and CUNY Graduate Center), Jouko Väänänen (University of Helsinki and University of Amsterdam) · Language Track: Pauline Jacobson (Brown University), Geoffrey K. Pullum (University of Edinburgh and Brown University), Dag Westerståhl (Stockholm University) · Computation Track: Krzysztof R. Apt (CWI and University of Amsterdam), Phokion G. Kolaitis (University of California Santa Cruz and IBM Research ? Almaden), Moshe Y. Vardi (Rice University) - There will be student sessions in the late afternoon/early evening of some days of the School in which students will give short presentations of work in progress. Students are invited to submit an abstract of maximum 3 pages on any topic in logic, language and computation. The abstract should be written properly in English, and must be in PDF format and be submitted to our EasyChair website<https://www.easychair.org/conferences/?conf=easllc2012stus>. * Important Dates:* May 28, 2012 - deadline for short abstracts of papers (at most 3 pages) June 10, 2012 - notification date of acceptance/rejection of the papers Detailed information about the student session can be found at http://home.hib.no/prosjekter/easllc2012/stusess.asp EASSLC 2012 is an ASL-Sponsored Meeting. ASL offers student travel awards ? for details, please see http://aslonline.org/studenttravelawards.html - Prior to the School, an International Conference will take place on August 25 and 26, Scientific Organization: - Program Committee Chair: Phokion G. Kolaitis - Program Committee co-Chairs: Xiangdong He (Southwest University), Jouko Väänänen, Dag Westerståhl Local Organization: - Meiyun Guo (Southwest University), Minghui Ma (Southwest University), Jing Wang (Southwest University), Xiaojia Tang (Southwest University) Student Program Organization: - Chair: Yi Wang (Bergen University College) - Co-Chair: Fan Yang (University of Helsinki)

1 0

Talk by Bart Jacobs (Radboud U. Nijmegen), Tue 15 May 2012
by Ichiro Hasuo 11 May '12

11 May '12

みなさま，こんにちは！東京大学の蓮尾と申します．来週 5/15（火）に，現在滞在中の Bart Jacobs さん (Radboud U. Nijmegen) にご講演いただきます．詳細は下記のとおりです．タイトルに「量子」とありますが，量子論理等の知識がなくても，categorical logic の話として聞いていただけるはずです．ぜひ！参加登録等は必要ありませんが，部屋の都合で人数の見積もりをしたいので， - 当研究室のセミナーにはじめておいでになる方は， - こちら http://www.doodle.com/7zsyhidh2r478xyk に参加表明をいただけるとうれしいです．（ペンネームでかまいません）お目にかかれること，楽しみにしております．それでは！蓮尾一郎東京大学大学院情報理工学系研究科コンピュータ科学専攻 http://www-mmm.is.s.u-tokyo.ac.jp ======================================================================= Tue 15 May 2012, 16:40-18:10 Bart Jacobs (Radboud U. Njimegen, http://www.cs.ru.nl/~bart/) New directions in quantum logic 場所：東京大学本郷キャンパス理学部7号館1階 102教室（アクセス： http://www-mmm.is.s.u-tokyo.ac.jp/ の一番下を見てください） The talk will use categorical techniques to give a new way of representing predicates that is especially suited for "quantitative" predicate logic. The relevant structure is illustrated for classical, probabilistic and quantum logic. These new predicates give rise to fibred/indexed categories. In the quantum case the Born rule appears as a form of substitution. Predicates can also be used to specify measurements in this setting.

1 0

Call for Participation: HOR'12, Nagoya
by Makoto Hamana 08 May '12

08 May '12

皆様、今月末RTA併設の、高階書換系ワークショップHOR'12の参加ご案内です。今年はスペシャルセッションとして、停止性自動検証ツールの最新成果のセッションを設けました。特に応用として - Haskell - Isabelle のプログラムの停止性検証ツール、および高階書換え系の停止性ツール制作者に、実装とその理論を発表していただきます。また論文発表の一つには、IBMでの実際のコンパイラにおける高階書換えの応用プロジェクト(Kristoffer Rose氏)の話題などもあり、関数型言語、定理証明系などの利用者にも有用な情報になると思いますので、関連研究者の皆様は、ぜひ参加をご検討ください。レギュラーレジストレーション〆切は明日5/9ですが、直接会場での参加費払いも可能です。ワークショップのみでも参加可能で、でしたら当日でも参加費はほとんど変わりませんし、RTA参加者でしたら同じです。同日併設のツリーオートマタのTTATTワークショップ登録の方は、両方参加できますので、部分的な参加でも歓迎です。 -- 浜名誠/群馬大学 ===================================================================== Call for Participation 6th International Workshop on Higher-Order Rewriting HOR 2012 June 2, 2012, Nagoya, Japan Colocated with RTA'12 http://www.cs.gunma-u.ac.jp/events/hor/ ====================================================================== Invited speaker --------------- * Zhenjiang Hu (National Institute of Informatics, Japan) Can Graph Transformation be Bidirectionalized? -- Bidirectional Semantics of Structural Recursion on Graphs -- Special Session: Current Status of Higher-Order Termination Tools ----------------------------------------------------------------- * Carsten Fuhs: Haskell termination tool * Rene Thiemann: Isabelle termination tool * Aoto,Yamada: Simply-typed TRS termination tool * Cynthia Kop: WANDA, termination tool for AFS Accepted papers ---------------- * Beniamino Accattoli and Delia Kesner: The permutative lambda-calculus (The original paper was presented at LPAR'12, LNCS 7180, pp.381-395) * Thibaut Balabonski: A Unified Approach to Fully Lazy Sharing (The original paper was presented at POPL'12, pp.233-246) * Yuki Chiba and Takahito Aoto: Pattern Matching Algorithm for Higher Order Program Transformations * Jean-Pierre Jouannaud and Jian-Qi Li: Termination of higher-order rewriting in dependent type calculi * Vincent van Oostrom: Confluence via Critical Valleys * Kristoffer Rose: Higher Order Rewriting for Real Programmers

1 0

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Logic-ml May 2012