Kisoron-ml January 2016

2 participants
2 discussions

Tenth NII Type Theory Workshop
by Makoto Tatsuta 30 Jan '16

30 Jan '16

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(a)nii.ac.jp)

1 0

SLS 2016：Vaught予想他
by Tanaka Kazuyuki 10 Jan '16

10 Jan '16

皆様冬の恒例行事となりました仙台ロジックスクールSLSを本年も下記の日程で開催致します。２０１６年１月２８日（木）～２９日（金）東北大学理学部青葉山キャンパス合同C棟１階多目的室（サイエンスホールでない方）備考：昨年１２月に地下鉄東西線が開通しましたので、仙台駅から青葉山駅まで１０分足らずで着き、会場の理学部合同C棟は青葉山駅を出てすぐの所にあります（１階にセブン・イレブンが見える建物）。今回は主なチュートリアルとして、カリフォルニア大学バークレー校のMontalban先生に、最近話題になっている「Vaught予想」への計算可能性理論からの取り組みについてご紹介いただくことになっています。また、シンガポール南洋大学の呉国華先生には、 automatic sequences と transcendence property についてご講演いただく予定です。この他にもいくつか研究発表などを計画しています。時間割の詳細などは、遅くなって申し訳ありませんが、１月２０日頃ウェブサイトでご案内致します。 http://www.sendailogic.com/SLS2016/index_J.html 講演会自体は無料ですが、会場や懇親会等の付加的準備の都合上、ご参加を予定される方は下記アドレスまで一言ご連絡くだされば幸いです。連絡先：sendailogicschool[at]gmail.com 尚、私は海外出張中のため、お問い合わせにはすぐお応えできないかもしれませんが、どうぞ悪しからず。広い分野から気楽なご参加をお待ちしております。田中一之

1 0

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Kisoron-ml January 2016