Talk slots are by default either 30 min. or 45 min. long.
プログラム詳細
2013/9/24 （火）
10:30-10:45 オープニング
Session 1 (Chair: 星野直彦）
10:45-11:15 浅田和之 (東京大学 情報理工学系研究科) タイトル未定
アブストラクト未定
11:15-12:00 本浦 庄太 (京都大学 数理解析研究所) On the Semantic Meaning of Reduction Axioms in Public Announcement Logic
Public
announcement logic is a branch of modal logic which studies change of
knowledge caused by announcements. In the logic we express a state of
knowledge by a Kripke model and change of knowledge by transformation of
Kripke models. Public annoucement logic has a complete axiomatization
PAL which contains special axioms called reduction axiomx. In this talk
we give completeness between subsystems of PAL and natural classes of
Kripke models and clarify the semantic meanings of reduction axioms. At
the last of this talk, we give an alternative proof to the completeness
of PAL as a corollary.
12:00-13:15 昼食
Session 2 (Chair: 中澤 巧爾）
13:15-14:00 菊池健太郎 (東北大学 電気通信研究所) Non-deterministic CPS-translation for lambda-mu calculus
We
give an alternative solution to the erasing-continuation problem
(Nakazawa and Tatsuta 2003) on proving strong normalisation for
lambda-mu calculus, using a non-deterministic translation into Klop's
extended lambda calculus.
14:00-14:30 木戸 肩吾 (東京大学 情報理工) An Alternative Denotational Semantics for WHILE^dt
WHILE^dt,
an imperative language with infinitesimals, is introduced in (Suenaga
and Hasuo, ICALP2011) to model hybrid systems. In that paper, a
denotational semantics for the command while is defined using the idea
of sectionwise execution. It is not a straightforward extension of that
of the WHILE language. We define an alternative denotational semantics
as a straightforward extension using *-transform of the existence of the
least fixed point.
14:30-14:45 休憩
Session 3 (Chair: 古澤 仁）
14:45-15:15 松田直祐 (東京工業大学 情報理工) ChurchーRosser性の証明とその進展
ラ
ムダ計算のシステム λβ のChurch-Rosser性の証明は，Tait, Martin-Lof によるparallel
reductionの使用を機に，証明の簡略化が進んだ．また， M.Takahashi
による証明の簡略化も有名なところである．これらの証明の思想を推し進め，Church-Rosser性の証明の更なる簡略化を図る．
15:15-15:45 山本華子 (お茶の水女子大学 人間文化創成科学研究科、理学専攻) Neighborhood-Sheaf Semantics of First-Order Conditional Logic
In
this study,we define the neighborhood-sheaf semantics (NSS) of VC^+, a
first-order conditional logic system [Priest 2008, chapter 5 and 19].
NSS was proposed in [Kishida 2011]. Additionally, we prove that the
traditional Kripke semantics of VC^+ can be constructed in terms of NSS.
Neighborhood semantics is more general than Kripke semantics because it
allows a family of sets of possible worlds `near' a certain world to
have more than two members. On the other hand, Kripke semantics of
conditional logic uses special Kripke frames in which accessibility
relations of a world vary depending on formula. This special frame is
properly represented by NSS.
15:45-16:15 本多健太郎 (東京大学 情報理工) Towards Quantum Pseudo-telepathic Game Semantics
In
contrast to classical physics, quantum theory is known to be
essentially non-local. A pseudo-telepathy game is a dialogue game to
study such non-locality. We formalise this game in terms of
game-semantics, which preserves some theorems in pseudo-telepathy games.
16:15-16:30 休憩
Session 4 (Chair: 塚田 武志）
16:30-17:00 関根 大剛 (東京大学 情報理工) Nakano's Modal Type System for Guarded Recursion
Nakano’s
λ●μ-calculus and modal type system enable us to assert convergence of
some kind of self-referencing programs. His framework is applicable
to stream-processing programs (reactive programs).
In this talk, I explain about Nakano’s framework and its application to
stream-processing programs by Krishnaswami and Benton.
17:00-17:45 佐藤雅大 (名古屋大学 多元数理科学研究科) Intuitionistic Model of CIC
CIC is a type theory of Coq.
It is known that there is no complete model of CIC because of impredicative type 'Prop'.
But, there is non complete model of CIC, in which PEM is hold.
I'll talk about I tried to construct a new intuitionistic model of CIC.
18:30- 懇親会
2013/9/25 （水）
Session 1 (Chair: 小林 聡）
10:30-11:00 蓮尾 一郎 (東京大 情報理工) Coinductive Predicates and Final Sequences in a Fibration
Coinductive
predicates express persisting “safety” specifications of transition
systems. Previous observations by Hermida and Jacobs identify
coinductive predicates as suitable final coalgebras in a fibration—a
categorical abstraction of predicate logic. In this paper we follow the
spirit of a seminal work by Worrell and study final sequences in a
fibration. Our main contribution is to identify some categorical “size
restriction” axioms that guarantee stabilization of final sequences
after omega steps. In its course we develop a relevant categorical
infrastructure that relates fibrations and locally presentable
categories, a combination that does not seem to be studied a lot. The
genericity of our fibrational framework can be exploited for: binary
relations (i.e. the logic of “binary predicates”) for which a
coinductive predicate is bisimilarity; constructive logics (where
interests are growing in coinductive predicates); and logics for
name-passing processes.
Reference: Ichiro Hasuo,
Kenta Cho, Toshiki Kataoka, and Bart Jacobs. Coinductive Predicates and
Final Sequences in a Fibration. To appear in Proc. MFPS XXIX, 2013.
11:00-11:30 長谷川真人 (京都大学 数理解析研究所) Traced *-autonomous categories are compact closed
For
years we have been bothered by a small mistery on categorical models of
Linear Logic (*-autonomous categories) and Geometry of Interaction
(compact closed categories, typically arising from traced monoidal
categories via Int-construction): Is there a proper intermediate
structure between *-autonomous categories and compact closed categories,
that is, a traced *-autonomous category which is not compact closed? We
settle this issue by showing that any traced *-autonomous category is
actually compact closed.
This talk is based on a joint work with Tamas Hajgato.
11:30-12:00 吉田聡 (鳥取環境大学 人間形成教育センター) 構成的解析学における超関数の空間の弱位相について
アブストラクト未定
12:00-13:15 昼食
Session 2 (Chair: 長谷川 真人）
13:15-13:45 中野圭介 (電気通信大学 情報理工学研究科) Repetitive right applications of B terms
The combinator B = λfgx.f(g x) is well-known as a 'bracketing' combinator or a composition operator. Interestingly, the repetitive right applications of B form a cycle of period 4 after 10-fold applications. This behavior, we call ρ-property due to the shape of the cycle, can be observed also in a specific form of B terms constructed from only B combinators. In this talk, I will show when a B term does NOT have the ρ-property through several equational laws for B.
13:45-14:30 片岡俊基 (東京大学 情報理工) Homotopy Type Theory の紹介
アブストラクト未定
14:30-14:45 休憩
Session 3 (Chair: 鴨 浩靖）
14:45-15:30 吉村 和人 (北陸先端科学技術大学院大学 情報科学研究科) From Weihrauch lattice, Toward Logic
Weihrauch
lattice is a degree structure whose underlying reducibility requires
uniform computability. V. Brattka proposed to classify
non-constructive principles in Weihrauch lattice. The previous
results of Brattka's classification project suggest a close connection
between Weihrauch lattice analysis and constructive reverse
mathematics. If such a connection was established once, it would
bring useful separation techniques on constructive reverse mathematics
likewise various degree structures are broadly used in
Friedman-Simpson's reverse mathematics. We show some new results
in this direction which utilize a foundation from categorical logic: 1. a
sound and complete semantics for restricted formulae of a logic
enritched type theory; 2. a sound semantics for restricted formulae of
logic enriched type theory whose logical part is resource
sensitive. Those results enable us to translate separation results
in Weihrauch lattice (or in its variants) to separation results on
constructive reverse mathematics.
15:30-16:00 藤原 誠 (東北大学 理学研究科) 逆数学における一様証明可能性と直観主義証明可能性
存在定理「任意に与えられた問題Xに対して条件を満たす解Yが存在する」の証明において, 問題Xに対する解Yの構成法が, 場合分け等により一様に与えられず, それぞれ異なる場合がある.
このような非一様証明は「数学の議論において存在はその構成によって示されるべき」とする直観主義の立場では認められない.
近年, 逆数学における存在定理の一様証明可能性の解析が、その定理の直観主義証明不可能性の解析に寄与することを示す理論的結果(メタ定理)が得られている.
これらのメタ定理の証明はProof interpretationと呼ばれる証明論の手法に基づく.
本講演では, 新しく得られた結果を含め, これらのメタ定理を概観する.
16:00-16:15 休憩
Session 4 (Chair: 蓮尾 一郎）
16:15-17:15 塚田 武志 (東京大学 情報理工）Invited Tutorial on Game Semantics
アブストラクト未定
17:15-18:00 議論
2013/9/26 （木）
Session 1 (Chair: 星野 直彦）
10:00-10:30
滝坂 透 (京都大学 数理解析研究所) On two definitions of quantum Kolmogorov complexity
In the early
2000s, several definitions of quantum Kolmogorov complexity (QKC) were
proposed. QKC is expected to be a useful tool for analyzing quantum states
(e.g. quantum entanglement) or to be the foundation of the theory of “quantum
randomness”.
Definitions of
QKC by Berthiaume et al. and Gács are two of the major ones. Berthiaume et al.
defines QKC based on the notion of a quantum Turing machine, that is, a
probabilistic Turing machine which allows amplitudes of a computable complex
number, of which transition function can be expressed by a unitary operator. Gács
approaches QKC by defining a universal semi-density matrix, a quantum analogue
of a universal semimeasure.
It can be
expected that there is some relationship between these two definitions which
extends Levin’s coding theorem to quantum domain. We review some facts about them
to see what should be done to examine this relationship. In particular, we see
the modification of Gács’ definition to an infinite dimensional case and some
problem about it.
10:30-11:00 倉永崇 (名古屋大学 多元数理科学) タイトル未定
アブストラクト未定
11:00-11:30 只野 誉 (大阪大学大学院 理学研究科 数学専攻) タイトル未定
アブストラクト未定
11:30-11:45 休憩
Session 2 (Chair: 蓮尾 一郎）
11:45-12:15 三好博之 (京都産業大学 理) タイトル未定
アブストラクト未定
12:15-12:45 浦本 武雄 (京都大学 理学研究科数学教室) An Equationally Definable Model for KAT
The
equational system of Kleene algebras with tests (KAT) was introduced by
Kozen, which is a conservative extension of KA, the equational system
of Kleene algebras. Similarly to the classical result that KA is
deductively complete to the algebra R of regular languages, Kozen and
Smith proved that there exists a certain language-theoretic model G of
KAT to which KAT is deductively complete. However, the critical
difference between R and G is that G does not have non-trivial subclass
definable by a set of pseudo identities in the sense of Polak, while R
does. This issue prevents us from applying a traditional algebraic
method in combinatorics of regular languages to decision problems of
optimizing combinatorial complexity of KAT terms. In this talk, we first
prove the existence of an equationally definable language-theoretic
model for KAT, to which KAT is deductively complete and which is
isomorphic to G under a decidable isomorphism. After that, as a
demonstration, we prove the decidability of whether Boolean conditionals
in a given KAT term can be moved out externally by using the first
result.
