皆様、
(重複してお受け取りになられた場合はご容赦ください)
産業技術総合研究所の武山と申します。この場をお借りしまして
来年1月22日にPOPL 2013に併設して開催される国際ワークショップ
PLPV 2013のCFPをご案内させていただきます。
プログラミング言語とプログラム検証に跨る話題について、
幅広く多くの研究コミュニティーからの論文投稿をお待ちしておりますので、
ご検討いただけますようよろしくお願い申し上げます。
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
The Seventh ACM SIGPLAN Workshop
on
Programming Languages meets Program Verification (PLPV 2013)
http://plpv.tcs.ifi.lmu.de/
22nd January, 2013
Rome, Italy
(Affiliated with POPL 2013)
Call for Papers
Overview
The goal of PLPV is to foster and stimulate research at the
intersection of programming languages and program verification, by
bringing together experts from diverse areas like types, contracts,
interactive theorem proving, model checking and program analysis. Work
in this area typically attempts to reduce the burden of program
verification by taking advantage of particular semantic or structural
properties of the programming language. One example are dependently
typed programming languages, which leverage a language's type system
to specify and check rich specifications. Another example are
extended static checking systems which incorporate contracts with
either static or dynamic contract checking.
We invite submissions on all aspects, both theoretical and practical,
of the integration of programming language and program verification
technology. To encourage interaction between different
communities, we seek a broad scope for PLPV. In particular,
submissions may have diverse foundations for verification (based on
types, Hoare-logic, abstract interpretation, etc), target
different kinds of programming languages (functional, imperative,
object-oriented, etc), and apply to diverse kinds of program
properties (data structure invariants, security properties, temporal
protocols, resource constraints, etc).
Important Dates
Submission 8th October, 2012 (Monday)
Notification 1st November, 2012 (Thursday)
Final Version 8th November, 2012 (Thursday)
Workshop 22nd January, 2013 (Tuesday)
Submissions
We seek submissions of up to 12 pages related to the above
topics; shorter submissions are also welcome. Submissions may describe
new work, propose new challenge problems for language-based
verification techniques, or present a known idea in an elegant way
(i.e., a pearl).
Submissions should be prepared with SIGPLAN two-column conference
format. Submitted papers must adhere to the SIGPLAN republication
policy. Concurrent submissions to other workshops, conferences,
journals, or similar forums of publication are not allowed.
To submit a paper, access the online submission site at
http://www.easychair.org/conferences/?conf=plpv2013.
Publication
Accepted papers will be published by the ACM and will appear in the
ACM Digital library.
Program Committee
Andreas Abel Ludwig-Maximilians-University Munich (co-chair)
Robert Atkey University of Strathclyde
Harley Eades The University of Iowa
Chung-Kil Hur Max Planck Institute for Software Systems
Brigitte Pientka McGill University
Andrew Pitts University of Cambridge
François Pottier INRIA
Tim Sheard Portland State University (co-chair)
Makoto Takeyama Advanced Industrial Science and Technology
--
Makoto Takeyama <makoto.takeyama(a)aist.go.jp>
AIST/RISEC (National Institute of Advanced Industrial Science and Technology /
Research Institute for Secure Systems)
tel: +81-6-6494-8045
皆様:
神戸大学の酒井拓史と申します.
8月1日(水)に開催される
Kobe Colloquium on Logic, Statistics and Informatics
のアナウンスをさせていただきます.
ご興味をお持ちの方は是非ご参加ください:
------------------------------------------------------
Kobe Colloquium on Logic, Statistics and Informatics:
------------------------------------------------------
August 1, 2012 (Wed.) 16:30 - 18:00 (teabreak: 15:30 -)
``Topological Set Theory''
Dr. Andreas Fackler (LMU Munich)
Abstract
The idea behind positive set theory is to weaken the naive comprehension
principle by omitting all instances in which negation occurs. For example, the
universal class V is a set while the Russell class is not. Surprisingly, this
approach leads to a theory in which V is a topological space in a natural way.
Inspired by that fact, topological set theory TS instead of a comprehension
principle has as its axioms several topological statements about V. Topological
and positive set theory are closely related and in both of them there is an
interesting interplay between the set theoretic and topological properties of
V. Many basic theorems of TS remain true even without the axiom that the
universal class V is a set, although one decisive statement about the ordinal
numbers goes missing. Instead, a surprising connection to another familiar set
theory arises ...
In my talk, I will present this family of axiom systems and give an overview of
results about their implications, their consistency strengths, and their
interrelations. We will also look briefly at their (known) models --
topological structures called hyperuniverses -- and at methods to construct
such objects.
------------------------------------------------------------------------------
The talk will be given in the presentation room of the group of Logic,
Statistics and Informatics (inside the glass door with "Fuchino group"
(written in Japanese) on the 4th floor in the Sience and Technology Building 3
http://kurt.scitec.kobe-u.ac.jp/~brendle/Forcing2012/university.jpg
in Rokkodai Campus of Kobe University)
There will be a dinner after the talk.
酒井 拓史
神戸大学大学院
システム情報学研究科 講師
e-mail: hsakai(a)people.kobe-u.ac.jp
tel: 078-803-6245
筑波大学の石川竜一郎さんからの依頼により、代理でご案内を投稿します。
国際ワークショップ:
International Workshop on Game Theory, Epistemic Logic, & Related Topics
が8月27日から30日まで、筑波大学で開かれます。
詳しくは
http://infoshako.sk.tsukuba.ac.jp/~ishikawa/gamelogic12/
をご覧ください。
宜しくお願い致します。
鈴木信行@静岡大学
Logic-ml $B$N3'MM!$(B
$B$3$s$P$s$O!$ElKLBg3X$NKYH*2B9($G$9!%(B
7$B7n(B20$BF|!J6b!K$KElKLBg3X$K$F2<5-%;%_%J!<$r9T$$$^$9$N$G!$6=L#$N$"$kJ}$O$<$R$4;22C$/$@$5$$!%(B
$BFs9V1i$4$6$$$^$9!%(B
*************************************************************************
$BF|;~!'(B7$B7n(B20$BF|!J6b!K(B15:30$B!A(B17:00
$B>l=j!'ElKLBg3X(B $BKL@DMU;3%-%c%s%Q%9(B $BM}3X9gF1Eo(B 1201$B9f<<(B
$B-!(B15:30$B!A(B16:00
$B9V1i<T!'(B $B;3:j!!Ip(B $B!J(B $BElKLBg3XBg3X1!!&M}3X8&5f2J(B $B!K(B
$B%?%$%H%k!'(B The Optimal Bounded Marriage Theorem
$B%"%V%9%H%i%/%H!'(B
J. Hirst showed that WKL_0 is equivalent over RCA_0 to the assertion
that every bounded marriage problem satisfying Hall condition has a
solution. In this talk, arranging the result, we mainly prove that
ACA_0 is equivalent over RCA_0 to the assertion that every bounded
marriage problem of the finite total utility satisfying Hall condition
has an optimal solution.
$B-"(B16:00$B!A(B17:00
$B9V1i<T!'(B $B2,K\(B $B7=;K(B $B!J@gBf9bEy@lLg3X9;!&Am9g2J3X7O!K(B
$B%?%$%H%k!'(B $BL?BjMMAj&L7W;;$N0l3,3HD%$K$D$$$F(B
$B%"%V%9%H%i%/%H!'(B
$BK\H/I=$G$O!$0l3,MMAj&L7W;;(B($BL?BjMMAj&L7W;;$N0l3,3HD%(B)$B$H$=$N<~JU>u67$K$D$$$F2r@b$9$k!%$^$:!$0l3,MMAj&L7W;;$r9=C[$9$k$K;j$kGX7J$H$7$F!$7A<0<jK!$K$D$$$F=R$Y$k!%(B
$B<!$K!$L?BjMMAj&L7W;;$H0l3,=R8lO@M}$r9g$o$;$F!$0l3,MMAj&L7W;;$rDj5A$9$k!%$=$N8e!$0l3,MMAj&L7W;;$N@-<A$N$&$A!$40A4@-$HI=8=NO$K$D$$$F=R$Y$k!%$5$i$K!$0l3,MMAj&L7W;;$NE,MQNc$H$7$F!$%;%^%U%)$K$h$kAj8_GS=|$NBEEv@->ZL@$r>R2p$9$k!%:G8e$K!$$^$H$a$H4XO"2]Bj$N>R2p$r9T$&!%(B
*************************************************************************
$B0J>e$G$9!%(B
$B%;%_%J!<>pJs$N>\:YEy$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