Author name cluster

Kohei Honda

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

6 papers

1 author row

TCS Journal 2017 Journal Article

Monitoring networks through multiparty session types

Laura Bocchi
Tzu-Chun Chen
Romain Demangeon
Kohei Honda
Nobuko Yoshida

In large-scale distributed infrastructures, applications are realised through communications among distributed components. The need for methods for assuring safe interactions in such environments is recognised, however the existing frameworks, relying on centralised verification or restricted specification methods, have limited applicability. This paper proposes a new theory of monitored π-calculus with dynamic usage of multiparty session types (MPST), offering a rigorous foundation for safety assurance of distributed components which asynchronously communicate through multiparty sessions. Our theory establishes a framework for semantically precise decentralised run-time enforcement and provides reasoning principles over monitored distributed applications, which complement existing static analysis techniques. We introduce asynchrony through the means of explicit routers and global queues, and propose novel equivalences between networks, that capture the notion of interface equivalence, i. e. equating networks offering the same services to a user. We illustrate our static–dynamic analysis system with an ATM protocol as a running example and justify our theory with results: satisfaction equivalence, local/global safety and transparency, and session fidelity.

Details DOI

TCS Journal 2014 Journal Article

An observationally complete program logic for imperative higher-order functions

Kohei Honda
Nobuko Yoshida
Martin Berger

We establish a strong completeness property called observational completeness of the program logic for imperative, higher-order functions introduced in [1]. Observational completeness states that valid assertions characterise program behaviour up to observational congruence, giving a precise correspondence between operational and axiomatic semantics. The proof layout for the observational completeness which uses a restricted syntactic structure called finite canonical forms originally introduced in game-based semantics, and characteristic formulae originally introduced in the process calculi, is generally applicable for a precise axiomatic characterisation of more complex program behaviour, such as aliasing and local state.

Details DOI

TCS Journal 2010 Journal Article

An exact correspondence between a typed pi-calculus and polarised proof-nets

Kohei Honda
Olivier Laurent

This paper presents an exact correspondence in typing and dynamics between polarised linear logic and a typed π -calculus based on IO-typing. The respective incremental constraints, one on geometric structures of proof-nets and one based on types, precisely correspond to each other, leading to the exact correspondence of the respective formalisms as they appear in Olivier Laurent (2003) [27] (for proof-nets) and Kohei Honda et al. (2004) [24] (for the π -calculus).

Details DOI

I&C Journal 2004 Journal Article

Strong normalisation in the π-calculus

Nobuko Yoshida
Martin Berger
Kohei Honda

We introduce a typed π-calculus where strong normalisation is ensured by typability. Strong normalisation is a useful property in many computational contexts, including distributed systems. In spite of its simplicity, our type discipline captures a wide class of converging name-passing interactive behaviour. The proof of strong normalisability combines methods from typed λ-calculi and linear logic with process-theoretic reasoning. It is adaptable to systems involving state, non-determinism, polymorphism, control and other extensions. Strong normalisation is shown to have significant consequences, including finite axiomatisation of weak bisimilarity, a fully abstract embedding of the simply typed λ-calculus with products and sums and basic liveness in interaction. Strong normalisability has been extensively studied as a fundamental property in functional calculi, term rewriting and logical systems. This work is one of the first steps to extend theories and proof methods for strong normalisability to the context of name-passing processes.

Details DOI

TCS Journal 1999 Journal Article

Game-theoretic analysis of call-by-value computation

Kohei Honda
Nobuko Yoshida

We present a general semantic universe of call-by-value computation based on elements of game semantics, and validate its appropriateness as a semantic universe by the full abstraction result for call-by-value PCF, a generic typed programming language with call-by-value evaluation. The key idea is to consider the distinction between call-by-name and call-by-value as that of the structure of information flow, which determines the basic form of games. In this way the call-by-name computation and call-by-value computation arise as two independent instances of sequential functional computation with distinct algebraic structures. We elucidate the type structures of the universe following the standard categorical framework developed in the context of domain theory. Mutual relationship between the presented category of games and the corresponding call-by-name universe is also clarified.

Details DOI

TCS Journal 1995 Journal Article

On reduction-based process semantics

Kohei Honda
Nobuko Yoshida

A formulation of semantic theories for processes which does not rely on the notion of observables or convergence is studied. The new construction is based solely on a reduction relation and equational reasoning, but can induce meaningful theories for processes, both in weak and strong settings. The resulting theories in many cases coincide with, and sometimes generalise, observation-based formulation of behavioural equivalence. The basic construction of reduction-based theories is studied, taking a simple name passing calculus (called ν-calculus) and its extensions as an example. Results concerning the application of our construction to other calculi are also briefly discussed.

Details DOI