[logic-ml] Tenth NII Type Theory Workshop

[Makoto Tatsuta]

		    Tenth NII Type Theory Workshop

Date: February 3, 2016, 13:30--17:00

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

Program:

13:30--14:10 Mahmudul faisal Al Ameen (National Institute of Informatics)
Title: Completeness for Recursive Procedures in Separation Logic

14:10--14:50 Daisuke Kimura (National Institute of Informatics)
Title: An Implementation of Cyclic Proof-Search in Separation Logic
with Inductive Definitions

14:50--15:00 Break

15:00--15:50 Makoto Tatsuta (National Institute of Informatics)
Title: Completeness of Cyclic Proofs for Symbolic Heaps

15:50--16:00 Break

16:00--17:00 Stefano Berardi (Torino University)
Title: Game Semantics and the Complexity of Interaction

Abstracts:
----------------------------------------------------------------------
Mahmudul faisal Al Ameen (National Institute of Informatics)
Title: Completeness for Recursive Procedures in Separation Logic

Abstract: This talk proves the completeness of an extension of
Hoare's logic and separation logic for pointer programs with mutual
recursive procedures. A new system will be discussed by introducing
two new inference rules, and removes an axiom that is unsound in
separation logic and other redundant inference rules for showing
completeness. It introduces a novel expression that is used to
describe complete information of a given state in a precondition. It
also uses the necessary and sufficient precondition of a program for
the abort-free execution, which enables us to utilize strongest
postconditions.  Admissibility of the frame rules in the system will
also be discussed.
----------------------------------------------------------------------
Daisuke Kimura (National Institute of Informatics)
Title: An Implementation of Cyclic Proof-Search in Separation Logic
with Inductive Definitions

Abstract: The entailment problem in separation logic is important for
program verification.  This talk presents a proof system for a
fragment of separation logic with inductive definitions, whose proofs
have cyclic graph structures.  The system is sound for validity of
entailments, and provides a decision procedure of entailment problem
based on proof-search of its cyclic proofs.  We implement this
decision procedure, and report the results evaluating our decision
procedure with benchmark files of SLCOMP14.
----------------------------------------------------------------------
Makoto Tatsuta (National Institute of Informatics)
Title: Completeness of Cyclic Proofs for Symbolic Heaps

Abstract: Separation logic is successful for software verification in
both theory and practice.  Decision procedure for symbolic heaps is
one of key issues.  This talk proposes a cyclic proof system for
symbolic heaps with general form of inductive definitions, and
discusses its soundness, completeness, and decidability.  The decision
procedure of entailments of symbolic heaps with inductive definitions
is also discussed.  Decidability of entailments of symbolic heaps with
inductive definitions is an important question.  Completeness of
cyclic proof systems is also an important question.  The results of
this talk tries to answer both questions. The system is based on
cyclic proof systems by Brotherston et al, and the bounded-treewidth
inductive definitions by Iosif et al.  In order for obtaining the
completeness, some restrictions are added to inductive definitions, an
entailment is extended to a multiple entailment which allows
disjunction in the succeedent, and it introduces new predicates for
describing whether a given address is in the heap or not.  The
inductive definitions under the restrictions are quite general, since
they covers doubly-linked lists, nested lists, and skip lists.  The
main techniques are grouping for showing the local completeness of the
rule of splitting separating conjunction, and normal form of multiple
entailments, which has some upper bounds for both the number of
disjuncts and the length of spatial parts.
----------------------------------------------------------------------
Stefano Berardi (Torino University)
Title: Game Semantics and the Complexity of Interaction (about a
result of Federico Aschieri)

Abstract: We present a new abstract complexity result obtained by
F. Aschieri about Coquand and Hyland-Ong game semantics, that will
lead to new bounds on the length of first-order cut-elimination,
normalization, interaction between expansion trees and any other
dialogical process game semantics can model and apply to. In
particular, Aschieri provides a novel method to bound the length of
interactions between visible strategies and to measure precisely the
tower of exponentials defining the worst-case complexity. This study
improves the old estimates by possibly several exponentials and is
based on Berardi-de'Liguoro notion of level of backtracking.
----------------------------------------------------------------------

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