皆様
9月にオーストリアで開催される「合流性に関するワークショップ IWC 2016」の 論文募集をご案内致します。今回は TRS Meeting, WST, LC&A との合同開催と なっております。関連する話題をお持ちの方は、ぜひ投稿をご検討下さい。
廣川 (JAIST)
===================================================================== Call for Papers IWC 2016 5th International Workshop on Confluence
Sep 8-9, 2016, Obergurgl, Austria, Part of Computational Logic in the Alps, CLA 2016
http://www.csl.sri.com/~tiwari/iwc2016/ =====================================================================
Confluence provides a general notion of determinism and is widely viewed as one of the central properties of rewriting. Confluence relates to many topics of rewriting (completion, modularity, termination, commutation, etc.) and had been investigated in many formalisms of rewriting such as first-order rewriting, lambda-calculi, higher-order rewriting, constrained rewriting, conditional rewriting, etc. Recently there is a renewed interest in confluence research, resulting in new techniques, tool support, certification as well as new applications. The International Workshop on Confluence (IWC) aims at promoting further research in confluence and related properties. IWC 2016 is part of the Computational Logic in the Alps event to be held in Obergurgl, Austria, during the week Sep 4-10, 2016. Previous editions of the workshop were held in Nagoya (2012), Eindhoven (2013), Vienna (2014), and Berlin (2015). During the workshop, the 5th Confluence Competition (CoCo 2016) takes place.
IMPORTANT DATES: * submission June 22, 2016 * notification July 12, 2016 * final version Aug 03, 2016 * workshop Sep 8-9, 2016
TOPICS: Specific topics of interest include: * confluence and related properties (unique normal forms, commutation, ground confluence) * completion * critical pair criteria * decidability issues * complexity issues * system descriptions * certification * applications of confluence
INVITED SPEAKERS: * TBD
PROGRAM COMMITTEE: * Beniamino Accattoli (INRIA) * Bertram Felgenhauer (University of Innsbruck) * Yves Guiraud (University of Paris 7) * Nao Hirokawa (JAIST) * Koji Nakazawa (Nagoya) * Ashish Tiwari (Menlo Park)
SUBMISSION: We solicit short papers or extended abstracts of at most five pages. There will be no formal reviewing. In particular, we welcome short versions of recently published articles and papers submitted elsewhere. The program committee checks relevance and may provide additional feedback. The accepted papers will be made available electronically before the workshop.
The page limit for papers is 5 pages in EasyChair style. Short papers or extended abstracts must be submitted electronically through the EasyChair system at: https://www.easychair.org/conferences/?conf=iwc2016
現在筑波大学で上記について講義を 行っていますが、それの講義Notesを 筑波大学のRepositoryに置いていきますので、 ご案内しておきます。
https://tsukuba.repo.nii.ac.jp/?action=pages_view_main&active_action=rep...
にしむら 筑波大学 数学
追伸:オマケです。手持無沙汰な折にどうぞ。
まだ第4回目の講義録をupしていませんが、 ここまでで
depdendent type theory with intensional identities
がどんなものかは感触はつかめたと思うので、 第5回からはそれのModelがどのようなものかの 感触をつかんでもらうことを目指します。 古典的なCategory theoryをざっと復習した後、 higher categoriesとは何なのか、どんなものでなければ いけないか、といった点を理解してもらうつもりです。 Higher categoriesも一昔前は
そこへ踏み込んではいけない、泥沼に 足をとられるから、
と言われたものですが、今は逆にhigher categoriesなしでは 21世紀の数学を語ることができないと言える状況だと 思います。たとえば
http://www.math.harvard.edu/~lurie/papers/highertopoi.pdf
や
https://webusers.imj-prg.fr/~frederic.paugam/documents/enseignement/master-m...
をご覧ください。後者については私のreviewを
https://www.ems-ph.org/journals/journal.php?jrn=news
を今年の3月号でご覧いただけます。Spaceの関係で 全文を載せられなかったので、 それは筑波大学のRepositoryにおいています。
https://tsukuba.repo.nii.ac.jp/?action=pages_view_main&active_action=rep...
その後、∞ーgroupoidsの織り成す世界が上記の
depdendent type theory with intensional identities
のModelにほぼなっているという話をします。”ほぼ”と いったのは、とりあえずcoherenceの問題は捨象して という意味です。
これは強調されていることですが、上記の
depdendent type theory with intensional identities
はdecidableです。これはTaitの方法で簡単に 示すことができます。しかし
Homotopy type theory
と言った場合は、そこにunivalence axiomが入ってきますから、 これがdecidabilityを破壊してしまわないかは、まだ未解決問題です。 もしもこれが破壊してしまうという話になると homotopy type theoristsの間に激震が走るでしょう。 その衝撃はGödelが不完全定理でHilbertの第2問題に 対して与えた衝撃に匹敵すると思います。 皆さん、そんなことはありえないとかなり楽天的に 構えています。
にしむら
追伸:オマケです。手持無沙汰な折にでもどうぞ。
https://www.youtube.com/watch?v=ibjTE5LsN1U
現在筑波大学で上記について講義を 行っていますが、それの講義Notesを 筑波大学のRepositoryに置いていきますので、 ご案内しておきます。
https://tsukuba.repo.nii.ac.jp/?action=pages_view_main&active_action=rep...
にしむら 筑波大学 数学
追伸:オマケです。手持無沙汰な折にどうぞ。
https://www.youtube.com/watch?v=RpppLxnESaU
Logic-ml mailing list [email protected] http://www.fos.kuis.kyoto-u.ac.jp/cgi-bin/mailman/listinfo/logic-ml
$B>/$7JdB-$7$F$*$-$^$9!#(B
$B-!!!(BHilbert$B$NBh#2LdBj$H$$$&$N$O#13,=R8lO@M}$GDj<02=(B $B$5$l$?<+A3?tO@$r4^$`$h$&$J8xM}7O!J$H$/$K(BZFC$B!K$O(Bdecidable$B$+$H(B $B$$$&LdBj$G!"$3$l$K$D$$$F$O(BGodel$B$NIT40A4@-DjM}$GH]DjE*$K2r7h$5$l$F(B $B$$$^$9!#$7$+$7$3$N(BHilbert$B$NBh#2LdBj$r0ULu$7$F(B
$B?t3X$N4pAC$E$1$H$7$F;H$($k7A<0E*BN7O$G(Bdecidable$B$J$b$N$O(B $BB8:_$9$k$+!)(B
$B$H$9$k$H!"$=$l$OB8:_$7$F$^$5$K(BHomotopy Type Theory (HTT)$B$,(B $B$=$&$G$"$k$H$$$&$N$,!"2f!9$NN)>l$J$N$G!"K|0l$3$l$,(Bdecidable$B$G$J$$(B $B$H$$$&$3$H$K$J$k$H!"7c?L$,Av$k$H8@$C$?$N$O!"$=$&$$$&0UL#$G$9!#(B $B$A$J$_$K(B
dependent type theory with extensional identities
$B$O(Bundecidable$B$G$9!#(B
$B-"!!(BHigher categories$B$OJ*M}3X$G$b$9$4$/4pK\E*$G!"(B $B$3$l$K$D$$$F$O0J2<$N(BSurvey$B$r$4Mw$/$@$5$$!#(B
https://zbmath.org/?q=an:1236.81006
$B$K$7$`$i(B $BC^GHBg3X(B $B?t3X(B
$BDI?-!'%*%^%1$G$9!#<j;}$AL5:;BA$J@^$K$G$b$I$&$>!#(B
https://www.youtube.com/watch?v=iugcK5rZueE
$B$^$@Bh#42sL$N9V5AO?$r(Bup$B$7$F$$$^$;$s$,!"(B $B$3$3$^$G$G(B
depdendent type theory with intensional identities
$B$,$I$s$J$b$N$+$O46?($O$D$+$a$?$H;W$&$N$G!"(B $BBh#52s$+$i$O$=$l$N(BModel$B$,$I$N$h$&$J$b$N$+$N(B $B46?($r$D$+$s$G$b$i$&$3$H$rL;X$7$^$9!#(B $B8EE5E*$J(BCategory theory$B$r$6$C$HI|=,$7$?8e!"(B higher categories$B$H$O2?$J$N$+!"$I$s$J$b$N$G$J$1$l$P(B $B$$$1$J$$$+!"$H$$$C$?E@$rM}2r$7$F$b$i$&$D$b$j$G$9!#(B Higher categories$B$b0l@NA0$O(B
$B$=$3$XF'$_9~$s$G$O$$$1$J$$!"E%>B$K(B $BB-$r$H$i$l$k$+$i!"(B
$B$H8@$o$l$?$b$N$G$9$,!":#$O5U$K(Bhigher categories$B$J$7$G$O(B $B#2#1@$5*$N?t3X$r8l$k$3$H$,$G$-$J$$$H8@$($k>u67$@$H(B $B;W$$$^$9!#$?$H$($P(B
http://www.math.harvard.edu/~lurie/papers/highertopoi.pdf
$B$d(B
https://webusers.imj-prg.fr/~frederic.paugam/documents/enseignement/master-m...
$B$r$4Mw$/$@$5$$!#8e<T$K$D$$$F$O;d$N(Breview$B$r(B
https://www.ems-ph.org/journals/journal.php?jrn=news
$B$r:#G/$N#37n9f$G$4Mw$$$?$@$1$^$9!#(BSpace$B$N4X78$G(B $BA4J8$r:$;$i$l$J$+$C$?$N$G!"(B $B$=$l$OC^GHBg3X$N(BRepository$B$K$*$$$F$$$^$9!#(B
https://tsukuba.repo.nii.ac.jp/?action=pages_view_main&active_action=rep...
$B$=$N8e!"!g!<(Bgroupoids$B$N?%$j@.$9@$3&$,>e5-$N(B
depdendent type theory with intensional identities
$B$N(BModel$B$K$[$$J$C$F$$$k$H$$$&OC$r$7$^$9!#!I$[$!I$H(B $B$$$C$?$N$O!"$H$j$"$($:(Bcoherence$B$NLdBj$O<N>]$7$F(B $B$H$$$&0UL#$G$9!#(B
$B$3$l$O6/D4$5$l$F$$$k$3$H$G$9$,!">e5-$N(B
depdendent type theory with intensional identities
$B$O(Bdecidable$B$G$9!#$3$l$O(BTait$B$NJ}K!$G4JC1$K(B $B<($9$3$H$,$G$-$^$9!#$7$+$7(B
Homotopy type theory
$B$H8@$C$?>l9g$O!"$=$3$K(Bunivalence axiom$B$,F~$C$F$-$^$9$+$i!"(B $B$3$l$,(Bdecidability$B$rGK2u$7$F$7$^$o$J$$$+$O!"$^$@L$2r7hLdBj$G$9!#(B $B$b$7$b$3$l$,GK2u$7$F$7$^$&$H$$$&OC$K$J$k$H(B homotopy type theorists$B$N4V$K7c?L$,Av$k$G$7$g$&!#(B $B$=$N>W7b$O(BGödel$B$,IT40A4DjM}$G(BHilbert$B$NBh#2LdBj$K(B $BBP$7$FM?$($?>W7b$KI$E($9$k$H;W$$$^$9!#(B $B3'$5$s!"$=$s$J$3$H$O$"$j$($J$$$H$+$J$j3ZE7E*$K(B $B9=$($F$$$^$9!#(B
$B$K$7$`$i(B
$BDI?-!'%*%^%1$G$9!#<j;}L5:;BA$J@^$K$G$b$I$&$>!#(B
https://www.youtube.com/watch?v=ibjTE5LsN1U
$B8=:_C^GHBg3X$G>e5-$K$D$$$F9V5A$r(B $B9T$C$F$$$^$9$,!"$=$l$N9V5A(BNotes$B$r(B $BC^GHBg3X$N(BRepository$B$KCV$$$F$$$-$^$9$N$G!"(B $B$40FFb$7$F$*$-$^$9!#(B
https://tsukuba.repo.nii.ac.jp/?action=pages_view_main&active_action=rep...
$B$K$7$`$i(B $BC^GHBg3X(B $B?t3X(B
$BDI?-!'%*%^%1$G$9!#<j;}L5:;BA$J@^$K$I$&$>!#(B
https://www.youtube.com/watch?v=RpppLxnESaU
Logic-ml mailing list [email protected] http://www.fos.kuis.kyoto-u.ac.jp/cgi-bin/mailman/listinfo/logic-ml
Logic-ml mailing list [email protected] http://www.fos.kuis.kyoto-u.ac.jp/cgi-bin/mailman/listinfo/logic-ml