arXiv subjects

Eijiro Sumii

Publications and source records attributed to Eijiro Sumii.

4 recordsLinked to original sources

arXiv2026

Type-based information flow analysis for $\pi$-calculus with a dynamically extensible security lattice

We develop a type system for secure information flow where new security levels can be created and inserted into the security lattice dynamically, i.e., even in the middle of an execution of a system. Our system is formalized by extending Kobayashi's type-based secure information flow analysis for Milner's pi-calculus, which is one of the most expressive models (or "languages") supporting both sequential and concurrent computations, with concise syntax, reduction-based semantics, and bisimulation equivalence as a robust formalization of secrecy as non-interference. The development required careful treatment of extensions of lattices themselves as well as deliberate generalization from the simple 2-element lattice (consisting of only High and Low) in the original system.

cs.CR↗

arXiv2017

Specialization of Generic Array Accesses After Inlining

We have implemented an optimization that specializes type-generic array accesses after inlining of polymorphic functions in the native-code OCaml compiler. Polymorphic array operations (read and write) in OCaml require runtime type dispatch because of ad hoc memory representations of integer and float arrays. It cannot be removed even after being monomorphized by inlining because the intermediate language is mostly untyped. We therefore extended it with explicit type application like System F (while keeping implicit type abstraction by means of unique identifiers for type variables). Our optimization has achieved up to 21% speed-up of numerical programs.

cs.PL↗

arXiv2015

A Simple and Practical Linear Algebra Library Interface with Static Size Checking

Linear algebra is a major field of numerical computation and is widely applied. Most linear algebra libraries (in most programming languages) do not statically guarantee consistency of the dimensions of vectors and matrices, causing runtime errors. While advanced type systems--specifically, dependent types on natural numbers--can ensure consistency among the sizes of collections such as lists and arrays, such type systems generally require non-trivial changes to existing languages and application programs, or tricky type-level programming. We have developed a linear algebra library interface that verifies the consistency (with respect to dimensions) of matrix operations by means of generative phantom types, implemented via fairly standard ML types and module system. To evaluate its usability, we ported to it a practical machine learning library from a traditional linear algebra library. We found that most of the changes required for the porting could be made mechanically, and changes that needed human thought are minor.

cs.PL↗

arXiv2011

Sound Bisimulations for Higher-Order Distributed Process Calculus

While distributed systems with transfer of processes have become pervasive, methods for reasoning about their behaviour are underdeveloped. In this paper we propose a bisimulation technique for proving behavioural equivalence of such systems modelled in the \emph{higher-order $π$-calculus with passivation} (and restriction). Previous research for this calculus is limited to context bisimulations and normal bisimulations which are either impractical or unsound. In contrast, we provide a sound and useful definition of \emph{environmental bisimulations}, with several non-trivial examples. Technically, a central point in our bisimulations is the clause for parallel composition, which must account for passivation of the spawned processes in the middle of their execution.

cs.LO↗