20 citations · 84 across the 17 of their papers we have counts for
16 papers · 1 filter
Type-based Qubit Allocation for a First-Order Quantum Programming Language
Ryo Wakizaka, Atsushi Igarashi
Qubit allocation is a process to assign physical qubits to logical qubits in a quantum program. Since some quantum computers have connectivity constraints on applications of two-qu…
HELMHOLTZ: A Verifier for Tezos Smart Contracts Based on Refinement Types
Yuki Nishida, Hiromasa Saito, Ran Chen +4
A smart contract is a program executed on a blockchain, based on which many cryptocurrencies are implemented, and is being used for automating transactions. Due to the large amount…
Verification of a Merkle Patricia Tree Library Using F*
Sota Sato, Ryotaro Banno, Jun Furuse +2
A Merkle tree is a data structure for representing a key-value store as a tree. Each node of a Merkle tree is equipped with a hash value computed from those of their descendants. A…
Compilation of Coordinated Choice
Yuki Nishida, Atsushi Igarashi
Recently, we have proposed coordinated choices, which are nondeterministic choices equipped with names. The main characteristic of coordinated choices is that they synchronize nond…
Signature Restriction for Polymorphic Algebraic Effects
Taro Sekiyama, Takeshi Tsukada, Atsushi Igarashi
The naive combination of polymorphic effects and polymorphic type assignment has been well known to break type safety. Existing approaches to this problem are classified into two g…
ConSORT: Context- and Flow-Sensitive Ownership Refinement Types for Imperative Programs
John Toman, Ren Siqi, Kohei Suenaga +2
We present ConSORT, a type system for safety verification in the presence of mutability and aliasing. Mutability requires strong updates to model changing invariants during program…
Gradual Typing for Extensibility by Rows
Taro Sekiyama, Atsushi Igarashi
This work studies gradual typing for row types and row polymorphism. Key ingredients in this work are the dynamic row type, which represents a statically unknown part of a row, and…
Manifest Contracts with Intersection Types
Yuki Nishida, Atsushi Igarashi
We present a manifest contract system PCFvH with intersection types. A manifest contract system is a typed functional calculus in which software contracts are integrated into a…
Space-Efficient Gradual Typing in Coercion-Passing Style
Yuya Tsuda, Atsushi Igarashi, Tomoya Tabuchi
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…
A Dependently Typed Multi-Stage Calculus
Akira Kawata, Atsushi Igarashi
We study a dependently typed extension of a multi-stage programming language à la MetaOCaml, which supports quasi-quotation and cross-stage persistence for manipulation of code fra…
A Type System for First-Class Layers with Inheritance, Subtyping, and Swapping
Hiroaki Inoue, Atsushi Igarashi
Context-Oriented Programming (COP) is a programming paradigm to encourage modularization of context-dependent software. Key features of COP are layers---modules to describe context…
Dynamic Type Inference for Gradual Hindley--Milner Typing
Yusuke Miyazaki, Taro Sekiyama, Atsushi Igarashi
Garcia and Cimini study a type inference problem for the ITGL, an implicitly and gradually typed language with let-polymorphism, and develop a sound and complete inference algorith…
Handling polymorphic algebraic effects
Taro Sekiyama, Atsushi Igarashi
Algebraic effects and handlers are a powerful abstraction mechanism to represent and implement control effects. In this work, we study their extension with parametric polymorphism…
Reasoning about Polymorphic Manifest Contracts
Taro Sekiyama, Atsushi Igarashi
Manifest contract calculi, which integrate cast-based dynamic contract checking and refinement type systems, have been studied as foundations for hybrid contract checking. In this…
A Logical Foundation for Environment Classifiers
Takeshi Tsukada, Atsushi Igarashi
Taha and Nielsen have developed a multi-stage calculus λα with a sound type system using the notion of environment classifiers. They are special identifiers, with which code fragme…
Proving Noninterference by a Fully Complete Translation to the Simply Typed lambda-calculus
Naokata Shikuma, Atsushi Igarashi
Tse and Zdancewic have formalized the notion of noninterference for Abadi et al.'s DCC in terms of logical relations and given a proof of noninterference by reduction to parametric…