１１月３０日　１３：３０ー　＠IB015

関・楫・結縁・中澤研の合同研究会は拡大ワークショップとして実施します．(今回だけ全部英語)

プログラム

1. Vasco Vasconcelos (University of Lisbon) [slides]  13:30-14:45
   Title: FreeST and the Higher-order Polymorphic Lambda Calculus [slides]

Abstract: We start with a gentle introduction to FreeST, a message-passing

concurrent functional language where communication channels are typed against

context-free session types. We then discuss the main challenges faced by FreeST:

deciding type equivalence in the presence of the sequential composition operator

on types, and its interplay with polymorphism and type operators. This is joint

work with Bernardo Almeida, Diana Costa, Andreia Mordido, and Diogo Poças.

2.  Y.Inoue [Accepted for ICCA2023] (関研) [slides] 15:00-15:30
   Title: When Is Context-Freeness Distinguishable from Regularity? An Extension of Parikh’s Theorem
   Abstract: Parikh’s theorem states that for every CFL X, there exists a regular language X′ such that X is
   Parikh equivalent to X'. As a corollary of Parikh’s theorem, it is known that every unary CFL is regular. This is because if words w and w′ are Parikh equivalent, then their lengths are also equal. In general, if an equivalence relation ≡ is coarser than Parikh equivalence, it has Parikh property; for every CFL X, there exists a regular language X′ which is equivalent to X in the sense of ≡. Otherwise, ≡ does not always have Parikh property. In this paper, focusing on the fact that Parikh equivalence is compatible with swapping adjacent letters, we propose an equivalence relation compatible with swapping adjacent subwords in a regular language given as a parameter. We also identify conditions on the parameter language that guarantee Parikh property for the resulting equivalence relation.  

3. Y.Lee(結縁・中澤研) [slides] 15:30-16:00

Ttitle: Decidable entailment checking for concurrent separation logic with fractional permissions
Abstract:  We propose a subsystem of concurrent separation logic with fractional permissions
introduced by Brotherston et al. Separation logic is an extension of Hoare logic that reasons about programs using shared mutable data. This logic has separating conjunction asserting that its subformulas hold for separated (disjoint) parts in the heap.

Fractional permissions manage access permission of shared resources between concurrent threads. Brotherston et al. introduced an extension of concurrent separation logic with fractional permissions, but they did not discuss the decidability of logic. The heart of this paper is restricting formulas of the system to symbolic heaps. We argue that

our system has sufficient expressiveness by showing some examples. We prove the decidability of the entailment checking for our system by normalization of formulas. We eliminate permissions by normalization, and therefore we can reduce the entailment checking problem to the existing decidable one.

4. R. Nakanishi  [Accepted for ICTAC2023] (関研) [slides] 16:00-16:30

Title: A Game-Theoretic Approach to Indistinguishability of WinningObjectives as User Privacy

 Abstract:

Game theory on graphs is a basic tool in computer science.

In this paper, we propose a new game-theoretic framework for studying

the privacy protection of a user who interactively uses a software

service. Our framework is based on the idea that an objective of a user

using software services should not be known to an adversary because

the objective is often closely related to personal information of the user.

We propose two new notions, O-indistinguishable strategy (O-IS) and

objective-indistinguishability equilibrium (OIE). For a given game and

a subset O of winning objectives (or objectives in short), a strategy of a

player is O-indistinguishable if an adversary cannot shrink O by excluding

any objective from O as an impossible objective. A strategy profile,

which is a tuple of strategies of all players, is an OIE if the profile

is locally maximal in the sense that no player can expand her set of objectives

indistinguishable from her real objective from the viewpoint of an

adversary. We show that for a given multiplayer game with Muller objectives,

both of the existence of an O-IS and that of OIE are decidable.

5. S.Oguchi [SOS/EXPRESS 2023] (結縁・中澤研) [slides] 16:30-17:00

Title: CRIL: A Concurrent Reversible Intermediate Language

Abstract:

We present a reversible intermediate language with concurrency for

translating a high-level concurrent programming language to another

lower-level concurrent programming language, keeping reversibility.

Intermediate languages are commonly used in compiling a source program

to an object code program closer to the machine code, where an

intermediate language enables behavioral analysis and optimization to

be decomposed in steps. We propose CRIL (Concurrent Reversible

Intermediate Language) as an extension of RIL used by Mogensen for a

functional reversible language, incorporating a multi-thread process

invocation and the synchronization primitives based on the P-V

operations. We show that the operational semantics of CRIL enjoy the

properties of reversibility, including the causal safety and causal

liveness proposed by Lanese et al., checking the axiomatic properties.

The operational semantics is defined by composing the bidirectional

control flow with the dependency information on updating the memory,

called annotation DAG. We show a simple example of `airline ticketing'

to illustrate how CRIL preserves the causality for reversibility in

imperative programs with concurrency.