Tomoyuki Aotani

dblp:68/3745 · DBLP profile ↗
← Back
8ranked-venue papers
1as first author
3since 2021 · last 2023
0000-0003-4538-0230ORCID · verified

Domains — the database's venue-derived domains; a paper can count in several

Software engineering, systems software and programming languages · 7 · 1 first-author · 3 since 2021
YearPublicationVenuePosition
2023 Compilation Semantics for a Programming Language with Versions
abstract
Abstract Programming with versions is a paradigm that allows a program to use multiple versions of a module so that the programmer can selectively use functions from both older and newer versions of a single module. Previous work formalized $$\lambda _{\textrm{VL}}$$ λ VL , a core calculus for programming with versions, but it has not been integrated into practical programming languages. In this paper, we propose VL, a Haskell-subset surface language for $$\lambda _{\textrm{VL}}$$ λ VL along with its compilation method. We formally describe the core part of the VL compiler, which translates from the surface language to the core language by leveraging Girard’s translation, soundly infers the consistent version of expressions along with their types, and generates a multi-version interface by bundling specific-version interfaces. We conduct a case study to show how VL supports practical software evolution scenarios and discuss the method’s scalability.
Yudai Tanabe, Luthfan Anshar Lubis, Tomoyuki Aotani, Hidehiko Masuhara
APLAS3
2022 BatakJava: An Object-Oriented Programming Language with Versions
abstract
Programming with versions is a recent proposal that supports multiple versions of software components in a program. Though it would provide greater freedom for the programmer, the concept is only realized as a simple core calculus, called λVL, where a value consists of λ-terms with multiple versions. We explore a design space of programming with versions in the presence of data structures and module systems, and propose BatakJava, an object-oriented programming language in which multiple versions of a class can be used in a program. This paper presents BatakJava’s language design, its core semantics with subject reduction, an implementation as a source-to-Java translator, and a case study to understand how we can exploit multiple versions in BatakJava for developing an application program with an evolving library.
Luthfan Anshar Lubis, Yudai Tanabe, Tomoyuki Aotani, Hidehiko Masuhara
SLE3
2021 Signal Classes: A Mechanism for Building Synchronous and Persistent Signal Networks
abstract
Signals are principal abstraction in reactive programming languages and constitute the basics of reactive computations in modern systems, such as the Internet of Things. Signals sometimes utilize past values, which leads to space leak, a problem where accumulated past values waste resources such as the main memory. Persistent signals, an abstraction for time-varying values with their execution histories, provide a generalized and standardized way of space leak management by leaving this management to the database system. However, the current design of persistent signals is very rudimental. For example, they cannot represent complex data structures; they can only be connected using pre-defined API methods that implicitly synchronize the persistent signal network; and they cannot be created dynamically. In this paper, we show that these problems are derived from more fundamental one: no language mechanism is provided to group related persistent signals. To address this problem, we propose a new language mechanism signal classes. A signal class packages a network of related persistent signals that comprises a complex data structure. A signal class defines the scope of synchronization, making it possible to flexibly create persistent signal networks by methods not limited to the use of pre-defined API methods. Furthermore, a signal class can be instantiated, and this instance forms a unit of lifecycle management, which enables the dynamic creation of persistent signals. We formalize signal classes as a small core language where the computation is deliberately defined to interact with the underlying database system using relational algebra. Based on this formalization, we prove the language’s glitch freedom. We also formulate its type soundness by introducing an additional check of program well-formedness. This mechanism is implemented as a compiler and a runtime library that is based on a time-series database. The usefulness of the language is demonstrated through the vehicle tracking simulator and viewer case study. We also conducted a performance evaluation that confirms the feasibility of this case study.
Tetsuo Kamina, Tomoyuki Aotani, Hidehiko Masuhara
ECOOP2
2018 ContextWorkflow: A Monadic DSL for Compensable and Interruptible Executions
abstract
Context-aware applications, whose behavior reactively depends on the time-varying status of the surrounding environment - such as network connection, battery level, and sensors - are getting more and more pervasive and important. The term "context-awareness" usually suggests prompt reactions to context changes: as the context change signals that the current execution cannot be continued, the application should immediately abort its execution, possibly does some clean-up tasks, and suspend until the context allows it to restart. Interruptions, or asynchronous exceptions, are useful to achieve context-awareness. It is, however, difficult to program with interruptions in a compositional way in most programming languages because their support is too primitive, relying on synchronous exception handling mechanism such as try-catch. We propose a new domain-specific language ContextWorkflow for interruptible programs as a solution to the problem. A basic unit of an interruptible program is a workflow, i.e., a sequence of atomic computations accompanied with compensation actions. The uniqueness of ContextWorkflow is that, during its execution, a workflow keeps watching the context between atomic actions and decides if the computation should be continued, aborted, or suspended. Our contribution of this paper is as follows; (1) the design of a workflow-like language with asynchronous interruption, checkpointing, sub-workflows and suspension; (2) a formal semantics of the core language; (3) a monadic interpreter corresponding to the semantics; and (4) its concrete implementation as an embedded domain-specific language in Scala.
Hiroaki Inoue, Tomoyuki Aotani, Atsushi Igarashi
ECOOP2
2018 Method safety mechanism for asynchronous layer deactivation
Tetsuo Kamina, Tomoyuki Aotani, Hidehiko Masuhara, Atsushi Igarashi
Sci. Comput. Program.2
2016 Towards Modular Reasoning for Context-Oriented Programs
Tomoyuki Aotani, Gary T. Leavens
FTfJP@ECOOP1
2016 Specifying and Verifying Advanced Control Features
Gary T. Leavens, David A. Naumann, Hridesh Rajan, Tomoyuki Aotani
ISoLA (2)4
2011 Combining Static Analysis and Runtime Checking in Security Aspects for Distributed Tuple Spaces
Tomoyuki Aotani, Hidehiko Masuhara, Flemming Nielson, Hanne Riis Nielson
COORDINATION2