[kisoron-ml] Ninth NII Type Theory Workshop

[Makoto Tatsuta]

		    Ninth NII Type Theory Workshop

Date: January 15, 2015, 10:20--17:30

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

Program:

10:20--11:00 Daisuke Kimura (National Institute of Informatics)
Title: A framework of models of functional PTSs

11:00--11:40 Josh Ko (National Institute of Informatics)
Title: Relational algebraic ornamentation

11:40--13:10 Lunch Break

13:10--13:50 Makoto Fujiwara (Tohoku University)
Title: On the strength of ¥Delta^0_1-LEM over Intuitionistic Analysis

13:50--14:30 Koji Nakazawa (Kyoto University)
Title: Confluence of lambda-calculi with permutative conversion

14:30--14:50 Break

14:50--15:30 Mahmudul Faisal Al Ameen (The Graduate University for
Advanced Studies)
Title: Completeness of Separation Logic with Recursive Procedures

15:30--16:10 Makoto Tatsuta (National Institute of Informatics)
Title: Decidability of Separation Logic with Monadic Inductive Definitions

16:10--16:30 Break

16:30--17:30 Stefano Berardi (Torino University)
Title: Realizability and Strong Normalization for Heyting Arithmetic
with EM1

Abstracts:
----------------------------------------------------------------------
Daisuke Kimura (National Institute of Informatics)
Title: A framework of models of functional PTSs

Abstract: This talk presents a framework of models of functional PTSs.
The class of functional PTSs is a class of PTS which contains
well-known type theories such as the simply typed lambda calculus,
System F, lambda P (dependent type system), and Calculus of
Constructions.  This framework of models is obtained by using
Cousineau and Dowek's embedding from a functional PTS into a lambda P
modulo.  As a result of this talk, a semantical condition for a
functional PTS to be a strongly normalizing system is given.  This
result is expected to give a semantical approach to
Barendregt-Geuvers-Klop conjecture.
----------------------------------------------------------------------
Josh Ko (National Institute of Informatics)
Title: Relational algebraic ornamentation

Abstract: Type theory makes it possible to treat programs and proofs
uniformly as the same entities.  Dependently typed programmers aim to
design programs that carry their own correctness proofs, exploiting
the coincidence of programs and proofs to the full extent.  A generic
construction that can help to achieve this is relational algebraic
ornamentation, with which we can synthesise datatypes satisfying
properties that can be expressed in terms of folds.  In this talk I
will show how relational algebraic ornamentation can help with
designing a dependently typed program for solving the well-known
minimum coin change problem.
----------------------------------------------------------------------
Makoto Fujiwara (Tohoku University)
Title: On the strength of ¥Delta^0_1-LEM over Intuitionistic Analysis

Abstract: Ishihara [2] showed over intuitionistic analysis EL that
Markov’s principle MP is equivalent to WMP+¥Pi^0_1-DML(under the name
of MP^v).  On the other hand, Akama et al. [1] showed that
¥Delta^0_1-LEM is implied from both of MP(under the name of
¥Sigma^0_1-DNE) and ¥Sigma^0_1-DML(under the name of ¥Sigma^0_1-LLPO).
In this talk, we show over EL that ¥Delta^0_1-LEM is implied from
¥Pi^0_1-DML and equivalent to ¥Delta^0_1 comprehension axiom, which is
from reverse mathematics.  In addition, some separation results are
also presented.  This is a joint work with Hajime Ishihara and Takako
Nemoto.
References:
[1] Y. Akama, S. Berardi, S. Hayashi and U. Kohlenbach, An
arithmetical hierarchy of the law of excluded middle and related
principles. Proc. of the 19th Annual IEEE Symposium on Logic in
Computer Science (LICS'04), pp. 192--201, IEEE Press (2004).
[2] H. Ishihara, Markov's principle, Church's thesis and Lindel¥"of
theorem, Indag. Math. (N.S.) 4 (1993), pp. 321--325.
----------------------------------------------------------------------
Koji Nakazawa (Kyoto University)
Title: Confluence of lambda-calculi with permutative conversion

Abstract: We give a new proof of confluence for the lambda and the
lambda-mu calculi with permutative conversion for case branching. For
such calculi, naive approaches with parallel reductions do not work,
and we adopt a proof technique with generalized notions of complete
development with the Z property, introduced by Dehornoy and van
Oostrom.  Our idea also gives a simpler proof for confluence of the
first-order classical natural deduction, which has been proved by Ando
with more complicated notions.
----------------------------------------------------------------------
Mahmudul Faisal Al Ameen (The Graduate University for Advanced Studies)
Title: Completeness of Separation Logic with Recursive Procedures

Abstract: This talk proves the completeness of Hoare's Logic extended
by separation logic for verification of while programs with pointers
and recursive procedures.
----------------------------------------------------------------------
Makoto Tatsuta (National Institute of Informatics)
Title: Decidability of Separation Logic with Monadic Inductive Definitions

Abstract: This talk shows the decidability of entailments of symbolic
heaps in separation logic with monadic inductive definitions under
certain conditions.
----------------------------------------------------------------------
Stefano Berardi (Torino University)
Title: Realizability and Strong Normalization for Heyting Arithmetic
with EM1

Abstract: We present a new Curry-Howard correspondence for HA+EM1,
first order constructive Heyting Arithmetic with the excluded middle
on Sigma-0-1-formulas. We add to the lambda calculus an operator k_a
which represents, from the viewpoint of programming, an exception
operator with a delimited scope, and from the viewpoint of logic, a
restricted version of the excluded middle. We motivate the restriction
of the excluded middle by its use in proof mining; we introduce new
techniques to prove strong normalization for HA + EM1 and the witness
property for simply existential statements.  One may consider our
results as an application of the ideas of Interactive realizability,
which we have adapted to the new setting and used to prove our main
theorems. This technique has been recently extended by F. Aschieri to
the entire excluded middle for First Order Arithmetic.  This is a
joint work with F. Aschieri and G. Birolo.
----------------------------------------------------------------------

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