[logic-ml] NII Type Theory Workshop

[Makoto Tatsuta]

		   Seventh NII Type Theory Workshop


Date: February 6, 2012, 13:00--17:00

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

Program:

13:00--13:30 Daisuke Kimura (National Institute of Informatics)
Title: A generalized modal lambda calculus

13:30--14:00 Kazuyuki Asada (National Institute of Informatics)
Title: Semantics of Multi-rooted Graph with Ordered Branch

14:00--14:20 Tea Break

14:20--15:00 Makoto Tatsuta (National Institute of Informatics)
Title: Type Inference for Bimorphic Recursion

15:00--15:40 Yukiyoshi Kameyama (University of Tsukuba)
Title: Pseudo-Classical Modal Logic for Staged Computation

15:40--16:00 Tea Break

16:00--17:00 Stefano Berardi (Torino University)
Title: A Game Semantic for various Subclassical Logics

Abstracts:
----------------------------------------------------------------------
Daisuke Kimura (National Institute of Informatics)
Title: A generalized modal lambda calculus

Abstract: In this talk, we introduce a lambda calculus with modal
types. The types of this system contain information of possible worlds
explicitly.  This information can be considered as a position which is
an abstraction of time or place.  The feature of our calculus is that
we can change the property of modalities by changing information about
the relationship between positions.  The aim of our research is the
following: (1) To clarify the computational meaning of necessity and
possibility modal operators.  (2) To give a uniform framework that can
treat several calculi with modal types.
----------------------------------------------------------------------
Kazuyuki Asada (National Institute of Informatics)
Title: Semantics of Multi-rooted Graph with Ordered Branch

Abstract: Buneman et al. introduced a graph transformation language
UnCAL, where graph has bisimilarity semantics.  There structural
recursion plays an important role, and in order to define it, they
introduced multi-rooted graph and its algebraic representation.  In
this talk we give coalgebraic semantics for multi-rooted graph, and
see that such final coalgebras has some call-by-value structure. Then
we introduce a CBV equational theory.  Next we modify the results of
graph with un-ordered branch to that with ordered branch, which is
important for application to XML.  For this ordered graphs,
bisimilarity is defined in some subtle way, but we can use the ordered
version of above CBV equational theory for reasoning of the
bisimilarity between ordered graphs.
----------------------------------------------------------------------
Makoto Tatsuta (National Institute of Informatics)
Title: Type Inference for Bimorphic Recursion

Abstract: This talk proposes bimorphic recursion, which is restricted
polymorphic recursion such that every recursive call in the body of a
function definition has the same type.  Bimorphic recursion allows us
to assign two different types to a recursively defined function: one
is for its recursive calls and the other is for its calls outside its
definition.  Bimorphic recursion in this talk can be nested.  This
talk shows bimorphic recursion has principal types and decidable type
inference.  Hence bimorphic recursion gives us flexible typing for
recursion with decidable type inference.  This talk also shows that
its typability becomes undecidable because of nesting of recursions
when one removes the instantiation property from the bimorphic
recursion. This is a joint work with Ferruccio Damiani.
----------------------------------------------------------------------
Yukiyoshi Kameyama (University of Tsukuba)
Title: Pseudo-Classical Modal Logic for Staged Computation

Abstract: In this talk, we study a pseudo-classical modal logic, which
corresponds to the staged calculus with control operators introduced
by our earlier work.  Staged computation is a means for run-time code
generation, and has been proved useful in improving efficiency and
maintainability of software.  We are interested in the use of control
operators in staged computation, since they play an essential role to
avoid the code duplication problem.  Combining a staged calculus with
control operators in a naive way results in an unsound calculus, and
we need a restriction on the typing rule for lambda.  We show that
this restriction has a logical counterpart similar to Nakano's
catch/throw calculus.
----------------------------------------------------------------------
Stefano Berardi (Torino University)
Title: A Game Semantic for various Subclassical Logics

Abstract: In this talk we describe the state of the art of game
semantics for Logic and lambda-calculus, and the motivations for
having a game semantics. Then we define a game semantic for
Intuitionism extending both Coquands and Hyland-Ongs game
semantics. The semantics refines a paper of TLCA 2007. We have two
kind of results: (1) (Soundness and Completeness) The recursive
winning strategy of our game semantics are isomorphic to the cut-free
proofs of some variant of HA-omega (Infinitary Intuitionistic
Arithmetic) (2) (Cut Elimination) Any debate between two terminating
strategies terminates. This is an ongoing joint work with M. Tatsuta.
----------------------------------------------------------------------

連絡先
龍田 真 (国立情報学研究所)