Kobe Colloquium on Logic, Statistics and Informatics
以下の要領でコロキウムを開催します。
日時:2012年12月10日(月)13:20-14:50
場所:神戸大学自然科学総合研究棟3号館4階421室(プレゼンテーション室)
講演者:David Aspero (Technische Universitaet Wien, Austria)
========================================================================
題目:Some set theory with restricted choice
アブストラクト:I am planning to present the proofs of three theorems involving set
theory without the Axiom of Choice or with just restricted forms of AC. One
is an observation of mine concerning very large cardinals in a ZF context,
another one is a result from a paper by P. Larson and Shelah, and another
one a result of Shelah from [Sh835].
========================================================================
交通:阪急六甲駅またはJR六甲道駅から神戸市バス36系統「鶴甲団地」
行きに乗車,「神大本部工学部前」停留所下車,徒歩すぐ.
http://www.kobe-u.ac.jp/info/access/rokko/rokkodai-dai2.htm
連絡先:ブレンドレ ヨーグ brendle(a)kurt.scitec.kobe-u.ac.jp
みなさま、
こんにちは。産総研の北村崇師と申します。
本研究所の Cyrille Artho に代わり、ポスドク募集のご案内させて頂きます。
応募のご検討、及び、関係各位へのご周知をいただけますと幸いです。
====================================================
Post-doc position available at AIST Kansai: Test generation/optimization
====================================================
Research related to:
• Test generation using model-based testing/constraint solving.
• Test case minimization using heuristics like delta debugging.
Start: 2013 (ideally April, but can be adjusted).
Duration: 1 year (extensible dep. on evaluation and restrictions below).
• Location: AIST Amagasaki, Japan (20 minutes from Osaka);
Research Institute for Secure Systems, System Life-cycle Group.
http://www.risec.aist.go.jp/
• Requirements:
– Ph.D.at the time when the contract starts;
degree must have been awarded less than 7 years ago.
– Strong know-how in software analysis and algorithms.
– Experience with Java or Scala, and C.
– Good written and spoken communication in English.
• If interested, please submit your résumé with your publications
and a list software projects in which you have participated.
• Contact:[email protected]
--
Takashi KITAMURA
t.kitamura(a)aist.go.jp, http://staff.aist.go.jp/t.kitamura/
Research Institute for Secure Systems (RISEC)
National Institute of Advanced Industrial Science and Technology (AIST)
[Apologies for multiple copies]
Dear all,
I am pleased to announce the 55th Tokyo Programming Seminar,
which will be held at NII on December 18th (Tue).
Oleg Kiselyov
Non-deterministic choice in a conventional programming language:
Enough for logic programming?
Hugo Pacheco
Bidirectional Data Transformation by Calculation
A detailed program is attached below.
I'm looking forward to meeting you at the seminar.
Best regards,
Kazuyuki Asada
----
The 55th ToPS
http://takeichi.ipl-lab.org/~tops/upcoming_seminar.html
Time:
December 18th (Tue) 2012, 13:30--15:30
Place:
Rm. 1208, 12F, National Institute of Informatics
Speaker:
1. Oleg Kiselyov
Non-deterministic choice in a conventional programming language:
Enough for logic programming?
Abstract:
Logic programming is a fascinating approach, especially for AI and
natural language processing. It is greatly appealing to declaratively
state the properties of the problem and let the system find the
solution. Most intriguing is the ability to run programs `forwards'
and `backwards'.
However, the built-in search methods of logic programming systems
don't fit all problems and hardly if at all customizable. Mainly,
quite many computations and models are mostly
deterministic. Implementing them in a logic programming language is
significantly inefficient and requires extensive use of problematic
features such as cut. Another problem is interfacing logic programs
with mainstream language libraries: if mode analysis is not available
(as is often the case), one has to live with run-time instantiatedness
errors.
An alternative to logic programming, where non-determinism is default,
is a deterministic programming system (such as Scheme, OCaml, Scala or
Haskell -- or even C) with (probabilistic) non-determinism as an
option. Is this a good alternative? We explore this question. We will
use Hansei -- a probabilistic programming system implemented as a
library in OCaml -- to solve a number of classic logic programming
problems, from zebra to scheduling, to parser combinators, to reversible
type checking.
http://okmij.org/ftp/kakuritu/logic-programming.html
2. Hugo Pacheco
Bidirectional Data Transformation by Calculation
Abstract:
The advent of bidirectional programming, in recent years, has led to
the development of a vast number of approaches from various computer
science disciplines. These are often based on domain-specific
languages in which a program can be read both as a forward and a
backward transformation that satisfy some desirable consistency
properties.
Despite the high demand and recognized potential of intrinsically
bidirectional languages, they have still not matured to the point of
mainstream adoption. We contemplate some usually disregarded features
of bidirectional transformation languages that are vital for
deployment at a larger scale. The first concerns efficiency. Most of
these languages provide a rich set of primitive combinators that can
be composed to build more sophisticated transformations. Although
convenient, such compositional languages are plagued by inefficiency
and their optimization is mandatory for a serious application. The
second relates to configurability. As update translation is inherently
ambiguous, users shall be allowed to control the choice of a suitable
strategy. The third regards genericity. Writing a bidirectional
transformation typically implies describing the concrete steps that
convert values in a source schema to values a target schema, making it
impractical to express very complex transformations, and practical
tools shall support concise and generic coding patterns.
皆様
RTA 2013 の論文募集をご案内致します。今回の RTA はオランダ Eindhoven で
行われ、TLCA 2013 との共催となっています。ぜひ投稿をご検討下さい。
廣川 直 (JAIST)
*************************************************************************
RTA 2013: SECOND CALL FOR PAPERS
24th International Conference on Rewriting Techniques and Applications
June 24 - 26, 2013
Eindhoven, The Netherlands
collocated with TLCA 2013 as part of RDP 2013
http://rta2013.few.vu.nl/
*************************************************************************
abstract submission February 1 2013
paper submission February 5 2013
rebuttal period March 18-21 2013
notification April 4 2013
final version April 26 2013
*************************************************************************
The 24th International Conference on Rewriting Techniques and Applications
(RTA 2013) is organized as part of the Federated Conference on Rewriting,
Deduction, and Programming (RDP 2013), together with the 11th International
Conference on Typed Lambda Calculi and Applications (TLCA 2013), and several
workshops. RDP 2013 will be held at the Eindhoven University of Technology
in the Netherlands.
*** INVITED SPEAKERS (NEW) ***
- Simon Peyton-Jones (Microsoft Research, UK) joint invited speaker for TLCA+RTA 2013
- Jarkko Kari (University of Turku, Finland) invited speaker for RTA 2013
- Mitsu Okada (Keio University, Japan) invited speaker for RTA 2013
*** TOPICS OF INTEREST ***
RTA is the major forum for the presentation of research on all aspects of
rewriting. Typical areas of interest include (but are not limited to):
Applications: case studies; analysis of cryptographic protocols; rule-based
(functional and logic) programming; symbolic and algebraic computation;
SMT solving; theorem proving; system synthesis and verification; proof
checking; reasoning about programming languages and logics; program
transformation; XML queries and transformations; systems biology;
homotopy theory; implicit computational complexity;
Foundations: equational logic; universal algebra; rewriting logic;
rewriting models of programs; matching and unification; narrowing;
completion techniques; strategies; rewriting calculi; constraint solving;
tree automata; termination; complexity; modularity;
Frameworks: string, term, and graph rewriting; lambda-calculus and
higher-order rewriting; constrained rewriting/deduction; categorical and
infinitary rewriting; stochastic rewriting; net rewriting; binding
techniques; Petri nets; higher-dimensional rewriting;
Implementation: implementation techniques; parallel execution; rewrite and
completion tools; certification of rewriting properties; abstract
machines; explicit substitutions; automated (non)termination and
confluence provers; automated complexity analysis.
*** PUBLICATION ***
The proceedings will be published by LIPIcs (Leibniz International
Proceedings in Informatics). LIPIcs is open access, meaning that
publications will be available online and free of charge, and authors
keep the copyright for their papers. LIPIcs publications are indexed
in DBLP. For more information about LIPIcs please consult:
<http://www.dagstuhl.de/en/publications/lipics>
*** SUBMISSION GUIDELINES ***
Submissions must be
- original and not submitted for publication elsewhere,
- written in English,
- a research paper, or a problem set, or a system description,
- in pdf prepared with pdflatex using the LIPIcs stylefile:
<http://drops.dagstuhl.de/styles/lipics/lipics-authors.tgz>,
- at most 10 pages for system description,
at most 15 pages for the other two types of submissions
- submitted electronically through the EasyChair system at:
<https://www.easychair.org/conferences/?conf=rta2013>.
The page limit and the deadline for submission are strict.
Additional material for instance proof details, may be given in an appendix
which is not subject to the page limit. However, submissions must be
self-contained within the respective page limit; reading the appendix should
not be necessary to assess the merits of a submission.
*** PROGRAMME COMMITTEE CHAIR ***
Femke van Raamsdonk (VU University Amsterdam, The Netherlands)
*** PROGRAMME COMMITTEE ***
Eduardo Bonelli National University of Quilmes, Argentina
Byron Cook Microsoft Research Cambridge, UK
Stephanie Delaune ENS Cachan, France
Gilles Dowek Inria Paris-Rocquencourt, France
Maribel Fernandez King's College London, UK
Nao Hirokawa JAIST Ishikawa, Japan
Delia Kesner University Paris-Diderot, France
Helene Kirchner Inria Paris-Rocquencourt, France
Barbara Koenig University Duisburg Essen, Germany
Temur Kutsia Johannes Kepler University Linz, Austria
Aart Middeldorp University of Innsbruck, Austria
Vincent van Oostrom Utrecht University, The Netherlands
Femke van Raamsdonk VU University Amsterdam, The Netherlands
Kristoffer Rose IBM Research New York, USA
Manfred Schmidt-Schauss Goethe University Frankfurt, Germany
Peter Selinger Dalhousie University, Canada
Paula Severi University of Leicester, UK
Aaron Stump The University of Iowa, USA
Tarmo Uustalu Institute of Cybernetics Tallinn, Estonia
Roel de Vrijer VU University Amsterdam, The Netherlands
Johannes Waldmann HTWK Leipzig, Germany
Hans Zantema Eindhoven University of Technology, The Netherlands
*** CONFERENCE CHAIR ***
Hans Zantema (Eindhoven University of Technology, The Netherlands)
*** STEERING COMMITTEE ***
Mauricio Ayala-Rincon Brasilia University, Brasilia
Frederic Blanqui INRIA Tsinghua University Beijing, China
Salvador Lucas Technical University of Valencia, Spain
Georg Moser (chair) University of Innsbruck, Austria
Masahiko Sakai Nagoya University, Japan
Sophie Tison University of Lille, France
*** FURTHER INFORMATION ***
Questions related to submission, reviewing, and programme should be sent to
the programme committee chair Femke van Raamsdonk, email femke at few.vu.nl.
みなさま,
東京大学の蓮尾と申します.
来る12月18日,タリン工科大学の中田景子さんをお迎えしてご講演いただきます.
(2題,連続講演です)
詳細は以下です.ご興味のある方はぜひお越しください!
蓮尾 一郎
http://www-mmm.is.s.u-tokyo.ac.jp/
--------------------------------------------------------------------------------------------------------------
Tue 18 December 2012, 16:40-18:10
Keiko Nakata (Tallinn University of Technology), 2 titles
理学部7号館1階 102教室 Room 102, School of Science Bldg. No. 7
Title
Proving open induction using delimited control operators
Abstract
Open Induction (OI) is a principle classically equivalent to Dependent
Choice, which is, unlike the later, closed under double-negation
translation and A-translation. In the context of Constructive Reverse
Mathematics, Wim Veldman has shown that, in presence of Markov's
Principle, OI on Cantor space is equivalent to Double-negation Shift
(DNS). With Danko Ilik, we have reworked Veldman's proof to give a
constructive proof of OI, where DNS is interpreted using delimited
control operators.
Joint work with Danko Ilik.
---
Title
Walking through infinite trees with mixed induction and coinduction:
A Proof Pearl with the Fan Theorem and Bar Induction.
Abstract
We study temporal properties over infinite binary red-blue trees in
the setting of constructive type theory. We consider several familiar
path-based properties, typical to linear-time and branching-time
temporal logics like LTL and CTL*, and the corresponding tree-based
properties, in the spirit of the modal mu-calculus. We conduct a
systematic study of the relationships of the path-based and tree-based
versions of ``eventually always blueness '' and mixed
inductive-coinductive ``almost always blueness'' and arrive at a
diagram relating these properties to each other in terms of
implications that hold either unconditionally or under specific
assumptions (Weak Continuity for Numbers, the Fan Theorem, Lesser
Principle of Omniscience, Bar Induction).
Joint work with Marc Bezem and Tarmo Uustalu.
Logic-ml の皆様,
先日ご案内しました計算可能性,逆数学等に関する研究会
Computability Theory and Foundations of Mathematics (CTFM)
(2013年2月18日(月)〜2月20日(水),東京工業大学大岡山キャンパス)
http://sendailogic.math.tohoku.ac.jp/CTFM/
につきまして,講演申し込み締め切りが2013年12月18日と
なっていましたが*2012年*12月18日(火)の誤りでした.
訂正してお詫び申し上げます.
江口直日 (CTFM プログラム委員)
問い合わせ先 CTFM(a)math.tohoku.ac.jp
============================================================
Computability Theory and Foundations of Mathematics
(Tokyo Institute of Technology, Tokyo, Japan, February 18 - 20, 2013)
http://sendailogic.math.tohoku.ac.jp/CTFM/
============================================================
Computability Theory and Foundations of Mathematics (CTFM) aims to
develop computability theory and logical foundations of Mathematics. The
scope involves the topics Computability Theory, Reverse Mathematics,
Nonstandard Analysis, Proof Theory, Constructive Mathematics, Theory of
Randomness and Computational Complexity Theory.
This is a successor workshop to Workshop on Proof Theory and
Computability Theory 2012 - Philosophical Frontiers in Reverse
Mathematics (February 20 - 23, 2012, Tokyo, Japan).
--------------------------------------------
Deadline of Submission for Presentations:
December 18, 2013 /*2012*/
--------------------------------------------
Invited Speakers:
Chi Tat Chong (National University of Singapore)
Erik Palmgren (Stockholm University)
Michael Rathjen (University of Leeds)
Helmut Schwichtenberg (LMU Munich)
Stephen G. Simpson (Pennsylvania State University)
Yang Yue (National University of Singapore)
Wu Guohua (Nanyang Technological University)
--------------------------------------------
Programme Committee:
Toshiyasu Arai (Chiba)
Naohi Eguchi (Tohoku)
Hajime Ishihara (JAIST)
Ryo Kashima (Tokyo Institute of Technology)
Sam Sanders (Ghent)
Kazuyuki Tanaka (Tohoku, Co-chair)
Andreas Weiermann (Ghent, Co-chair)
Takeshi Yamazaki (Tohoku)
Keita Yokoyama (Tokyo Institute of Technology)
--------------------------------------------
皆様
東京大学の河村と申します
メーリングリストをお借りして
新学術領域研究「計算限界解明」(代表:渡辺治)の
研究員の公募(締切12月20日)について御案内させて頂きます
計算量理論の諸問題への挑戦を目標とする研究領域ですが
ウェブページにありますように数理論理学的手法も中心テーマの一つでございます
国内外を問わず皆様の周りの方々に広くお知らせ頂ければ幸いです
--
河村彰星
東京大学大学院情報理工学系研究科コンピュータ科学専攻 助教
http://www-imai.is.s.u-tokyo.ac.jp/~kawamura/index_j.html
%%%%%%%%%%%%%%%%%%%%%%%%%%%
ポスドク募集
文部科学省 科学研究費補助金 新学術領域研究
「多面的アプローチの統合による計算限界の解明」代表者:渡辺 治 (東京工業大学)
http://www.al.ics.saitama-u.ac.jp/elc/
では、下記のように4名の研究員を募集いたします。
国際公募する予定で英語での文章しかございませんが、ご容赦下さい。
よろしくお願いいたします。
---------------------------------------------------------------------
Two-year post-doctoral positions, Tokyo and Kyoto, Computation Theory
---------------------------------------------------------------------
http://www.al.ics.saitama-u.ac.jp/elc/en/?pd
The newly established Center for Exploring the Limits of Computation
(CELC, Tokyo, Japan) seeks applications for four post-doctoral fellow
positions in Computational Complexity Theory and related areas. The
appointments are for two years starting in April 2013 (or as soon as
possible). A monthly salary of approximately 350,000 Japanese yen
plus a research allowance will be offered. Applicants should hold a
PhD in theoretical computer science or related fields (or be expected
to do so by July 2013).
Two of the fellows will be based at the Tokyo site (Tokyo Institute of
Technology and the CELC) and two at the Kyoto site (Kyoto University).
Collaboration with other research groups of the ELC project (including
visits for several months) will be encouraged and supported.
Applications should include
* a curriculum vitae,
* list of publications,
* a research statement, and
* three letters of referees (to be sent directly from the referees).
Applications and letters of referees should be sent via email to
elc-pd-application(a)is.titech.ac.jp. Priority will be given to
applications received by December 20, 2012. Applicants may be invited
to an interview in early 2013 (the travel expenses will be covered).
---------
About ELC
---------
Exploring the Limits of Computation (ELC) is a five-year research
project funded by the Japanese Ministry of Education, Culture, Sports,
Science and Technology.
Project Title (formal):
A multifaceted approach toward understanding the limitations of computation
Short Title: Exploring the Limits of Computation (ELC)
Project Term: 2012.7 - 2017.3
Researchers have proposed various techniques for investigating the
limits of computation, many of which have been sharpened in depth
during the last two decades. We may soon be entering the stage of
expecting some big breakthrough results toward understanding the
limits of computation.
In this project, we investigate these techniques and relationships
among them with the goal of finding the next steps toward a big
breakthrough. We propose the following three lines of research, each
of which will be conducted by three core research groups (i.e., nine
core research groups altogether).
A. Team for pushing the current frontier of research on the limits of
computation.
B. Team for investigating the limits of computation by using various
algorithmic/optimization techniques (even by using supercomputers).
C. Team for introducing new approaches to and interpretations of the
existing techniques for investigating the limits of computation.
We also create a research center (CELC) in Tokyo for investigating
computational complexity theory by stimulating worldwide
collaborations among researchers based on our core research groups,
hosting short/long term visitors and postdoctoral researchers, and
organizing various meetings and workshops. We welcome researchers
working on subjects related to computational complexity theory to join
us for various occasions.
Project webpage
http://www.al.ics.saitama-u.ac.jp/elc/en/