11 Search Results for "Igarashi, Atsushi"

Document
Artifact
DOI: 10.4230/DARTS.12.1.14
Compile-Time Tensor Shape Checking via Staged Shape-Dependent Types (Artifact)

Authors: Takashi Suwa

Published in: DARTS, Volume 12, Issue 1, Special Issue of the 40th European Conference on Object-Oriented Programming (ECOOP 2026)

Abstract
Based on the method proposed in the corresponding paper, we implemented a prototype type-checker (and a simple interpreter) for compile-time tensor shape checking. we ported a number of DNN-related example programs offered by ocaml-torch to our language and checked them by using the prototype implementation. The results indicated that our method can be considered effective enough to accommodate realistic tensor-handling programs.
Cite as

Takashi Suwa. Compile-Time Tensor Shape Checking via Staged Shape-Dependent Types (Artifact). In Special Issue of the 40th European Conference on Object-Oriented Programming (ECOOP 2026). Dagstuhl Artifacts Series (DARTS), Volume 12, Issue 1, pp. 14:1-14:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@Article{suwa:DARTS.12.1.14,
  author =	{Suwa, Takashi},
  title =	{{Compile-Time Tensor Shape Checking via Staged Shape-Dependent Types (Artifact)}},
  pages =	{14:1--14:5},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2026},
  volume =	{12},
  number =	{1},
  editor =	{Suwa, Takashi},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.12.1.14},
  URN =		{urn:nbn:de:0030-drops-261517},
  doi =		{10.4230/DARTS.12.1.14},
  annote =	{Keywords: Metaprogramming, Staged computation, Dependent types, Refinement types, Tensor shape checking}
}
Document
Artifact
DOI: 10.4230/DARTS.12.1.23
Ownership Refinement Types for Pointer Arithmetic and Nested Arrays (Artifact)

Authors: Yusuke Fujiwara, Yusuke Matsushita, Kohei Suenaga, and Atsushi Igarashi

Published in: DARTS, Volume 12, Issue 1, Special Issue of the 40th European Conference on Object-Oriented Programming (ECOOP 2026)

Abstract
This artifact accompanies the paper "Ownership Refinement Types for Pointer Arithmetic and Nested Arrays." It provides nested_array_ConSORT, a tool for automated ownership type inference and refinement type checking for imperative programs with pointer arithmetic and nested arrays. The artifact includes the tool implementation, benchmark programs, evaluation scripts to reproduce the experimental results (Tables 1, 3, 4, and 5) from the paper, and a comparison baseline (Extended_ConSORT by Tanaka et al. [Tanaka et al., 2024]). The artifact is packaged as a Docker image with all dependencies pre-installed, supporting both x86_64 and ARM64 platforms.
Cite as

Yusuke Fujiwara, Yusuke Matsushita, Kohei Suenaga, and Atsushi Igarashi. Ownership Refinement Types for Pointer Arithmetic and Nested Arrays (Artifact). In Special Issue of the 40th European Conference on Object-Oriented Programming (ECOOP 2026). Dagstuhl Artifacts Series (DARTS), Volume 12, Issue 1, pp. 23:1-23:6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@Article{fujiwara_et_al:DARTS.12.1.23,
  author =	{Fujiwara, Yusuke and Matsushita, Yusuke and Suenaga, Kohei and Igarashi, Atsushi},
  title =	{{Ownership Refinement Types for Pointer Arithmetic and Nested Arrays (Artifact)}},
  pages =	{23:1--23:6},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2026},
  volume =	{12},
  number =	{1},
  editor =	{Fujiwara, Yusuke and Matsushita, Yusuke and Suenaga, Kohei and Igarashi, Atsushi},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.12.1.23},
  URN =		{urn:nbn:de:0030-drops-261603},
  doi =		{10.4230/DARTS.12.1.23},
  annote =	{Keywords: aliasing, fractional ownership, program verification, refinement types, type systems}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2026.6
Ownership Refinement Types for Pointer Arithmetic and Nested Arrays

Authors: Yusuke Fujiwara, Yusuke Matsushita, Kohei Suenaga, and Atsushi Igarashi

Published in: LIPIcs, Volume 372, 40th European Conference on Object-Oriented Programming (ECOOP 2026)

Abstract
Tanaka et al. proposed a type system for verifying functional correctness properties of programs that use arrays and pointer arithmetic. Their system extends ConSORT - a type system combining fractional ownership and refinement types for imperative program verification - with support for pointer arithmetic. Their idea was to extend fractional ownership so that it can depend on an array index. Their formulation, however, does not handle nested arrays, which are essential for representing practical data structures such as matrices. We extend Tanaka et al.’s type system to support nested arrays by generalizing the notion of ownership to be able to refer to the indices of the outer arrays and prove the soundness of the extended type system. We have implemented a verifier based on the proposed type system and demonstrated that it can verify the correctness of programs that manipulate nested arrays, which were beyond the reach of Tanaka et al.
Cite as

Yusuke Fujiwara, Yusuke Matsushita, Kohei Suenaga, and Atsushi Igarashi. Ownership Refinement Types for Pointer Arithmetic and Nested Arrays. In 40th European Conference on Object-Oriented Programming (ECOOP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 372, pp. 6:1-6:31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{fujiwara_et_al:LIPIcs.ECOOP.2026.6,
  author =	{Fujiwara, Yusuke and Matsushita, Yusuke and Suenaga, Kohei and Igarashi, Atsushi},
  title =	{{Ownership Refinement Types for Pointer Arithmetic and Nested Arrays}},
  booktitle =	{40th European Conference on Object-Oriented Programming (ECOOP 2026)},
  pages =	{6:1--6:31},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-423-9},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{372},
  editor =	{Krebbers, Robbert and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2026.6},
  URN =		{urn:nbn:de:0030-drops-261029},
  doi =		{10.4230/LIPIcs.ECOOP.2026.6},
  annote =	{Keywords: aliasing, fractional ownership, program verification, refinement types, type systems}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2026.28
Compile-Time Tensor Shape Checking via Staged Shape-Dependent Types

Authors: Takashi Suwa and Atsushi Igarashi

Published in: LIPIcs, Volume 372, 40th European Conference on Object-Oriented Programming (ECOOP 2026)

Abstract
When writing programs involving matrices or tensors in general, it is desirable to rule out the inconsistency of tensor shapes (i.e., the generalization of matrix sizes) before actual computation. For this purpose, some languages provide dependent types such as Mat m n, and others offer refinement types to track predicates for shapes. Despite the theoretical maturity, however, such methods are often unhandy for continuous software development due to the requirement of proofs for judging type equality or subtyping; even automated proving is often unsuitable due to its unforeseeable time consumption. To remedy this, our study provides an alternative formalization by using staging. Based on the observation that conditions for the shape consistency can be extracted before running the actual tensor computations in many typical cases, we ensure such consistency by assertions evaluated as compile-time computations, not by proofs. Under this formalization, we can verify the consistency virtually statically in the sense that inconsistencies will be immediately detected as failures during compile-time computation. Our work achieves a mathematical guarantee that successfully generated code is always consistent with respect to tensor shapes. Furthermore, to vastly lessen the burden of adding shape- or stage-related descriptions, we (1) allow shape-related arguments to be implicit and infer them in a best-effort manner, and (2) offer a non-staged surface language that seemingly resembles ordinary dependently-typed languages and translate its programs into the staged core language. By a prototype implementation, we confirm that our language is expressive enough to verify a number of programs, including several examples offered by ocaml-torch.
Cite as

Takashi Suwa and Atsushi Igarashi. Compile-Time Tensor Shape Checking via Staged Shape-Dependent Types. In 40th European Conference on Object-Oriented Programming (ECOOP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 372, pp. 28:1-28:31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{suwa_et_al:LIPIcs.ECOOP.2026.28,
  author =	{Suwa, Takashi and Igarashi, Atsushi},
  title =	{{Compile-Time Tensor Shape Checking via Staged Shape-Dependent Types}},
  booktitle =	{40th European Conference on Object-Oriented Programming (ECOOP 2026)},
  pages =	{28:1--28:31},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-423-9},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{372},
  editor =	{Krebbers, Robbert and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2026.28},
  URN =		{urn:nbn:de:0030-drops-261247},
  doi =		{10.4230/LIPIcs.ECOOP.2026.28},
  annote =	{Keywords: Metaprogramming, Staged computation, Dependent types, Refinement types, Tensor shape checking}
}
Document
Extended Abstract
DOI: 10.4230/OASIcs.Programming.2025.24
Toward a Typed Intermediate Language for R (Extended Abstract)

Authors: Mickaël Laurent, Jakob Hain, Filip Krikava, Sebastián Krynski, and Jan Vitek

Published in: OASIcs, Volume 134, Companion Proceedings of the 9th International Conference on the Art, Science, and Engineering of Programming (Programming 2025)

Abstract
Compilers for dynamic languages often rely on intermediate representations with explicit type annotations to facilitate writing program transformations. This paper documents the design of a new typed intermediate representation for a just-in-time compiler for the R programming language called FIŘ. Type annotations, in FIŘ, capture properties such as sharing, the potential for effects, and compiler speculations. In this extended abstract, we focus on the sharing properties that may be used to optimize away some copies of values.
Cite as

Mickaël Laurent, Jakob Hain, Filip Krikava, Sebastián Krynski, and Jan Vitek. Toward a Typed Intermediate Language for R (Extended Abstract). In Companion Proceedings of the 9th International Conference on the Art, Science, and Engineering of Programming (Programming 2025). Open Access Series in Informatics (OASIcs), Volume 134, pp. 24:1-24:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{laurent_et_al:OASIcs.Programming.2025.24,
  author =	{Laurent, Micka\"{e}l and Hain, Jakob and Krikava, Filip and Krynski, Sebasti\'{a}n and Vitek, Jan},
  title =	{{Toward a Typed Intermediate Language for R}},
  booktitle =	{Companion Proceedings of the 9th International Conference on the Art, Science, and Engineering of Programming (Programming 2025)},
  pages =	{24:1--24:4},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-382-9},
  ISSN =	{2190-6807},
  year =	{2025},
  volume =	{134},
  editor =	{Edwards, Jonathan and Perera, Roly and Petricek, Tomas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.Programming.2025.24},
  URN =		{urn:nbn:de:0030-drops-243086},
  doi =		{10.4230/OASIcs.Programming.2025.24},
  annote =	{Keywords: JIT, compilation, static typing, ownership, copy-on-write, dynamic language}
}
Document
DOI: 10.4230/OASIcs.Gabbrielli.3
Deconfined Intersection Types in Java

Authors: Mariangiola Dezani-Ciancaglini, Paola Giannini, and Betti Venneri

Published in: OASIcs, Volume 86, Recent Developments in the Design and Implementation of Programming Languages (2020)

Abstract
We show how Java intersection types can be freed from their confinement in type casts, in such a way that the proposed Java extension is safe and fully compatible with the current language. To this aim, we exploit two calculi which formalise the simple Java core and the extended language, respectively. Namely, the second calculus extends the first one by allowing an intersection type to be used anywhere in place of a nominal type. We define a translation algorithm, compiling programs of the extended language into programs of the former calculus. The key point is the interaction between λ-expressions and intersection types, that adds safe expressiveness while being the crucial matter in the translation. We prove that the translation preserves typing and semantics. Thus, typed programs in the proposed extension are translated to typed Java programs. Moreover, semantics of translated programs coincides with the one of the source programs.
Cite as

Mariangiola Dezani-Ciancaglini, Paola Giannini, and Betti Venneri. Deconfined Intersection Types in Java. In Recent Developments in the Design and Implementation of Programming Languages. Open Access Series in Informatics (OASIcs), Volume 86, pp. 3:1-3:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{dezaniciancaglini_et_al:OASIcs.Gabbrielli.3,
  author =	{Dezani-Ciancaglini, Mariangiola and Giannini, Paola and Venneri, Betti},
  title =	{{Deconfined Intersection Types in Java}},
  booktitle =	{Recent Developments in the Design and Implementation of Programming Languages},
  pages =	{3:1--3:25},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-171-9},
  ISSN =	{2190-6807},
  year =	{2020},
  volume =	{86},
  editor =	{de Boer, Frank S. and Mauro, Jacopo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.Gabbrielli.3},
  URN =		{urn:nbn:de:0030-drops-132256},
  doi =		{10.4230/OASIcs.Gabbrielli.3},
  annote =	{Keywords: Intersection Types, Featherweight Java, Lambda Expressions}
}
Document
DOI: 10.4230/OASIcs.Gabbrielli.1
Locally Static, Globally Dynamic Session Types for Active Objects

Authors: Reiner Hähnle, Anton W. Haubner, and Eduard Kamburjan

Published in: OASIcs, Volume 86, Recent Developments in the Design and Implementation of Programming Languages (2020)

Abstract
Active object languages offer an attractive trade-off between low-level, preemptive concurrency and fully distributed actors: syntactically identifiable atomic code segments and asynchronous calls are the basis of cooperative concurrency, still permitting interleaving, but nevertheless being mechanically analyzable. The challenge is to reconcile local static analysis of atomic segments with the global scheduling constraints it depends on. Here, we propose an approximate, hybrid approach; At compile-time we perform a local static analysis: later, any run not complying to a global specification is excluded via runtime checks. That specification is expressed in a type-theoretic language inspired by session types. The approach reverses the usual (first global, then local) order of analysis and, thereby, supports analysis of open distributed systems.
Cite as

Reiner Hähnle, Anton W. Haubner, and Eduard Kamburjan. Locally Static, Globally Dynamic Session Types for Active Objects. In Recent Developments in the Design and Implementation of Programming Languages. Open Access Series in Informatics (OASIcs), Volume 86, pp. 1:1-1:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{hahnle_et_al:OASIcs.Gabbrielli.1,
  author =	{H\"{a}hnle, Reiner and Haubner, Anton W. and Kamburjan, Eduard},
  title =	{{Locally Static, Globally Dynamic Session Types for Active Objects}},
  booktitle =	{Recent Developments in the Design and Implementation of Programming Languages},
  pages =	{1:1--1:24},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-171-9},
  ISSN =	{2190-6807},
  year =	{2020},
  volume =	{86},
  editor =	{de Boer, Frank S. and Mauro, Jacopo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.Gabbrielli.1},
  URN =		{urn:nbn:de:0030-drops-132237},
  doi =		{10.4230/OASIcs.Gabbrielli.1},
  annote =	{Keywords: Session Types, Active Objects, Runtime Verification, Static Verification}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2020.8
Space-Efficient Gradual Typing in Coercion-Passing Style

Authors: Yuya Tsuda, Atsushi Igarashi, and Tomoya Tabuchi

Published in: LIPIcs, Volume 166, 34th European Conference on Object-Oriented Programming (ECOOP 2020)

Abstract
Herman et al. pointed out that the insertion of run-time checks into a gradually typed program could hamper tail-call optimization and, as a result, worsen the space complexity of the program. To address the problem, they proposed a space-efficient coercion calculus, which was subsequently improved by Siek et al. The semantics of these calculi involves eager composition of run-time checks expressed by coercions to prevent the size of a term from growing. However, it relies also on a nonstandard reduction rule, which does not seem easy to implement. In fact, no compiler implementation of gradually typed languages fully supports the space-efficient semantics faithfully. In this paper, we study coercion-passing style, which Herman et al. have already mentioned, as a technique for straightforward space-efficient implementation of gradually typed languages. A program in coercion-passing style passes "the rest of the run-time checks" around - just like continuation-passing style (CPS), in which "the rest of the computation" is passed around - and (unlike CPS) composes coercions eagerly. We give a formal coercion-passing translation from λS by Siek et al. to λS₁, which is a new calculus of first-class coercions tailored for coercion-passing style, and prove correctness of the translation. We also implement our coercion-passing style transformation for the Grift compiler developed by Kuhlenschmidt et al. An experimental result shows stack overflow can be prevented properly at the cost of up to 3 times slower execution for most partially typed practical programs.
Cite as

Yuya Tsuda, Atsushi Igarashi, and Tomoya Tabuchi. Space-Efficient Gradual Typing in Coercion-Passing Style. In 34th European Conference on Object-Oriented Programming (ECOOP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 166, pp. 8:1-8:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{tsuda_et_al:LIPIcs.ECOOP.2020.8,
  author =	{Tsuda, Yuya and Igarashi, Atsushi and Tabuchi, Tomoya},
  title =	{{Space-Efficient Gradual Typing in Coercion-Passing Style}},
  booktitle =	{34th European Conference on Object-Oriented Programming (ECOOP 2020)},
  pages =	{8:1--8:29},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-154-2},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{166},
  editor =	{Hirschfeld, Robert and Pape, Tobias},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2020.8},
  URN =		{urn:nbn:de:0030-drops-131658},
  doi =		{10.4230/LIPIcs.ECOOP.2020.8},
  annote =	{Keywords: Gradual typing, coercion calculus, coercion-passing style, dynamic type checking, tail-call optimization}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2019.20
A Linear-Logical Reconstruction of Intuitionistic Modal Logic S4

Authors: Yosuke Fukuda and Akira Yoshimizu

Published in: LIPIcs, Volume 131, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)

Abstract
We propose a modal linear logic to reformulate intuitionistic modal logic S4 (IS4) in terms of linear logic, establishing an S4-version of Girard translation from IS4 to it. While the Girard translation from intuitionistic logic to linear logic is well-known, its extension to modal logic is non-trivial since a naive combination of the S4 modality and the exponential modality causes an undesirable interaction between the two modalities. To solve the problem, we introduce an extension of intuitionistic multiplicative exponential linear logic with a modality combining the S4 modality and the exponential modality, and show that it admits a sound translation from IS4. Through the Curry-Howard correspondence we further obtain a Geometry of Interaction Machine semantics of the modal lambda-calculus by Pfenning and Davies for staged computation.
Cite as

Yosuke Fukuda and Akira Yoshimizu. A Linear-Logical Reconstruction of Intuitionistic Modal Logic S4. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 20:1-20:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{fukuda_et_al:LIPIcs.FSCD.2019.20,
  author =	{Fukuda, Yosuke and Yoshimizu, Akira},
  title =	{{A Linear-Logical Reconstruction of Intuitionistic Modal Logic S4}},
  booktitle =	{4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)},
  pages =	{20:1--20:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-107-8},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{131},
  editor =	{Geuvers, Herman},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.20},
  URN =		{urn:nbn:de:0030-drops-105271},
  doi =		{10.4230/LIPIcs.FSCD.2019.20},
  annote =	{Keywords: linear logic, modal logic, Girard translation, Curry-Howard correspondence, geometry of interaction, staged computation}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2018.2
ContextWorkflow: A Monadic DSL for Compensable and Interruptible Executions

Authors: Hiroaki Inoue, Tomoyuki Aotani, and Atsushi Igarashi

Published in: LIPIcs, Volume 109, 32nd European Conference on Object-Oriented Programming (ECOOP 2018)

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.
Cite as

Hiroaki Inoue, Tomoyuki Aotani, and Atsushi Igarashi. ContextWorkflow: A Monadic DSL for Compensable and Interruptible Executions. In 32nd European Conference on Object-Oriented Programming (ECOOP 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 109, pp. 2:1-2:33, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{inoue_et_al:LIPIcs.ECOOP.2018.2,
  author =	{Inoue, Hiroaki and Aotani, Tomoyuki and Igarashi, Atsushi},
  title =	{{ContextWorkflow: A Monadic DSL for Compensable and Interruptible Executions}},
  booktitle =	{32nd European Conference on Object-Oriented Programming (ECOOP 2018)},
  pages =	{2:1--2:33},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-079-8},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{109},
  editor =	{Millstein, Todd},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2018.2},
  URN =		{urn:nbn:de:0030-drops-92074},
  doi =		{10.4230/LIPIcs.ECOOP.2018.2},
  annote =	{Keywords: workflow, asynchronous exception, checkpoint, monad, embedded domain specific language}
}
Document
DOI: 10.4230/DARTS.4.3.4
ContextWorkflow: A Monadic DSL for Compensable and Interruptible Executions (Artifact)

Authors: Hiroaki Inoue, Tomoyuki Aotani, and Atsushi Igarashi

Published in: DARTS, Volume 4, Issue 3, Special Issue of the 32nd European Conference on Object-Oriented Programming (ECOOP 2018)

Abstract
This artifact provides the Scala, Haskell, and Purescript implementations of ContextWorkflow, an embedded domain-specific language for interruptible and compensable executions, and demonstrates the maze search example described in the companion paper. The Haskell and Purescript implementations provide the core language constructs including \texttt{checkpoint} for partial aborts and \texttt{sub} for sub-workflows and show that ContextWorkflow can be embedded in eager and lazy languages as described in the companion paper. The Scala implementation does not only provide user-friendly syntax of ContextWorkflow but also gives the maze search example as an interactive GUI application.
Cite as

Hiroaki Inoue, Tomoyuki Aotani, and Atsushi Igarashi. ContextWorkflow: A Monadic DSL for Compensable and Interruptible Executions (Artifact). In Special Issue of the 32nd European Conference on Object-Oriented Programming (ECOOP 2018). Dagstuhl Artifacts Series (DARTS), Volume 4, Issue 3, pp. 4:1-4:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@Article{inoue_et_al:DARTS.4.3.4,
  author =	{Inoue, Hiroaki and Aotani, Tomoyuki and Igarashi, Atsushi},
  title =	{{ContextWorkflow: A Monadic DSL for Compensable and Interruptible Executions (Artifact)}},
  pages =	{4:1--4:2},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2018},
  volume =	{4},
  number =	{3},
  editor =	{Inoue, Hiroaki and Aotani, Tomoyuki and Igarashi, Atsushi},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.4.3.4},
  URN =		{urn:nbn:de:0030-drops-92356},
  doi =		{10.4230/DARTS.4.3.4},
  annote =	{Keywords: workflow, asynchronous exception, checkpoint, monad, embedded domain specific language}
}
  • Refine by Type
  • 11 Document/PDF
  • 1 Document/HTML

  • Refine by Publication Year
  • 4 2026
  • 1 2025
  • 3 2020
  • 1 2019
  • 2 2018

  • Refine by Author
  • 6 Igarashi, Atsushi
  • 2 Aotani, Tomoyuki
  • 2 Fujiwara, Yusuke
  • 2 Inoue, Hiroaki
  • 2 Matsushita, Yusuke
  • Show More...

  • Refine by Series/Journal
  • 5 LIPIcs
  • 3 OASIcs
  • 3 DARTS

  • Refine by Classification
  • 4 Theory of computation → Type structures
  • 2 Software and its engineering → Functional languages
  • 2 Software and its engineering → Software verification and validation
  • 2 Theory of computation → Program verification
  • 2 Theory of computation → Semantics and reasoning
  • Show More...

  • Refine by Keyword
  • 2 Dependent types
  • 2 Metaprogramming
  • 2 Refinement types
  • 2 Staged computation
  • 2 Tensor shape checking
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact