皆様
ルートヴィヒ・マクシミリアン大学ミュンヘンのJosef Berger先生、および
スワンジー大学のAnton Setzer先生・Bashar Igriedさんの講演のお知らせです。
どうぞふるってご参加ください。
問合せ先:
石原 哉
北陸先端科学技術大学院大学 情報科学系
e-mail: ishihara(a)jaist.ac.jp
-----------------------------------------------
* JAIST Logic Seminar Series *
* The lectures below are held as a part of JSPS Core-to-Core Program,
A. Advanced Research Networks, and EU FP7 Marie Curie Actions IRSES
project CORCON.
(http://www.jaist.ac.jp/logic/ja/core2core, https://corcon.net/)
Date: Tuesday 6 September, 2016, 13:30-17:00
Place: JAIST, Lecture room I2
(Access: http://www.jaist.ac.jp/english/location/access.html)
*LECTURE 1*
Speaker: Josef Berger (Ludwig-Maximilians-Universität München)
Title: The fan theorem and convexity (joint work with Gregor Svindland)
Abstract:
The fan theorem is the following statement:
(FAN) Let B be a decidable set of finite binary sequences.
Assume that every infinite binary sequence
has an initial part that belongs to B.
Then there exist an N such that every infinite binary
sequence has an initial part of length smaller than N
that belongs to B.
This axiom plays an important role in Intuitionism,
a philosophy of mathematics that was introduced by
the Dutch mathematician L.E.J. Brouwer. We work
in constructive mathematics in the tradition of Errett Bishop.
Here, the fan theorem is neither provable nor falsifiable.
Many theorems of analysis are equivalent
to the fan theorem. One example for such a theorem is:
(POS) Every positive-valued uniformly continuous function
on the unit interval has positive infimum.
In our paper 'Convexity and constructive infamy’ we have shown that,
under the additional condition of convexity of the function, POS is
constructively valid.
In this talk, we discuss to which extent this gives rise to
a notion of 'convex bars' and a corresponding constructively
valid 'convex fan theorem'.
*LECTURE 2*
Speaker: Anton Setzer and Bashar Igried (Swansea University)
Title: Coinductive Reasoning in Dependent Type Theory - Copatterns,
Objects, Processes
(part on Processes joint work with Bashar Igried)
Abstract:
When working in logic in computer science, one is very often confronted
with bisimulation. The reason for its importance is that in computer
science, one often reasons about interactive or concurrent programs.
Such programs can have infinite execution paths, and therefore
correspond to coinductive data types. The natural equality on coinductive
data types is bisimulation. Proofs of bisimulation form one of the main
principles for reasoning about coinductive data types.
However, bisimulation is often very difficult to understand and to teach.
This is in contrast to the principle of induction, where
there exists a well established tradition of carrying out proofs by
induction.
One goal of this talk is to demonstrate that one can reason about
coinductive data types in a similar way as one can reason inductively
about inductive
data types.
Reasoning about inductive data types can be done by pattern matching.
For instance
for reasoning about natural numbers one makes a case distinction on
whether the
argument is 0 or a successor. For coinductive data types the dual is
copattern
matching, which is essentially a case distinction on the observations
one can make for a coinductively defined set. For instance, streams have
observations head and tail, and one can introduce a stream by determining
its head and its tail.
We then look at examples of the use of coinductive data types. One is
the notion of an object, as it occurs in object-oriented program.
Objects are defined by their method calls, which are observations, so they
are defined coinductively. The final example will be the representation
of processes in dependent type theory, where we will refer
to the process algebra CSP.
皆様
(複数受け取られた場合はご容赦下さい)
シンポジウムとサマースクールの案内を転送いたします.
宮部
---------- Forwarded message ----------
International Symposium on Computability and Complexity
(in honour of Rod Downey's 60th birthday), and
Summer School in Mathematical Logic
In early 2017, Victoria University of Wellington will be hosting a
Computability and Complexity Symposium. These areas have seen
significant development in recent years. The purpose of this symposium
is to bring together a wide cross-section of researchers in the area,
from leading researchers to graduate students, to discuss these
developments and future directions. The symposium will take place
between the 5th and 8th of January 2017 at the town of Raumati, a
short drive from Wellington. For details and updates please see
http://sms.victoria.ac.nz/Events/CCS2017/WebHome
After the symposium, a summer school in mathematical logic will take
place in Napier, between the Monday 9th and Saturday 14th of January
2017. The topic is mathematical logic and computability. We plan to
have five tutorial series, the level aimed at graduate students. The
speakers will be:
• Denis Hirschfeldt (Chicago)
• Jack Lutz (Iowa State)
• Maryanthe Malliaris (Chicago)
• Antonio Montalban (UC Berkeley)
• Hugh Woodin (Harvard)
Details can be found at http://sms.victoria.ac.nz/Events/NZMRI2017/WebHome
We anticipate receiving NSF funding in early October to help cover the
travel cost of US-based researchers and students. To apply for this
funding please email Peter Cholak, at cholak(a)nd.edu, by October 15.
We are particularly interested having women, minorities, students and
postdocs apply. We are working on getting ASL sponsorship. Students
also can apply to the ASL for travel support.
Please share with your colleagues and students and postdocs. Sorry if
you received multiple copies of this.
--
Kenshi Miyabe
email (research) : research(a)kenshi.miyabe.name
email (other) : miyabe(a)meiji.ac.jp
Senior Assistant Professor
Department of Mathematics
School of Science and Technology
Meiji University
Tel: +81-44-934-7460
皆様
早稲田大学の藤原誠です。
以下の要領で研究集会
Computability Theory and Foundations of Mathematics 2016
(2016年9月20日(火)~9月21日(水)、早稲田大学国際会議場)
を開催いたします。
講演を希望される方は8月31日までに以下に沿って講演要旨をお送り下さい。
(締切日が迫ってからの連絡となってしまい申し訳ありません。)
http://www.sendailogic.com/CTFM2016/submission.html
本研究集会への参加は自由ですが、20日夜の懇親会に参加される方は9月12日までに以下より参加登録をお願いいたします。
準備の都合上、懇親会に参加されない方も事前に参加登録をしていただけると助かります。
http://www.sendailogic.com/CTFM2016/registration.html
詳しくは下記ホームページをご覧ください。
http://www.sendailogic.com/CTFM2016/
本研究集会に関するお問い合わせは以下へお願いいたします。
ctfm2016[at]fastmail.com
どうぞよろしくお願いいたします。
==============================================================
Computability Theory and Foundations of Mathematics 2016
Waseda University, Tokyo, Japan, September 20 - 21, 2016
http://www.sendailogic.com/CTFM2016/
==============================================================
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, Set Theory, Philosophy of
Mathematics, Constructive Mathematics, Theory of Randomness and
Computational Complexity Theory.
This is the sixth conference of the CTFM conference series:
http://www.jaist.ac.jp/CTFM/CTFM_SERIES/
This conference is supported by the Waseda Insitute for Advanced Study
and JSPS KAKENHI Grant Numbers JP26540001 and JP15H03634.
-------------------------------------------------------------------------------------------------------------------------
Invited speakers:
• David Belanger (National University of Singapore)
• Chi Tat Chong (National University of Singapore)
• Daisuke Ikegami (Tokyo Denki University)
• Wei Li (National University of Singapore)
• Kenshi Miyabe (Meiji University)
• Paul Shafer (Ghent University)
• Frank Stephan (National University of Singapore)
• Philip Welch (University of Bristol)
• Guohua Wu (Nanyang Technological University)
• Takeshi Yamazaki (Tohoku University)
• Yang Yue (National University of Singapore)
-------------------------------------------------------------------------------------------------------------------------
Submission deadline for presentations:
August 31, 2016
-------------------------------------------------------------------------------------------------------------------------
Registration deadline:
September 12, 2016.
(It will still be possible to register for the conference after the deadline, but in that case the participant cannot attend the banquet.
The banquet will be held on September 20 (18:30-20:30), at the same place as the conference venue.)
-------------------------------------------------------------------------------------------------------------------------
Organising Committee:
Makoto Fujiwara (Waseda University, co-chair)
Florian Pelupessy (Tohoku University)
Kazuyuki Tanaka (Tohoku University, co-chair)
Toshimichi Usuba (Waseda University)
Keita Yokoyama (JAIST)
============================================
藤原 誠 (Makoto Fujiwara)
早稲田大学高等研究所
(Waseda Institute for Advanced Study, Waseda University)
E-mail: makoto_fujiwara(a)aoni.waseda.jp
============================================