[kisoron-ml] Eighth NII Type Theory Workshop

[Makoto Tatsuta]

		   Eighth NII Type Theory Workshop

Date: February 6, 2013, 10:40--16:50

Place: National Institute of Informatics, Room 1904 (19th floor)
場所: 国立情報学研究所 19階 1904室
    (半蔵門線,都営地下鉄三田線・新宿線 神保町駅または東西線 竹橋駅より徒歩5分)
    (地図 http://www.nii.ac.jp/about/access/)

Program:

10:40--11:20 Toshihiko Uchida (The Graduate University for Advanced Studies)
Title: A Partial Translation from lambda U to lambda 2

11:20--12:00 Daisuke Kimura (National Institute of Informatics)
Title: Linear Pure Type Systems

12:00--14:00 Lunch Break

14:00--14:40 Kazuyuki ASADA (National Institute of Informatics)
Title: Curry-Howard Correspondence between Dialectica Interpretation
and Bidirectional Transformation

14:40--15:20 Makoto Tatsuta (National Institute of Informatics)
Title: Dual Calculus with Inductive and Coinductive Types

15:20--15:50 Tea Break

15:50--16:50 Stefano Berardi (Torino University)
Title: A Curry-Howard result for various subclassical logics

Abstracts:
----------------------------------------------------------------------
Toshihiko Uchida (The Graduate University for Advanced Studies)
Title: A Partial Translation from lambda U to lambda 2

Abstract: Girard showed that every type of sort * (i.e., proposition)
is inhabited in lambda U. Barendregt state without proof that every
type of sort Box (i.e., domain) is also inhabited in the system. In
this talk, we show that the second statement is not the case by giving
a partial translation from lambda U to lambda 2.
----------------------------------------------------------------------
Daisuke Kimura (National Institute of Informatics)
Title: Linear Pure Type Systems

Abstract: This talk proposes a linear variant of Pure Type Systems
(PTSs), called linear pure type systems (LPTSs). It is a general
framework, which provides a uniform way to treat various linear type
systems that have the features of linear logic. We first introduce a
subframework of LPTSs, called multiplicative linear pure type systems
(MLPTSs), in which only variables that linearly occur are
abstracted. All MLPTSs are consistent and satisfy strong
normalization. However their expressive power is rather weak. We then
give LPTSs by extending MLPTSs with exponentials. Each PTS can be
embedded into a LPTS. We also show the equivalence of strong
normalizability of PTSs and LPTSs by giving mutual translations
between them.
----------------------------------------------------------------------
Kazuyuki ASADA (National Institute of Informatics)
Title: Curry-Howard Correspondence between Dialectica Interpretation
and Bidirectional Transformation

Abstract: We give Curry-Howard style correspondence between
(propositional logic part of) Dialectica interpretation and
bidirectional transformation.  Dialectica interpretation was
introduced by Godel to show relative consistency of Heyting Arithmetic
to System T. Independently, bidirectional transformation arose in
database community for automatic view-update problem, and recently
have been studied in programming language community to formulate
languages for bidirectional transformations. A bidirectional
transformation consists of a pair of forward ("usual") transformation
and a backward ("inverse") transformation, and we usually assume that
they satisfy some standard axioms called GetPut law and PutGet law. We
show GetPut law naturally fits the above correspondence to Dialectica
interpretation, and this gives a way of extending a language for
bidirectional transformations with GetPut law. Then we modify the
above scheme for PutGet law and the combination of GetPut and PutGet
laws. We also show that Paiva's variant of Dialectica model, GC,
corresponds to the category for inverse computation. Then for the
result by Paiva that the original Dialectica category is the coKleisli
category of some comonad on GC, we give similar result for PutGet law,
and we utilize this to investigate further categorical structures of
these models. Also we see that a kind of Diller-Nahm variant of
Dialectica interpretation corresponds to backward-partial
bidirectional transformation.
----------------------------------------------------------------------
Makoto Tatsuta (National Institute of Informatics)
Title: Dual Calculus with Inductive and Coinductive Types

Abstract: This talk gives an extension of Dual Calculus by
introducing inductive types and coinductive types.  The same duality
as Dual Calculus is shown to hold in the new system, that is, this
talk presents its involution for the new system and proves that it
preserves both typing and reduction.  The duality between inductive
types and coinductive types is shown by the existence of the
involution that maps an inductive type and a coinductive type to each
other.  The strong normalization in this system is also proved.
First, strong normalization in second-order Dual Calculus is shown by
translating it into second-order symmetric lambda calculus. Next,
strong normalization in Dual Calculus with inductive and coinductive
types is proved by translating it into second-order Dual Calculus.
This is a joint work with Daisuke Kimura.
----------------------------------------------------------------------
Stefano Berardi (Torino University)
Title: A Curry-Howard result for various subclassical logics

Abstract: We introduce games with Sequential Backtracking as a model
for various sub-classical logic that have implication as a primitive
connective. We define a one-sided version of the logical systems,
whose proofs have a tree isomorphism (a kind of ``Curry Howard''
isomorphism) with respect to the winning strategies of the game
semantics. We use this correspondence to interpret various classical
proofs as learning algorithms.
----------------------------------------------------------------------

問合せ先　龍田 (tatsuta at nii.ac.jp)