Publications
2026Compile-Time Tensor Shape Checking via Staged Shape-Dependent Types
Proceedings of ECOOP 2026, 2026
Ownership Refinement Types for Pointer Arithmetic and Nested Arrays
Proceedings of ECOOP 2026, 2026
Contextual Metaprogramming for Session Types
Programming Languages and Systems - 35th European Symposium on Programming, ESOP 2026, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2026, Turin, Italy, April 11-16, 2026, Proceedings, Part I., 2026
DOI: 10.1007/978-3-032-22720-1_2An ML-style module system for cross-stage type abstraction in multi-stage programming
Science of Computer Programming, 2026
DOI: 10.1016/j.scico.2025.103379A Fast and Soft Pattern Matcher for Trillion-Scale Corpus
ICML 2026 (accepted), 2026
Evaluating Hybrid Automata Learning Tools Based on Their Success in Formal Verification
MED 2026 (Accepted), 2026
SoftMatcha 2: 1 兆語規模コーパスの超高速かつ柔らかい検索
言語処理学会 第32回年次大会 発表論文集, 2026
In-Situ Hardware Error Detection Using Specification-Derived Petri Net Models and Behavior-Derived State Sequences
IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems (Accepted), 2026
Componentwise Automata Learning for System Integration
ATVA 2025, 2026
DOI: 10.1007/978-3-032-08707-2_1SoftMatcha 2: A Fast and Soft Pattern Matcher for Trillion-Scale Corpora
DOI: 10.48550/ARXIV.2602.10908RapunSL: Untangling Quantum Computing with Separation, Linear Combination and Mixing
Proceedings of the ACM on Programming Languages, 2026
DOI: 10.1145/37766482025Making Rabbit Run for Security Verification of Networked Systems with Unbounded Loops
Proceedings of Formal Methods in Computer-Aided Design (FMCAD), 2025
動的型推論を備えた空間効率の良い漸進的型付け
日本ソフトウェア科学会第42回大会論文集, 2025
Unifying Function- and Argument-First Bidirectional Type Systems
日本ソフトウェア科学会第42回大会論文集, 2025
Efficient Black-Box Checking with Specification-Guided Abstraction
ACM Transactions on Embedded Computing Systems, 2025
DOI: 10.1145/3762659StatWhy: Formal Verification Tool for Statistical Hypothesis Testing Programs
CAV 2025, 2025
DOI: 10.1007/978-3-031-98679-6_10Certifying Lyapunov Stability of Black-Box Nonlinear Systems via Counterexample Guided Synthesis
HSCC 2025 (To appear), 2025
A Soft and Fast Pattern Matcher for Billion-Scale Corpus Searches
ICLR 2025 (To appear), 2025
Hardware Error Detection with In-Situ Monitoring of Control Flow-Related Specifications
Proceedings of the 30th Asia and South Pacific Design Automation Conference, 2025
DOI: 10.1145/3658617.3697744CHLOE: Loop Transformation over Fully Homomorphic Encryption via Multi-Level Vectorization and Control-Path Reduction.
IEEE Symposium on Security and Privacy(SP), 2025
DOI: 10.1109/SP61157.2025.00035Hyper Pattern Matching.
Runtime Verification - 25th International Conference(RV), 2025
DOI: 10.1007/978-3-032-05435-7_22SoftMatcha: A Soft and Fast Pattern Matcher for Billion-Scale Corpus Searches.
The Thirteenth International Conference on Learning Representations(ICLR), 2025
Nola: Later-Free Ghost State for Verifying Termination in Iris
Proceedings of the ACM on Programming Languages, 2025
DOI: 10.1145/3729250SoftMatcha: A Soft and Fast Pattern Matcher for Billion-Scale Corpus Searches
13th International Conference on Learning Representations (ICLR 2025), 2025
2024Type-Based Verification of Connectivity Constraints in Lattice Surgery
Proceedings of the 22nd Asian Symposium on Programming Languages and Systems, 2024
DOI: 10.1007/978-981-97-8943-6_11Rabbit: A Language to Model and Verify Data Flow in Networked Systems
2024 International Symposium on Networks, Computers and Communications (ISNCC), 2024
DOI: 10.1109/isncc62547.2024.10758938Space-Efficient Polymorphic Gradual Typing, Mostly Parametric
Proceedings of the ACM on Programming Languages, 2024
DOI: 10.1145/3656441Signature restriction for polymorphic algebraic effects
Journal of Functional Programming, 2024
DOI: 10.1017/s0956796824000054Linear Contextual Metaprogramming and Session Types
Electronic Proceedings in Theoretical Computer Science, 2024
DOI: 10.4204/eptcs.401.1命令型プログラムの安全性検証のための所有権主導変換
第26回プログラミングおよびプログラミング言語ワークショップ(PPL2024)論文集, 2024
iCon: Automated Verification of Inter-Transaction Properties in Tezos Smart Contracts with Unknowns
Proceedings of 2024 IEEE International Conference on Blockchain and Cryptocurrency (ICBC), 2024
Oblivious Monitoring for Discrete-Time STL via Fully Homomorphic Encryption.
Runtime Verification - 24th International Conference(RV), 2024
DOI: 10.1007/978-3-031-74234-7_4HEIR: A Unified Representation for Cross-Scheme Compilation of Fully Homomorphic Computation.
31st Annual Network and Distributed System Security Symposium(NDSS), 2024
制御フロー仕様から生成したペトリネットに基づくハードウェア誤動作検出手法
DAシンポジウム2024論文集, 2024
Goal-Aware RSS for Complex Scenarios via Program Logic
2024 IEEE Intelligent Vehicles Symposium (IV), 2024
DOI: 10.1109/iv55156.2024.10588754Sound and relatively complete belief Hoare logic for statistical hypothesis testing programs.
Artif. Intell., 2024
DOI: 10.1016/j.artint.2023.104045Control-data separation and logical condition propagation for efficient inference on probabilistic programs
Journal of Logical and Algebraic Methods in Programming, 2024
DOI: 10.1016/j.jlamp.2023.100922Hyper Parametric Timed CTL.
IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2024
DOI: 10.1109/TCAD.2024.3443704Temporal Logic Formalisation of ISO 34502 Critical Scenarios: Modular Construction with the RSS Safety Distance
39th ACM/SIGAPP Symposium On Applied Computing, 2024
DOI: 10.1145/3605098.3636014Temporal Logic Formalisation of ISO 34502 Critical Scenarios: Modular Construction with the RSS Safety Distance.
CoRR, 2024
DOI: 10.48550/arXiv.2403.18764Learning Weighted Finite Automata over the Max-Plus Semiring and its Termination.
CoRR, 2024
DOI: 10.48550/arXiv.2407.09775Bi-Abduction in Separation Logic with Arrays and Lists for Program Analysis
Computer Software, 2024
DOI: 10.11309/jssst.41.1_502023Rabbit: a modeling language for verifying cybersecurity in IoT system
第145回情報処理学会プログラミング研究会資料, 2023
Contextual Modal Type Theory with Polymorphic Contexts
Proceedings of European Symposium on Programming, 2023
DOI: 10.1007/978-3-031-30044-8_11LLTZ: LLMV IR からスマートコントラクト記述言語 Michelson へのコンパイラ
第25回プログラミングおよびプログラミング言語ワークショップ(PPL2023)論文集, 2023
Probabilistic Black-Box Checking via Active MDP Learning
ACM Transactions on Embedded Computing Systems, 2023
DOI: 10.1145/3609127Feature Attributionを用いたdlshogiの指し手の解釈可能性向上手法
研究報告ゲーム情報学（GI）, 2023
LLTZ: LLVM IR からスマートコントラクト記述言語 Michelson へのコンパイラ
第25回プログラミングおよびプログラミング言語ワークショップ (PPL 2023) 論文集, 2023
Learning Nonlinear Hybrid Automata from Input-Output Time-Series Data.
ATVA (1), 2023
DOI: 10.1007/978-3-031-45329-8_2Active Learning of Deterministic Timed Automata with Myhill-Nerode Style Characterization.
Computer Aided Verification - 35th International Conference, Part I, 2023
DOI: 10.1007/978-3-031-37706-8_1Parametric Timed Pattern Matching."
ACM Transactions on Software Engineering and Methodology, 2023
DOI: 10.1145/35171942022SCameleer: スマートコントラクト記述言語SCamlのための自動検証器
日本ソフトウェア科学会第39回大会論文集, 2022
スマートコントラクト検証器Helmholtzのためのエラー原因提示手法
日本ソフトウェア科学会第39回大会論文集, 2022
暗黙に相互運用可能なレコードとハッシュテーブルのための型推論とコンパイル手法
日本ソフトウェア科学会第39回大会論文集, 2022
Helmholtz: A Verifier for Tezos Smart Contracts Based on Refinement Types
New Generation Computing, 2022
DOI: 10.1007/s00354-022-00167-1ZT-IoT: ゼロトラストIoTのためのシステムソフトウェア構築に向けて
第154回情報処理学会システムソフトウェアとオペレーティング・システム研究会資料, 2022
Stage-Aware Equality Types for a Dependently-Typed Multi-Stage Calculus
第24回プログラミングおよびプログラミング言語ワークショップ(PPL2022)論文集, 2022
Type-based Qubit Allocation for a First-Order Quantum Programming Language
第24回プログラミングおよびプログラミング言語ワークショップ(PPL2022)論文集, 2022
BOREx: Bayesian-Optimization-Based Refinement of Saliency Map for Image- and Video-Classification Models.
ACCV (7), 2022
DOI: 10.1007/978-3-031-26293-7_17Oblivious Online Monitoring for Safety LTL Specification via Fully Homomorphic Encryption.
CAV 2022, 2022
DOI: 10.1007/978-3-031-13185-1_22The Lattice-Theoretic Essence of Property Directed Reachability Analysis.
CAV 2022, 2022
DOI: 10.1007/978-3-031-13185-1_12ARCH-COMP 2022 Category Report: Falsification with Ubounded Resources
EPiC Series in Computing, 2022
DOI: 10.29007/fhnkDynamic Shielding for Reinforcement Learning in Black-Box Environments.
International Symposium on Automated Technology for Verification and Analysis, 2022
DOI: 10.1007/978-3-031-19992-9_2Exemplifying parametric timed specifications over signals with bounded behavior.
NASA Formal Methods Symposium, 2022
DOI: 10.1007/978-3-031-06773-0_25Data for "Exemplifying parametric timed specifications over signals with bounded behavior".
DOI: 10.5281/zenodo.6382893Model-Bounded Monitoring of Hybrid Systems."
ACM Transactions on Cyber-Physical Systems, 2022
DOI: 10.1145/35290952021Is Space-Efficient Polymorphic Gradual Typing Possible?
Informal Proceedings of Scheme and Functional Programming Workshop, 2021
HELMHOLTZ: A Verifier for Tezos Smart Contracts Based on Refinement Types.
CoRR, 2021
Verification of a Merkle Patricia Tree Library Using F.
CoRR, 2021
完全準同型暗号を用いた秘匿LTLオンラインモニタリング
コンピュータセキュリティシンポジウム 2021 (CSS 2021), 2021
Formalizing Statistical Beliefs in Hypothesis Testing Using Program Logic.
Proceedings of the 18th International Conference on Principles of Knowledge Representation and Reasoning(KR), 2021
DOI: 10.24963/kr.2021/39Efficient Black-Box Checking via Model Checking with Strengthened Specifications
Runtime Verification - 21st International Conference(RV), 2021
DOI: 10.1007/978-3-030-88494-9_6Enhancing Loop-Invariant Synthesis via Reinforcement Learning.
CoRR, 2021
Verification of a Merkle Patricia Tree Library Using F*
CoRR, 2021
ARCH-COMP 2021 Category Report: Falsification with Validation of Results.
ARCH@ADHS, 2021
DOI: 10.29007/xwl1Hybrid System Falsification for Multiple-Constraint Parameter Synthesis: a Gas Turbine Case Study.
24th International Symposium on Formal Methods, 2021
DOI: 10.1007/978-3-030-90870-6_17Constrained Optimization for Falsification and Conjunctive Synthesis.
6th IFAC Conference on Analysis and Design of Hybrid Systems, 2021
DOI: 10.1016/j.ifacol.2021.08.501Model-Bounded Monitoring of Hybrid Systems.
12th ACM/IEEE International Conference on Cyber-Physical Systems, 2021
DOI: 10.1145/3450267.34505312020Space-Efficient Gradual Typing in Coercion-Passing Style.
34th European Conference on Object-Oriented Programming, ECOOP 2020, 2020
DOI: 10.4230/LIPIcs.ECOOP.2020.8量子ビット連結性制約検査のための依存型システム
日本ソフトウェア科学会第37回大会論文集, 2020
ConSORT: Context- and Flow-Sensitive Ownership Refinement Types for Imperative Programs
Programming Languages and Systems, 2020
DOI: 10.1007/978-3-030-44914-8_25スタック領域上での時間的メモリ安全性を保証する静的解析手法
第22回プログラミングおよびプログラミング言語ワークショップ(PPL2020)論文集, 2020
スマートコントラクトのための Effectively Callback-Free 性の型に基づく静的検証
第22回プログラミングおよびプログラミング言語ワークショップ(PPL2020)論文集, 2020
F* を用いた Merkle Patricia Tree ライブラリの形式検証
第22回プログラミングおよびプログラミング言語ワークショップ(PPL2020)論文集, 2020
Compilation of Coordinated Choice.
CoRR, 2020
Signature restriction for polymorphic algebraic effects.
Proc. ACM Program. Lang., 2020
DOI: 10.1145/3408999Space-Efficient Gradual Typing in Coercion-Passing Style
Informal Proceedings of the 1st International Workshop on Gradual Typing (WGT2020), 2020
Gradual Typing for Extensibility by Rows
Informal Proceedings of the 1st International Workshop on Gradual Typing (WGT2020), 2020
Visualizing Color-Wise Saliency of Black-Box Image Classification Models.
Proceedings of ACCV 2020, 2020
DOI: 10.1007/978-3-030-69535-4_12Generalized Property-Directed Reachability for Hybrid Systems
Verification, Model Checking, and Abstract Interpretation - 21st International Conference(VMCAI), 2020
DOI: 10.1007/978-3-030-39322-9_14A Contract Corpus for Recognizing Rights and Obligations.
Proceedings of The 12th Language Resources and Evaluation Conference(LREC), 2020
2019A Dependently Typed Multi-stage Calculus.
Programming Languages and Systems - 17th Asian Symposium, APLAS 2019, Nusa Dua, Bali, Indonesia, December 1-4, 2019, Proceedings, 2019
DOI: 10.1007/978-3-030-34175-6_4Manifest Contracts with Intersection Types.
Programming Languages and Systems - 17th Asian Symposium, APLAS 2019, Nusa Dua, Bali, Indonesia, December 1-4, 2019, Proceedings, 2019
DOI: 10.1007/978-3-030-34175-6_3Temporal Verification of Programs via First-Order Fixpoint Logic.
Static Analysis - 26th International Symposium, SAS 2019, Porto, Portugal, October 8-11, 2019, Proceedings, 2019
DOI: 10.1007/978-3-030-32304-2_20A Type System for First-Class Layers with Inheritance, Subtyping, and Swapping
Science of Computer Programming, 2019
Handling Polymorphic Algebraic Effects
Proceedings of European Symposium on Programming (ESOP2019), 2019
空間効率の良いコアーション計算のためのコアーション渡し形式
第21回プログラミングおよびプログラミング言語ワークショップ(PPL2019)論文集, 2019
Dynamic Type Inference for Gradual Hindley-Milner Typing
Proceedings of the ACM on Programming Languages, 2019
ワーカの重要度を考慮した並列実行フレームワークの障害耐性評価手法の検討
2019年並列／分散／協調処理に関する『北見』サマー・ワークショップ (SWoPP2019), 2019
汎用送受信に対応したHOPEコンパイラの研究
2019年並列／分散／協調処理に関する『北見』サマー・ワークショップ (SWoPP2019), 2019
JVM上の動的言語のための抽象解釈の実装
第60回プログラミング・シンポジウム, 2019
Extending a Work-Stealing Framework with Priorities and Weights
2019 IEEE/ACM 9th Workshop on Irregular Applications: Architectures and Algorithms (IA3), 2019
DOI: 10.1109/IA349570.2019.00008HOPE: A Parallel Execution Model Based on Hierarchical Omission
Proceedings of the 48th International Conference on Parallel Processing ({ICPP} 2019), 2019
DOI: 10.1145/3337821.33378992018Nondetermnistic Manifest Contracts
Proceedings of theInternational Symposium on Principles and Practice of Declarative Programming, 2018
DOI: 10.1145/3236950.3236964ContextWorkflow: A Monadic DSL for Compensable and Interruptible Executions
Proceedings of the 32nd European Conference on Object-Oriented Programming, 2018
Method Safety Mechanism for Asynchronous Layer Deactivation
Science of Computer Programming, 2018
DOI: 10.1016/j.scico.2018.01.006Automated Verification of Functional Correctness of Race-Free GPU Programs
Journal of Automated Reasoning, 2018
DOI: 10.1007/978-3-319-48869-1_7Reasoning about Polymorphic Manifest Contracts.
CoRR, 2018
A Guess-and-Assume Approach to Loop Fusion for Program Verification
Proceedings of the ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, 2018
DOI: 10.1145/3162070Automated Proof Synthesis for the Minimal Propositional Logic with Deep Neural Networks
APLAS 2018, 2018
DOI: 10.1007/978-3-030-02768-1_17MONAA: A Tool for Timed Pattern Matching with Automata-Based Acceleration.
3rd Workshop on Monitoring and Testing of Cyber-Physical Systems, MT@CPSWeek 2018, Porto, Portugal, April 10, 2018, 2018
DOI: 10.1109/MT-CPS.2018.00014Generalized homogeneous polynomials for efficient template-based nonlinear invariant synthesis.
Theor. Comput. Sci., 2018
DOI: 10.1016/j.tcs.2018.06.005Probabilistic guards: A mechanism for increasing the granularity of work-stealing programs
Parallel Computing, 2018
分割統治型総和の部分的計算結果を効率よく利用する方式の研究
情報処理学会第121回プログラミング研究会, 2018
並列分散フレームワークの耐障害性評価のための通信障害模擬機能
第20回プログラミングおよびプログラミング言語ワークショップ(PPL2018), 2018
JVM上の動的言語のための抽象解釈
情報処理学会第121回プログラミング研究会, 2018
2017A Nonstandard Functional Programming Language
Proceedings of Asian Symposium on Programming Languages and Systems (APLAS2017), 2017
DOI: 10.1007/978-3-319-71237-6_25A DSL for Compensable and Interruptible Executions
Proceedings of 4th Workshop on Reactive and Event-based Languages & Systems (REBLS), 2017
C言語における無効なスタック領域へのポインタを検出する静的解析
日本ソフトウェア科学会第34回大会論文集, 2017
On Polymorphic Gradual Typing
Proceedings of the ACM on Programming Languages, 2017
A Type Reconstruction Algorithm for Gradually Typed Delimited Continuations
第19回プログラミングおよびプログラミング言語ワークショップ(PPL2017)論文集, 2017
Stateful manifest contracts
Conference Record of the Annual ACM Symposium on Principles of Programming Languages, 2017
DOI: 10.1145/3009837.3009875Verification of Code Generators via Higher-Order Model Checking
Proceedings of the 2017 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM'17), 2017
DOI: 10.1145/3018882.3018886Polymorphic Manifest Contracts, Revised and Resolved
ACM Transactions on Programming Languages and Systems, 2017
Sharper and Simpler Nonlinear Interpolants for Program Verification.
Programming Languages and Systems - 15th Asian Symposium(APLAS), 2017
DOI: 10.1007/978-3-319-71237-6_24Efficient Online Timed Pattern Matching by Automata-Based Skipping
FORMATS 2017, 2017
DOI: 10.1007/978-3-319-65765-3_13Towards Proof Synthesis Guided by Neural Machine Translation for Intuitionistic Propositional Logic
CoRR, 2017
アクセス制御論理に基づくIoT向け分散型アクセス制御フレームワーク
第15回 ディペンダブルシステムワークショップ (DSW 2017), 2017
アクセス制御機能の組み込まれた拡張オブジェクト指向言語
情報処理学会 第58回プログラミング・シンポジウム, 2017
優先度ならびに重みを用いたワークスティールフレームワークの性能改善
The 1st. cross-disciplinary Workshop on Computing Systems, Infrastructures, and Programming (xSIG 2017), 2017
仮想環境を考慮した要求駆動型負荷分散
日本ソフトウェア科学会第34回大会, 2017
HOPEコンパイラのプロトタイプ実装
2017年並列/分散/協調処理に関する『秋田』サマー・ワークショップ (SWoPP2017), 2017
2016階層的グループ化に基づきAndroidアプリの安全性を向上するバイトコード書換えツール
日本ソフトウェア科学会第33回大会論文集, 2016
An Extended Behavioral Type System for Memory-Leak Freedom
日本ソフトウェア科学会第33回大会論文集, 2016
SIMT のための Hoare 論理の Coq を用いた形式化と 並列 prefix-sum アルゴリズムの検証
第18回プログラミングおよびプログラミング言語ワークショップ(PPL2016)論文集, 2016
Gradual typing for delimited continuations
The 5th Script To Program Evolution Workshop, 2016
A Library-Based Approach to Context-Dependent Computation with Reactive Values
Proceedings of Constrained and Reactive Objects Workshop (CROW2016), 2016
DOI: 10.1145/2892664.2892669規則違反コードの構造を反映した木パタンを用いるコード検査器
情報処理学会論文誌 プログラミング, 2016
仮想環境を考慮した要求駆動型負荷分散の検討
第18回プログラミングおよびプログラミング言語ワークショップ(PPL2016), 2016
Preliminary Evaluations of Probabilistic Guards for a Work-Stealing Framework
Annual Meeting on Advanced Computing System and Infrastructure (ACSI) 2016, 2016
HOPEコンパイラの実装に向けて
第18回プログラミングおよびプログラミング言語ワークショップ(PPL2016), 2016
An MPI-based Implementation of the Tascell Task-Parallel Programming Language
Annual Meeting on Advanced Computing System and Infrastructure (ACSI) 2016, 2016
Evaluation of an MPI-based Implementation of the Tascell Task-Parallel Language on Massively Parallel Systems
PROCEEDINGS OF 45TH INTERNATIONAL CONFERENCE ON PARALLEL PROCESSING WORKSHOPS (ICPPW 2016), 2016
DOI: 10.1109/ICPPW.2016.36Extending aWork-Stealing Framework with Probabilistic Guards
PROCEEDINGS OF 45TH INTERNATIONAL CONFERENCE ON PARALLEL PROCESSING WORKSHOPS (ICPPW 2016), 2016
DOI: 10.1109/ICPPW.2016.372015参照を備えた多段階計算のための多相的型システム
日本ソフトウェア科学会第32回大会論文集, 2015
Visibility of Context-oriented Behavior and State in L
Computer Software, 2015
DOI: 10.11309/jssst.32.3_149Manifest contracts for datatypes
Conference Record of the Annual ACM Symposium on Principles of Programming Languages, 2015
DOI: 10.1145/2676726.2676996A Sound Type System for Layer Subtyping and Dynamically Activated First-Class Layers
Proceedings of Asian Symposium on Programming Languages and Systems (APLAS 2015), 2015
DOI: 10.1007/978-3-319-26529-2_24Shifting the Blame: A Blame Calculus with Delimited Control
Proceedings of Asian Symposium on Programming Languages and Systems (APLAS 2015), 2015
DOI: 10.1007/978-3-319-26529-2_11Input Synthesis for Sampled Data Systems by Program Logic
Proc. of the 4th Workshop on Hybrid Autonomous Systems (HAS 2014), 2015
DOI: 10.4204/EPTCS.174.3Validated Numerics Meets Reachability Analysis for CPS Design (NII Shonan Meeting 2015-14).
NII Shonan Meet. Rep., 2015
Design and Implementation of a Java Bytecode Manipulation Library for Clojure
Journal of Information Processing, 2015
メッセージ媒介システムの構想と試験実装
Annual Meeting on Advanced Computing System and Infrastructure (ACSI) 2015, 2015
Clojure用JVMバイトコード操作ライブラリの設計と実装
情報処理学会第102回プログラミング研究会, 2015
2014Automatic Memory Management Based on Program Transformation using Ownerships
Proceedings of Asian Symposium on Programming Languages and Systems (APLAS), 2014
DOI: 10.1007/978-3-319-12736-1_4Formalization of Featherweight Java and Featherweight GJ by using weak HOAS on Coq
日本ソフトウェア科学会大会論文集, 2014
Automatic Synthesis of Combiners in the MapReduce Framework: An Approach with Right Inverse
Proceedings of International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR), 2014
On-Demand Layer Activation for Type-Safe Deactivation
International Workshop on Context-Oriented Programming, COP'14 - Co-located with the 26th European Conference on Object-Oriented Programming, ECOOP'14, 2014
DOI: 10.1145/2637066.2637070Towards Type-Safe JCop: A type system for layer inheritance and first-class layers
International Workshop on Context-Oriented Programming, COP'12 - Co-located with the 26th European Conference on Object-Oriented Programming, ECOOP'14, 2014
DOI: 10.1145/2637066.2637073On Cross-Stage Persistence in Multi-Stage Programming
Proceedings of Intl. Symposium on Functional and Logic Programming (FLOPS2014), 2014
DOI: 10.1007/978-3-319-07151-0_7顕在的契約計算のための代数的データ型
第16回プログラミングおよびプログラミング言語ワークショップ(PPL2014)論文集, 2014
Formal Verification of CPS : A Nonstandard Analysis Approach
Journal of The Society of Instrument and Control Engineers, 2014
DOI: 10.11499/sicejl.53.1080Practical Implementation Techniques of Ambient Calculus in Conventional Dynamic Languages
29th Symposium on Applied Computing (SAC 2014), 2014
JVMバイトコードへの低水準操作を簡潔に記述可能なマクロシステム
情報処理学会 第55回プログラミング・シンポジウム, 2014
2013A Hoare Logic for SIMT Programs
Proceedings of Asian Symposium on Programming Languages and Systems (APLAS2013), 2013
DOI: 10.1007/978-3-319-03542-0_5多段階計算λ▹のための越段階埋込
日本ソフトウェア科学会第30回大会論文集, 2013
Layer Refinement in L
並列/分散/協調処理に関するサマー・ワークショップ (SWoPP), 2013
L: Context-oriented programming with only layers
Proceedings of the 5th International Workshop on Context-Oriented Programming, COP 2013, 2013
DOI: 10.1145/2489793.2489797Model-Checking Higher-Order Programs with Recursive Types
Proceedings of European Symposium on Programming (ESOP2013), 2013
DOI: 10.1007/978-3-642-37036-6_24Hyperstream processing systems: Nonstandard modeling of continuous-time signals
Conference Record of the Annual ACM Symposium on Principles of Programming Languages, 2013
DOI: 10.1145/2429069.2429120Safeアンビエントに基づく分散アプリケーション開発用Lisp環境
コンピュータソフトウェア, 2013
L-Closureの呼び出しコストの削減
情報処理学会論文誌 プログラミング, 2013
2012Type-based safe resource deallocation for shared-memory concurrency
Proceedings of Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), 2012
DOI: 10.1145/2398857.2384618A Type System for Dynamic Layer Composition
Proceedings of the International Workshop on Foundations of Object-Oriented Languages (FOOL2012), 2012
顕在的契約計算におけるアップキャスト除去
第14回プログラミングおよびプログラミング言語ワークショップ, 2012
Exercises in Nonstandard Static Analysis of Hybrid Systems
24th International Conference, CAV 2012, 2012
DOI: 10.1007/978-3-642-31424-7_34SEAN: Support Tool for Detecting Rule Violations in JNI Coding
IPSJ Transactions on Programming, 2012
JNIコーディングの規則違反を検出するための支援ツールSEANの開発
情報処理学会第87回プログラミング研究会, 2012
Detecting Bugs in Android Using a Static Escape Analyzer SEAN for Native Code
10th Asian Symposium on Programming Languages and Systems (APLAS 2012), 2012
2011Constructive linear-time temporal logic: Proof systems and Kripke semantics
Information and Computation, 2011
DOI: 10.1016/j.ic.2010.09.008Systematic Derivation of a λ○ Virtual Machine with Low-Level Code Generation by using Fusion Transformation
日本ソフトウェア科学会第28回大会論文集, 2011
Polymorphic Contracts
Proceedings of European Symposium on Programming (ESOP2011), 2011
DOI: 10.1007/978-3-642-19718-5_2Special track on object-oriented languages and systems
Proceedings of the ACM Symposium on Applied Computing, 2011
Gradual typing for generics
Proceedings of the 2011 ACM international conference on Object oriented programming systems languages and applications - OOPSLA '11, 2011
DOI: 10.1145/2048066.2048114ContextFJ: A minimal core calculus for context-oriented programming
Proceedings of the 10th International Workshop on Foundations of Aspect-Oriented Languages, FOAL 2011, 2011
DOI: 10.1145/1960510.1960515Ordered Types for Stream Processing of Tree-Structured Data
Information and Media Technologies, 2011
DOI: 10.11185/imt.6.385Programming with Infinitesimals: A WHILE-Language for Hybrid System Modeling
Automata, Languages and Programming, ICALP, Pt II, 2011
DOI: 10.1007/978-3-642-22012-8_312010A Logical Foundation for Environment Classifiers
Logical Methods in Computer Science, 2010
DOI: 10.2168/lmcs-6(4:8)2010Mostly modular compilation of crosscutting concerns by contextual predicate dispatch
Proceedings of Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), 2010
DOI: 10.1145/1932682.1869503Type relaxed weaving
AOSD.10 - 9th International Conference on Aspect-Oriented Software Development, 2010
DOI: 10.1145/1739230.17392452009Matching ThisType to subtyping
Proceedings of the ACM Symposium on Applied Computing, 2009
DOI: 10.1145/1529282.1529699Self type constructors
Proceeding of the 24th ACM SIGPLAN conference on Object oriented programming systems languages and applications - OOPSLA 09, 2009
DOI: 10.1145/1640089.1640109Towards gradual typing for generics
Proceedings for the 1st Workshop on Script to Program Evolution, STOP'09 in Conjunction with European Conference on Object-Oriented Programming, ECOOP'09, 2009
DOI: 10.1145/1570506.15705092008Proving Noninterference by a Fully Complete Translation to the Simply Typed lambda-calculus
Logical Methods in Computer Science, 2008
DOI: 10.2168/lmcs-4(3:10)2008On Constructive Linear-Time Temporal Logic
Proceedings of the Workshop on Intuitionistil Modal Logic and Applications (IMLA'08), 2008
Lightweight family polymorphism
Journal of Functional Programming, 2008
DOI: 10.1017/s0956796807006405Featherweight Java のための漸進的型付け
第10回プログラミングおよびプログラミング言語ワークショップ(PPL2008)論文集, 2008
文脈依存資源使用解析のための型システム
第10回プログラミングおよびプログラミング言語ワークショップ(PPL2008)論文集, 2008
The essence of lightweight family polymorphism
Journal of Object Technology, 2008
DOI: 10.5381/jot.2008.7.5.a32007Proving Noninterference by a Fully Complete Translation to the Simply Typed λ-Calculus
Advances in Computer Science - ASIAN 2006. Secure Software and Related Issues, 2007
DOI: 10.1007/978-3-540-77505-8_24Variant path types for scalable extensibility
Proceedings of the 22nd annual ACM SIGPLAN conference on Object oriented programming systems and applications - OOPSLA '07, 2007
DOI: 10.1145/1297027.1297037An Algorithm to Decide Conformance of Resource Usage to Specification for Resource Usage Verification
情報処理学会論文誌. プログラミング, 2007
Union types for object-oriented programming
Journal of Object Technology, 2007
Deriving compilers and virtual machines for a multi-level language
Proceedings of Asian Symposium on Programming Languages and Systems (APLAS 2007), 2007
2006Variant parametric types: A flexible subtyping scheme for generics
ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2006
DOI: 10.1145/1152649.1152650様相型に基づく情報流解析における非干渉性の論理関係による一般化とその証明
第8回プログラミングおよびプログラミング言語ワークショップ(PPL2006)論文集, 2006
Resource usage analysis for a functional language with exceptions
Proceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, 2006
DOI: 10.1145/1111542.1111550A modal type system for multi-level generating extensions with persistent code
PPDP'06 - Proceedings of the Eight ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming, 2006
2005Resource usage analysis
ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2005
DOI: 10.1145/1057387.1057390例外機構を備えた言語のための資源使用法解析
第7回プログラミングおよびプログラミング言語ワークショップ(PPL2005)論文集, 2005
メタプログラミングのための時相論理に基づく型付λ計算
第7回プログラミングおよびプログラミング言語ワークショップ(PPL2005)論文集, 2005
2004Generics・Union 型を導入したオブジェクト指向計算体系
第6回プログラミングおよびプログラミング言語ワークショップ(PPL2004)論文集, 2004
A generic type system for the Pi-calculus
THEORETICAL COMPUTER SCIENCE, 2004
DOI: 10.1016/S0304-3975(03)00325-6A modal foundation for secure information flow
Proceedings of the Workshop on Foundations of Computer Security (FCS'04), number 31 in Turku Centre for Computer Science General Publication,187-203, 2004
2003Union 型を導入したオブジェクト指向計算体系
日本ソフトウェア科学会第20回大会論文集, 2003
擬似引用を持つ型付計算体系λq
第5回プログラミングおよびプログラミング言語ワークショップ(PPL2003)論文集, 2003
2002On variance-based subtyping for parametric types
ECOOP 2002 - OBJECT-ORIENTED PROGRAMMING, 2002
2001Featherweight Java: A minimal core calculus for Java and GJ
ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2001
DOI: 10.1145/503502.503505A Recipe for Raw Types
Proceedings of the International Workshop on Foundations of Object-Oriented Languages (FOOL8), 2001
2000Garbage Collection Based on a Linear Type System
Proceedings of the 3rd ACM SIGPLAN Wokshop on Types in Compilation (TIC'00), 2000
Type reconstruction for linear pi-calculus with I/O subtyping
INFORMATION AND COMPUTATION, 2000
DOI: 10.1006/inco.2000.28721999Featherweight Java - A minimal core calculus for Java and GJ
Proceedings of ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA'99), 1999
1997Type-based Analysis of Communication for Concurrent Programming Languages
Proceedings of the Fourth International Static Analysis Symposium, 1997
Compile-Time Tensor Shape Checking via Staged Shape-Dependent Types
Proceedings of ECOOP 2026, 2026
Proceedings of ECOOP 2026, 2026
Ownership Refinement Types for Pointer Arithmetic and Nested Arrays
Proceedings of ECOOP 2026, 2026
Proceedings of ECOOP 2026, 2026
Contextual Metaprogramming for Session Types
Programming Languages and Systems - 35th European Symposium on Programming, ESOP 2026, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2026, Turin, Italy, April 11-16, 2026, Proceedings, Part I., 2026
DOI: 10.1007/978-3-032-22720-1_2
Programming Languages and Systems - 35th European Symposium on Programming, ESOP 2026, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2026, Turin, Italy, April 11-16, 2026, Proceedings, Part I., 2026
DOI: 10.1007/978-3-032-22720-1_2
An ML-style module system for cross-stage type abstraction in multi-stage programming
Science of Computer Programming, 2026
DOI: 10.1016/j.scico.2025.103379
Science of Computer Programming, 2026
DOI: 10.1016/j.scico.2025.103379
A Fast and Soft Pattern Matcher for Trillion-Scale Corpus
ICML 2026 (accepted), 2026
ICML 2026 (accepted), 2026
Evaluating Hybrid Automata Learning Tools Based on Their Success in Formal Verification
MED 2026 (Accepted), 2026
MED 2026 (Accepted), 2026
SoftMatcha 2: 1 兆語規模コーパスの超高速かつ柔らかい検索
言語処理学会 第32回年次大会 発表論文集, 2026
言語処理学会 第32回年次大会 発表論文集, 2026
In-Situ Hardware Error Detection Using Specification-Derived Petri Net Models and Behavior-Derived State Sequences
IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems (Accepted), 2026
IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems (Accepted), 2026
Componentwise Automata Learning for System Integration
ATVA 2025, 2026
DOI: 10.1007/978-3-032-08707-2_1
ATVA 2025, 2026
DOI: 10.1007/978-3-032-08707-2_1
SoftMatcha 2: A Fast and Soft Pattern Matcher for Trillion-Scale Corpora
DOI: 10.48550/ARXIV.2602.10908
DOI: 10.48550/ARXIV.2602.10908
RapunSL: Untangling Quantum Computing with Separation, Linear Combination and Mixing
Proceedings of the ACM on Programming Languages, 2026
DOI: 10.1145/3776648
Proceedings of the ACM on Programming Languages, 2026
DOI: 10.1145/3776648
Making Rabbit Run for Security Verification of Networked Systems with Unbounded Loops
Proceedings of Formal Methods in Computer-Aided Design (FMCAD), 2025
Proceedings of Formal Methods in Computer-Aided Design (FMCAD), 2025
動的型推論を備えた空間効率の良い漸進的型付け
日本ソフトウェア科学会第42回大会論文集, 2025
日本ソフトウェア科学会第42回大会論文集, 2025
Unifying Function- and Argument-First Bidirectional Type Systems
日本ソフトウェア科学会第42回大会論文集, 2025
日本ソフトウェア科学会第42回大会論文集, 2025
Efficient Black-Box Checking with Specification-Guided Abstraction
ACM Transactions on Embedded Computing Systems, 2025
DOI: 10.1145/3762659
ACM Transactions on Embedded Computing Systems, 2025
DOI: 10.1145/3762659
StatWhy: Formal Verification Tool for Statistical Hypothesis Testing Programs
CAV 2025, 2025
DOI: 10.1007/978-3-031-98679-6_10
CAV 2025, 2025
DOI: 10.1007/978-3-031-98679-6_10
Certifying Lyapunov Stability of Black-Box Nonlinear Systems via Counterexample Guided Synthesis
HSCC 2025 (To appear), 2025
HSCC 2025 (To appear), 2025
A Soft and Fast Pattern Matcher for Billion-Scale Corpus Searches
ICLR 2025 (To appear), 2025
ICLR 2025 (To appear), 2025
Hardware Error Detection with In-Situ Monitoring of Control Flow-Related Specifications
Proceedings of the 30th Asia and South Pacific Design Automation Conference, 2025
DOI: 10.1145/3658617.3697744
Proceedings of the 30th Asia and South Pacific Design Automation Conference, 2025
DOI: 10.1145/3658617.3697744
CHLOE: Loop Transformation over Fully Homomorphic Encryption via Multi-Level Vectorization and Control-Path Reduction.
IEEE Symposium on Security and Privacy(SP), 2025
DOI: 10.1109/SP61157.2025.00035
IEEE Symposium on Security and Privacy(SP), 2025
DOI: 10.1109/SP61157.2025.00035
Hyper Pattern Matching.
Runtime Verification - 25th International Conference(RV), 2025
DOI: 10.1007/978-3-032-05435-7_22
Runtime Verification - 25th International Conference(RV), 2025
DOI: 10.1007/978-3-032-05435-7_22
SoftMatcha: A Soft and Fast Pattern Matcher for Billion-Scale Corpus Searches.
The Thirteenth International Conference on Learning Representations(ICLR), 2025
The Thirteenth International Conference on Learning Representations(ICLR), 2025
Nola: Later-Free Ghost State for Verifying Termination in Iris
Proceedings of the ACM on Programming Languages, 2025
DOI: 10.1145/3729250
Proceedings of the ACM on Programming Languages, 2025
DOI: 10.1145/3729250
SoftMatcha: A Soft and Fast Pattern Matcher for Billion-Scale Corpus Searches
13th International Conference on Learning Representations (ICLR 2025), 2025
13th International Conference on Learning Representations (ICLR 2025), 2025
2024Type-Based Verification of Connectivity Constraints in Lattice Surgery
Proceedings of the 22nd Asian Symposium on Programming Languages and Systems, 2024
DOI: 10.1007/978-981-97-8943-6_11Rabbit: A Language to Model and Verify Data Flow in Networked Systems
2024 International Symposium on Networks, Computers and Communications (ISNCC), 2024
DOI: 10.1109/isncc62547.2024.10758938Space-Efficient Polymorphic Gradual Typing, Mostly Parametric
Proceedings of the ACM on Programming Languages, 2024
DOI: 10.1145/3656441Signature restriction for polymorphic algebraic effects
Journal of Functional Programming, 2024
DOI: 10.1017/s0956796824000054Linear Contextual Metaprogramming and Session Types
Electronic Proceedings in Theoretical Computer Science, 2024
DOI: 10.4204/eptcs.401.1命令型プログラムの安全性検証のための所有権主導変換
第26回プログラミングおよびプログラミング言語ワークショップ(PPL2024)論文集, 2024
iCon: Automated Verification of Inter-Transaction Properties in Tezos Smart Contracts with Unknowns
Proceedings of 2024 IEEE International Conference on Blockchain and Cryptocurrency (ICBC), 2024
Oblivious Monitoring for Discrete-Time STL via Fully Homomorphic Encryption.
Runtime Verification - 24th International Conference(RV), 2024
DOI: 10.1007/978-3-031-74234-7_4HEIR: A Unified Representation for Cross-Scheme Compilation of Fully Homomorphic Computation.
31st Annual Network and Distributed System Security Symposium(NDSS), 2024
制御フロー仕様から生成したペトリネットに基づくハードウェア誤動作検出手法
DAシンポジウム2024論文集, 2024
Goal-Aware RSS for Complex Scenarios via Program Logic
2024 IEEE Intelligent Vehicles Symposium (IV), 2024
DOI: 10.1109/iv55156.2024.10588754Sound and relatively complete belief Hoare logic for statistical hypothesis testing programs.
Artif. Intell., 2024
DOI: 10.1016/j.artint.2023.104045Control-data separation and logical condition propagation for efficient inference on probabilistic programs
Journal of Logical and Algebraic Methods in Programming, 2024
DOI: 10.1016/j.jlamp.2023.100922Hyper Parametric Timed CTL.
IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2024
DOI: 10.1109/TCAD.2024.3443704Temporal Logic Formalisation of ISO 34502 Critical Scenarios: Modular Construction with the RSS Safety Distance
39th ACM/SIGAPP Symposium On Applied Computing, 2024
DOI: 10.1145/3605098.3636014Temporal Logic Formalisation of ISO 34502 Critical Scenarios: Modular Construction with the RSS Safety Distance.
CoRR, 2024
DOI: 10.48550/arXiv.2403.18764Learning Weighted Finite Automata over the Max-Plus Semiring and its Termination.
CoRR, 2024
DOI: 10.48550/arXiv.2407.09775Bi-Abduction in Separation Logic with Arrays and Lists for Program Analysis
Computer Software, 2024
DOI: 10.11309/jssst.41.1_502023Rabbit: a modeling language for verifying cybersecurity in IoT system
第145回情報処理学会プログラミング研究会資料, 2023
Contextual Modal Type Theory with Polymorphic Contexts
Proceedings of European Symposium on Programming, 2023
DOI: 10.1007/978-3-031-30044-8_11LLTZ: LLMV IR からスマートコントラクト記述言語 Michelson へのコンパイラ
第25回プログラミングおよびプログラミング言語ワークショップ(PPL2023)論文集, 2023
Probabilistic Black-Box Checking via Active MDP Learning
ACM Transactions on Embedded Computing Systems, 2023
DOI: 10.1145/3609127Feature Attributionを用いたdlshogiの指し手の解釈可能性向上手法
研究報告ゲーム情報学（GI）, 2023
LLTZ: LLVM IR からスマートコントラクト記述言語 Michelson へのコンパイラ
第25回プログラミングおよびプログラミング言語ワークショップ (PPL 2023) 論文集, 2023
Learning Nonlinear Hybrid Automata from Input-Output Time-Series Data.
ATVA (1), 2023
DOI: 10.1007/978-3-031-45329-8_2Active Learning of Deterministic Timed Automata with Myhill-Nerode Style Characterization.
Computer Aided Verification - 35th International Conference, Part I, 2023
DOI: 10.1007/978-3-031-37706-8_1Parametric Timed Pattern Matching."
ACM Transactions on Software Engineering and Methodology, 2023
DOI: 10.1145/35171942022SCameleer: スマートコントラクト記述言語SCamlのための自動検証器
日本ソフトウェア科学会第39回大会論文集, 2022
スマートコントラクト検証器Helmholtzのためのエラー原因提示手法
日本ソフトウェア科学会第39回大会論文集, 2022
暗黙に相互運用可能なレコードとハッシュテーブルのための型推論とコンパイル手法
日本ソフトウェア科学会第39回大会論文集, 2022
Helmholtz: A Verifier for Tezos Smart Contracts Based on Refinement Types
New Generation Computing, 2022
DOI: 10.1007/s00354-022-00167-1ZT-IoT: ゼロトラストIoTのためのシステムソフトウェア構築に向けて
第154回情報処理学会システムソフトウェアとオペレーティング・システム研究会資料, 2022
Stage-Aware Equality Types for a Dependently-Typed Multi-Stage Calculus
第24回プログラミングおよびプログラミング言語ワークショップ(PPL2022)論文集, 2022
Type-based Qubit Allocation for a First-Order Quantum Programming Language
第24回プログラミングおよびプログラミング言語ワークショップ(PPL2022)論文集, 2022
BOREx: Bayesian-Optimization-Based Refinement of Saliency Map for Image- and Video-Classification Models.
ACCV (7), 2022
DOI: 10.1007/978-3-031-26293-7_17Oblivious Online Monitoring for Safety LTL Specification via Fully Homomorphic Encryption.
CAV 2022, 2022
DOI: 10.1007/978-3-031-13185-1_22The Lattice-Theoretic Essence of Property Directed Reachability Analysis.
CAV 2022, 2022
DOI: 10.1007/978-3-031-13185-1_12ARCH-COMP 2022 Category Report: Falsification with Ubounded Resources
EPiC Series in Computing, 2022
DOI: 10.29007/fhnkDynamic Shielding for Reinforcement Learning in Black-Box Environments.
International Symposium on Automated Technology for Verification and Analysis, 2022
DOI: 10.1007/978-3-031-19992-9_2Exemplifying parametric timed specifications over signals with bounded behavior.
NASA Formal Methods Symposium, 2022
DOI: 10.1007/978-3-031-06773-0_25Data for "Exemplifying parametric timed specifications over signals with bounded behavior".
DOI: 10.5281/zenodo.6382893Model-Bounded Monitoring of Hybrid Systems."
ACM Transactions on Cyber-Physical Systems, 2022
DOI: 10.1145/35290952021Is Space-Efficient Polymorphic Gradual Typing Possible?
Informal Proceedings of Scheme and Functional Programming Workshop, 2021
HELMHOLTZ: A Verifier for Tezos Smart Contracts Based on Refinement Types.
CoRR, 2021
Verification of a Merkle Patricia Tree Library Using F.
CoRR, 2021
完全準同型暗号を用いた秘匿LTLオンラインモニタリング
コンピュータセキュリティシンポジウム 2021 (CSS 2021), 2021
Formalizing Statistical Beliefs in Hypothesis Testing Using Program Logic.
Proceedings of the 18th International Conference on Principles of Knowledge Representation and Reasoning(KR), 2021
DOI: 10.24963/kr.2021/39Efficient Black-Box Checking via Model Checking with Strengthened Specifications
Runtime Verification - 21st International Conference(RV), 2021
DOI: 10.1007/978-3-030-88494-9_6Enhancing Loop-Invariant Synthesis via Reinforcement Learning.
CoRR, 2021
Verification of a Merkle Patricia Tree Library Using F*
CoRR, 2021
ARCH-COMP 2021 Category Report: Falsification with Validation of Results.
ARCH@ADHS, 2021
DOI: 10.29007/xwl1Hybrid System Falsification for Multiple-Constraint Parameter Synthesis: a Gas Turbine Case Study.
24th International Symposium on Formal Methods, 2021
DOI: 10.1007/978-3-030-90870-6_17Constrained Optimization for Falsification and Conjunctive Synthesis.
6th IFAC Conference on Analysis and Design of Hybrid Systems, 2021
DOI: 10.1016/j.ifacol.2021.08.501Model-Bounded Monitoring of Hybrid Systems.
12th ACM/IEEE International Conference on Cyber-Physical Systems, 2021
DOI: 10.1145/3450267.34505312020Space-Efficient Gradual Typing in Coercion-Passing Style.
34th European Conference on Object-Oriented Programming, ECOOP 2020, 2020
DOI: 10.4230/LIPIcs.ECOOP.2020.8量子ビット連結性制約検査のための依存型システム
日本ソフトウェア科学会第37回大会論文集, 2020
ConSORT: Context- and Flow-Sensitive Ownership Refinement Types for Imperative Programs
Programming Languages and Systems, 2020
DOI: 10.1007/978-3-030-44914-8_25スタック領域上での時間的メモリ安全性を保証する静的解析手法
第22回プログラミングおよびプログラミング言語ワークショップ(PPL2020)論文集, 2020
スマートコントラクトのための Effectively Callback-Free 性の型に基づく静的検証
第22回プログラミングおよびプログラミング言語ワークショップ(PPL2020)論文集, 2020
F* を用いた Merkle Patricia Tree ライブラリの形式検証
第22回プログラミングおよびプログラミング言語ワークショップ(PPL2020)論文集, 2020
Compilation of Coordinated Choice.
CoRR, 2020
Signature restriction for polymorphic algebraic effects.
Proc. ACM Program. Lang., 2020
DOI: 10.1145/3408999Space-Efficient Gradual Typing in Coercion-Passing Style
Informal Proceedings of the 1st International Workshop on Gradual Typing (WGT2020), 2020
Gradual Typing for Extensibility by Rows
Informal Proceedings of the 1st International Workshop on Gradual Typing (WGT2020), 2020
Visualizing Color-Wise Saliency of Black-Box Image Classification Models.
Proceedings of ACCV 2020, 2020
DOI: 10.1007/978-3-030-69535-4_12Generalized Property-Directed Reachability for Hybrid Systems
Verification, Model Checking, and Abstract Interpretation - 21st International Conference(VMCAI), 2020
DOI: 10.1007/978-3-030-39322-9_14A Contract Corpus for Recognizing Rights and Obligations.
Proceedings of The 12th Language Resources and Evaluation Conference(LREC), 2020
2019A Dependently Typed Multi-stage Calculus.
Programming Languages and Systems - 17th Asian Symposium, APLAS 2019, Nusa Dua, Bali, Indonesia, December 1-4, 2019, Proceedings, 2019
DOI: 10.1007/978-3-030-34175-6_4Manifest Contracts with Intersection Types.
Programming Languages and Systems - 17th Asian Symposium, APLAS 2019, Nusa Dua, Bali, Indonesia, December 1-4, 2019, Proceedings, 2019
DOI: 10.1007/978-3-030-34175-6_3Temporal Verification of Programs via First-Order Fixpoint Logic.
Static Analysis - 26th International Symposium, SAS 2019, Porto, Portugal, October 8-11, 2019, Proceedings, 2019
DOI: 10.1007/978-3-030-32304-2_20A Type System for First-Class Layers with Inheritance, Subtyping, and Swapping
Science of Computer Programming, 2019
Handling Polymorphic Algebraic Effects
Proceedings of European Symposium on Programming (ESOP2019), 2019
空間効率の良いコアーション計算のためのコアーション渡し形式
第21回プログラミングおよびプログラミング言語ワークショップ(PPL2019)論文集, 2019
Dynamic Type Inference for Gradual Hindley-Milner Typing
Proceedings of the ACM on Programming Languages, 2019
ワーカの重要度を考慮した並列実行フレームワークの障害耐性評価手法の検討
2019年並列／分散／協調処理に関する『北見』サマー・ワークショップ (SWoPP2019), 2019
汎用送受信に対応したHOPEコンパイラの研究
2019年並列／分散／協調処理に関する『北見』サマー・ワークショップ (SWoPP2019), 2019
JVM上の動的言語のための抽象解釈の実装
第60回プログラミング・シンポジウム, 2019
Extending a Work-Stealing Framework with Priorities and Weights
2019 IEEE/ACM 9th Workshop on Irregular Applications: Architectures and Algorithms (IA3), 2019
DOI: 10.1109/IA349570.2019.00008HOPE: A Parallel Execution Model Based on Hierarchical Omission
Proceedings of the 48th International Conference on Parallel Processing ({ICPP} 2019), 2019
DOI: 10.1145/3337821.33378992018Nondetermnistic Manifest Contracts
Proceedings of theInternational Symposium on Principles and Practice of Declarative Programming, 2018
DOI: 10.1145/3236950.3236964ContextWorkflow: A Monadic DSL for Compensable and Interruptible Executions
Proceedings of the 32nd European Conference on Object-Oriented Programming, 2018
Method Safety Mechanism for Asynchronous Layer Deactivation
Science of Computer Programming, 2018
DOI: 10.1016/j.scico.2018.01.006Automated Verification of Functional Correctness of Race-Free GPU Programs
Journal of Automated Reasoning, 2018
DOI: 10.1007/978-3-319-48869-1_7Reasoning about Polymorphic Manifest Contracts.
CoRR, 2018
A Guess-and-Assume Approach to Loop Fusion for Program Verification
Proceedings of the ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, 2018
DOI: 10.1145/3162070Automated Proof Synthesis for the Minimal Propositional Logic with Deep Neural Networks
APLAS 2018, 2018
DOI: 10.1007/978-3-030-02768-1_17MONAA: A Tool for Timed Pattern Matching with Automata-Based Acceleration.
3rd Workshop on Monitoring and Testing of Cyber-Physical Systems, MT@CPSWeek 2018, Porto, Portugal, April 10, 2018, 2018
DOI: 10.1109/MT-CPS.2018.00014Generalized homogeneous polynomials for efficient template-based nonlinear invariant synthesis.
Theor. Comput. Sci., 2018
DOI: 10.1016/j.tcs.2018.06.005Probabilistic guards: A mechanism for increasing the granularity of work-stealing programs
Parallel Computing, 2018
分割統治型総和の部分的計算結果を効率よく利用する方式の研究
情報処理学会第121回プログラミング研究会, 2018
並列分散フレームワークの耐障害性評価のための通信障害模擬機能
第20回プログラミングおよびプログラミング言語ワークショップ(PPL2018), 2018
JVM上の動的言語のための抽象解釈
情報処理学会第121回プログラミング研究会, 2018
2017A Nonstandard Functional Programming Language
Proceedings of Asian Symposium on Programming Languages and Systems (APLAS2017), 2017
DOI: 10.1007/978-3-319-71237-6_25A DSL for Compensable and Interruptible Executions
Proceedings of 4th Workshop on Reactive and Event-based Languages & Systems (REBLS), 2017
C言語における無効なスタック領域へのポインタを検出する静的解析
日本ソフトウェア科学会第34回大会論文集, 2017
On Polymorphic Gradual Typing
Proceedings of the ACM on Programming Languages, 2017
A Type Reconstruction Algorithm for Gradually Typed Delimited Continuations
第19回プログラミングおよびプログラミング言語ワークショップ(PPL2017)論文集, 2017
Stateful manifest contracts
Conference Record of the Annual ACM Symposium on Principles of Programming Languages, 2017
DOI: 10.1145/3009837.3009875Verification of Code Generators via Higher-Order Model Checking
Proceedings of the 2017 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM'17), 2017
DOI: 10.1145/3018882.3018886Polymorphic Manifest Contracts, Revised and Resolved
ACM Transactions on Programming Languages and Systems, 2017
Sharper and Simpler Nonlinear Interpolants for Program Verification.
Programming Languages and Systems - 15th Asian Symposium(APLAS), 2017
DOI: 10.1007/978-3-319-71237-6_24Efficient Online Timed Pattern Matching by Automata-Based Skipping
FORMATS 2017, 2017
DOI: 10.1007/978-3-319-65765-3_13Towards Proof Synthesis Guided by Neural Machine Translation for Intuitionistic Propositional Logic
CoRR, 2017
アクセス制御論理に基づくIoT向け分散型アクセス制御フレームワーク
第15回 ディペンダブルシステムワークショップ (DSW 2017), 2017
アクセス制御機能の組み込まれた拡張オブジェクト指向言語
情報処理学会 第58回プログラミング・シンポジウム, 2017
優先度ならびに重みを用いたワークスティールフレームワークの性能改善
The 1st. cross-disciplinary Workshop on Computing Systems, Infrastructures, and Programming (xSIG 2017), 2017
仮想環境を考慮した要求駆動型負荷分散
日本ソフトウェア科学会第34回大会, 2017
HOPEコンパイラのプロトタイプ実装
2017年並列/分散/協調処理に関する『秋田』サマー・ワークショップ (SWoPP2017), 2017
2016階層的グループ化に基づきAndroidアプリの安全性を向上するバイトコード書換えツール
日本ソフトウェア科学会第33回大会論文集, 2016
An Extended Behavioral Type System for Memory-Leak Freedom
日本ソフトウェア科学会第33回大会論文集, 2016
SIMT のための Hoare 論理の Coq を用いた形式化と 並列 prefix-sum アルゴリズムの検証
第18回プログラミングおよびプログラミング言語ワークショップ(PPL2016)論文集, 2016
Gradual typing for delimited continuations
The 5th Script To Program Evolution Workshop, 2016
A Library-Based Approach to Context-Dependent Computation with Reactive Values
Proceedings of Constrained and Reactive Objects Workshop (CROW2016), 2016
DOI: 10.1145/2892664.2892669規則違反コードの構造を反映した木パタンを用いるコード検査器
情報処理学会論文誌 プログラミング, 2016
仮想環境を考慮した要求駆動型負荷分散の検討
第18回プログラミングおよびプログラミング言語ワークショップ(PPL2016), 2016
Preliminary Evaluations of Probabilistic Guards for a Work-Stealing Framework
Annual Meeting on Advanced Computing System and Infrastructure (ACSI) 2016, 2016
HOPEコンパイラの実装に向けて
第18回プログラミングおよびプログラミング言語ワークショップ(PPL2016), 2016
An MPI-based Implementation of the Tascell Task-Parallel Programming Language
Annual Meeting on Advanced Computing System and Infrastructure (ACSI) 2016, 2016
Evaluation of an MPI-based Implementation of the Tascell Task-Parallel Language on Massively Parallel Systems
PROCEEDINGS OF 45TH INTERNATIONAL CONFERENCE ON PARALLEL PROCESSING WORKSHOPS (ICPPW 2016), 2016
DOI: 10.1109/ICPPW.2016.36Extending aWork-Stealing Framework with Probabilistic Guards
PROCEEDINGS OF 45TH INTERNATIONAL CONFERENCE ON PARALLEL PROCESSING WORKSHOPS (ICPPW 2016), 2016
DOI: 10.1109/ICPPW.2016.372015参照を備えた多段階計算のための多相的型システム
日本ソフトウェア科学会第32回大会論文集, 2015
Visibility of Context-oriented Behavior and State in L
Computer Software, 2015
DOI: 10.11309/jssst.32.3_149Manifest contracts for datatypes
Conference Record of the Annual ACM Symposium on Principles of Programming Languages, 2015
DOI: 10.1145/2676726.2676996A Sound Type System for Layer Subtyping and Dynamically Activated First-Class Layers
Proceedings of Asian Symposium on Programming Languages and Systems (APLAS 2015), 2015
DOI: 10.1007/978-3-319-26529-2_24Shifting the Blame: A Blame Calculus with Delimited Control
Proceedings of Asian Symposium on Programming Languages and Systems (APLAS 2015), 2015
DOI: 10.1007/978-3-319-26529-2_11Input Synthesis for Sampled Data Systems by Program Logic
Proc. of the 4th Workshop on Hybrid Autonomous Systems (HAS 2014), 2015
DOI: 10.4204/EPTCS.174.3Validated Numerics Meets Reachability Analysis for CPS Design (NII Shonan Meeting 2015-14).
NII Shonan Meet. Rep., 2015
Design and Implementation of a Java Bytecode Manipulation Library for Clojure
Journal of Information Processing, 2015
メッセージ媒介システムの構想と試験実装
Annual Meeting on Advanced Computing System and Infrastructure (ACSI) 2015, 2015
Clojure用JVMバイトコード操作ライブラリの設計と実装
情報処理学会第102回プログラミング研究会, 2015
2014Automatic Memory Management Based on Program Transformation using Ownerships
Proceedings of Asian Symposium on Programming Languages and Systems (APLAS), 2014
DOI: 10.1007/978-3-319-12736-1_4Formalization of Featherweight Java and Featherweight GJ by using weak HOAS on Coq
日本ソフトウェア科学会大会論文集, 2014
Automatic Synthesis of Combiners in the MapReduce Framework: An Approach with Right Inverse
Proceedings of International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR), 2014
On-Demand Layer Activation for Type-Safe Deactivation
International Workshop on Context-Oriented Programming, COP'14 - Co-located with the 26th European Conference on Object-Oriented Programming, ECOOP'14, 2014
DOI: 10.1145/2637066.2637070Towards Type-Safe JCop: A type system for layer inheritance and first-class layers
International Workshop on Context-Oriented Programming, COP'12 - Co-located with the 26th European Conference on Object-Oriented Programming, ECOOP'14, 2014
DOI: 10.1145/2637066.2637073On Cross-Stage Persistence in Multi-Stage Programming
Proceedings of Intl. Symposium on Functional and Logic Programming (FLOPS2014), 2014
DOI: 10.1007/978-3-319-07151-0_7顕在的契約計算のための代数的データ型
第16回プログラミングおよびプログラミング言語ワークショップ(PPL2014)論文集, 2014
Formal Verification of CPS : A Nonstandard Analysis Approach
Journal of The Society of Instrument and Control Engineers, 2014
DOI: 10.11499/sicejl.53.1080Practical Implementation Techniques of Ambient Calculus in Conventional Dynamic Languages
29th Symposium on Applied Computing (SAC 2014), 2014
JVMバイトコードへの低水準操作を簡潔に記述可能なマクロシステム
情報処理学会 第55回プログラミング・シンポジウム, 2014
2013A Hoare Logic for SIMT Programs
Proceedings of Asian Symposium on Programming Languages and Systems (APLAS2013), 2013
DOI: 10.1007/978-3-319-03542-0_5多段階計算λ▹のための越段階埋込
日本ソフトウェア科学会第30回大会論文集, 2013
Layer Refinement in L
並列/分散/協調処理に関するサマー・ワークショップ (SWoPP), 2013
L: Context-oriented programming with only layers
Proceedings of the 5th International Workshop on Context-Oriented Programming, COP 2013, 2013
DOI: 10.1145/2489793.2489797Model-Checking Higher-Order Programs with Recursive Types
Proceedings of European Symposium on Programming (ESOP2013), 2013
DOI: 10.1007/978-3-642-37036-6_24Hyperstream processing systems: Nonstandard modeling of continuous-time signals
Conference Record of the Annual ACM Symposium on Principles of Programming Languages, 2013
DOI: 10.1145/2429069.2429120Safeアンビエントに基づく分散アプリケーション開発用Lisp環境
コンピュータソフトウェア, 2013
L-Closureの呼び出しコストの削減
情報処理学会論文誌 プログラミング, 2013
2012Type-based safe resource deallocation for shared-memory concurrency
Proceedings of Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), 2012
DOI: 10.1145/2398857.2384618A Type System for Dynamic Layer Composition
Proceedings of the International Workshop on Foundations of Object-Oriented Languages (FOOL2012), 2012
顕在的契約計算におけるアップキャスト除去
第14回プログラミングおよびプログラミング言語ワークショップ, 2012
Exercises in Nonstandard Static Analysis of Hybrid Systems
24th International Conference, CAV 2012, 2012
DOI: 10.1007/978-3-642-31424-7_34SEAN: Support Tool for Detecting Rule Violations in JNI Coding
IPSJ Transactions on Programming, 2012
JNIコーディングの規則違反を検出するための支援ツールSEANの開発
情報処理学会第87回プログラミング研究会, 2012
Detecting Bugs in Android Using a Static Escape Analyzer SEAN for Native Code
10th Asian Symposium on Programming Languages and Systems (APLAS 2012), 2012
2011Constructive linear-time temporal logic: Proof systems and Kripke semantics
Information and Computation, 2011
DOI: 10.1016/j.ic.2010.09.008Systematic Derivation of a λ○ Virtual Machine with Low-Level Code Generation by using Fusion Transformation
日本ソフトウェア科学会第28回大会論文集, 2011
Polymorphic Contracts
Proceedings of European Symposium on Programming (ESOP2011), 2011
DOI: 10.1007/978-3-642-19718-5_2Special track on object-oriented languages and systems
Proceedings of the ACM Symposium on Applied Computing, 2011
Gradual typing for generics
Proceedings of the 2011 ACM international conference on Object oriented programming systems languages and applications - OOPSLA '11, 2011
DOI: 10.1145/2048066.2048114ContextFJ: A minimal core calculus for context-oriented programming
Proceedings of the 10th International Workshop on Foundations of Aspect-Oriented Languages, FOAL 2011, 2011
DOI: 10.1145/1960510.1960515Ordered Types for Stream Processing of Tree-Structured Data
Information and Media Technologies, 2011
DOI: 10.11185/imt.6.385Programming with Infinitesimals: A WHILE-Language for Hybrid System Modeling
Automata, Languages and Programming, ICALP, Pt II, 2011
DOI: 10.1007/978-3-642-22012-8_312010A Logical Foundation for Environment Classifiers
Logical Methods in Computer Science, 2010
DOI: 10.2168/lmcs-6(4:8)2010Mostly modular compilation of crosscutting concerns by contextual predicate dispatch
Proceedings of Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), 2010
DOI: 10.1145/1932682.1869503Type relaxed weaving
AOSD.10 - 9th International Conference on Aspect-Oriented Software Development, 2010
DOI: 10.1145/1739230.17392452009Matching ThisType to subtyping
Proceedings of the ACM Symposium on Applied Computing, 2009
DOI: 10.1145/1529282.1529699Self type constructors
Proceeding of the 24th ACM SIGPLAN conference on Object oriented programming systems languages and applications - OOPSLA 09, 2009
DOI: 10.1145/1640089.1640109Towards gradual typing for generics
Proceedings for the 1st Workshop on Script to Program Evolution, STOP'09 in Conjunction with European Conference on Object-Oriented Programming, ECOOP'09, 2009
DOI: 10.1145/1570506.15705092008Proving Noninterference by a Fully Complete Translation to the Simply Typed lambda-calculus
Logical Methods in Computer Science, 2008
DOI: 10.2168/lmcs-4(3:10)2008On Constructive Linear-Time Temporal Logic
Proceedings of the Workshop on Intuitionistil Modal Logic and Applications (IMLA'08), 2008
Lightweight family polymorphism
Journal of Functional Programming, 2008
DOI: 10.1017/s0956796807006405Featherweight Java のための漸進的型付け
第10回プログラミングおよびプログラミング言語ワークショップ(PPL2008)論文集, 2008
文脈依存資源使用解析のための型システム
第10回プログラミングおよびプログラミング言語ワークショップ(PPL2008)論文集, 2008
The essence of lightweight family polymorphism
Journal of Object Technology, 2008
DOI: 10.5381/jot.2008.7.5.a32007Proving Noninterference by a Fully Complete Translation to the Simply Typed λ-Calculus
Advances in Computer Science - ASIAN 2006. Secure Software and Related Issues, 2007
DOI: 10.1007/978-3-540-77505-8_24Variant path types for scalable extensibility
Proceedings of the 22nd annual ACM SIGPLAN conference on Object oriented programming systems and applications - OOPSLA '07, 2007
DOI: 10.1145/1297027.1297037An Algorithm to Decide Conformance of Resource Usage to Specification for Resource Usage Verification
情報処理学会論文誌. プログラミング, 2007
Union types for object-oriented programming
Journal of Object Technology, 2007
Deriving compilers and virtual machines for a multi-level language
Proceedings of Asian Symposium on Programming Languages and Systems (APLAS 2007), 2007
2006Variant parametric types: A flexible subtyping scheme for generics
ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2006
DOI: 10.1145/1152649.1152650様相型に基づく情報流解析における非干渉性の論理関係による一般化とその証明
第8回プログラミングおよびプログラミング言語ワークショップ(PPL2006)論文集, 2006
Resource usage analysis for a functional language with exceptions
Proceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, 2006
DOI: 10.1145/1111542.1111550A modal type system for multi-level generating extensions with persistent code
PPDP'06 - Proceedings of the Eight ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming, 2006
2005Resource usage analysis
ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2005
DOI: 10.1145/1057387.1057390例外機構を備えた言語のための資源使用法解析
第7回プログラミングおよびプログラミング言語ワークショップ(PPL2005)論文集, 2005
メタプログラミングのための時相論理に基づく型付λ計算
第7回プログラミングおよびプログラミング言語ワークショップ(PPL2005)論文集, 2005
2004Generics・Union 型を導入したオブジェクト指向計算体系
第6回プログラミングおよびプログラミング言語ワークショップ(PPL2004)論文集, 2004
A generic type system for the Pi-calculus
THEORETICAL COMPUTER SCIENCE, 2004
DOI: 10.1016/S0304-3975(03)00325-6A modal foundation for secure information flow
Proceedings of the Workshop on Foundations of Computer Security (FCS'04), number 31 in Turku Centre for Computer Science General Publication,187-203, 2004
2003Union 型を導入したオブジェクト指向計算体系
日本ソフトウェア科学会第20回大会論文集, 2003
擬似引用を持つ型付計算体系λq
第5回プログラミングおよびプログラミング言語ワークショップ(PPL2003)論文集, 2003
2002On variance-based subtyping for parametric types
ECOOP 2002 - OBJECT-ORIENTED PROGRAMMING, 2002
2001Featherweight Java: A minimal core calculus for Java and GJ
ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2001
DOI: 10.1145/503502.503505A Recipe for Raw Types
Proceedings of the International Workshop on Foundations of Object-Oriented Languages (FOOL8), 2001
2000Garbage Collection Based on a Linear Type System
Proceedings of the 3rd ACM SIGPLAN Wokshop on Types in Compilation (TIC'00), 2000
Type reconstruction for linear pi-calculus with I/O subtyping
INFORMATION AND COMPUTATION, 2000
DOI: 10.1006/inco.2000.28721999Featherweight Java - A minimal core calculus for Java and GJ
Proceedings of ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA'99), 1999
1997Type-based Analysis of Communication for Concurrent Programming Languages
Proceedings of the Fourth International Static Analysis Symposium, 1997
Type-Based Verification of Connectivity Constraints in Lattice Surgery
Proceedings of the 22nd Asian Symposium on Programming Languages and Systems, 2024
DOI: 10.1007/978-981-97-8943-6_11
Proceedings of the 22nd Asian Symposium on Programming Languages and Systems, 2024
DOI: 10.1007/978-981-97-8943-6_11
Rabbit: A Language to Model and Verify Data Flow in Networked Systems
2024 International Symposium on Networks, Computers and Communications (ISNCC), 2024
DOI: 10.1109/isncc62547.2024.10758938
2024 International Symposium on Networks, Computers and Communications (ISNCC), 2024
DOI: 10.1109/isncc62547.2024.10758938
Space-Efficient Polymorphic Gradual Typing, Mostly Parametric
Proceedings of the ACM on Programming Languages, 2024
DOI: 10.1145/3656441
Proceedings of the ACM on Programming Languages, 2024
DOI: 10.1145/3656441
Signature restriction for polymorphic algebraic effects
Journal of Functional Programming, 2024
DOI: 10.1017/s0956796824000054
Journal of Functional Programming, 2024
DOI: 10.1017/s0956796824000054
Linear Contextual Metaprogramming and Session Types
Electronic Proceedings in Theoretical Computer Science, 2024
DOI: 10.4204/eptcs.401.1
Electronic Proceedings in Theoretical Computer Science, 2024
DOI: 10.4204/eptcs.401.1
命令型プログラムの安全性検証のための所有権主導変換
第26回プログラミングおよびプログラミング言語ワークショップ(PPL2024)論文集, 2024
第26回プログラミングおよびプログラミング言語ワークショップ(PPL2024)論文集, 2024
iCon: Automated Verification of Inter-Transaction Properties in Tezos Smart Contracts with Unknowns
Proceedings of 2024 IEEE International Conference on Blockchain and Cryptocurrency (ICBC), 2024
Proceedings of 2024 IEEE International Conference on Blockchain and Cryptocurrency (ICBC), 2024
Oblivious Monitoring for Discrete-Time STL via Fully Homomorphic Encryption.
Runtime Verification - 24th International Conference(RV), 2024
DOI: 10.1007/978-3-031-74234-7_4
Runtime Verification - 24th International Conference(RV), 2024
DOI: 10.1007/978-3-031-74234-7_4
HEIR: A Unified Representation for Cross-Scheme Compilation of Fully Homomorphic Computation.
31st Annual Network and Distributed System Security Symposium(NDSS), 2024
31st Annual Network and Distributed System Security Symposium(NDSS), 2024
制御フロー仕様から生成したペトリネットに基づくハードウェア誤動作検出手法
DAシンポジウム2024論文集, 2024
DAシンポジウム2024論文集, 2024
Goal-Aware RSS for Complex Scenarios via Program Logic
2024 IEEE Intelligent Vehicles Symposium (IV), 2024
DOI: 10.1109/iv55156.2024.10588754
2024 IEEE Intelligent Vehicles Symposium (IV), 2024
DOI: 10.1109/iv55156.2024.10588754
Sound and relatively complete belief Hoare logic for statistical hypothesis testing programs.
Artif. Intell., 2024
DOI: 10.1016/j.artint.2023.104045
Artif. Intell., 2024
DOI: 10.1016/j.artint.2023.104045
Control-data separation and logical condition propagation for efficient inference on probabilistic programs
Journal of Logical and Algebraic Methods in Programming, 2024
DOI: 10.1016/j.jlamp.2023.100922
Journal of Logical and Algebraic Methods in Programming, 2024
DOI: 10.1016/j.jlamp.2023.100922
Hyper Parametric Timed CTL.
IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2024
DOI: 10.1109/TCAD.2024.3443704
IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2024
DOI: 10.1109/TCAD.2024.3443704
Temporal Logic Formalisation of ISO 34502 Critical Scenarios: Modular Construction with the RSS Safety Distance
39th ACM/SIGAPP Symposium On Applied Computing, 2024
DOI: 10.1145/3605098.3636014
39th ACM/SIGAPP Symposium On Applied Computing, 2024
DOI: 10.1145/3605098.3636014
Temporal Logic Formalisation of ISO 34502 Critical Scenarios: Modular Construction with the RSS Safety Distance.
CoRR, 2024
DOI: 10.48550/arXiv.2403.18764
CoRR, 2024
DOI: 10.48550/arXiv.2403.18764
Learning Weighted Finite Automata over the Max-Plus Semiring and its Termination.
CoRR, 2024
DOI: 10.48550/arXiv.2407.09775
CoRR, 2024
DOI: 10.48550/arXiv.2407.09775
Bi-Abduction in Separation Logic with Arrays and Lists for Program Analysis
Computer Software, 2024
DOI: 10.11309/jssst.41.1_50
Computer Software, 2024
DOI: 10.11309/jssst.41.1_50
Rabbit: a modeling language for verifying cybersecurity in IoT system
第145回情報処理学会プログラミング研究会資料, 2023
第145回情報処理学会プログラミング研究会資料, 2023
Contextual Modal Type Theory with Polymorphic Contexts
Proceedings of European Symposium on Programming, 2023
DOI: 10.1007/978-3-031-30044-8_11
Proceedings of European Symposium on Programming, 2023
DOI: 10.1007/978-3-031-30044-8_11
LLTZ: LLMV IR からスマートコントラクト記述言語 Michelson へのコンパイラ
第25回プログラミングおよびプログラミング言語ワークショップ(PPL2023)論文集, 2023
第25回プログラミングおよびプログラミング言語ワークショップ(PPL2023)論文集, 2023
Probabilistic Black-Box Checking via Active MDP Learning
ACM Transactions on Embedded Computing Systems, 2023
DOI: 10.1145/3609127
ACM Transactions on Embedded Computing Systems, 2023
DOI: 10.1145/3609127
Feature Attributionを用いたdlshogiの指し手の解釈可能性向上手法
研究報告ゲーム情報学（GI）, 2023
研究報告ゲーム情報学（GI）, 2023
LLTZ: LLVM IR からスマートコントラクト記述言語 Michelson へのコンパイラ
第25回プログラミングおよびプログラミング言語ワークショップ (PPL 2023) 論文集, 2023
第25回プログラミングおよびプログラミング言語ワークショップ (PPL 2023) 論文集, 2023
Learning Nonlinear Hybrid Automata from Input-Output Time-Series Data.
ATVA (1), 2023
DOI: 10.1007/978-3-031-45329-8_2
ATVA (1), 2023
DOI: 10.1007/978-3-031-45329-8_2
Active Learning of Deterministic Timed Automata with Myhill-Nerode Style Characterization.
Computer Aided Verification - 35th International Conference, Part I, 2023
DOI: 10.1007/978-3-031-37706-8_1
Computer Aided Verification - 35th International Conference, Part I, 2023
DOI: 10.1007/978-3-031-37706-8_1
Parametric Timed Pattern Matching."
ACM Transactions on Software Engineering and Methodology, 2023
DOI: 10.1145/3517194
ACM Transactions on Software Engineering and Methodology, 2023
DOI: 10.1145/3517194
2022SCameleer: スマートコントラクト記述言語SCamlのための自動検証器
日本ソフトウェア科学会第39回大会論文集, 2022
スマートコントラクト検証器Helmholtzのためのエラー原因提示手法
日本ソフトウェア科学会第39回大会論文集, 2022
暗黙に相互運用可能なレコードとハッシュテーブルのための型推論とコンパイル手法
日本ソフトウェア科学会第39回大会論文集, 2022
Helmholtz: A Verifier for Tezos Smart Contracts Based on Refinement Types
New Generation Computing, 2022
DOI: 10.1007/s00354-022-00167-1ZT-IoT: ゼロトラストIoTのためのシステムソフトウェア構築に向けて
第154回情報処理学会システムソフトウェアとオペレーティング・システム研究会資料, 2022
Stage-Aware Equality Types for a Dependently-Typed Multi-Stage Calculus
第24回プログラミングおよびプログラミング言語ワークショップ(PPL2022)論文集, 2022
Type-based Qubit Allocation for a First-Order Quantum Programming Language
第24回プログラミングおよびプログラミング言語ワークショップ(PPL2022)論文集, 2022
BOREx: Bayesian-Optimization-Based Refinement of Saliency Map for Image- and Video-Classification Models.
ACCV (7), 2022
DOI: 10.1007/978-3-031-26293-7_17Oblivious Online Monitoring for Safety LTL Specification via Fully Homomorphic Encryption.
CAV 2022, 2022
DOI: 10.1007/978-3-031-13185-1_22The Lattice-Theoretic Essence of Property Directed Reachability Analysis.
CAV 2022, 2022
DOI: 10.1007/978-3-031-13185-1_12ARCH-COMP 2022 Category Report: Falsification with Ubounded Resources
EPiC Series in Computing, 2022
DOI: 10.29007/fhnkDynamic Shielding for Reinforcement Learning in Black-Box Environments.
International Symposium on Automated Technology for Verification and Analysis, 2022
DOI: 10.1007/978-3-031-19992-9_2Exemplifying parametric timed specifications over signals with bounded behavior.
NASA Formal Methods Symposium, 2022
DOI: 10.1007/978-3-031-06773-0_25Data for "Exemplifying parametric timed specifications over signals with bounded behavior".
DOI: 10.5281/zenodo.6382893Model-Bounded Monitoring of Hybrid Systems."
ACM Transactions on Cyber-Physical Systems, 2022
DOI: 10.1145/35290952021Is Space-Efficient Polymorphic Gradual Typing Possible?
Informal Proceedings of Scheme and Functional Programming Workshop, 2021
HELMHOLTZ: A Verifier for Tezos Smart Contracts Based on Refinement Types.
CoRR, 2021
Verification of a Merkle Patricia Tree Library Using F.
CoRR, 2021
完全準同型暗号を用いた秘匿LTLオンラインモニタリング
コンピュータセキュリティシンポジウム 2021 (CSS 2021), 2021
Formalizing Statistical Beliefs in Hypothesis Testing Using Program Logic.
Proceedings of the 18th International Conference on Principles of Knowledge Representation and Reasoning(KR), 2021
DOI: 10.24963/kr.2021/39Efficient Black-Box Checking via Model Checking with Strengthened Specifications
Runtime Verification - 21st International Conference(RV), 2021
DOI: 10.1007/978-3-030-88494-9_6Enhancing Loop-Invariant Synthesis via Reinforcement Learning.
CoRR, 2021
Verification of a Merkle Patricia Tree Library Using F*
CoRR, 2021
ARCH-COMP 2021 Category Report: Falsification with Validation of Results.
ARCH@ADHS, 2021
DOI: 10.29007/xwl1Hybrid System Falsification for Multiple-Constraint Parameter Synthesis: a Gas Turbine Case Study.
24th International Symposium on Formal Methods, 2021
DOI: 10.1007/978-3-030-90870-6_17Constrained Optimization for Falsification and Conjunctive Synthesis.
6th IFAC Conference on Analysis and Design of Hybrid Systems, 2021
DOI: 10.1016/j.ifacol.2021.08.501Model-Bounded Monitoring of Hybrid Systems.
12th ACM/IEEE International Conference on Cyber-Physical Systems, 2021
DOI: 10.1145/3450267.34505312020Space-Efficient Gradual Typing in Coercion-Passing Style.
34th European Conference on Object-Oriented Programming, ECOOP 2020, 2020
DOI: 10.4230/LIPIcs.ECOOP.2020.8量子ビット連結性制約検査のための依存型システム
日本ソフトウェア科学会第37回大会論文集, 2020
ConSORT: Context- and Flow-Sensitive Ownership Refinement Types for Imperative Programs
Programming Languages and Systems, 2020
DOI: 10.1007/978-3-030-44914-8_25スタック領域上での時間的メモリ安全性を保証する静的解析手法
第22回プログラミングおよびプログラミング言語ワークショップ(PPL2020)論文集, 2020
スマートコントラクトのための Effectively Callback-Free 性の型に基づく静的検証
第22回プログラミングおよびプログラミング言語ワークショップ(PPL2020)論文集, 2020
F* を用いた Merkle Patricia Tree ライブラリの形式検証
第22回プログラミングおよびプログラミング言語ワークショップ(PPL2020)論文集, 2020
Compilation of Coordinated Choice.
CoRR, 2020
Signature restriction for polymorphic algebraic effects.
Proc. ACM Program. Lang., 2020
DOI: 10.1145/3408999Space-Efficient Gradual Typing in Coercion-Passing Style
Informal Proceedings of the 1st International Workshop on Gradual Typing (WGT2020), 2020
Gradual Typing for Extensibility by Rows
Informal Proceedings of the 1st International Workshop on Gradual Typing (WGT2020), 2020
Visualizing Color-Wise Saliency of Black-Box Image Classification Models.
Proceedings of ACCV 2020, 2020
DOI: 10.1007/978-3-030-69535-4_12Generalized Property-Directed Reachability for Hybrid Systems
Verification, Model Checking, and Abstract Interpretation - 21st International Conference(VMCAI), 2020
DOI: 10.1007/978-3-030-39322-9_14A Contract Corpus for Recognizing Rights and Obligations.
Proceedings of The 12th Language Resources and Evaluation Conference(LREC), 2020
2019A Dependently Typed Multi-stage Calculus.
Programming Languages and Systems - 17th Asian Symposium, APLAS 2019, Nusa Dua, Bali, Indonesia, December 1-4, 2019, Proceedings, 2019
DOI: 10.1007/978-3-030-34175-6_4Manifest Contracts with Intersection Types.
Programming Languages and Systems - 17th Asian Symposium, APLAS 2019, Nusa Dua, Bali, Indonesia, December 1-4, 2019, Proceedings, 2019
DOI: 10.1007/978-3-030-34175-6_3Temporal Verification of Programs via First-Order Fixpoint Logic.
Static Analysis - 26th International Symposium, SAS 2019, Porto, Portugal, October 8-11, 2019, Proceedings, 2019
DOI: 10.1007/978-3-030-32304-2_20A Type System for First-Class Layers with Inheritance, Subtyping, and Swapping
Science of Computer Programming, 2019
Handling Polymorphic Algebraic Effects
Proceedings of European Symposium on Programming (ESOP2019), 2019
空間効率の良いコアーション計算のためのコアーション渡し形式
第21回プログラミングおよびプログラミング言語ワークショップ(PPL2019)論文集, 2019
Dynamic Type Inference for Gradual Hindley-Milner Typing
Proceedings of the ACM on Programming Languages, 2019
ワーカの重要度を考慮した並列実行フレームワークの障害耐性評価手法の検討
2019年並列／分散／協調処理に関する『北見』サマー・ワークショップ (SWoPP2019), 2019
汎用送受信に対応したHOPEコンパイラの研究
2019年並列／分散／協調処理に関する『北見』サマー・ワークショップ (SWoPP2019), 2019
JVM上の動的言語のための抽象解釈の実装
第60回プログラミング・シンポジウム, 2019
Extending a Work-Stealing Framework with Priorities and Weights
2019 IEEE/ACM 9th Workshop on Irregular Applications: Architectures and Algorithms (IA3), 2019
DOI: 10.1109/IA349570.2019.00008HOPE: A Parallel Execution Model Based on Hierarchical Omission
Proceedings of the 48th International Conference on Parallel Processing ({ICPP} 2019), 2019
DOI: 10.1145/3337821.33378992018Nondetermnistic Manifest Contracts
Proceedings of theInternational Symposium on Principles and Practice of Declarative Programming, 2018
DOI: 10.1145/3236950.3236964ContextWorkflow: A Monadic DSL for Compensable and Interruptible Executions
Proceedings of the 32nd European Conference on Object-Oriented Programming, 2018
Method Safety Mechanism for Asynchronous Layer Deactivation
Science of Computer Programming, 2018
DOI: 10.1016/j.scico.2018.01.006Automated Verification of Functional Correctness of Race-Free GPU Programs
Journal of Automated Reasoning, 2018
DOI: 10.1007/978-3-319-48869-1_7Reasoning about Polymorphic Manifest Contracts.
CoRR, 2018
A Guess-and-Assume Approach to Loop Fusion for Program Verification
Proceedings of the ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, 2018
DOI: 10.1145/3162070Automated Proof Synthesis for the Minimal Propositional Logic with Deep Neural Networks
APLAS 2018, 2018
DOI: 10.1007/978-3-030-02768-1_17MONAA: A Tool for Timed Pattern Matching with Automata-Based Acceleration.
3rd Workshop on Monitoring and Testing of Cyber-Physical Systems, MT@CPSWeek 2018, Porto, Portugal, April 10, 2018, 2018
DOI: 10.1109/MT-CPS.2018.00014Generalized homogeneous polynomials for efficient template-based nonlinear invariant synthesis.
Theor. Comput. Sci., 2018
DOI: 10.1016/j.tcs.2018.06.005Probabilistic guards: A mechanism for increasing the granularity of work-stealing programs
Parallel Computing, 2018
分割統治型総和の部分的計算結果を効率よく利用する方式の研究
情報処理学会第121回プログラミング研究会, 2018
並列分散フレームワークの耐障害性評価のための通信障害模擬機能
第20回プログラミングおよびプログラミング言語ワークショップ(PPL2018), 2018
JVM上の動的言語のための抽象解釈
情報処理学会第121回プログラミング研究会, 2018
2017A Nonstandard Functional Programming Language
Proceedings of Asian Symposium on Programming Languages and Systems (APLAS2017), 2017
DOI: 10.1007/978-3-319-71237-6_25A DSL for Compensable and Interruptible Executions
Proceedings of 4th Workshop on Reactive and Event-based Languages & Systems (REBLS), 2017
C言語における無効なスタック領域へのポインタを検出する静的解析
日本ソフトウェア科学会第34回大会論文集, 2017
On Polymorphic Gradual Typing
Proceedings of the ACM on Programming Languages, 2017
A Type Reconstruction Algorithm for Gradually Typed Delimited Continuations
第19回プログラミングおよびプログラミング言語ワークショップ(PPL2017)論文集, 2017
Stateful manifest contracts
Conference Record of the Annual ACM Symposium on Principles of Programming Languages, 2017
DOI: 10.1145/3009837.3009875Verification of Code Generators via Higher-Order Model Checking
Proceedings of the 2017 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM'17), 2017
DOI: 10.1145/3018882.3018886Polymorphic Manifest Contracts, Revised and Resolved
ACM Transactions on Programming Languages and Systems, 2017
Sharper and Simpler Nonlinear Interpolants for Program Verification.
Programming Languages and Systems - 15th Asian Symposium(APLAS), 2017
DOI: 10.1007/978-3-319-71237-6_24Efficient Online Timed Pattern Matching by Automata-Based Skipping
FORMATS 2017, 2017
DOI: 10.1007/978-3-319-65765-3_13Towards Proof Synthesis Guided by Neural Machine Translation for Intuitionistic Propositional Logic
CoRR, 2017
アクセス制御論理に基づくIoT向け分散型アクセス制御フレームワーク
第15回 ディペンダブルシステムワークショップ (DSW 2017), 2017
アクセス制御機能の組み込まれた拡張オブジェクト指向言語
情報処理学会 第58回プログラミング・シンポジウム, 2017
優先度ならびに重みを用いたワークスティールフレームワークの性能改善
The 1st. cross-disciplinary Workshop on Computing Systems, Infrastructures, and Programming (xSIG 2017), 2017
仮想環境を考慮した要求駆動型負荷分散
日本ソフトウェア科学会第34回大会, 2017
HOPEコンパイラのプロトタイプ実装
2017年並列/分散/協調処理に関する『秋田』サマー・ワークショップ (SWoPP2017), 2017
2016階層的グループ化に基づきAndroidアプリの安全性を向上するバイトコード書換えツール
日本ソフトウェア科学会第33回大会論文集, 2016
An Extended Behavioral Type System for Memory-Leak Freedom
日本ソフトウェア科学会第33回大会論文集, 2016
SIMT のための Hoare 論理の Coq を用いた形式化と 並列 prefix-sum アルゴリズムの検証
第18回プログラミングおよびプログラミング言語ワークショップ(PPL2016)論文集, 2016
Gradual typing for delimited continuations
The 5th Script To Program Evolution Workshop, 2016
A Library-Based Approach to Context-Dependent Computation with Reactive Values
Proceedings of Constrained and Reactive Objects Workshop (CROW2016), 2016
DOI: 10.1145/2892664.2892669規則違反コードの構造を反映した木パタンを用いるコード検査器
情報処理学会論文誌 プログラミング, 2016
仮想環境を考慮した要求駆動型負荷分散の検討
第18回プログラミングおよびプログラミング言語ワークショップ(PPL2016), 2016
Preliminary Evaluations of Probabilistic Guards for a Work-Stealing Framework
Annual Meeting on Advanced Computing System and Infrastructure (ACSI) 2016, 2016
HOPEコンパイラの実装に向けて
第18回プログラミングおよびプログラミング言語ワークショップ(PPL2016), 2016
An MPI-based Implementation of the Tascell Task-Parallel Programming Language
Annual Meeting on Advanced Computing System and Infrastructure (ACSI) 2016, 2016
Evaluation of an MPI-based Implementation of the Tascell Task-Parallel Language on Massively Parallel Systems
PROCEEDINGS OF 45TH INTERNATIONAL CONFERENCE ON PARALLEL PROCESSING WORKSHOPS (ICPPW 2016), 2016
DOI: 10.1109/ICPPW.2016.36Extending aWork-Stealing Framework with Probabilistic Guards
PROCEEDINGS OF 45TH INTERNATIONAL CONFERENCE ON PARALLEL PROCESSING WORKSHOPS (ICPPW 2016), 2016
DOI: 10.1109/ICPPW.2016.372015参照を備えた多段階計算のための多相的型システム
日本ソフトウェア科学会第32回大会論文集, 2015
Visibility of Context-oriented Behavior and State in L
Computer Software, 2015
DOI: 10.11309/jssst.32.3_149Manifest contracts for datatypes
Conference Record of the Annual ACM Symposium on Principles of Programming Languages, 2015
DOI: 10.1145/2676726.2676996A Sound Type System for Layer Subtyping and Dynamically Activated First-Class Layers
Proceedings of Asian Symposium on Programming Languages and Systems (APLAS 2015), 2015
DOI: 10.1007/978-3-319-26529-2_24Shifting the Blame: A Blame Calculus with Delimited Control
Proceedings of Asian Symposium on Programming Languages and Systems (APLAS 2015), 2015
DOI: 10.1007/978-3-319-26529-2_11Input Synthesis for Sampled Data Systems by Program Logic
Proc. of the 4th Workshop on Hybrid Autonomous Systems (HAS 2014), 2015
DOI: 10.4204/EPTCS.174.3Validated Numerics Meets Reachability Analysis for CPS Design (NII Shonan Meeting 2015-14).
NII Shonan Meet. Rep., 2015
Design and Implementation of a Java Bytecode Manipulation Library for Clojure
Journal of Information Processing, 2015
メッセージ媒介システムの構想と試験実装
Annual Meeting on Advanced Computing System and Infrastructure (ACSI) 2015, 2015
Clojure用JVMバイトコード操作ライブラリの設計と実装
情報処理学会第102回プログラミング研究会, 2015
2014Automatic Memory Management Based on Program Transformation using Ownerships
Proceedings of Asian Symposium on Programming Languages and Systems (APLAS), 2014
DOI: 10.1007/978-3-319-12736-1_4Formalization of Featherweight Java and Featherweight GJ by using weak HOAS on Coq
日本ソフトウェア科学会大会論文集, 2014
Automatic Synthesis of Combiners in the MapReduce Framework: An Approach with Right Inverse
Proceedings of International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR), 2014
On-Demand Layer Activation for Type-Safe Deactivation
International Workshop on Context-Oriented Programming, COP'14 - Co-located with the 26th European Conference on Object-Oriented Programming, ECOOP'14, 2014
DOI: 10.1145/2637066.2637070Towards Type-Safe JCop: A type system for layer inheritance and first-class layers
International Workshop on Context-Oriented Programming, COP'12 - Co-located with the 26th European Conference on Object-Oriented Programming, ECOOP'14, 2014
DOI: 10.1145/2637066.2637073On Cross-Stage Persistence in Multi-Stage Programming
Proceedings of Intl. Symposium on Functional and Logic Programming (FLOPS2014), 2014
DOI: 10.1007/978-3-319-07151-0_7顕在的契約計算のための代数的データ型
第16回プログラミングおよびプログラミング言語ワークショップ(PPL2014)論文集, 2014
Formal Verification of CPS : A Nonstandard Analysis Approach
Journal of The Society of Instrument and Control Engineers, 2014
DOI: 10.11499/sicejl.53.1080Practical Implementation Techniques of Ambient Calculus in Conventional Dynamic Languages
29th Symposium on Applied Computing (SAC 2014), 2014
JVMバイトコードへの低水準操作を簡潔に記述可能なマクロシステム
情報処理学会 第55回プログラミング・シンポジウム, 2014
2013A Hoare Logic for SIMT Programs
Proceedings of Asian Symposium on Programming Languages and Systems (APLAS2013), 2013
DOI: 10.1007/978-3-319-03542-0_5多段階計算λ▹のための越段階埋込
日本ソフトウェア科学会第30回大会論文集, 2013
Layer Refinement in L
並列/分散/協調処理に関するサマー・ワークショップ (SWoPP), 2013
L: Context-oriented programming with only layers
Proceedings of the 5th International Workshop on Context-Oriented Programming, COP 2013, 2013
DOI: 10.1145/2489793.2489797Model-Checking Higher-Order Programs with Recursive Types
Proceedings of European Symposium on Programming (ESOP2013), 2013
DOI: 10.1007/978-3-642-37036-6_24Hyperstream processing systems: Nonstandard modeling of continuous-time signals
Conference Record of the Annual ACM Symposium on Principles of Programming Languages, 2013
DOI: 10.1145/2429069.2429120Safeアンビエントに基づく分散アプリケーション開発用Lisp環境
コンピュータソフトウェア, 2013
L-Closureの呼び出しコストの削減
情報処理学会論文誌 プログラミング, 2013
2012Type-based safe resource deallocation for shared-memory concurrency
Proceedings of Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), 2012
DOI: 10.1145/2398857.2384618A Type System for Dynamic Layer Composition
Proceedings of the International Workshop on Foundations of Object-Oriented Languages (FOOL2012), 2012
顕在的契約計算におけるアップキャスト除去
第14回プログラミングおよびプログラミング言語ワークショップ, 2012
Exercises in Nonstandard Static Analysis of Hybrid Systems
24th International Conference, CAV 2012, 2012
DOI: 10.1007/978-3-642-31424-7_34SEAN: Support Tool for Detecting Rule Violations in JNI Coding
IPSJ Transactions on Programming, 2012
JNIコーディングの規則違反を検出するための支援ツールSEANの開発
情報処理学会第87回プログラミング研究会, 2012
Detecting Bugs in Android Using a Static Escape Analyzer SEAN for Native Code
10th Asian Symposium on Programming Languages and Systems (APLAS 2012), 2012
2011Constructive linear-time temporal logic: Proof systems and Kripke semantics
Information and Computation, 2011
DOI: 10.1016/j.ic.2010.09.008Systematic Derivation of a λ○ Virtual Machine with Low-Level Code Generation by using Fusion Transformation
日本ソフトウェア科学会第28回大会論文集, 2011
Polymorphic Contracts
Proceedings of European Symposium on Programming (ESOP2011), 2011
DOI: 10.1007/978-3-642-19718-5_2Special track on object-oriented languages and systems
Proceedings of the ACM Symposium on Applied Computing, 2011
Gradual typing for generics
Proceedings of the 2011 ACM international conference on Object oriented programming systems languages and applications - OOPSLA '11, 2011
DOI: 10.1145/2048066.2048114ContextFJ: A minimal core calculus for context-oriented programming
Proceedings of the 10th International Workshop on Foundations of Aspect-Oriented Languages, FOAL 2011, 2011
DOI: 10.1145/1960510.1960515Ordered Types for Stream Processing of Tree-Structured Data
Information and Media Technologies, 2011
DOI: 10.11185/imt.6.385Programming with Infinitesimals: A WHILE-Language for Hybrid System Modeling
Automata, Languages and Programming, ICALP, Pt II, 2011
DOI: 10.1007/978-3-642-22012-8_312010A Logical Foundation for Environment Classifiers
Logical Methods in Computer Science, 2010
DOI: 10.2168/lmcs-6(4:8)2010Mostly modular compilation of crosscutting concerns by contextual predicate dispatch
Proceedings of Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), 2010
DOI: 10.1145/1932682.1869503Type relaxed weaving
AOSD.10 - 9th International Conference on Aspect-Oriented Software Development, 2010
DOI: 10.1145/1739230.17392452009Matching ThisType to subtyping
Proceedings of the ACM Symposium on Applied Computing, 2009
DOI: 10.1145/1529282.1529699Self type constructors
Proceeding of the 24th ACM SIGPLAN conference on Object oriented programming systems languages and applications - OOPSLA 09, 2009
DOI: 10.1145/1640089.1640109Towards gradual typing for generics
Proceedings for the 1st Workshop on Script to Program Evolution, STOP'09 in Conjunction with European Conference on Object-Oriented Programming, ECOOP'09, 2009
DOI: 10.1145/1570506.15705092008Proving Noninterference by a Fully Complete Translation to the Simply Typed lambda-calculus
Logical Methods in Computer Science, 2008
DOI: 10.2168/lmcs-4(3:10)2008On Constructive Linear-Time Temporal Logic
Proceedings of the Workshop on Intuitionistil Modal Logic and Applications (IMLA'08), 2008
Lightweight family polymorphism
Journal of Functional Programming, 2008
DOI: 10.1017/s0956796807006405Featherweight Java のための漸進的型付け
第10回プログラミングおよびプログラミング言語ワークショップ(PPL2008)論文集, 2008
文脈依存資源使用解析のための型システム
第10回プログラミングおよびプログラミング言語ワークショップ(PPL2008)論文集, 2008
The essence of lightweight family polymorphism
Journal of Object Technology, 2008
DOI: 10.5381/jot.2008.7.5.a32007Proving Noninterference by a Fully Complete Translation to the Simply Typed λ-Calculus
Advances in Computer Science - ASIAN 2006. Secure Software and Related Issues, 2007
DOI: 10.1007/978-3-540-77505-8_24Variant path types for scalable extensibility
Proceedings of the 22nd annual ACM SIGPLAN conference on Object oriented programming systems and applications - OOPSLA '07, 2007
DOI: 10.1145/1297027.1297037An Algorithm to Decide Conformance of Resource Usage to Specification for Resource Usage Verification
情報処理学会論文誌. プログラミング, 2007
Union types for object-oriented programming
Journal of Object Technology, 2007
Deriving compilers and virtual machines for a multi-level language
Proceedings of Asian Symposium on Programming Languages and Systems (APLAS 2007), 2007
2006Variant parametric types: A flexible subtyping scheme for generics
ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2006
DOI: 10.1145/1152649.1152650様相型に基づく情報流解析における非干渉性の論理関係による一般化とその証明
第8回プログラミングおよびプログラミング言語ワークショップ(PPL2006)論文集, 2006
Resource usage analysis for a functional language with exceptions
Proceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, 2006
DOI: 10.1145/1111542.1111550A modal type system for multi-level generating extensions with persistent code
PPDP'06 - Proceedings of the Eight ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming, 2006
2005Resource usage analysis
ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2005
DOI: 10.1145/1057387.1057390例外機構を備えた言語のための資源使用法解析
第7回プログラミングおよびプログラミング言語ワークショップ(PPL2005)論文集, 2005
メタプログラミングのための時相論理に基づく型付λ計算
第7回プログラミングおよびプログラミング言語ワークショップ(PPL2005)論文集, 2005
2004Generics・Union 型を導入したオブジェクト指向計算体系
第6回プログラミングおよびプログラミング言語ワークショップ(PPL2004)論文集, 2004
A generic type system for the Pi-calculus
THEORETICAL COMPUTER SCIENCE, 2004
DOI: 10.1016/S0304-3975(03)00325-6A modal foundation for secure information flow
Proceedings of the Workshop on Foundations of Computer Security (FCS'04), number 31 in Turku Centre for Computer Science General Publication,187-203, 2004
2003Union 型を導入したオブジェクト指向計算体系
日本ソフトウェア科学会第20回大会論文集, 2003
擬似引用を持つ型付計算体系λq
第5回プログラミングおよびプログラミング言語ワークショップ(PPL2003)論文集, 2003
2002On variance-based subtyping for parametric types
ECOOP 2002 - OBJECT-ORIENTED PROGRAMMING, 2002
2001Featherweight Java: A minimal core calculus for Java and GJ
ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2001
DOI: 10.1145/503502.503505A Recipe for Raw Types
Proceedings of the International Workshop on Foundations of Object-Oriented Languages (FOOL8), 2001
2000Garbage Collection Based on a Linear Type System
Proceedings of the 3rd ACM SIGPLAN Wokshop on Types in Compilation (TIC'00), 2000
Type reconstruction for linear pi-calculus with I/O subtyping
INFORMATION AND COMPUTATION, 2000
DOI: 10.1006/inco.2000.28721999Featherweight Java - A minimal core calculus for Java and GJ
Proceedings of ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA'99), 1999
1997Type-based Analysis of Communication for Concurrent Programming Languages
Proceedings of the Fourth International Static Analysis Symposium, 1997
SCameleer: スマートコントラクト記述言語SCamlのための自動検証器
日本ソフトウェア科学会第39回大会論文集, 2022
日本ソフトウェア科学会第39回大会論文集, 2022
スマートコントラクト検証器Helmholtzのためのエラー原因提示手法
日本ソフトウェア科学会第39回大会論文集, 2022
日本ソフトウェア科学会第39回大会論文集, 2022
暗黙に相互運用可能なレコードとハッシュテーブルのための型推論とコンパイル手法
日本ソフトウェア科学会第39回大会論文集, 2022
日本ソフトウェア科学会第39回大会論文集, 2022
Helmholtz: A Verifier for Tezos Smart Contracts Based on Refinement Types
New Generation Computing, 2022
DOI: 10.1007/s00354-022-00167-1
New Generation Computing, 2022
DOI: 10.1007/s00354-022-00167-1
ZT-IoT: ゼロトラストIoTのためのシステムソフトウェア構築に向けて
第154回情報処理学会システムソフトウェアとオペレーティング・システム研究会資料, 2022
第154回情報処理学会システムソフトウェアとオペレーティング・システム研究会資料, 2022
Stage-Aware Equality Types for a Dependently-Typed Multi-Stage Calculus
第24回プログラミングおよびプログラミング言語ワークショップ(PPL2022)論文集, 2022
第24回プログラミングおよびプログラミング言語ワークショップ(PPL2022)論文集, 2022
Type-based Qubit Allocation for a First-Order Quantum Programming Language
第24回プログラミングおよびプログラミング言語ワークショップ(PPL2022)論文集, 2022
第24回プログラミングおよびプログラミング言語ワークショップ(PPL2022)論文集, 2022
BOREx: Bayesian-Optimization-Based Refinement of Saliency Map for Image- and Video-Classification Models.
ACCV (7), 2022
DOI: 10.1007/978-3-031-26293-7_17
ACCV (7), 2022
DOI: 10.1007/978-3-031-26293-7_17
Oblivious Online Monitoring for Safety LTL Specification via Fully Homomorphic Encryption.
CAV 2022, 2022
DOI: 10.1007/978-3-031-13185-1_22
CAV 2022, 2022
DOI: 10.1007/978-3-031-13185-1_22
The Lattice-Theoretic Essence of Property Directed Reachability Analysis.
CAV 2022, 2022
DOI: 10.1007/978-3-031-13185-1_12
CAV 2022, 2022
DOI: 10.1007/978-3-031-13185-1_12
ARCH-COMP 2022 Category Report: Falsification with Ubounded Resources
EPiC Series in Computing, 2022
DOI: 10.29007/fhnk
EPiC Series in Computing, 2022
DOI: 10.29007/fhnk
Dynamic Shielding for Reinforcement Learning in Black-Box Environments.
International Symposium on Automated Technology for Verification and Analysis, 2022
DOI: 10.1007/978-3-031-19992-9_2
International Symposium on Automated Technology for Verification and Analysis, 2022
DOI: 10.1007/978-3-031-19992-9_2
Exemplifying parametric timed specifications over signals with bounded behavior.
NASA Formal Methods Symposium, 2022
DOI: 10.1007/978-3-031-06773-0_25
NASA Formal Methods Symposium, 2022
DOI: 10.1007/978-3-031-06773-0_25
Data for "Exemplifying parametric timed specifications over signals with bounded behavior".
DOI: 10.5281/zenodo.6382893
DOI: 10.5281/zenodo.6382893
Model-Bounded Monitoring of Hybrid Systems."
ACM Transactions on Cyber-Physical Systems, 2022
DOI: 10.1145/3529095
ACM Transactions on Cyber-Physical Systems, 2022
DOI: 10.1145/3529095
Is Space-Efficient Polymorphic Gradual Typing Possible?
Informal Proceedings of Scheme and Functional Programming Workshop, 2021
Informal Proceedings of Scheme and Functional Programming Workshop, 2021
HELMHOLTZ: A Verifier for Tezos Smart Contracts Based on Refinement Types.
CoRR, 2021
CoRR, 2021
Verification of a Merkle Patricia Tree Library Using F.
CoRR, 2021
CoRR, 2021
完全準同型暗号を用いた秘匿LTLオンラインモニタリング
コンピュータセキュリティシンポジウム 2021 (CSS 2021), 2021
コンピュータセキュリティシンポジウム 2021 (CSS 2021), 2021
Formalizing Statistical Beliefs in Hypothesis Testing Using Program Logic.
Proceedings of the 18th International Conference on Principles of Knowledge Representation and Reasoning(KR), 2021
DOI: 10.24963/kr.2021/39
Proceedings of the 18th International Conference on Principles of Knowledge Representation and Reasoning(KR), 2021
DOI: 10.24963/kr.2021/39
Efficient Black-Box Checking via Model Checking with Strengthened Specifications
Runtime Verification - 21st International Conference(RV), 2021
DOI: 10.1007/978-3-030-88494-9_6
Runtime Verification - 21st International Conference(RV), 2021
DOI: 10.1007/978-3-030-88494-9_6
Enhancing Loop-Invariant Synthesis via Reinforcement Learning.
CoRR, 2021
CoRR, 2021
Verification of a Merkle Patricia Tree Library Using F*
CoRR, 2021
CoRR, 2021
ARCH-COMP 2021 Category Report: Falsification with Validation of Results.
ARCH@ADHS, 2021
DOI: 10.29007/xwl1
ARCH@ADHS, 2021
DOI: 10.29007/xwl1
Hybrid System Falsification for Multiple-Constraint Parameter Synthesis: a Gas Turbine Case Study.
24th International Symposium on Formal Methods, 2021
DOI: 10.1007/978-3-030-90870-6_17
24th International Symposium on Formal Methods, 2021
DOI: 10.1007/978-3-030-90870-6_17
Constrained Optimization for Falsification and Conjunctive Synthesis.
6th IFAC Conference on Analysis and Design of Hybrid Systems, 2021
DOI: 10.1016/j.ifacol.2021.08.501
6th IFAC Conference on Analysis and Design of Hybrid Systems, 2021
DOI: 10.1016/j.ifacol.2021.08.501
Model-Bounded Monitoring of Hybrid Systems.
12th ACM/IEEE International Conference on Cyber-Physical Systems, 2021
DOI: 10.1145/3450267.3450531
12th ACM/IEEE International Conference on Cyber-Physical Systems, 2021
DOI: 10.1145/3450267.3450531
2020Space-Efficient Gradual Typing in Coercion-Passing Style.
34th European Conference on Object-Oriented Programming, ECOOP 2020, 2020
DOI: 10.4230/LIPIcs.ECOOP.2020.8量子ビット連結性制約検査のための依存型システム
日本ソフトウェア科学会第37回大会論文集, 2020
ConSORT: Context- and Flow-Sensitive Ownership Refinement Types for Imperative Programs
Programming Languages and Systems, 2020
DOI: 10.1007/978-3-030-44914-8_25スタック領域上での時間的メモリ安全性を保証する静的解析手法
第22回プログラミングおよびプログラミング言語ワークショップ(PPL2020)論文集, 2020
スマートコントラクトのための Effectively Callback-Free 性の型に基づく静的検証
第22回プログラミングおよびプログラミング言語ワークショップ(PPL2020)論文集, 2020
F* を用いた Merkle Patricia Tree ライブラリの形式検証
第22回プログラミングおよびプログラミング言語ワークショップ(PPL2020)論文集, 2020
Compilation of Coordinated Choice.
CoRR, 2020
Signature restriction for polymorphic algebraic effects.
Proc. ACM Program. Lang., 2020
DOI: 10.1145/3408999Space-Efficient Gradual Typing in Coercion-Passing Style
Informal Proceedings of the 1st International Workshop on Gradual Typing (WGT2020), 2020
Gradual Typing for Extensibility by Rows
Informal Proceedings of the 1st International Workshop on Gradual Typing (WGT2020), 2020
Visualizing Color-Wise Saliency of Black-Box Image Classification Models.
Proceedings of ACCV 2020, 2020
DOI: 10.1007/978-3-030-69535-4_12Generalized Property-Directed Reachability for Hybrid Systems
Verification, Model Checking, and Abstract Interpretation - 21st International Conference(VMCAI), 2020
DOI: 10.1007/978-3-030-39322-9_14A Contract Corpus for Recognizing Rights and Obligations.
Proceedings of The 12th Language Resources and Evaluation Conference(LREC), 2020
2019A Dependently Typed Multi-stage Calculus.
Programming Languages and Systems - 17th Asian Symposium, APLAS 2019, Nusa Dua, Bali, Indonesia, December 1-4, 2019, Proceedings, 2019
DOI: 10.1007/978-3-030-34175-6_4Manifest Contracts with Intersection Types.
Programming Languages and Systems - 17th Asian Symposium, APLAS 2019, Nusa Dua, Bali, Indonesia, December 1-4, 2019, Proceedings, 2019
DOI: 10.1007/978-3-030-34175-6_3Temporal Verification of Programs via First-Order Fixpoint Logic.
Static Analysis - 26th International Symposium, SAS 2019, Porto, Portugal, October 8-11, 2019, Proceedings, 2019
DOI: 10.1007/978-3-030-32304-2_20A Type System for First-Class Layers with Inheritance, Subtyping, and Swapping
Science of Computer Programming, 2019
Handling Polymorphic Algebraic Effects
Proceedings of European Symposium on Programming (ESOP2019), 2019
空間効率の良いコアーション計算のためのコアーション渡し形式
第21回プログラミングおよびプログラミング言語ワークショップ(PPL2019)論文集, 2019
Dynamic Type Inference for Gradual Hindley-Milner Typing
Proceedings of the ACM on Programming Languages, 2019
ワーカの重要度を考慮した並列実行フレームワークの障害耐性評価手法の検討
2019年並列／分散／協調処理に関する『北見』サマー・ワークショップ (SWoPP2019), 2019
汎用送受信に対応したHOPEコンパイラの研究
2019年並列／分散／協調処理に関する『北見』サマー・ワークショップ (SWoPP2019), 2019
JVM上の動的言語のための抽象解釈の実装
第60回プログラミング・シンポジウム, 2019
Extending a Work-Stealing Framework with Priorities and Weights
2019 IEEE/ACM 9th Workshop on Irregular Applications: Architectures and Algorithms (IA3), 2019
DOI: 10.1109/IA349570.2019.00008HOPE: A Parallel Execution Model Based on Hierarchical Omission
Proceedings of the 48th International Conference on Parallel Processing ({ICPP} 2019), 2019
DOI: 10.1145/3337821.33378992018Nondetermnistic Manifest Contracts
Proceedings of theInternational Symposium on Principles and Practice of Declarative Programming, 2018
DOI: 10.1145/3236950.3236964ContextWorkflow: A Monadic DSL for Compensable and Interruptible Executions
Proceedings of the 32nd European Conference on Object-Oriented Programming, 2018
Method Safety Mechanism for Asynchronous Layer Deactivation
Science of Computer Programming, 2018
DOI: 10.1016/j.scico.2018.01.006Automated Verification of Functional Correctness of Race-Free GPU Programs
Journal of Automated Reasoning, 2018
DOI: 10.1007/978-3-319-48869-1_7Reasoning about Polymorphic Manifest Contracts.
CoRR, 2018
A Guess-and-Assume Approach to Loop Fusion for Program Verification
Proceedings of the ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, 2018
DOI: 10.1145/3162070Automated Proof Synthesis for the Minimal Propositional Logic with Deep Neural Networks
APLAS 2018, 2018
DOI: 10.1007/978-3-030-02768-1_17MONAA: A Tool for Timed Pattern Matching with Automata-Based Acceleration.
3rd Workshop on Monitoring and Testing of Cyber-Physical Systems, MT@CPSWeek 2018, Porto, Portugal, April 10, 2018, 2018
DOI: 10.1109/MT-CPS.2018.00014Generalized homogeneous polynomials for efficient template-based nonlinear invariant synthesis.
Theor. Comput. Sci., 2018
DOI: 10.1016/j.tcs.2018.06.005Probabilistic guards: A mechanism for increasing the granularity of work-stealing programs
Parallel Computing, 2018
分割統治型総和の部分的計算結果を効率よく利用する方式の研究
情報処理学会第121回プログラミング研究会, 2018
並列分散フレームワークの耐障害性評価のための通信障害模擬機能
第20回プログラミングおよびプログラミング言語ワークショップ(PPL2018), 2018
JVM上の動的言語のための抽象解釈
情報処理学会第121回プログラミング研究会, 2018
2017A Nonstandard Functional Programming Language
Proceedings of Asian Symposium on Programming Languages and Systems (APLAS2017), 2017
DOI: 10.1007/978-3-319-71237-6_25A DSL for Compensable and Interruptible Executions
Proceedings of 4th Workshop on Reactive and Event-based Languages & Systems (REBLS), 2017
C言語における無効なスタック領域へのポインタを検出する静的解析
日本ソフトウェア科学会第34回大会論文集, 2017
On Polymorphic Gradual Typing
Proceedings of the ACM on Programming Languages, 2017
A Type Reconstruction Algorithm for Gradually Typed Delimited Continuations
第19回プログラミングおよびプログラミング言語ワークショップ(PPL2017)論文集, 2017
Stateful manifest contracts
Conference Record of the Annual ACM Symposium on Principles of Programming Languages, 2017
DOI: 10.1145/3009837.3009875Verification of Code Generators via Higher-Order Model Checking
Proceedings of the 2017 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM'17), 2017
DOI: 10.1145/3018882.3018886Polymorphic Manifest Contracts, Revised and Resolved
ACM Transactions on Programming Languages and Systems, 2017
Sharper and Simpler Nonlinear Interpolants for Program Verification.
Programming Languages and Systems - 15th Asian Symposium(APLAS), 2017
DOI: 10.1007/978-3-319-71237-6_24Efficient Online Timed Pattern Matching by Automata-Based Skipping
FORMATS 2017, 2017
DOI: 10.1007/978-3-319-65765-3_13Towards Proof Synthesis Guided by Neural Machine Translation for Intuitionistic Propositional Logic
CoRR, 2017
アクセス制御論理に基づくIoT向け分散型アクセス制御フレームワーク
第15回 ディペンダブルシステムワークショップ (DSW 2017), 2017
アクセス制御機能の組み込まれた拡張オブジェクト指向言語
情報処理学会 第58回プログラミング・シンポジウム, 2017
優先度ならびに重みを用いたワークスティールフレームワークの性能改善
The 1st. cross-disciplinary Workshop on Computing Systems, Infrastructures, and Programming (xSIG 2017), 2017
仮想環境を考慮した要求駆動型負荷分散
日本ソフトウェア科学会第34回大会, 2017
HOPEコンパイラのプロトタイプ実装
2017年並列/分散/協調処理に関する『秋田』サマー・ワークショップ (SWoPP2017), 2017
2016階層的グループ化に基づきAndroidアプリの安全性を向上するバイトコード書換えツール
日本ソフトウェア科学会第33回大会論文集, 2016
An Extended Behavioral Type System for Memory-Leak Freedom
日本ソフトウェア科学会第33回大会論文集, 2016
SIMT のための Hoare 論理の Coq を用いた形式化と 並列 prefix-sum アルゴリズムの検証
第18回プログラミングおよびプログラミング言語ワークショップ(PPL2016)論文集, 2016
Gradual typing for delimited continuations
The 5th Script To Program Evolution Workshop, 2016
A Library-Based Approach to Context-Dependent Computation with Reactive Values
Proceedings of Constrained and Reactive Objects Workshop (CROW2016), 2016
DOI: 10.1145/2892664.2892669規則違反コードの構造を反映した木パタンを用いるコード検査器
情報処理学会論文誌 プログラミング, 2016
仮想環境を考慮した要求駆動型負荷分散の検討
第18回プログラミングおよびプログラミング言語ワークショップ(PPL2016), 2016
Preliminary Evaluations of Probabilistic Guards for a Work-Stealing Framework
Annual Meeting on Advanced Computing System and Infrastructure (ACSI) 2016, 2016
HOPEコンパイラの実装に向けて
第18回プログラミングおよびプログラミング言語ワークショップ(PPL2016), 2016
An MPI-based Implementation of the Tascell Task-Parallel Programming Language
Annual Meeting on Advanced Computing System and Infrastructure (ACSI) 2016, 2016
Evaluation of an MPI-based Implementation of the Tascell Task-Parallel Language on Massively Parallel Systems
PROCEEDINGS OF 45TH INTERNATIONAL CONFERENCE ON PARALLEL PROCESSING WORKSHOPS (ICPPW 2016), 2016
DOI: 10.1109/ICPPW.2016.36Extending aWork-Stealing Framework with Probabilistic Guards
PROCEEDINGS OF 45TH INTERNATIONAL CONFERENCE ON PARALLEL PROCESSING WORKSHOPS (ICPPW 2016), 2016
DOI: 10.1109/ICPPW.2016.372015参照を備えた多段階計算のための多相的型システム
日本ソフトウェア科学会第32回大会論文集, 2015
Visibility of Context-oriented Behavior and State in L
Computer Software, 2015
DOI: 10.11309/jssst.32.3_149Manifest contracts for datatypes
Conference Record of the Annual ACM Symposium on Principles of Programming Languages, 2015
DOI: 10.1145/2676726.2676996A Sound Type System for Layer Subtyping and Dynamically Activated First-Class Layers
Proceedings of Asian Symposium on Programming Languages and Systems (APLAS 2015), 2015
DOI: 10.1007/978-3-319-26529-2_24Shifting the Blame: A Blame Calculus with Delimited Control
Proceedings of Asian Symposium on Programming Languages and Systems (APLAS 2015), 2015
DOI: 10.1007/978-3-319-26529-2_11Input Synthesis for Sampled Data Systems by Program Logic
Proc. of the 4th Workshop on Hybrid Autonomous Systems (HAS 2014), 2015
DOI: 10.4204/EPTCS.174.3Validated Numerics Meets Reachability Analysis for CPS Design (NII Shonan Meeting 2015-14).
NII Shonan Meet. Rep., 2015
Design and Implementation of a Java Bytecode Manipulation Library for Clojure
Journal of Information Processing, 2015
メッセージ媒介システムの構想と試験実装
Annual Meeting on Advanced Computing System and Infrastructure (ACSI) 2015, 2015
Clojure用JVMバイトコード操作ライブラリの設計と実装
情報処理学会第102回プログラミング研究会, 2015
2014Automatic Memory Management Based on Program Transformation using Ownerships
Proceedings of Asian Symposium on Programming Languages and Systems (APLAS), 2014
DOI: 10.1007/978-3-319-12736-1_4Formalization of Featherweight Java and Featherweight GJ by using weak HOAS on Coq
日本ソフトウェア科学会大会論文集, 2014
Automatic Synthesis of Combiners in the MapReduce Framework: An Approach with Right Inverse
Proceedings of International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR), 2014
On-Demand Layer Activation for Type-Safe Deactivation
International Workshop on Context-Oriented Programming, COP'14 - Co-located with the 26th European Conference on Object-Oriented Programming, ECOOP'14, 2014
DOI: 10.1145/2637066.2637070Towards Type-Safe JCop: A type system for layer inheritance and first-class layers
International Workshop on Context-Oriented Programming, COP'12 - Co-located with the 26th European Conference on Object-Oriented Programming, ECOOP'14, 2014
DOI: 10.1145/2637066.2637073On Cross-Stage Persistence in Multi-Stage Programming
Proceedings of Intl. Symposium on Functional and Logic Programming (FLOPS2014), 2014
DOI: 10.1007/978-3-319-07151-0_7顕在的契約計算のための代数的データ型
第16回プログラミングおよびプログラミング言語ワークショップ(PPL2014)論文集, 2014
Formal Verification of CPS : A Nonstandard Analysis Approach
Journal of The Society of Instrument and Control Engineers, 2014
DOI: 10.11499/sicejl.53.1080Practical Implementation Techniques of Ambient Calculus in Conventional Dynamic Languages
29th Symposium on Applied Computing (SAC 2014), 2014
JVMバイトコードへの低水準操作を簡潔に記述可能なマクロシステム
情報処理学会 第55回プログラミング・シンポジウム, 2014
2013A Hoare Logic for SIMT Programs
Proceedings of Asian Symposium on Programming Languages and Systems (APLAS2013), 2013
DOI: 10.1007/978-3-319-03542-0_5多段階計算λ▹のための越段階埋込
日本ソフトウェア科学会第30回大会論文集, 2013
Layer Refinement in L
並列/分散/協調処理に関するサマー・ワークショップ (SWoPP), 2013
L: Context-oriented programming with only layers
Proceedings of the 5th International Workshop on Context-Oriented Programming, COP 2013, 2013
DOI: 10.1145/2489793.2489797Model-Checking Higher-Order Programs with Recursive Types
Proceedings of European Symposium on Programming (ESOP2013), 2013
DOI: 10.1007/978-3-642-37036-6_24Hyperstream processing systems: Nonstandard modeling of continuous-time signals
Conference Record of the Annual ACM Symposium on Principles of Programming Languages, 2013
DOI: 10.1145/2429069.2429120Safeアンビエントに基づく分散アプリケーション開発用Lisp環境
コンピュータソフトウェア, 2013
L-Closureの呼び出しコストの削減
情報処理学会論文誌 プログラミング, 2013
2012Type-based safe resource deallocation for shared-memory concurrency
Proceedings of Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), 2012
DOI: 10.1145/2398857.2384618A Type System for Dynamic Layer Composition
Proceedings of the International Workshop on Foundations of Object-Oriented Languages (FOOL2012), 2012
顕在的契約計算におけるアップキャスト除去
第14回プログラミングおよびプログラミング言語ワークショップ, 2012
Exercises in Nonstandard Static Analysis of Hybrid Systems
24th International Conference, CAV 2012, 2012
DOI: 10.1007/978-3-642-31424-7_34SEAN: Support Tool for Detecting Rule Violations in JNI Coding
IPSJ Transactions on Programming, 2012
JNIコーディングの規則違反を検出するための支援ツールSEANの開発
情報処理学会第87回プログラミング研究会, 2012
Detecting Bugs in Android Using a Static Escape Analyzer SEAN for Native Code
10th Asian Symposium on Programming Languages and Systems (APLAS 2012), 2012
2011Constructive linear-time temporal logic: Proof systems and Kripke semantics
Information and Computation, 2011
DOI: 10.1016/j.ic.2010.09.008Systematic Derivation of a λ○ Virtual Machine with Low-Level Code Generation by using Fusion Transformation
日本ソフトウェア科学会第28回大会論文集, 2011
Polymorphic Contracts
Proceedings of European Symposium on Programming (ESOP2011), 2011
DOI: 10.1007/978-3-642-19718-5_2Special track on object-oriented languages and systems
Proceedings of the ACM Symposium on Applied Computing, 2011
Gradual typing for generics
Proceedings of the 2011 ACM international conference on Object oriented programming systems languages and applications - OOPSLA '11, 2011
DOI: 10.1145/2048066.2048114ContextFJ: A minimal core calculus for context-oriented programming
Proceedings of the 10th International Workshop on Foundations of Aspect-Oriented Languages, FOAL 2011, 2011
DOI: 10.1145/1960510.1960515Ordered Types for Stream Processing of Tree-Structured Data
Information and Media Technologies, 2011
DOI: 10.11185/imt.6.385Programming with Infinitesimals: A WHILE-Language for Hybrid System Modeling
Automata, Languages and Programming, ICALP, Pt II, 2011
DOI: 10.1007/978-3-642-22012-8_312010A Logical Foundation for Environment Classifiers
Logical Methods in Computer Science, 2010
DOI: 10.2168/lmcs-6(4:8)2010Mostly modular compilation of crosscutting concerns by contextual predicate dispatch
Proceedings of Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), 2010
DOI: 10.1145/1932682.1869503Type relaxed weaving
AOSD.10 - 9th International Conference on Aspect-Oriented Software Development, 2010
DOI: 10.1145/1739230.17392452009Matching ThisType to subtyping
Proceedings of the ACM Symposium on Applied Computing, 2009
DOI: 10.1145/1529282.1529699Self type constructors
Proceeding of the 24th ACM SIGPLAN conference on Object oriented programming systems languages and applications - OOPSLA 09, 2009
DOI: 10.1145/1640089.1640109Towards gradual typing for generics
Proceedings for the 1st Workshop on Script to Program Evolution, STOP'09 in Conjunction with European Conference on Object-Oriented Programming, ECOOP'09, 2009
DOI: 10.1145/1570506.15705092008Proving Noninterference by a Fully Complete Translation to the Simply Typed lambda-calculus
Logical Methods in Computer Science, 2008
DOI: 10.2168/lmcs-4(3:10)2008On Constructive Linear-Time Temporal Logic
Proceedings of the Workshop on Intuitionistil Modal Logic and Applications (IMLA'08), 2008
Lightweight family polymorphism
Journal of Functional Programming, 2008
DOI: 10.1017/s0956796807006405Featherweight Java のための漸進的型付け
第10回プログラミングおよびプログラミング言語ワークショップ(PPL2008)論文集, 2008
文脈依存資源使用解析のための型システム
第10回プログラミングおよびプログラミング言語ワークショップ(PPL2008)論文集, 2008
The essence of lightweight family polymorphism
Journal of Object Technology, 2008
DOI: 10.5381/jot.2008.7.5.a32007Proving Noninterference by a Fully Complete Translation to the Simply Typed λ-Calculus
Advances in Computer Science - ASIAN 2006. Secure Software and Related Issues, 2007
DOI: 10.1007/978-3-540-77505-8_24Variant path types for scalable extensibility
Proceedings of the 22nd annual ACM SIGPLAN conference on Object oriented programming systems and applications - OOPSLA '07, 2007
DOI: 10.1145/1297027.1297037An Algorithm to Decide Conformance of Resource Usage to Specification for Resource Usage Verification
情報処理学会論文誌. プログラミング, 2007
Union types for object-oriented programming
Journal of Object Technology, 2007
Deriving compilers and virtual machines for a multi-level language
Proceedings of Asian Symposium on Programming Languages and Systems (APLAS 2007), 2007
2006Variant parametric types: A flexible subtyping scheme for generics
ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2006
DOI: 10.1145/1152649.1152650様相型に基づく情報流解析における非干渉性の論理関係による一般化とその証明
第8回プログラミングおよびプログラミング言語ワークショップ(PPL2006)論文集, 2006
Resource usage analysis for a functional language with exceptions
Proceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, 2006
DOI: 10.1145/1111542.1111550A modal type system for multi-level generating extensions with persistent code
PPDP'06 - Proceedings of the Eight ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming, 2006
2005Resource usage analysis
ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2005
DOI: 10.1145/1057387.1057390例外機構を備えた言語のための資源使用法解析
第7回プログラミングおよびプログラミング言語ワークショップ(PPL2005)論文集, 2005
メタプログラミングのための時相論理に基づく型付λ計算
第7回プログラミングおよびプログラミング言語ワークショップ(PPL2005)論文集, 2005
2004Generics・Union 型を導入したオブジェクト指向計算体系
第6回プログラミングおよびプログラミング言語ワークショップ(PPL2004)論文集, 2004
A generic type system for the Pi-calculus
THEORETICAL COMPUTER SCIENCE, 2004
DOI: 10.1016/S0304-3975(03)00325-6A modal foundation for secure information flow
Proceedings of the Workshop on Foundations of Computer Security (FCS'04), number 31 in Turku Centre for Computer Science General Publication,187-203, 2004
2003Union 型を導入したオブジェクト指向計算体系
日本ソフトウェア科学会第20回大会論文集, 2003
擬似引用を持つ型付計算体系λq
第5回プログラミングおよびプログラミング言語ワークショップ(PPL2003)論文集, 2003
2002On variance-based subtyping for parametric types
ECOOP 2002 - OBJECT-ORIENTED PROGRAMMING, 2002
2001Featherweight Java: A minimal core calculus for Java and GJ
ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2001
DOI: 10.1145/503502.503505A Recipe for Raw Types
Proceedings of the International Workshop on Foundations of Object-Oriented Languages (FOOL8), 2001
2000Garbage Collection Based on a Linear Type System
Proceedings of the 3rd ACM SIGPLAN Wokshop on Types in Compilation (TIC'00), 2000
Type reconstruction for linear pi-calculus with I/O subtyping
INFORMATION AND COMPUTATION, 2000
DOI: 10.1006/inco.2000.28721999Featherweight Java - A minimal core calculus for Java and GJ
Proceedings of ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA'99), 1999
1997Type-based Analysis of Communication for Concurrent Programming Languages
Proceedings of the Fourth International Static Analysis Symposium, 1997
Space-Efficient Gradual Typing in Coercion-Passing Style.
34th European Conference on Object-Oriented Programming, ECOOP 2020, 2020
DOI: 10.4230/LIPIcs.ECOOP.2020.8
34th European Conference on Object-Oriented Programming, ECOOP 2020, 2020
DOI: 10.4230/LIPIcs.ECOOP.2020.8
量子ビット連結性制約検査のための依存型システム
日本ソフトウェア科学会第37回大会論文集, 2020
日本ソフトウェア科学会第37回大会論文集, 2020
ConSORT: Context- and Flow-Sensitive Ownership Refinement Types for Imperative Programs
Programming Languages and Systems, 2020
DOI: 10.1007/978-3-030-44914-8_25
Programming Languages and Systems, 2020
DOI: 10.1007/978-3-030-44914-8_25
スタック領域上での時間的メモリ安全性を保証する静的解析手法
第22回プログラミングおよびプログラミング言語ワークショップ(PPL2020)論文集, 2020
第22回プログラミングおよびプログラミング言語ワークショップ(PPL2020)論文集, 2020
スマートコントラクトのための Effectively Callback-Free 性の型に基づく静的検証
第22回プログラミングおよびプログラミング言語ワークショップ(PPL2020)論文集, 2020
第22回プログラミングおよびプログラミング言語ワークショップ(PPL2020)論文集, 2020
F* を用いた Merkle Patricia Tree ライブラリの形式検証
第22回プログラミングおよびプログラミング言語ワークショップ(PPL2020)論文集, 2020
第22回プログラミングおよびプログラミング言語ワークショップ(PPL2020)論文集, 2020
Compilation of Coordinated Choice.
CoRR, 2020
CoRR, 2020
Signature restriction for polymorphic algebraic effects.
Proc. ACM Program. Lang., 2020
DOI: 10.1145/3408999
Proc. ACM Program. Lang., 2020
DOI: 10.1145/3408999
Space-Efficient Gradual Typing in Coercion-Passing Style
Informal Proceedings of the 1st International Workshop on Gradual Typing (WGT2020), 2020
Informal Proceedings of the 1st International Workshop on Gradual Typing (WGT2020), 2020
Gradual Typing for Extensibility by Rows
Informal Proceedings of the 1st International Workshop on Gradual Typing (WGT2020), 2020
Informal Proceedings of the 1st International Workshop on Gradual Typing (WGT2020), 2020
Visualizing Color-Wise Saliency of Black-Box Image Classification Models.
Proceedings of ACCV 2020, 2020
DOI: 10.1007/978-3-030-69535-4_12
Proceedings of ACCV 2020, 2020
DOI: 10.1007/978-3-030-69535-4_12
Generalized Property-Directed Reachability for Hybrid Systems
Verification, Model Checking, and Abstract Interpretation - 21st International Conference(VMCAI), 2020
DOI: 10.1007/978-3-030-39322-9_14
Verification, Model Checking, and Abstract Interpretation - 21st International Conference(VMCAI), 2020
DOI: 10.1007/978-3-030-39322-9_14
A Contract Corpus for Recognizing Rights and Obligations.
Proceedings of The 12th Language Resources and Evaluation Conference(LREC), 2020
Proceedings of The 12th Language Resources and Evaluation Conference(LREC), 2020
A Dependently Typed Multi-stage Calculus.
Programming Languages and Systems - 17th Asian Symposium, APLAS 2019, Nusa Dua, Bali, Indonesia, December 1-4, 2019, Proceedings, 2019
DOI: 10.1007/978-3-030-34175-6_4
Programming Languages and Systems - 17th Asian Symposium, APLAS 2019, Nusa Dua, Bali, Indonesia, December 1-4, 2019, Proceedings, 2019
DOI: 10.1007/978-3-030-34175-6_4
Manifest Contracts with Intersection Types.
Programming Languages and Systems - 17th Asian Symposium, APLAS 2019, Nusa Dua, Bali, Indonesia, December 1-4, 2019, Proceedings, 2019
DOI: 10.1007/978-3-030-34175-6_3
Programming Languages and Systems - 17th Asian Symposium, APLAS 2019, Nusa Dua, Bali, Indonesia, December 1-4, 2019, Proceedings, 2019
DOI: 10.1007/978-3-030-34175-6_3
Temporal Verification of Programs via First-Order Fixpoint Logic.
Static Analysis - 26th International Symposium, SAS 2019, Porto, Portugal, October 8-11, 2019, Proceedings, 2019
DOI: 10.1007/978-3-030-32304-2_20
Static Analysis - 26th International Symposium, SAS 2019, Porto, Portugal, October 8-11, 2019, Proceedings, 2019
DOI: 10.1007/978-3-030-32304-2_20
A Type System for First-Class Layers with Inheritance, Subtyping, and Swapping
Science of Computer Programming, 2019
Science of Computer Programming, 2019
Handling Polymorphic Algebraic Effects
Proceedings of European Symposium on Programming (ESOP2019), 2019
Proceedings of European Symposium on Programming (ESOP2019), 2019
空間効率の良いコアーション計算のためのコアーション渡し形式
第21回プログラミングおよびプログラミング言語ワークショップ(PPL2019)論文集, 2019
第21回プログラミングおよびプログラミング言語ワークショップ(PPL2019)論文集, 2019
Dynamic Type Inference for Gradual Hindley-Milner Typing
Proceedings of the ACM on Programming Languages, 2019
Proceedings of the ACM on Programming Languages, 2019
ワーカの重要度を考慮した並列実行フレームワークの障害耐性評価手法の検討
2019年並列／分散／協調処理に関する『北見』サマー・ワークショップ (SWoPP2019), 2019
2019年並列／分散／協調処理に関する『北見』サマー・ワークショップ (SWoPP2019), 2019
汎用送受信に対応したHOPEコンパイラの研究
2019年並列／分散／協調処理に関する『北見』サマー・ワークショップ (SWoPP2019), 2019
2019年並列／分散／協調処理に関する『北見』サマー・ワークショップ (SWoPP2019), 2019
JVM上の動的言語のための抽象解釈の実装
第60回プログラミング・シンポジウム, 2019
第60回プログラミング・シンポジウム, 2019
Extending a Work-Stealing Framework with Priorities and Weights
2019 IEEE/ACM 9th Workshop on Irregular Applications: Architectures and Algorithms (IA3), 2019
DOI: 10.1109/IA349570.2019.00008
2019 IEEE/ACM 9th Workshop on Irregular Applications: Architectures and Algorithms (IA3), 2019
DOI: 10.1109/IA349570.2019.00008
HOPE: A Parallel Execution Model Based on Hierarchical Omission
Proceedings of the 48th International Conference on Parallel Processing ({ICPP} 2019), 2019
DOI: 10.1145/3337821.3337899
Proceedings of the 48th International Conference on Parallel Processing ({ICPP} 2019), 2019
DOI: 10.1145/3337821.3337899
2018Nondetermnistic Manifest Contracts
Proceedings of theInternational Symposium on Principles and Practice of Declarative Programming, 2018
DOI: 10.1145/3236950.3236964ContextWorkflow: A Monadic DSL for Compensable and Interruptible Executions
Proceedings of the 32nd European Conference on Object-Oriented Programming, 2018
Method Safety Mechanism for Asynchronous Layer Deactivation
Science of Computer Programming, 2018
DOI: 10.1016/j.scico.2018.01.006Automated Verification of Functional Correctness of Race-Free GPU Programs
Journal of Automated Reasoning, 2018
DOI: 10.1007/978-3-319-48869-1_7Reasoning about Polymorphic Manifest Contracts.
CoRR, 2018
A Guess-and-Assume Approach to Loop Fusion for Program Verification
Proceedings of the ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, 2018
DOI: 10.1145/3162070Automated Proof Synthesis for the Minimal Propositional Logic with Deep Neural Networks
APLAS 2018, 2018
DOI: 10.1007/978-3-030-02768-1_17MONAA: A Tool for Timed Pattern Matching with Automata-Based Acceleration.
3rd Workshop on Monitoring and Testing of Cyber-Physical Systems, MT@CPSWeek 2018, Porto, Portugal, April 10, 2018, 2018
DOI: 10.1109/MT-CPS.2018.00014Generalized homogeneous polynomials for efficient template-based nonlinear invariant synthesis.
Theor. Comput. Sci., 2018
DOI: 10.1016/j.tcs.2018.06.005Probabilistic guards: A mechanism for increasing the granularity of work-stealing programs
Parallel Computing, 2018
分割統治型総和の部分的計算結果を効率よく利用する方式の研究
情報処理学会第121回プログラミング研究会, 2018
並列分散フレームワークの耐障害性評価のための通信障害模擬機能
第20回プログラミングおよびプログラミング言語ワークショップ(PPL2018), 2018
JVM上の動的言語のための抽象解釈
情報処理学会第121回プログラミング研究会, 2018
2017A Nonstandard Functional Programming Language
Proceedings of Asian Symposium on Programming Languages and Systems (APLAS2017), 2017
DOI: 10.1007/978-3-319-71237-6_25A DSL for Compensable and Interruptible Executions
Proceedings of 4th Workshop on Reactive and Event-based Languages & Systems (REBLS), 2017
C言語における無効なスタック領域へのポインタを検出する静的解析
日本ソフトウェア科学会第34回大会論文集, 2017
On Polymorphic Gradual Typing
Proceedings of the ACM on Programming Languages, 2017
A Type Reconstruction Algorithm for Gradually Typed Delimited Continuations
第19回プログラミングおよびプログラミング言語ワークショップ(PPL2017)論文集, 2017
Stateful manifest contracts
Conference Record of the Annual ACM Symposium on Principles of Programming Languages, 2017
DOI: 10.1145/3009837.3009875Verification of Code Generators via Higher-Order Model Checking
Proceedings of the 2017 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM'17), 2017
DOI: 10.1145/3018882.3018886Polymorphic Manifest Contracts, Revised and Resolved
ACM Transactions on Programming Languages and Systems, 2017
Sharper and Simpler Nonlinear Interpolants for Program Verification.
Programming Languages and Systems - 15th Asian Symposium(APLAS), 2017
DOI: 10.1007/978-3-319-71237-6_24Efficient Online Timed Pattern Matching by Automata-Based Skipping
FORMATS 2017, 2017
DOI: 10.1007/978-3-319-65765-3_13Towards Proof Synthesis Guided by Neural Machine Translation for Intuitionistic Propositional Logic
CoRR, 2017
アクセス制御論理に基づくIoT向け分散型アクセス制御フレームワーク
第15回 ディペンダブルシステムワークショップ (DSW 2017), 2017
アクセス制御機能の組み込まれた拡張オブジェクト指向言語
情報処理学会 第58回プログラミング・シンポジウム, 2017
優先度ならびに重みを用いたワークスティールフレームワークの性能改善
The 1st. cross-disciplinary Workshop on Computing Systems, Infrastructures, and Programming (xSIG 2017), 2017
仮想環境を考慮した要求駆動型負荷分散
日本ソフトウェア科学会第34回大会, 2017
HOPEコンパイラのプロトタイプ実装
2017年並列/分散/協調処理に関する『秋田』サマー・ワークショップ (SWoPP2017), 2017
2016階層的グループ化に基づきAndroidアプリの安全性を向上するバイトコード書換えツール
日本ソフトウェア科学会第33回大会論文集, 2016
An Extended Behavioral Type System for Memory-Leak Freedom
日本ソフトウェア科学会第33回大会論文集, 2016
SIMT のための Hoare 論理の Coq を用いた形式化と 並列 prefix-sum アルゴリズムの検証
第18回プログラミングおよびプログラミング言語ワークショップ(PPL2016)論文集, 2016
Gradual typing for delimited continuations
The 5th Script To Program Evolution Workshop, 2016
A Library-Based Approach to Context-Dependent Computation with Reactive Values
Proceedings of Constrained and Reactive Objects Workshop (CROW2016), 2016
DOI: 10.1145/2892664.2892669規則違反コードの構造を反映した木パタンを用いるコード検査器
情報処理学会論文誌 プログラミング, 2016
仮想環境を考慮した要求駆動型負荷分散の検討
第18回プログラミングおよびプログラミング言語ワークショップ(PPL2016), 2016
Preliminary Evaluations of Probabilistic Guards for a Work-Stealing Framework
Annual Meeting on Advanced Computing System and Infrastructure (ACSI) 2016, 2016
HOPEコンパイラの実装に向けて
第18回プログラミングおよびプログラミング言語ワークショップ(PPL2016), 2016
An MPI-based Implementation of the Tascell Task-Parallel Programming Language
Annual Meeting on Advanced Computing System and Infrastructure (ACSI) 2016, 2016
Evaluation of an MPI-based Implementation of the Tascell Task-Parallel Language on Massively Parallel Systems
PROCEEDINGS OF 45TH INTERNATIONAL CONFERENCE ON PARALLEL PROCESSING WORKSHOPS (ICPPW 2016), 2016
DOI: 10.1109/ICPPW.2016.36Extending aWork-Stealing Framework with Probabilistic Guards
PROCEEDINGS OF 45TH INTERNATIONAL CONFERENCE ON PARALLEL PROCESSING WORKSHOPS (ICPPW 2016), 2016
DOI: 10.1109/ICPPW.2016.372015参照を備えた多段階計算のための多相的型システム
日本ソフトウェア科学会第32回大会論文集, 2015
Visibility of Context-oriented Behavior and State in L
Computer Software, 2015
DOI: 10.11309/jssst.32.3_149Manifest contracts for datatypes
Conference Record of the Annual ACM Symposium on Principles of Programming Languages, 2015
DOI: 10.1145/2676726.2676996A Sound Type System for Layer Subtyping and Dynamically Activated First-Class Layers
Proceedings of Asian Symposium on Programming Languages and Systems (APLAS 2015), 2015
DOI: 10.1007/978-3-319-26529-2_24Shifting the Blame: A Blame Calculus with Delimited Control
Proceedings of Asian Symposium on Programming Languages and Systems (APLAS 2015), 2015
DOI: 10.1007/978-3-319-26529-2_11Input Synthesis for Sampled Data Systems by Program Logic
Proc. of the 4th Workshop on Hybrid Autonomous Systems (HAS 2014), 2015
DOI: 10.4204/EPTCS.174.3Validated Numerics Meets Reachability Analysis for CPS Design (NII Shonan Meeting 2015-14).
NII Shonan Meet. Rep., 2015
Design and Implementation of a Java Bytecode Manipulation Library for Clojure
Journal of Information Processing, 2015
メッセージ媒介システムの構想と試験実装
Annual Meeting on Advanced Computing System and Infrastructure (ACSI) 2015, 2015
Clojure用JVMバイトコード操作ライブラリの設計と実装
情報処理学会第102回プログラミング研究会, 2015
2014Automatic Memory Management Based on Program Transformation using Ownerships
Proceedings of Asian Symposium on Programming Languages and Systems (APLAS), 2014
DOI: 10.1007/978-3-319-12736-1_4Formalization of Featherweight Java and Featherweight GJ by using weak HOAS on Coq
日本ソフトウェア科学会大会論文集, 2014
Automatic Synthesis of Combiners in the MapReduce Framework: An Approach with Right Inverse
Proceedings of International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR), 2014
On-Demand Layer Activation for Type-Safe Deactivation
International Workshop on Context-Oriented Programming, COP'14 - Co-located with the 26th European Conference on Object-Oriented Programming, ECOOP'14, 2014
DOI: 10.1145/2637066.2637070Towards Type-Safe JCop: A type system for layer inheritance and first-class layers
International Workshop on Context-Oriented Programming, COP'12 - Co-located with the 26th European Conference on Object-Oriented Programming, ECOOP'14, 2014
DOI: 10.1145/2637066.2637073On Cross-Stage Persistence in Multi-Stage Programming
Proceedings of Intl. Symposium on Functional and Logic Programming (FLOPS2014), 2014
DOI: 10.1007/978-3-319-07151-0_7顕在的契約計算のための代数的データ型
第16回プログラミングおよびプログラミング言語ワークショップ(PPL2014)論文集, 2014
Formal Verification of CPS : A Nonstandard Analysis Approach
Journal of The Society of Instrument and Control Engineers, 2014
DOI: 10.11499/sicejl.53.1080Practical Implementation Techniques of Ambient Calculus in Conventional Dynamic Languages
29th Symposium on Applied Computing (SAC 2014), 2014
JVMバイトコードへの低水準操作を簡潔に記述可能なマクロシステム
情報処理学会 第55回プログラミング・シンポジウム, 2014
2013A Hoare Logic for SIMT Programs
Proceedings of Asian Symposium on Programming Languages and Systems (APLAS2013), 2013
DOI: 10.1007/978-3-319-03542-0_5多段階計算λ▹のための越段階埋込
日本ソフトウェア科学会第30回大会論文集, 2013
Layer Refinement in L
並列/分散/協調処理に関するサマー・ワークショップ (SWoPP), 2013
L: Context-oriented programming with only layers
Proceedings of the 5th International Workshop on Context-Oriented Programming, COP 2013, 2013
DOI: 10.1145/2489793.2489797Model-Checking Higher-Order Programs with Recursive Types
Proceedings of European Symposium on Programming (ESOP2013), 2013
DOI: 10.1007/978-3-642-37036-6_24Hyperstream processing systems: Nonstandard modeling of continuous-time signals
Conference Record of the Annual ACM Symposium on Principles of Programming Languages, 2013
DOI: 10.1145/2429069.2429120Safeアンビエントに基づく分散アプリケーション開発用Lisp環境
コンピュータソフトウェア, 2013
L-Closureの呼び出しコストの削減
情報処理学会論文誌 プログラミング, 2013
2012Type-based safe resource deallocation for shared-memory concurrency
Proceedings of Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), 2012
DOI: 10.1145/2398857.2384618A Type System for Dynamic Layer Composition
Proceedings of the International Workshop on Foundations of Object-Oriented Languages (FOOL2012), 2012
顕在的契約計算におけるアップキャスト除去
第14回プログラミングおよびプログラミング言語ワークショップ, 2012
Exercises in Nonstandard Static Analysis of Hybrid Systems
24th International Conference, CAV 2012, 2012
DOI: 10.1007/978-3-642-31424-7_34SEAN: Support Tool for Detecting Rule Violations in JNI Coding
IPSJ Transactions on Programming, 2012
JNIコーディングの規則違反を検出するための支援ツールSEANの開発
情報処理学会第87回プログラミング研究会, 2012
Detecting Bugs in Android Using a Static Escape Analyzer SEAN for Native Code
10th Asian Symposium on Programming Languages and Systems (APLAS 2012), 2012
2011Constructive linear-time temporal logic: Proof systems and Kripke semantics
Information and Computation, 2011
DOI: 10.1016/j.ic.2010.09.008Systematic Derivation of a λ○ Virtual Machine with Low-Level Code Generation by using Fusion Transformation
日本ソフトウェア科学会第28回大会論文集, 2011
Polymorphic Contracts
Proceedings of European Symposium on Programming (ESOP2011), 2011
DOI: 10.1007/978-3-642-19718-5_2Special track on object-oriented languages and systems
Proceedings of the ACM Symposium on Applied Computing, 2011
Gradual typing for generics
Proceedings of the 2011 ACM international conference on Object oriented programming systems languages and applications - OOPSLA '11, 2011
DOI: 10.1145/2048066.2048114ContextFJ: A minimal core calculus for context-oriented programming
Proceedings of the 10th International Workshop on Foundations of Aspect-Oriented Languages, FOAL 2011, 2011
DOI: 10.1145/1960510.1960515Ordered Types for Stream Processing of Tree-Structured Data
Information and Media Technologies, 2011
DOI: 10.11185/imt.6.385Programming with Infinitesimals: A WHILE-Language for Hybrid System Modeling
Automata, Languages and Programming, ICALP, Pt II, 2011
DOI: 10.1007/978-3-642-22012-8_312010A Logical Foundation for Environment Classifiers
Logical Methods in Computer Science, 2010
DOI: 10.2168/lmcs-6(4:8)2010Mostly modular compilation of crosscutting concerns by contextual predicate dispatch
Proceedings of Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), 2010
DOI: 10.1145/1932682.1869503Type relaxed weaving
AOSD.10 - 9th International Conference on Aspect-Oriented Software Development, 2010
DOI: 10.1145/1739230.17392452009Matching ThisType to subtyping
Proceedings of the ACM Symposium on Applied Computing, 2009
DOI: 10.1145/1529282.1529699Self type constructors
Proceeding of the 24th ACM SIGPLAN conference on Object oriented programming systems languages and applications - OOPSLA 09, 2009
DOI: 10.1145/1640089.1640109Towards gradual typing for generics
Proceedings for the 1st Workshop on Script to Program Evolution, STOP'09 in Conjunction with European Conference on Object-Oriented Programming, ECOOP'09, 2009
DOI: 10.1145/1570506.15705092008Proving Noninterference by a Fully Complete Translation to the Simply Typed lambda-calculus
Logical Methods in Computer Science, 2008
DOI: 10.2168/lmcs-4(3:10)2008On Constructive Linear-Time Temporal Logic
Proceedings of the Workshop on Intuitionistil Modal Logic and Applications (IMLA'08), 2008
Lightweight family polymorphism
Journal of Functional Programming, 2008
DOI: 10.1017/s0956796807006405Featherweight Java のための漸進的型付け
第10回プログラミングおよびプログラミング言語ワークショップ(PPL2008)論文集, 2008
文脈依存資源使用解析のための型システム
第10回プログラミングおよびプログラミング言語ワークショップ(PPL2008)論文集, 2008
The essence of lightweight family polymorphism
Journal of Object Technology, 2008
DOI: 10.5381/jot.2008.7.5.a32007Proving Noninterference by a Fully Complete Translation to the Simply Typed λ-Calculus
Advances in Computer Science - ASIAN 2006. Secure Software and Related Issues, 2007
DOI: 10.1007/978-3-540-77505-8_24Variant path types for scalable extensibility
Proceedings of the 22nd annual ACM SIGPLAN conference on Object oriented programming systems and applications - OOPSLA '07, 2007
DOI: 10.1145/1297027.1297037An Algorithm to Decide Conformance of Resource Usage to Specification for Resource Usage Verification
情報処理学会論文誌. プログラミング, 2007
Union types for object-oriented programming
Journal of Object Technology, 2007
Deriving compilers and virtual machines for a multi-level language
Proceedings of Asian Symposium on Programming Languages and Systems (APLAS 2007), 2007
2006Variant parametric types: A flexible subtyping scheme for generics
ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2006
DOI: 10.1145/1152649.1152650様相型に基づく情報流解析における非干渉性の論理関係による一般化とその証明
第8回プログラミングおよびプログラミング言語ワークショップ(PPL2006)論文集, 2006
Resource usage analysis for a functional language with exceptions
Proceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, 2006
DOI: 10.1145/1111542.1111550A modal type system for multi-level generating extensions with persistent code
PPDP'06 - Proceedings of the Eight ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming, 2006
2005Resource usage analysis
ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2005
DOI: 10.1145/1057387.1057390例外機構を備えた言語のための資源使用法解析
第7回プログラミングおよびプログラミング言語ワークショップ(PPL2005)論文集, 2005
メタプログラミングのための時相論理に基づく型付λ計算
第7回プログラミングおよびプログラミング言語ワークショップ(PPL2005)論文集, 2005
2004Generics・Union 型を導入したオブジェクト指向計算体系
第6回プログラミングおよびプログラミング言語ワークショップ(PPL2004)論文集, 2004
A generic type system for the Pi-calculus
THEORETICAL COMPUTER SCIENCE, 2004
DOI: 10.1016/S0304-3975(03)00325-6A modal foundation for secure information flow
Proceedings of the Workshop on Foundations of Computer Security (FCS'04), number 31 in Turku Centre for Computer Science General Publication,187-203, 2004
2003Union 型を導入したオブジェクト指向計算体系
日本ソフトウェア科学会第20回大会論文集, 2003
擬似引用を持つ型付計算体系λq
第5回プログラミングおよびプログラミング言語ワークショップ(PPL2003)論文集, 2003
2002On variance-based subtyping for parametric types
ECOOP 2002 - OBJECT-ORIENTED PROGRAMMING, 2002
2001Featherweight Java: A minimal core calculus for Java and GJ
ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2001
DOI: 10.1145/503502.503505A Recipe for Raw Types
Proceedings of the International Workshop on Foundations of Object-Oriented Languages (FOOL8), 2001
2000Garbage Collection Based on a Linear Type System
Proceedings of the 3rd ACM SIGPLAN Wokshop on Types in Compilation (TIC'00), 2000
Type reconstruction for linear pi-calculus with I/O subtyping
INFORMATION AND COMPUTATION, 2000
DOI: 10.1006/inco.2000.28721999Featherweight Java - A minimal core calculus for Java and GJ
Proceedings of ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA'99), 1999
1997Type-based Analysis of Communication for Concurrent Programming Languages
Proceedings of the Fourth International Static Analysis Symposium, 1997
Nondetermnistic Manifest Contracts
Proceedings of theInternational Symposium on Principles and Practice of Declarative Programming, 2018
DOI: 10.1145/3236950.3236964
Proceedings of theInternational Symposium on Principles and Practice of Declarative Programming, 2018
DOI: 10.1145/3236950.3236964
ContextWorkflow: A Monadic DSL for Compensable and Interruptible Executions
Proceedings of the 32nd European Conference on Object-Oriented Programming, 2018
Proceedings of the 32nd European Conference on Object-Oriented Programming, 2018
Method Safety Mechanism for Asynchronous Layer Deactivation
Science of Computer Programming, 2018
DOI: 10.1016/j.scico.2018.01.006
Science of Computer Programming, 2018
DOI: 10.1016/j.scico.2018.01.006
Automated Verification of Functional Correctness of Race-Free GPU Programs
Journal of Automated Reasoning, 2018
DOI: 10.1007/978-3-319-48869-1_7
Journal of Automated Reasoning, 2018
DOI: 10.1007/978-3-319-48869-1_7
Reasoning about Polymorphic Manifest Contracts.
CoRR, 2018
CoRR, 2018
A Guess-and-Assume Approach to Loop Fusion for Program Verification
Proceedings of the ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, 2018
DOI: 10.1145/3162070
Proceedings of the ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, 2018
DOI: 10.1145/3162070
Automated Proof Synthesis for the Minimal Propositional Logic with Deep Neural Networks
APLAS 2018, 2018
DOI: 10.1007/978-3-030-02768-1_17
APLAS 2018, 2018
DOI: 10.1007/978-3-030-02768-1_17
MONAA: A Tool for Timed Pattern Matching with Automata-Based Acceleration.
3rd Workshop on Monitoring and Testing of Cyber-Physical Systems, MT@CPSWeek 2018, Porto, Portugal, April 10, 2018, 2018
DOI: 10.1109/MT-CPS.2018.00014
3rd Workshop on Monitoring and Testing of Cyber-Physical Systems, MT@CPSWeek 2018, Porto, Portugal, April 10, 2018, 2018
DOI: 10.1109/MT-CPS.2018.00014
Generalized homogeneous polynomials for efficient template-based nonlinear invariant synthesis.
Theor. Comput. Sci., 2018
DOI: 10.1016/j.tcs.2018.06.005
Theor. Comput. Sci., 2018
DOI: 10.1016/j.tcs.2018.06.005
Probabilistic guards: A mechanism for increasing the granularity of work-stealing programs
Parallel Computing, 2018
Parallel Computing, 2018
分割統治型総和の部分的計算結果を効率よく利用する方式の研究
情報処理学会第121回プログラミング研究会, 2018
情報処理学会第121回プログラミング研究会, 2018
並列分散フレームワークの耐障害性評価のための通信障害模擬機能
第20回プログラミングおよびプログラミング言語ワークショップ(PPL2018), 2018
第20回プログラミングおよびプログラミング言語ワークショップ(PPL2018), 2018
JVM上の動的言語のための抽象解釈
情報処理学会第121回プログラミング研究会, 2018
情報処理学会第121回プログラミング研究会, 2018
A Nonstandard Functional Programming Language
Proceedings of Asian Symposium on Programming Languages and Systems (APLAS2017), 2017
DOI: 10.1007/978-3-319-71237-6_25
Proceedings of Asian Symposium on Programming Languages and Systems (APLAS2017), 2017
DOI: 10.1007/978-3-319-71237-6_25
A DSL for Compensable and Interruptible Executions
Proceedings of 4th Workshop on Reactive and Event-based Languages & Systems (REBLS), 2017
Proceedings of 4th Workshop on Reactive and Event-based Languages & Systems (REBLS), 2017
C言語における無効なスタック領域へのポインタを検出する静的解析
日本ソフトウェア科学会第34回大会論文集, 2017
日本ソフトウェア科学会第34回大会論文集, 2017
On Polymorphic Gradual Typing
Proceedings of the ACM on Programming Languages, 2017
Proceedings of the ACM on Programming Languages, 2017
A Type Reconstruction Algorithm for Gradually Typed Delimited Continuations
第19回プログラミングおよびプログラミング言語ワークショップ(PPL2017)論文集, 2017
第19回プログラミングおよびプログラミング言語ワークショップ(PPL2017)論文集, 2017
Stateful manifest contracts
Conference Record of the Annual ACM Symposium on Principles of Programming Languages, 2017
DOI: 10.1145/3009837.3009875
Conference Record of the Annual ACM Symposium on Principles of Programming Languages, 2017
DOI: 10.1145/3009837.3009875
Verification of Code Generators via Higher-Order Model Checking
Proceedings of the 2017 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM'17), 2017
DOI: 10.1145/3018882.3018886
Proceedings of the 2017 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM'17), 2017
DOI: 10.1145/3018882.3018886
Polymorphic Manifest Contracts, Revised and Resolved
ACM Transactions on Programming Languages and Systems, 2017
ACM Transactions on Programming Languages and Systems, 2017
Sharper and Simpler Nonlinear Interpolants for Program Verification.
Programming Languages and Systems - 15th Asian Symposium(APLAS), 2017
DOI: 10.1007/978-3-319-71237-6_24
Programming Languages and Systems - 15th Asian Symposium(APLAS), 2017
DOI: 10.1007/978-3-319-71237-6_24
Efficient Online Timed Pattern Matching by Automata-Based Skipping
FORMATS 2017, 2017
DOI: 10.1007/978-3-319-65765-3_13
FORMATS 2017, 2017
DOI: 10.1007/978-3-319-65765-3_13
Towards Proof Synthesis Guided by Neural Machine Translation for Intuitionistic Propositional Logic
CoRR, 2017
CoRR, 2017
アクセス制御論理に基づくIoT向け分散型アクセス制御フレームワーク
第15回 ディペンダブルシステムワークショップ (DSW 2017), 2017
第15回 ディペンダブルシステムワークショップ (DSW 2017), 2017
アクセス制御機能の組み込まれた拡張オブジェクト指向言語
情報処理学会 第58回プログラミング・シンポジウム, 2017
情報処理学会 第58回プログラミング・シンポジウム, 2017
優先度ならびに重みを用いたワークスティールフレームワークの性能改善
The 1st. cross-disciplinary Workshop on Computing Systems, Infrastructures, and Programming (xSIG 2017), 2017
The 1st. cross-disciplinary Workshop on Computing Systems, Infrastructures, and Programming (xSIG 2017), 2017
仮想環境を考慮した要求駆動型負荷分散
日本ソフトウェア科学会第34回大会, 2017
日本ソフトウェア科学会第34回大会, 2017
HOPEコンパイラのプロトタイプ実装
2017年並列/分散/協調処理に関する『秋田』サマー・ワークショップ (SWoPP2017), 2017
2017年並列/分散/協調処理に関する『秋田』サマー・ワークショップ (SWoPP2017), 2017
2016階層的グループ化に基づきAndroidアプリの安全性を向上するバイトコード書換えツール
日本ソフトウェア科学会第33回大会論文集, 2016
An Extended Behavioral Type System for Memory-Leak Freedom
日本ソフトウェア科学会第33回大会論文集, 2016
SIMT のための Hoare 論理の Coq を用いた形式化と 並列 prefix-sum アルゴリズムの検証
第18回プログラミングおよびプログラミング言語ワークショップ(PPL2016)論文集, 2016
Gradual typing for delimited continuations
The 5th Script To Program Evolution Workshop, 2016
A Library-Based Approach to Context-Dependent Computation with Reactive Values
Proceedings of Constrained and Reactive Objects Workshop (CROW2016), 2016
DOI: 10.1145/2892664.2892669規則違反コードの構造を反映した木パタンを用いるコード検査器
情報処理学会論文誌 プログラミング, 2016
仮想環境を考慮した要求駆動型負荷分散の検討
第18回プログラミングおよびプログラミング言語ワークショップ(PPL2016), 2016
Preliminary Evaluations of Probabilistic Guards for a Work-Stealing Framework
Annual Meeting on Advanced Computing System and Infrastructure (ACSI) 2016, 2016
HOPEコンパイラの実装に向けて
第18回プログラミングおよびプログラミング言語ワークショップ(PPL2016), 2016
An MPI-based Implementation of the Tascell Task-Parallel Programming Language
Annual Meeting on Advanced Computing System and Infrastructure (ACSI) 2016, 2016
Evaluation of an MPI-based Implementation of the Tascell Task-Parallel Language on Massively Parallel Systems
PROCEEDINGS OF 45TH INTERNATIONAL CONFERENCE ON PARALLEL PROCESSING WORKSHOPS (ICPPW 2016), 2016
DOI: 10.1109/ICPPW.2016.36Extending aWork-Stealing Framework with Probabilistic Guards
PROCEEDINGS OF 45TH INTERNATIONAL CONFERENCE ON PARALLEL PROCESSING WORKSHOPS (ICPPW 2016), 2016
DOI: 10.1109/ICPPW.2016.372015参照を備えた多段階計算のための多相的型システム
日本ソフトウェア科学会第32回大会論文集, 2015
Visibility of Context-oriented Behavior and State in L
Computer Software, 2015
DOI: 10.11309/jssst.32.3_149Manifest contracts for datatypes
Conference Record of the Annual ACM Symposium on Principles of Programming Languages, 2015
DOI: 10.1145/2676726.2676996A Sound Type System for Layer Subtyping and Dynamically Activated First-Class Layers
Proceedings of Asian Symposium on Programming Languages and Systems (APLAS 2015), 2015
DOI: 10.1007/978-3-319-26529-2_24Shifting the Blame: A Blame Calculus with Delimited Control
Proceedings of Asian Symposium on Programming Languages and Systems (APLAS 2015), 2015
DOI: 10.1007/978-3-319-26529-2_11Input Synthesis for Sampled Data Systems by Program Logic
Proc. of the 4th Workshop on Hybrid Autonomous Systems (HAS 2014), 2015
DOI: 10.4204/EPTCS.174.3Validated Numerics Meets Reachability Analysis for CPS Design (NII Shonan Meeting 2015-14).
NII Shonan Meet. Rep., 2015
Design and Implementation of a Java Bytecode Manipulation Library for Clojure
Journal of Information Processing, 2015
メッセージ媒介システムの構想と試験実装
Annual Meeting on Advanced Computing System and Infrastructure (ACSI) 2015, 2015
Clojure用JVMバイトコード操作ライブラリの設計と実装
情報処理学会第102回プログラミング研究会, 2015
2014Automatic Memory Management Based on Program Transformation using Ownerships
Proceedings of Asian Symposium on Programming Languages and Systems (APLAS), 2014
DOI: 10.1007/978-3-319-12736-1_4Formalization of Featherweight Java and Featherweight GJ by using weak HOAS on Coq
日本ソフトウェア科学会大会論文集, 2014
Automatic Synthesis of Combiners in the MapReduce Framework: An Approach with Right Inverse
Proceedings of International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR), 2014
On-Demand Layer Activation for Type-Safe Deactivation
International Workshop on Context-Oriented Programming, COP'14 - Co-located with the 26th European Conference on Object-Oriented Programming, ECOOP'14, 2014
DOI: 10.1145/2637066.2637070Towards Type-Safe JCop: A type system for layer inheritance and first-class layers
International Workshop on Context-Oriented Programming, COP'12 - Co-located with the 26th European Conference on Object-Oriented Programming, ECOOP'14, 2014
DOI: 10.1145/2637066.2637073On Cross-Stage Persistence in Multi-Stage Programming
Proceedings of Intl. Symposium on Functional and Logic Programming (FLOPS2014), 2014
DOI: 10.1007/978-3-319-07151-0_7顕在的契約計算のための代数的データ型
第16回プログラミングおよびプログラミング言語ワークショップ(PPL2014)論文集, 2014
Formal Verification of CPS : A Nonstandard Analysis Approach
Journal of The Society of Instrument and Control Engineers, 2014
DOI: 10.11499/sicejl.53.1080Practical Implementation Techniques of Ambient Calculus in Conventional Dynamic Languages
29th Symposium on Applied Computing (SAC 2014), 2014
JVMバイトコードへの低水準操作を簡潔に記述可能なマクロシステム
情報処理学会 第55回プログラミング・シンポジウム, 2014
2013A Hoare Logic for SIMT Programs
Proceedings of Asian Symposium on Programming Languages and Systems (APLAS2013), 2013
DOI: 10.1007/978-3-319-03542-0_5多段階計算λ▹のための越段階埋込
日本ソフトウェア科学会第30回大会論文集, 2013
Layer Refinement in L
並列/分散/協調処理に関するサマー・ワークショップ (SWoPP), 2013
L: Context-oriented programming with only layers
Proceedings of the 5th International Workshop on Context-Oriented Programming, COP 2013, 2013
DOI: 10.1145/2489793.2489797Model-Checking Higher-Order Programs with Recursive Types
Proceedings of European Symposium on Programming (ESOP2013), 2013
DOI: 10.1007/978-3-642-37036-6_24Hyperstream processing systems: Nonstandard modeling of continuous-time signals
Conference Record of the Annual ACM Symposium on Principles of Programming Languages, 2013
DOI: 10.1145/2429069.2429120Safeアンビエントに基づく分散アプリケーション開発用Lisp環境
コンピュータソフトウェア, 2013
L-Closureの呼び出しコストの削減
情報処理学会論文誌 プログラミング, 2013
2012Type-based safe resource deallocation for shared-memory concurrency
Proceedings of Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), 2012
DOI: 10.1145/2398857.2384618A Type System for Dynamic Layer Composition
Proceedings of the International Workshop on Foundations of Object-Oriented Languages (FOOL2012), 2012
顕在的契約計算におけるアップキャスト除去
第14回プログラミングおよびプログラミング言語ワークショップ, 2012
Exercises in Nonstandard Static Analysis of Hybrid Systems
24th International Conference, CAV 2012, 2012
DOI: 10.1007/978-3-642-31424-7_34SEAN: Support Tool for Detecting Rule Violations in JNI Coding
IPSJ Transactions on Programming, 2012
JNIコーディングの規則違反を検出するための支援ツールSEANの開発
情報処理学会第87回プログラミング研究会, 2012
Detecting Bugs in Android Using a Static Escape Analyzer SEAN for Native Code
10th Asian Symposium on Programming Languages and Systems (APLAS 2012), 2012
2011Constructive linear-time temporal logic: Proof systems and Kripke semantics
Information and Computation, 2011
DOI: 10.1016/j.ic.2010.09.008Systematic Derivation of a λ○ Virtual Machine with Low-Level Code Generation by using Fusion Transformation
日本ソフトウェア科学会第28回大会論文集, 2011
Polymorphic Contracts
Proceedings of European Symposium on Programming (ESOP2011), 2011
DOI: 10.1007/978-3-642-19718-5_2Special track on object-oriented languages and systems
Proceedings of the ACM Symposium on Applied Computing, 2011
Gradual typing for generics
Proceedings of the 2011 ACM international conference on Object oriented programming systems languages and applications - OOPSLA '11, 2011
DOI: 10.1145/2048066.2048114ContextFJ: A minimal core calculus for context-oriented programming
Proceedings of the 10th International Workshop on Foundations of Aspect-Oriented Languages, FOAL 2011, 2011
DOI: 10.1145/1960510.1960515Ordered Types for Stream Processing of Tree-Structured Data
Information and Media Technologies, 2011
DOI: 10.11185/imt.6.385Programming with Infinitesimals: A WHILE-Language for Hybrid System Modeling
Automata, Languages and Programming, ICALP, Pt II, 2011
DOI: 10.1007/978-3-642-22012-8_312010A Logical Foundation for Environment Classifiers
Logical Methods in Computer Science, 2010
DOI: 10.2168/lmcs-6(4:8)2010Mostly modular compilation of crosscutting concerns by contextual predicate dispatch
Proceedings of Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), 2010
DOI: 10.1145/1932682.1869503Type relaxed weaving
AOSD.10 - 9th International Conference on Aspect-Oriented Software Development, 2010
DOI: 10.1145/1739230.17392452009Matching ThisType to subtyping
Proceedings of the ACM Symposium on Applied Computing, 2009
DOI: 10.1145/1529282.1529699Self type constructors
Proceeding of the 24th ACM SIGPLAN conference on Object oriented programming systems languages and applications - OOPSLA 09, 2009
DOI: 10.1145/1640089.1640109Towards gradual typing for generics
Proceedings for the 1st Workshop on Script to Program Evolution, STOP'09 in Conjunction with European Conference on Object-Oriented Programming, ECOOP'09, 2009
DOI: 10.1145/1570506.15705092008Proving Noninterference by a Fully Complete Translation to the Simply Typed lambda-calculus
Logical Methods in Computer Science, 2008
DOI: 10.2168/lmcs-4(3:10)2008On Constructive Linear-Time Temporal Logic
Proceedings of the Workshop on Intuitionistil Modal Logic and Applications (IMLA'08), 2008
Lightweight family polymorphism
Journal of Functional Programming, 2008
DOI: 10.1017/s0956796807006405Featherweight Java のための漸進的型付け
第10回プログラミングおよびプログラミング言語ワークショップ(PPL2008)論文集, 2008
文脈依存資源使用解析のための型システム
第10回プログラミングおよびプログラミング言語ワークショップ(PPL2008)論文集, 2008
The essence of lightweight family polymorphism
Journal of Object Technology, 2008
DOI: 10.5381/jot.2008.7.5.a32007Proving Noninterference by a Fully Complete Translation to the Simply Typed λ-Calculus
Advances in Computer Science - ASIAN 2006. Secure Software and Related Issues, 2007
DOI: 10.1007/978-3-540-77505-8_24Variant path types for scalable extensibility
Proceedings of the 22nd annual ACM SIGPLAN conference on Object oriented programming systems and applications - OOPSLA '07, 2007
DOI: 10.1145/1297027.1297037An Algorithm to Decide Conformance of Resource Usage to Specification for Resource Usage Verification
情報処理学会論文誌. プログラミング, 2007
Union types for object-oriented programming
Journal of Object Technology, 2007
Deriving compilers and virtual machines for a multi-level language
Proceedings of Asian Symposium on Programming Languages and Systems (APLAS 2007), 2007
2006Variant parametric types: A flexible subtyping scheme for generics
ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2006
DOI: 10.1145/1152649.1152650様相型に基づく情報流解析における非干渉性の論理関係による一般化とその証明
第8回プログラミングおよびプログラミング言語ワークショップ(PPL2006)論文集, 2006
Resource usage analysis for a functional language with exceptions
Proceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, 2006
DOI: 10.1145/1111542.1111550A modal type system for multi-level generating extensions with persistent code
PPDP'06 - Proceedings of the Eight ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming, 2006
2005Resource usage analysis
ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2005
DOI: 10.1145/1057387.1057390例外機構を備えた言語のための資源使用法解析
第7回プログラミングおよびプログラミング言語ワークショップ(PPL2005)論文集, 2005
メタプログラミングのための時相論理に基づく型付λ計算
第7回プログラミングおよびプログラミング言語ワークショップ(PPL2005)論文集, 2005
2004Generics・Union 型を導入したオブジェクト指向計算体系
第6回プログラミングおよびプログラミング言語ワークショップ(PPL2004)論文集, 2004
A generic type system for the Pi-calculus
THEORETICAL COMPUTER SCIENCE, 2004
DOI: 10.1016/S0304-3975(03)00325-6A modal foundation for secure information flow
Proceedings of the Workshop on Foundations of Computer Security (FCS'04), number 31 in Turku Centre for Computer Science General Publication,187-203, 2004
2003Union 型を導入したオブジェクト指向計算体系
日本ソフトウェア科学会第20回大会論文集, 2003
擬似引用を持つ型付計算体系λq
第5回プログラミングおよびプログラミング言語ワークショップ(PPL2003)論文集, 2003
2002On variance-based subtyping for parametric types
ECOOP 2002 - OBJECT-ORIENTED PROGRAMMING, 2002
2001Featherweight Java: A minimal core calculus for Java and GJ
ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2001
DOI: 10.1145/503502.503505A Recipe for Raw Types
Proceedings of the International Workshop on Foundations of Object-Oriented Languages (FOOL8), 2001
2000Garbage Collection Based on a Linear Type System
Proceedings of the 3rd ACM SIGPLAN Wokshop on Types in Compilation (TIC'00), 2000
Type reconstruction for linear pi-calculus with I/O subtyping
INFORMATION AND COMPUTATION, 2000
DOI: 10.1006/inco.2000.28721999Featherweight Java - A minimal core calculus for Java and GJ
Proceedings of ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA'99), 1999
1997Type-based Analysis of Communication for Concurrent Programming Languages
Proceedings of the Fourth International Static Analysis Symposium, 1997
階層的グループ化に基づきAndroidアプリの安全性を向上するバイトコード書換えツール
日本ソフトウェア科学会第33回大会論文集, 2016
日本ソフトウェア科学会第33回大会論文集, 2016
An Extended Behavioral Type System for Memory-Leak Freedom
日本ソフトウェア科学会第33回大会論文集, 2016
日本ソフトウェア科学会第33回大会論文集, 2016
SIMT のための Hoare 論理の Coq を用いた形式化と 並列 prefix-sum アルゴリズムの検証
第18回プログラミングおよびプログラミング言語ワークショップ(PPL2016)論文集, 2016
第18回プログラミングおよびプログラミング言語ワークショップ(PPL2016)論文集, 2016
Gradual typing for delimited continuations
The 5th Script To Program Evolution Workshop, 2016
The 5th Script To Program Evolution Workshop, 2016
A Library-Based Approach to Context-Dependent Computation with Reactive Values
Proceedings of Constrained and Reactive Objects Workshop (CROW2016), 2016
DOI: 10.1145/2892664.2892669
Proceedings of Constrained and Reactive Objects Workshop (CROW2016), 2016
DOI: 10.1145/2892664.2892669
規則違反コードの構造を反映した木パタンを用いるコード検査器
情報処理学会論文誌 プログラミング, 2016
情報処理学会論文誌 プログラミング, 2016
仮想環境を考慮した要求駆動型負荷分散の検討
第18回プログラミングおよびプログラミング言語ワークショップ(PPL2016), 2016
第18回プログラミングおよびプログラミング言語ワークショップ(PPL2016), 2016
Preliminary Evaluations of Probabilistic Guards for a Work-Stealing Framework
Annual Meeting on Advanced Computing System and Infrastructure (ACSI) 2016, 2016
Annual Meeting on Advanced Computing System and Infrastructure (ACSI) 2016, 2016
HOPEコンパイラの実装に向けて
第18回プログラミングおよびプログラミング言語ワークショップ(PPL2016), 2016
第18回プログラミングおよびプログラミング言語ワークショップ(PPL2016), 2016
An MPI-based Implementation of the Tascell Task-Parallel Programming Language
Annual Meeting on Advanced Computing System and Infrastructure (ACSI) 2016, 2016
Annual Meeting on Advanced Computing System and Infrastructure (ACSI) 2016, 2016
Evaluation of an MPI-based Implementation of the Tascell Task-Parallel Language on Massively Parallel Systems
PROCEEDINGS OF 45TH INTERNATIONAL CONFERENCE ON PARALLEL PROCESSING WORKSHOPS (ICPPW 2016), 2016
DOI: 10.1109/ICPPW.2016.36
PROCEEDINGS OF 45TH INTERNATIONAL CONFERENCE ON PARALLEL PROCESSING WORKSHOPS (ICPPW 2016), 2016
DOI: 10.1109/ICPPW.2016.36
Extending aWork-Stealing Framework with Probabilistic Guards
PROCEEDINGS OF 45TH INTERNATIONAL CONFERENCE ON PARALLEL PROCESSING WORKSHOPS (ICPPW 2016), 2016
DOI: 10.1109/ICPPW.2016.37
PROCEEDINGS OF 45TH INTERNATIONAL CONFERENCE ON PARALLEL PROCESSING WORKSHOPS (ICPPW 2016), 2016
DOI: 10.1109/ICPPW.2016.37
参照を備えた多段階計算のための多相的型システム
日本ソフトウェア科学会第32回大会論文集, 2015
日本ソフトウェア科学会第32回大会論文集, 2015
Visibility of Context-oriented Behavior and State in L
Computer Software, 2015
DOI: 10.11309/jssst.32.3_149
Computer Software, 2015
DOI: 10.11309/jssst.32.3_149
Manifest contracts for datatypes
Conference Record of the Annual ACM Symposium on Principles of Programming Languages, 2015
DOI: 10.1145/2676726.2676996
Conference Record of the Annual ACM Symposium on Principles of Programming Languages, 2015
DOI: 10.1145/2676726.2676996
A Sound Type System for Layer Subtyping and Dynamically Activated First-Class Layers
Proceedings of Asian Symposium on Programming Languages and Systems (APLAS 2015), 2015
DOI: 10.1007/978-3-319-26529-2_24
Proceedings of Asian Symposium on Programming Languages and Systems (APLAS 2015), 2015
DOI: 10.1007/978-3-319-26529-2_24
Shifting the Blame: A Blame Calculus with Delimited Control
Proceedings of Asian Symposium on Programming Languages and Systems (APLAS 2015), 2015
DOI: 10.1007/978-3-319-26529-2_11
Proceedings of Asian Symposium on Programming Languages and Systems (APLAS 2015), 2015
DOI: 10.1007/978-3-319-26529-2_11
Input Synthesis for Sampled Data Systems by Program Logic
Proc. of the 4th Workshop on Hybrid Autonomous Systems (HAS 2014), 2015
DOI: 10.4204/EPTCS.174.3
Proc. of the 4th Workshop on Hybrid Autonomous Systems (HAS 2014), 2015
DOI: 10.4204/EPTCS.174.3
Validated Numerics Meets Reachability Analysis for CPS Design (NII Shonan Meeting 2015-14).
NII Shonan Meet. Rep., 2015
NII Shonan Meet. Rep., 2015
Design and Implementation of a Java Bytecode Manipulation Library for Clojure
Journal of Information Processing, 2015
Journal of Information Processing, 2015
メッセージ媒介システムの構想と試験実装
Annual Meeting on Advanced Computing System and Infrastructure (ACSI) 2015, 2015
Annual Meeting on Advanced Computing System and Infrastructure (ACSI) 2015, 2015
Clojure用JVMバイトコード操作ライブラリの設計と実装
情報処理学会第102回プログラミング研究会, 2015
情報処理学会第102回プログラミング研究会, 2015
2014Automatic Memory Management Based on Program Transformation using Ownerships
Proceedings of Asian Symposium on Programming Languages and Systems (APLAS), 2014
DOI: 10.1007/978-3-319-12736-1_4Formalization of Featherweight Java and Featherweight GJ by using weak HOAS on Coq
日本ソフトウェア科学会大会論文集, 2014
Automatic Synthesis of Combiners in the MapReduce Framework: An Approach with Right Inverse
Proceedings of International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR), 2014
On-Demand Layer Activation for Type-Safe Deactivation
International Workshop on Context-Oriented Programming, COP'14 - Co-located with the 26th European Conference on Object-Oriented Programming, ECOOP'14, 2014
DOI: 10.1145/2637066.2637070Towards Type-Safe JCop: A type system for layer inheritance and first-class layers
International Workshop on Context-Oriented Programming, COP'12 - Co-located with the 26th European Conference on Object-Oriented Programming, ECOOP'14, 2014
DOI: 10.1145/2637066.2637073On Cross-Stage Persistence in Multi-Stage Programming
Proceedings of Intl. Symposium on Functional and Logic Programming (FLOPS2014), 2014
DOI: 10.1007/978-3-319-07151-0_7顕在的契約計算のための代数的データ型
第16回プログラミングおよびプログラミング言語ワークショップ(PPL2014)論文集, 2014
Formal Verification of CPS : A Nonstandard Analysis Approach
Journal of The Society of Instrument and Control Engineers, 2014
DOI: 10.11499/sicejl.53.1080Practical Implementation Techniques of Ambient Calculus in Conventional Dynamic Languages
29th Symposium on Applied Computing (SAC 2014), 2014
JVMバイトコードへの低水準操作を簡潔に記述可能なマクロシステム
情報処理学会 第55回プログラミング・シンポジウム, 2014
2013A Hoare Logic for SIMT Programs
Proceedings of Asian Symposium on Programming Languages and Systems (APLAS2013), 2013
DOI: 10.1007/978-3-319-03542-0_5多段階計算λ▹のための越段階埋込
日本ソフトウェア科学会第30回大会論文集, 2013
Layer Refinement in L
並列/分散/協調処理に関するサマー・ワークショップ (SWoPP), 2013
L: Context-oriented programming with only layers
Proceedings of the 5th International Workshop on Context-Oriented Programming, COP 2013, 2013
DOI: 10.1145/2489793.2489797Model-Checking Higher-Order Programs with Recursive Types
Proceedings of European Symposium on Programming (ESOP2013), 2013
DOI: 10.1007/978-3-642-37036-6_24Hyperstream processing systems: Nonstandard modeling of continuous-time signals
Conference Record of the Annual ACM Symposium on Principles of Programming Languages, 2013
DOI: 10.1145/2429069.2429120Safeアンビエントに基づく分散アプリケーション開発用Lisp環境
コンピュータソフトウェア, 2013
L-Closureの呼び出しコストの削減
情報処理学会論文誌 プログラミング, 2013
2012Type-based safe resource deallocation for shared-memory concurrency
Proceedings of Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), 2012
DOI: 10.1145/2398857.2384618A Type System for Dynamic Layer Composition
Proceedings of the International Workshop on Foundations of Object-Oriented Languages (FOOL2012), 2012
顕在的契約計算におけるアップキャスト除去
第14回プログラミングおよびプログラミング言語ワークショップ, 2012
Exercises in Nonstandard Static Analysis of Hybrid Systems
24th International Conference, CAV 2012, 2012
DOI: 10.1007/978-3-642-31424-7_34SEAN: Support Tool for Detecting Rule Violations in JNI Coding
IPSJ Transactions on Programming, 2012
JNIコーディングの規則違反を検出するための支援ツールSEANの開発
情報処理学会第87回プログラミング研究会, 2012
Detecting Bugs in Android Using a Static Escape Analyzer SEAN for Native Code
10th Asian Symposium on Programming Languages and Systems (APLAS 2012), 2012
2011Constructive linear-time temporal logic: Proof systems and Kripke semantics
Information and Computation, 2011
DOI: 10.1016/j.ic.2010.09.008Systematic Derivation of a λ○ Virtual Machine with Low-Level Code Generation by using Fusion Transformation
日本ソフトウェア科学会第28回大会論文集, 2011
Polymorphic Contracts
Proceedings of European Symposium on Programming (ESOP2011), 2011
DOI: 10.1007/978-3-642-19718-5_2Special track on object-oriented languages and systems
Proceedings of the ACM Symposium on Applied Computing, 2011
Gradual typing for generics
Proceedings of the 2011 ACM international conference on Object oriented programming systems languages and applications - OOPSLA '11, 2011
DOI: 10.1145/2048066.2048114ContextFJ: A minimal core calculus for context-oriented programming
Proceedings of the 10th International Workshop on Foundations of Aspect-Oriented Languages, FOAL 2011, 2011
DOI: 10.1145/1960510.1960515Ordered Types for Stream Processing of Tree-Structured Data
Information and Media Technologies, 2011
DOI: 10.11185/imt.6.385Programming with Infinitesimals: A WHILE-Language for Hybrid System Modeling
Automata, Languages and Programming, ICALP, Pt II, 2011
DOI: 10.1007/978-3-642-22012-8_312010A Logical Foundation for Environment Classifiers
Logical Methods in Computer Science, 2010
DOI: 10.2168/lmcs-6(4:8)2010Mostly modular compilation of crosscutting concerns by contextual predicate dispatch
Proceedings of Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), 2010
DOI: 10.1145/1932682.1869503Type relaxed weaving
AOSD.10 - 9th International Conference on Aspect-Oriented Software Development, 2010
DOI: 10.1145/1739230.17392452009Matching ThisType to subtyping
Proceedings of the ACM Symposium on Applied Computing, 2009
DOI: 10.1145/1529282.1529699Self type constructors
Proceeding of the 24th ACM SIGPLAN conference on Object oriented programming systems languages and applications - OOPSLA 09, 2009
DOI: 10.1145/1640089.1640109Towards gradual typing for generics
Proceedings for the 1st Workshop on Script to Program Evolution, STOP'09 in Conjunction with European Conference on Object-Oriented Programming, ECOOP'09, 2009
DOI: 10.1145/1570506.15705092008Proving Noninterference by a Fully Complete Translation to the Simply Typed lambda-calculus
Logical Methods in Computer Science, 2008
DOI: 10.2168/lmcs-4(3:10)2008On Constructive Linear-Time Temporal Logic
Proceedings of the Workshop on Intuitionistil Modal Logic and Applications (IMLA'08), 2008
Lightweight family polymorphism
Journal of Functional Programming, 2008
DOI: 10.1017/s0956796807006405Featherweight Java のための漸進的型付け
第10回プログラミングおよびプログラミング言語ワークショップ(PPL2008)論文集, 2008
文脈依存資源使用解析のための型システム
第10回プログラミングおよびプログラミング言語ワークショップ(PPL2008)論文集, 2008
The essence of lightweight family polymorphism
Journal of Object Technology, 2008
DOI: 10.5381/jot.2008.7.5.a32007Proving Noninterference by a Fully Complete Translation to the Simply Typed λ-Calculus
Advances in Computer Science - ASIAN 2006. Secure Software and Related Issues, 2007
DOI: 10.1007/978-3-540-77505-8_24Variant path types for scalable extensibility
Proceedings of the 22nd annual ACM SIGPLAN conference on Object oriented programming systems and applications - OOPSLA '07, 2007
DOI: 10.1145/1297027.1297037An Algorithm to Decide Conformance of Resource Usage to Specification for Resource Usage Verification
情報処理学会論文誌. プログラミング, 2007
Union types for object-oriented programming
Journal of Object Technology, 2007
Deriving compilers and virtual machines for a multi-level language
Proceedings of Asian Symposium on Programming Languages and Systems (APLAS 2007), 2007
2006Variant parametric types: A flexible subtyping scheme for generics
ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2006
DOI: 10.1145/1152649.1152650様相型に基づく情報流解析における非干渉性の論理関係による一般化とその証明
第8回プログラミングおよびプログラミング言語ワークショップ(PPL2006)論文集, 2006
Resource usage analysis for a functional language with exceptions
Proceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, 2006
DOI: 10.1145/1111542.1111550A modal type system for multi-level generating extensions with persistent code
PPDP'06 - Proceedings of the Eight ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming, 2006
2005Resource usage analysis
ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2005
DOI: 10.1145/1057387.1057390例外機構を備えた言語のための資源使用法解析
第7回プログラミングおよびプログラミング言語ワークショップ(PPL2005)論文集, 2005
メタプログラミングのための時相論理に基づく型付λ計算
第7回プログラミングおよびプログラミング言語ワークショップ(PPL2005)論文集, 2005
2004Generics・Union 型を導入したオブジェクト指向計算体系
第6回プログラミングおよびプログラミング言語ワークショップ(PPL2004)論文集, 2004
A generic type system for the Pi-calculus
THEORETICAL COMPUTER SCIENCE, 2004
DOI: 10.1016/S0304-3975(03)00325-6A modal foundation for secure information flow
Proceedings of the Workshop on Foundations of Computer Security (FCS'04), number 31 in Turku Centre for Computer Science General Publication,187-203, 2004
2003Union 型を導入したオブジェクト指向計算体系
日本ソフトウェア科学会第20回大会論文集, 2003
擬似引用を持つ型付計算体系λq
第5回プログラミングおよびプログラミング言語ワークショップ(PPL2003)論文集, 2003
2002On variance-based subtyping for parametric types
ECOOP 2002 - OBJECT-ORIENTED PROGRAMMING, 2002
2001Featherweight Java: A minimal core calculus for Java and GJ
ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2001
DOI: 10.1145/503502.503505A Recipe for Raw Types
Proceedings of the International Workshop on Foundations of Object-Oriented Languages (FOOL8), 2001
2000Garbage Collection Based on a Linear Type System
Proceedings of the 3rd ACM SIGPLAN Wokshop on Types in Compilation (TIC'00), 2000
Type reconstruction for linear pi-calculus with I/O subtyping
INFORMATION AND COMPUTATION, 2000
DOI: 10.1006/inco.2000.28721999Featherweight Java - A minimal core calculus for Java and GJ
Proceedings of ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA'99), 1999
1997Type-based Analysis of Communication for Concurrent Programming Languages
Proceedings of the Fourth International Static Analysis Symposium, 1997
Automatic Memory Management Based on Program Transformation using Ownerships
Proceedings of Asian Symposium on Programming Languages and Systems (APLAS), 2014
DOI: 10.1007/978-3-319-12736-1_4
Proceedings of Asian Symposium on Programming Languages and Systems (APLAS), 2014
DOI: 10.1007/978-3-319-12736-1_4
Formalization of Featherweight Java and Featherweight GJ by using weak HOAS on Coq
日本ソフトウェア科学会大会論文集, 2014
日本ソフトウェア科学会大会論文集, 2014
Automatic Synthesis of Combiners in the MapReduce Framework: An Approach with Right Inverse
Proceedings of International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR), 2014
Proceedings of International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR), 2014
On-Demand Layer Activation for Type-Safe Deactivation
International Workshop on Context-Oriented Programming, COP'14 - Co-located with the 26th European Conference on Object-Oriented Programming, ECOOP'14, 2014
DOI: 10.1145/2637066.2637070
International Workshop on Context-Oriented Programming, COP'14 - Co-located with the 26th European Conference on Object-Oriented Programming, ECOOP'14, 2014
DOI: 10.1145/2637066.2637070
Towards Type-Safe JCop: A type system for layer inheritance and first-class layers
International Workshop on Context-Oriented Programming, COP'12 - Co-located with the 26th European Conference on Object-Oriented Programming, ECOOP'14, 2014
DOI: 10.1145/2637066.2637073
International Workshop on Context-Oriented Programming, COP'12 - Co-located with the 26th European Conference on Object-Oriented Programming, ECOOP'14, 2014
DOI: 10.1145/2637066.2637073
On Cross-Stage Persistence in Multi-Stage Programming
Proceedings of Intl. Symposium on Functional and Logic Programming (FLOPS2014), 2014
DOI: 10.1007/978-3-319-07151-0_7
Proceedings of Intl. Symposium on Functional and Logic Programming (FLOPS2014), 2014
DOI: 10.1007/978-3-319-07151-0_7
顕在的契約計算のための代数的データ型
第16回プログラミングおよびプログラミング言語ワークショップ(PPL2014)論文集, 2014
第16回プログラミングおよびプログラミング言語ワークショップ(PPL2014)論文集, 2014
Formal Verification of CPS : A Nonstandard Analysis Approach
Journal of The Society of Instrument and Control Engineers, 2014
DOI: 10.11499/sicejl.53.1080
Journal of The Society of Instrument and Control Engineers, 2014
DOI: 10.11499/sicejl.53.1080
Practical Implementation Techniques of Ambient Calculus in Conventional Dynamic Languages
29th Symposium on Applied Computing (SAC 2014), 2014
29th Symposium on Applied Computing (SAC 2014), 2014
JVMバイトコードへの低水準操作を簡潔に記述可能なマクロシステム
情報処理学会 第55回プログラミング・シンポジウム, 2014
情報処理学会 第55回プログラミング・シンポジウム, 2014
A Hoare Logic for SIMT Programs
Proceedings of Asian Symposium on Programming Languages and Systems (APLAS2013), 2013
DOI: 10.1007/978-3-319-03542-0_5
Proceedings of Asian Symposium on Programming Languages and Systems (APLAS2013), 2013
DOI: 10.1007/978-3-319-03542-0_5
多段階計算λ▹のための越段階埋込
日本ソフトウェア科学会第30回大会論文集, 2013
日本ソフトウェア科学会第30回大会論文集, 2013
Layer Refinement in L
並列/分散/協調処理に関するサマー・ワークショップ (SWoPP), 2013
並列/分散/協調処理に関するサマー・ワークショップ (SWoPP), 2013
L: Context-oriented programming with only layers
Proceedings of the 5th International Workshop on Context-Oriented Programming, COP 2013, 2013
DOI: 10.1145/2489793.2489797
Proceedings of the 5th International Workshop on Context-Oriented Programming, COP 2013, 2013
DOI: 10.1145/2489793.2489797
Model-Checking Higher-Order Programs with Recursive Types
Proceedings of European Symposium on Programming (ESOP2013), 2013
DOI: 10.1007/978-3-642-37036-6_24
Proceedings of European Symposium on Programming (ESOP2013), 2013
DOI: 10.1007/978-3-642-37036-6_24
Hyperstream processing systems: Nonstandard modeling of continuous-time signals
Conference Record of the Annual ACM Symposium on Principles of Programming Languages, 2013
DOI: 10.1145/2429069.2429120
Conference Record of the Annual ACM Symposium on Principles of Programming Languages, 2013
DOI: 10.1145/2429069.2429120
Safeアンビエントに基づく分散アプリケーション開発用Lisp環境
コンピュータソフトウェア, 2013
コンピュータソフトウェア, 2013
L-Closureの呼び出しコストの削減
情報処理学会論文誌 プログラミング, 2013
情報処理学会論文誌 プログラミング, 2013
2012Type-based safe resource deallocation for shared-memory concurrency
Proceedings of Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), 2012
DOI: 10.1145/2398857.2384618A Type System for Dynamic Layer Composition
Proceedings of the International Workshop on Foundations of Object-Oriented Languages (FOOL2012), 2012
顕在的契約計算におけるアップキャスト除去
第14回プログラミングおよびプログラミング言語ワークショップ, 2012
Exercises in Nonstandard Static Analysis of Hybrid Systems
24th International Conference, CAV 2012, 2012
DOI: 10.1007/978-3-642-31424-7_34SEAN: Support Tool for Detecting Rule Violations in JNI Coding
IPSJ Transactions on Programming, 2012
JNIコーディングの規則違反を検出するための支援ツールSEANの開発
情報処理学会第87回プログラミング研究会, 2012
Detecting Bugs in Android Using a Static Escape Analyzer SEAN for Native Code
10th Asian Symposium on Programming Languages and Systems (APLAS 2012), 2012
2011Constructive linear-time temporal logic: Proof systems and Kripke semantics
Information and Computation, 2011
DOI: 10.1016/j.ic.2010.09.008Systematic Derivation of a λ○ Virtual Machine with Low-Level Code Generation by using Fusion Transformation
日本ソフトウェア科学会第28回大会論文集, 2011
Polymorphic Contracts
Proceedings of European Symposium on Programming (ESOP2011), 2011
DOI: 10.1007/978-3-642-19718-5_2Special track on object-oriented languages and systems
Proceedings of the ACM Symposium on Applied Computing, 2011
Gradual typing for generics
Proceedings of the 2011 ACM international conference on Object oriented programming systems languages and applications - OOPSLA '11, 2011
DOI: 10.1145/2048066.2048114ContextFJ: A minimal core calculus for context-oriented programming
Proceedings of the 10th International Workshop on Foundations of Aspect-Oriented Languages, FOAL 2011, 2011
DOI: 10.1145/1960510.1960515Ordered Types for Stream Processing of Tree-Structured Data
Information and Media Technologies, 2011
DOI: 10.11185/imt.6.385Programming with Infinitesimals: A WHILE-Language for Hybrid System Modeling
Automata, Languages and Programming, ICALP, Pt II, 2011
DOI: 10.1007/978-3-642-22012-8_312010A Logical Foundation for Environment Classifiers
Logical Methods in Computer Science, 2010
DOI: 10.2168/lmcs-6(4:8)2010Mostly modular compilation of crosscutting concerns by contextual predicate dispatch
Proceedings of Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), 2010
DOI: 10.1145/1932682.1869503Type relaxed weaving
AOSD.10 - 9th International Conference on Aspect-Oriented Software Development, 2010
DOI: 10.1145/1739230.17392452009Matching ThisType to subtyping
Proceedings of the ACM Symposium on Applied Computing, 2009
DOI: 10.1145/1529282.1529699Self type constructors
Proceeding of the 24th ACM SIGPLAN conference on Object oriented programming systems languages and applications - OOPSLA 09, 2009
DOI: 10.1145/1640089.1640109Towards gradual typing for generics
Proceedings for the 1st Workshop on Script to Program Evolution, STOP'09 in Conjunction with European Conference on Object-Oriented Programming, ECOOP'09, 2009
DOI: 10.1145/1570506.15705092008Proving Noninterference by a Fully Complete Translation to the Simply Typed lambda-calculus
Logical Methods in Computer Science, 2008
DOI: 10.2168/lmcs-4(3:10)2008On Constructive Linear-Time Temporal Logic
Proceedings of the Workshop on Intuitionistil Modal Logic and Applications (IMLA'08), 2008
Lightweight family polymorphism
Journal of Functional Programming, 2008
DOI: 10.1017/s0956796807006405Featherweight Java のための漸進的型付け
第10回プログラミングおよびプログラミング言語ワークショップ(PPL2008)論文集, 2008
文脈依存資源使用解析のための型システム
第10回プログラミングおよびプログラミング言語ワークショップ(PPL2008)論文集, 2008
The essence of lightweight family polymorphism
Journal of Object Technology, 2008
DOI: 10.5381/jot.2008.7.5.a32007Proving Noninterference by a Fully Complete Translation to the Simply Typed λ-Calculus
Advances in Computer Science - ASIAN 2006. Secure Software and Related Issues, 2007
DOI: 10.1007/978-3-540-77505-8_24Variant path types for scalable extensibility
Proceedings of the 22nd annual ACM SIGPLAN conference on Object oriented programming systems and applications - OOPSLA '07, 2007
DOI: 10.1145/1297027.1297037An Algorithm to Decide Conformance of Resource Usage to Specification for Resource Usage Verification
情報処理学会論文誌. プログラミング, 2007
Union types for object-oriented programming
Journal of Object Technology, 2007
Deriving compilers and virtual machines for a multi-level language
Proceedings of Asian Symposium on Programming Languages and Systems (APLAS 2007), 2007
2006Variant parametric types: A flexible subtyping scheme for generics
ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2006
DOI: 10.1145/1152649.1152650様相型に基づく情報流解析における非干渉性の論理関係による一般化とその証明
第8回プログラミングおよびプログラミング言語ワークショップ(PPL2006)論文集, 2006
Resource usage analysis for a functional language with exceptions
Proceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, 2006
DOI: 10.1145/1111542.1111550A modal type system for multi-level generating extensions with persistent code
PPDP'06 - Proceedings of the Eight ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming, 2006
2005Resource usage analysis
ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2005
DOI: 10.1145/1057387.1057390例外機構を備えた言語のための資源使用法解析
第7回プログラミングおよびプログラミング言語ワークショップ(PPL2005)論文集, 2005
メタプログラミングのための時相論理に基づく型付λ計算
第7回プログラミングおよびプログラミング言語ワークショップ(PPL2005)論文集, 2005
2004Generics・Union 型を導入したオブジェクト指向計算体系
第6回プログラミングおよびプログラミング言語ワークショップ(PPL2004)論文集, 2004
A generic type system for the Pi-calculus
THEORETICAL COMPUTER SCIENCE, 2004
DOI: 10.1016/S0304-3975(03)00325-6A modal foundation for secure information flow
Proceedings of the Workshop on Foundations of Computer Security (FCS'04), number 31 in Turku Centre for Computer Science General Publication,187-203, 2004
2003Union 型を導入したオブジェクト指向計算体系
日本ソフトウェア科学会第20回大会論文集, 2003
擬似引用を持つ型付計算体系λq
第5回プログラミングおよびプログラミング言語ワークショップ(PPL2003)論文集, 2003
2002On variance-based subtyping for parametric types
ECOOP 2002 - OBJECT-ORIENTED PROGRAMMING, 2002
2001Featherweight Java: A minimal core calculus for Java and GJ
ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2001
DOI: 10.1145/503502.503505A Recipe for Raw Types
Proceedings of the International Workshop on Foundations of Object-Oriented Languages (FOOL8), 2001
2000Garbage Collection Based on a Linear Type System
Proceedings of the 3rd ACM SIGPLAN Wokshop on Types in Compilation (TIC'00), 2000
Type reconstruction for linear pi-calculus with I/O subtyping
INFORMATION AND COMPUTATION, 2000
DOI: 10.1006/inco.2000.28721999Featherweight Java - A minimal core calculus for Java and GJ
Proceedings of ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA'99), 1999
1997Type-based Analysis of Communication for Concurrent Programming Languages
Proceedings of the Fourth International Static Analysis Symposium, 1997
Type-based safe resource deallocation for shared-memory concurrency
Proceedings of Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), 2012
DOI: 10.1145/2398857.2384618
Proceedings of Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), 2012
DOI: 10.1145/2398857.2384618
A Type System for Dynamic Layer Composition
Proceedings of the International Workshop on Foundations of Object-Oriented Languages (FOOL2012), 2012
Proceedings of the International Workshop on Foundations of Object-Oriented Languages (FOOL2012), 2012
顕在的契約計算におけるアップキャスト除去
第14回プログラミングおよびプログラミング言語ワークショップ, 2012
第14回プログラミングおよびプログラミング言語ワークショップ, 2012
Exercises in Nonstandard Static Analysis of Hybrid Systems
24th International Conference, CAV 2012, 2012
DOI: 10.1007/978-3-642-31424-7_34
24th International Conference, CAV 2012, 2012
DOI: 10.1007/978-3-642-31424-7_34
SEAN: Support Tool for Detecting Rule Violations in JNI Coding
IPSJ Transactions on Programming, 2012
IPSJ Transactions on Programming, 2012
JNIコーディングの規則違反を検出するための支援ツールSEANの開発
情報処理学会第87回プログラミング研究会, 2012
情報処理学会第87回プログラミング研究会, 2012
Detecting Bugs in Android Using a Static Escape Analyzer SEAN for Native Code
10th Asian Symposium on Programming Languages and Systems (APLAS 2012), 2012
10th Asian Symposium on Programming Languages and Systems (APLAS 2012), 2012
Constructive linear-time temporal logic: Proof systems and Kripke semantics
Information and Computation, 2011
DOI: 10.1016/j.ic.2010.09.008
Information and Computation, 2011
DOI: 10.1016/j.ic.2010.09.008
Systematic Derivation of a λ○ Virtual Machine with Low-Level Code Generation by using Fusion Transformation
日本ソフトウェア科学会第28回大会論文集, 2011
日本ソフトウェア科学会第28回大会論文集, 2011
Polymorphic Contracts
Proceedings of European Symposium on Programming (ESOP2011), 2011
DOI: 10.1007/978-3-642-19718-5_2
Proceedings of European Symposium on Programming (ESOP2011), 2011
DOI: 10.1007/978-3-642-19718-5_2
Special track on object-oriented languages and systems
Proceedings of the ACM Symposium on Applied Computing, 2011
Proceedings of the ACM Symposium on Applied Computing, 2011
Gradual typing for generics
Proceedings of the 2011 ACM international conference on Object oriented programming systems languages and applications - OOPSLA '11, 2011
DOI: 10.1145/2048066.2048114
Proceedings of the 2011 ACM international conference on Object oriented programming systems languages and applications - OOPSLA '11, 2011
DOI: 10.1145/2048066.2048114
ContextFJ: A minimal core calculus for context-oriented programming
Proceedings of the 10th International Workshop on Foundations of Aspect-Oriented Languages, FOAL 2011, 2011
DOI: 10.1145/1960510.1960515
Proceedings of the 10th International Workshop on Foundations of Aspect-Oriented Languages, FOAL 2011, 2011
DOI: 10.1145/1960510.1960515
Ordered Types for Stream Processing of Tree-Structured Data
Information and Media Technologies, 2011
DOI: 10.11185/imt.6.385
Information and Media Technologies, 2011
DOI: 10.11185/imt.6.385
Programming with Infinitesimals: A WHILE-Language for Hybrid System Modeling
Automata, Languages and Programming, ICALP, Pt II, 2011
DOI: 10.1007/978-3-642-22012-8_31
Automata, Languages and Programming, ICALP, Pt II, 2011
DOI: 10.1007/978-3-642-22012-8_31
2010A Logical Foundation for Environment Classifiers
Logical Methods in Computer Science, 2010
DOI: 10.2168/lmcs-6(4:8)2010Mostly modular compilation of crosscutting concerns by contextual predicate dispatch
Proceedings of Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), 2010
DOI: 10.1145/1932682.1869503Type relaxed weaving
AOSD.10 - 9th International Conference on Aspect-Oriented Software Development, 2010
DOI: 10.1145/1739230.17392452009Matching ThisType to subtyping
Proceedings of the ACM Symposium on Applied Computing, 2009
DOI: 10.1145/1529282.1529699Self type constructors
Proceeding of the 24th ACM SIGPLAN conference on Object oriented programming systems languages and applications - OOPSLA 09, 2009
DOI: 10.1145/1640089.1640109Towards gradual typing for generics
Proceedings for the 1st Workshop on Script to Program Evolution, STOP'09 in Conjunction with European Conference on Object-Oriented Programming, ECOOP'09, 2009
DOI: 10.1145/1570506.15705092008Proving Noninterference by a Fully Complete Translation to the Simply Typed lambda-calculus
Logical Methods in Computer Science, 2008
DOI: 10.2168/lmcs-4(3:10)2008On Constructive Linear-Time Temporal Logic
Proceedings of the Workshop on Intuitionistil Modal Logic and Applications (IMLA'08), 2008
Lightweight family polymorphism
Journal of Functional Programming, 2008
DOI: 10.1017/s0956796807006405Featherweight Java のための漸進的型付け
第10回プログラミングおよびプログラミング言語ワークショップ(PPL2008)論文集, 2008
文脈依存資源使用解析のための型システム
第10回プログラミングおよびプログラミング言語ワークショップ(PPL2008)論文集, 2008
The essence of lightweight family polymorphism
Journal of Object Technology, 2008
DOI: 10.5381/jot.2008.7.5.a32007Proving Noninterference by a Fully Complete Translation to the Simply Typed λ-Calculus
Advances in Computer Science - ASIAN 2006. Secure Software and Related Issues, 2007
DOI: 10.1007/978-3-540-77505-8_24Variant path types for scalable extensibility
Proceedings of the 22nd annual ACM SIGPLAN conference on Object oriented programming systems and applications - OOPSLA '07, 2007
DOI: 10.1145/1297027.1297037An Algorithm to Decide Conformance of Resource Usage to Specification for Resource Usage Verification
情報処理学会論文誌. プログラミング, 2007
Union types for object-oriented programming
Journal of Object Technology, 2007
Deriving compilers and virtual machines for a multi-level language
Proceedings of Asian Symposium on Programming Languages and Systems (APLAS 2007), 2007
2006Variant parametric types: A flexible subtyping scheme for generics
ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2006
DOI: 10.1145/1152649.1152650様相型に基づく情報流解析における非干渉性の論理関係による一般化とその証明
第8回プログラミングおよびプログラミング言語ワークショップ(PPL2006)論文集, 2006
Resource usage analysis for a functional language with exceptions
Proceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, 2006
DOI: 10.1145/1111542.1111550A modal type system for multi-level generating extensions with persistent code
PPDP'06 - Proceedings of the Eight ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming, 2006
2005Resource usage analysis
ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2005
DOI: 10.1145/1057387.1057390例外機構を備えた言語のための資源使用法解析
第7回プログラミングおよびプログラミング言語ワークショップ(PPL2005)論文集, 2005
メタプログラミングのための時相論理に基づく型付λ計算
第7回プログラミングおよびプログラミング言語ワークショップ(PPL2005)論文集, 2005
2004Generics・Union 型を導入したオブジェクト指向計算体系
第6回プログラミングおよびプログラミング言語ワークショップ(PPL2004)論文集, 2004
A generic type system for the Pi-calculus
THEORETICAL COMPUTER SCIENCE, 2004
DOI: 10.1016/S0304-3975(03)00325-6A modal foundation for secure information flow
Proceedings of the Workshop on Foundations of Computer Security (FCS'04), number 31 in Turku Centre for Computer Science General Publication,187-203, 2004
2003Union 型を導入したオブジェクト指向計算体系
日本ソフトウェア科学会第20回大会論文集, 2003
擬似引用を持つ型付計算体系λq
第5回プログラミングおよびプログラミング言語ワークショップ(PPL2003)論文集, 2003
2002On variance-based subtyping for parametric types
ECOOP 2002 - OBJECT-ORIENTED PROGRAMMING, 2002
2001Featherweight Java: A minimal core calculus for Java and GJ
ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2001
DOI: 10.1145/503502.503505A Recipe for Raw Types
Proceedings of the International Workshop on Foundations of Object-Oriented Languages (FOOL8), 2001
2000Garbage Collection Based on a Linear Type System
Proceedings of the 3rd ACM SIGPLAN Wokshop on Types in Compilation (TIC'00), 2000
Type reconstruction for linear pi-calculus with I/O subtyping
INFORMATION AND COMPUTATION, 2000
DOI: 10.1006/inco.2000.28721999Featherweight Java - A minimal core calculus for Java and GJ
Proceedings of ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA'99), 1999
1997Type-based Analysis of Communication for Concurrent Programming Languages
Proceedings of the Fourth International Static Analysis Symposium, 1997
A Logical Foundation for Environment Classifiers
Logical Methods in Computer Science, 2010
DOI: 10.2168/lmcs-6(4:8)2010
Logical Methods in Computer Science, 2010
DOI: 10.2168/lmcs-6(4:8)2010
Mostly modular compilation of crosscutting concerns by contextual predicate dispatch
Proceedings of Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), 2010
DOI: 10.1145/1932682.1869503
Proceedings of Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), 2010
DOI: 10.1145/1932682.1869503
Type relaxed weaving
AOSD.10 - 9th International Conference on Aspect-Oriented Software Development, 2010
DOI: 10.1145/1739230.1739245
AOSD.10 - 9th International Conference on Aspect-Oriented Software Development, 2010
DOI: 10.1145/1739230.1739245
Matching ThisType to subtyping
Proceedings of the ACM Symposium on Applied Computing, 2009
DOI: 10.1145/1529282.1529699
Proceedings of the ACM Symposium on Applied Computing, 2009
DOI: 10.1145/1529282.1529699
Self type constructors
Proceeding of the 24th ACM SIGPLAN conference on Object oriented programming systems languages and applications - OOPSLA 09, 2009
DOI: 10.1145/1640089.1640109
Proceeding of the 24th ACM SIGPLAN conference on Object oriented programming systems languages and applications - OOPSLA 09, 2009
DOI: 10.1145/1640089.1640109
Towards gradual typing for generics
Proceedings for the 1st Workshop on Script to Program Evolution, STOP'09 in Conjunction with European Conference on Object-Oriented Programming, ECOOP'09, 2009
DOI: 10.1145/1570506.1570509
Proceedings for the 1st Workshop on Script to Program Evolution, STOP'09 in Conjunction with European Conference on Object-Oriented Programming, ECOOP'09, 2009
DOI: 10.1145/1570506.1570509
2008Proving Noninterference by a Fully Complete Translation to the Simply Typed lambda-calculus
Logical Methods in Computer Science, 2008
DOI: 10.2168/lmcs-4(3:10)2008On Constructive Linear-Time Temporal Logic
Proceedings of the Workshop on Intuitionistil Modal Logic and Applications (IMLA'08), 2008
Lightweight family polymorphism
Journal of Functional Programming, 2008
DOI: 10.1017/s0956796807006405Featherweight Java のための漸進的型付け
第10回プログラミングおよびプログラミング言語ワークショップ(PPL2008)論文集, 2008
文脈依存資源使用解析のための型システム
第10回プログラミングおよびプログラミング言語ワークショップ(PPL2008)論文集, 2008
The essence of lightweight family polymorphism
Journal of Object Technology, 2008
DOI: 10.5381/jot.2008.7.5.a32007Proving Noninterference by a Fully Complete Translation to the Simply Typed λ-Calculus
Advances in Computer Science - ASIAN 2006. Secure Software and Related Issues, 2007
DOI: 10.1007/978-3-540-77505-8_24Variant path types for scalable extensibility
Proceedings of the 22nd annual ACM SIGPLAN conference on Object oriented programming systems and applications - OOPSLA '07, 2007
DOI: 10.1145/1297027.1297037An Algorithm to Decide Conformance of Resource Usage to Specification for Resource Usage Verification
情報処理学会論文誌. プログラミング, 2007
Union types for object-oriented programming
Journal of Object Technology, 2007
Deriving compilers and virtual machines for a multi-level language
Proceedings of Asian Symposium on Programming Languages and Systems (APLAS 2007), 2007
2006Variant parametric types: A flexible subtyping scheme for generics
ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2006
DOI: 10.1145/1152649.1152650様相型に基づく情報流解析における非干渉性の論理関係による一般化とその証明
第8回プログラミングおよびプログラミング言語ワークショップ(PPL2006)論文集, 2006
Resource usage analysis for a functional language with exceptions
Proceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, 2006
DOI: 10.1145/1111542.1111550A modal type system for multi-level generating extensions with persistent code
PPDP'06 - Proceedings of the Eight ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming, 2006
2005Resource usage analysis
ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2005
DOI: 10.1145/1057387.1057390例外機構を備えた言語のための資源使用法解析
第7回プログラミングおよびプログラミング言語ワークショップ(PPL2005)論文集, 2005
メタプログラミングのための時相論理に基づく型付λ計算
第7回プログラミングおよびプログラミング言語ワークショップ(PPL2005)論文集, 2005
2004Generics・Union 型を導入したオブジェクト指向計算体系
第6回プログラミングおよびプログラミング言語ワークショップ(PPL2004)論文集, 2004
A generic type system for the Pi-calculus
THEORETICAL COMPUTER SCIENCE, 2004
DOI: 10.1016/S0304-3975(03)00325-6A modal foundation for secure information flow
Proceedings of the Workshop on Foundations of Computer Security (FCS'04), number 31 in Turku Centre for Computer Science General Publication,187-203, 2004
2003Union 型を導入したオブジェクト指向計算体系
日本ソフトウェア科学会第20回大会論文集, 2003
擬似引用を持つ型付計算体系λq
第5回プログラミングおよびプログラミング言語ワークショップ(PPL2003)論文集, 2003
2002On variance-based subtyping for parametric types
ECOOP 2002 - OBJECT-ORIENTED PROGRAMMING, 2002
2001Featherweight Java: A minimal core calculus for Java and GJ
ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2001
DOI: 10.1145/503502.503505A Recipe for Raw Types
Proceedings of the International Workshop on Foundations of Object-Oriented Languages (FOOL8), 2001
2000Garbage Collection Based on a Linear Type System
Proceedings of the 3rd ACM SIGPLAN Wokshop on Types in Compilation (TIC'00), 2000
Type reconstruction for linear pi-calculus with I/O subtyping
INFORMATION AND COMPUTATION, 2000
DOI: 10.1006/inco.2000.28721999Featherweight Java - A minimal core calculus for Java and GJ
Proceedings of ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA'99), 1999
1997Type-based Analysis of Communication for Concurrent Programming Languages
Proceedings of the Fourth International Static Analysis Symposium, 1997
Proving Noninterference by a Fully Complete Translation to the Simply Typed lambda-calculus
Logical Methods in Computer Science, 2008
DOI: 10.2168/lmcs-4(3:10)2008
Logical Methods in Computer Science, 2008
DOI: 10.2168/lmcs-4(3:10)2008
On Constructive Linear-Time Temporal Logic
Proceedings of the Workshop on Intuitionistil Modal Logic and Applications (IMLA'08), 2008
Proceedings of the Workshop on Intuitionistil Modal Logic and Applications (IMLA'08), 2008
Lightweight family polymorphism
Journal of Functional Programming, 2008
DOI: 10.1017/s0956796807006405
Journal of Functional Programming, 2008
DOI: 10.1017/s0956796807006405
Featherweight Java のための漸進的型付け
第10回プログラミングおよびプログラミング言語ワークショップ(PPL2008)論文集, 2008
第10回プログラミングおよびプログラミング言語ワークショップ(PPL2008)論文集, 2008
文脈依存資源使用解析のための型システム
第10回プログラミングおよびプログラミング言語ワークショップ(PPL2008)論文集, 2008
第10回プログラミングおよびプログラミング言語ワークショップ(PPL2008)論文集, 2008
The essence of lightweight family polymorphism
Journal of Object Technology, 2008
DOI: 10.5381/jot.2008.7.5.a3
Journal of Object Technology, 2008
DOI: 10.5381/jot.2008.7.5.a3
Proving Noninterference by a Fully Complete Translation to the Simply Typed λ-Calculus
Advances in Computer Science - ASIAN 2006. Secure Software and Related Issues, 2007
DOI: 10.1007/978-3-540-77505-8_24
Advances in Computer Science - ASIAN 2006. Secure Software and Related Issues, 2007
DOI: 10.1007/978-3-540-77505-8_24
Variant path types for scalable extensibility
Proceedings of the 22nd annual ACM SIGPLAN conference on Object oriented programming systems and applications - OOPSLA '07, 2007
DOI: 10.1145/1297027.1297037
Proceedings of the 22nd annual ACM SIGPLAN conference on Object oriented programming systems and applications - OOPSLA '07, 2007
DOI: 10.1145/1297027.1297037
An Algorithm to Decide Conformance of Resource Usage to Specification for Resource Usage Verification
情報処理学会論文誌. プログラミング, 2007
情報処理学会論文誌. プログラミング, 2007
Union types for object-oriented programming
Journal of Object Technology, 2007
Journal of Object Technology, 2007
Deriving compilers and virtual machines for a multi-level language
Proceedings of Asian Symposium on Programming Languages and Systems (APLAS 2007), 2007
Proceedings of Asian Symposium on Programming Languages and Systems (APLAS 2007), 2007
2006Variant parametric types: A flexible subtyping scheme for generics
ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2006
DOI: 10.1145/1152649.1152650様相型に基づく情報流解析における非干渉性の論理関係による一般化とその証明
第8回プログラミングおよびプログラミング言語ワークショップ(PPL2006)論文集, 2006
Resource usage analysis for a functional language with exceptions
Proceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, 2006
DOI: 10.1145/1111542.1111550A modal type system for multi-level generating extensions with persistent code
PPDP'06 - Proceedings of the Eight ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming, 2006
2005Resource usage analysis
ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2005
DOI: 10.1145/1057387.1057390例外機構を備えた言語のための資源使用法解析
第7回プログラミングおよびプログラミング言語ワークショップ(PPL2005)論文集, 2005
メタプログラミングのための時相論理に基づく型付λ計算
第7回プログラミングおよびプログラミング言語ワークショップ(PPL2005)論文集, 2005
2004Generics・Union 型を導入したオブジェクト指向計算体系
第6回プログラミングおよびプログラミング言語ワークショップ(PPL2004)論文集, 2004
A generic type system for the Pi-calculus
THEORETICAL COMPUTER SCIENCE, 2004
DOI: 10.1016/S0304-3975(03)00325-6A modal foundation for secure information flow
Proceedings of the Workshop on Foundations of Computer Security (FCS'04), number 31 in Turku Centre for Computer Science General Publication,187-203, 2004
2003Union 型を導入したオブジェクト指向計算体系
日本ソフトウェア科学会第20回大会論文集, 2003
擬似引用を持つ型付計算体系λq
第5回プログラミングおよびプログラミング言語ワークショップ(PPL2003)論文集, 2003
2002On variance-based subtyping for parametric types
ECOOP 2002 - OBJECT-ORIENTED PROGRAMMING, 2002
2001Featherweight Java: A minimal core calculus for Java and GJ
ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2001
DOI: 10.1145/503502.503505A Recipe for Raw Types
Proceedings of the International Workshop on Foundations of Object-Oriented Languages (FOOL8), 2001
2000Garbage Collection Based on a Linear Type System
Proceedings of the 3rd ACM SIGPLAN Wokshop on Types in Compilation (TIC'00), 2000
Type reconstruction for linear pi-calculus with I/O subtyping
INFORMATION AND COMPUTATION, 2000
DOI: 10.1006/inco.2000.28721999Featherweight Java - A minimal core calculus for Java and GJ
Proceedings of ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA'99), 1999
1997Type-based Analysis of Communication for Concurrent Programming Languages
Proceedings of the Fourth International Static Analysis Symposium, 1997
Variant parametric types: A flexible subtyping scheme for generics
ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2006
DOI: 10.1145/1152649.1152650
ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2006
DOI: 10.1145/1152649.1152650
様相型に基づく情報流解析における非干渉性の論理関係による一般化とその証明
第8回プログラミングおよびプログラミング言語ワークショップ(PPL2006)論文集, 2006
第8回プログラミングおよびプログラミング言語ワークショップ(PPL2006)論文集, 2006
Resource usage analysis for a functional language with exceptions
Proceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, 2006
DOI: 10.1145/1111542.1111550
Proceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, 2006
DOI: 10.1145/1111542.1111550
A modal type system for multi-level generating extensions with persistent code
PPDP'06 - Proceedings of the Eight ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming, 2006
PPDP'06 - Proceedings of the Eight ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming, 2006
Resource usage analysis
ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2005
DOI: 10.1145/1057387.1057390
ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2005
DOI: 10.1145/1057387.1057390
例外機構を備えた言語のための資源使用法解析
第7回プログラミングおよびプログラミング言語ワークショップ(PPL2005)論文集, 2005
第7回プログラミングおよびプログラミング言語ワークショップ(PPL2005)論文集, 2005
メタプログラミングのための時相論理に基づく型付λ計算
第7回プログラミングおよびプログラミング言語ワークショップ(PPL2005)論文集, 2005
第7回プログラミングおよびプログラミング言語ワークショップ(PPL2005)論文集, 2005
2004Generics・Union 型を導入したオブジェクト指向計算体系
第6回プログラミングおよびプログラミング言語ワークショップ(PPL2004)論文集, 2004
A generic type system for the Pi-calculus
THEORETICAL COMPUTER SCIENCE, 2004
DOI: 10.1016/S0304-3975(03)00325-6A modal foundation for secure information flow
Proceedings of the Workshop on Foundations of Computer Security (FCS'04), number 31 in Turku Centre for Computer Science General Publication,187-203, 2004
2003Union 型を導入したオブジェクト指向計算体系
日本ソフトウェア科学会第20回大会論文集, 2003
擬似引用を持つ型付計算体系λq
第5回プログラミングおよびプログラミング言語ワークショップ(PPL2003)論文集, 2003
2002On variance-based subtyping for parametric types
ECOOP 2002 - OBJECT-ORIENTED PROGRAMMING, 2002
2001Featherweight Java: A minimal core calculus for Java and GJ
ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2001
DOI: 10.1145/503502.503505A Recipe for Raw Types
Proceedings of the International Workshop on Foundations of Object-Oriented Languages (FOOL8), 2001
2000Garbage Collection Based on a Linear Type System
Proceedings of the 3rd ACM SIGPLAN Wokshop on Types in Compilation (TIC'00), 2000
Type reconstruction for linear pi-calculus with I/O subtyping
INFORMATION AND COMPUTATION, 2000
DOI: 10.1006/inco.2000.28721999Featherweight Java - A minimal core calculus for Java and GJ
Proceedings of ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA'99), 1999
1997Type-based Analysis of Communication for Concurrent Programming Languages
Proceedings of the Fourth International Static Analysis Symposium, 1997
Generics・Union 型を導入したオブジェクト指向計算体系
第6回プログラミングおよびプログラミング言語ワークショップ(PPL2004)論文集, 2004
第6回プログラミングおよびプログラミング言語ワークショップ(PPL2004)論文集, 2004
A generic type system for the Pi-calculus
THEORETICAL COMPUTER SCIENCE, 2004
DOI: 10.1016/S0304-3975(03)00325-6
THEORETICAL COMPUTER SCIENCE, 2004
DOI: 10.1016/S0304-3975(03)00325-6
A modal foundation for secure information flow
Proceedings of the Workshop on Foundations of Computer Security (FCS'04), number 31 in Turku Centre for Computer Science General Publication,187-203, 2004
Proceedings of the Workshop on Foundations of Computer Security (FCS'04), number 31 in Turku Centre for Computer Science General Publication,187-203, 2004
Union 型を導入したオブジェクト指向計算体系
日本ソフトウェア科学会第20回大会論文集, 2003
日本ソフトウェア科学会第20回大会論文集, 2003
擬似引用を持つ型付計算体系λq
第5回プログラミングおよびプログラミング言語ワークショップ(PPL2003)論文集, 2003
第5回プログラミングおよびプログラミング言語ワークショップ(PPL2003)論文集, 2003
2002On variance-based subtyping for parametric types
ECOOP 2002 - OBJECT-ORIENTED PROGRAMMING, 2002
2001Featherweight Java: A minimal core calculus for Java and GJ
ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2001
DOI: 10.1145/503502.503505A Recipe for Raw Types
Proceedings of the International Workshop on Foundations of Object-Oriented Languages (FOOL8), 2001
2000Garbage Collection Based on a Linear Type System
Proceedings of the 3rd ACM SIGPLAN Wokshop on Types in Compilation (TIC'00), 2000
Type reconstruction for linear pi-calculus with I/O subtyping
INFORMATION AND COMPUTATION, 2000
DOI: 10.1006/inco.2000.28721999Featherweight Java - A minimal core calculus for Java and GJ
Proceedings of ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA'99), 1999
1997Type-based Analysis of Communication for Concurrent Programming Languages
Proceedings of the Fourth International Static Analysis Symposium, 1997
On variance-based subtyping for parametric types
ECOOP 2002 - OBJECT-ORIENTED PROGRAMMING, 2002
ECOOP 2002 - OBJECT-ORIENTED PROGRAMMING, 2002
Featherweight Java: A minimal core calculus for Java and GJ
ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2001
DOI: 10.1145/503502.503505
ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2001
DOI: 10.1145/503502.503505
A Recipe for Raw Types
Proceedings of the International Workshop on Foundations of Object-Oriented Languages (FOOL8), 2001
Proceedings of the International Workshop on Foundations of Object-Oriented Languages (FOOL8), 2001
2000Garbage Collection Based on a Linear Type System
Proceedings of the 3rd ACM SIGPLAN Wokshop on Types in Compilation (TIC'00), 2000
Type reconstruction for linear pi-calculus with I/O subtyping
INFORMATION AND COMPUTATION, 2000
DOI: 10.1006/inco.2000.28721999Featherweight Java - A minimal core calculus for Java and GJ
Proceedings of ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA'99), 1999
1997Type-based Analysis of Communication for Concurrent Programming Languages
Proceedings of the Fourth International Static Analysis Symposium, 1997
Garbage Collection Based on a Linear Type System
Proceedings of the 3rd ACM SIGPLAN Wokshop on Types in Compilation (TIC'00), 2000
Proceedings of the 3rd ACM SIGPLAN Wokshop on Types in Compilation (TIC'00), 2000
Type reconstruction for linear pi-calculus with I/O subtyping
INFORMATION AND COMPUTATION, 2000
DOI: 10.1006/inco.2000.2872
INFORMATION AND COMPUTATION, 2000
DOI: 10.1006/inco.2000.2872
Featherweight Java - A minimal core calculus for Java and GJ
Proceedings of ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA'99), 1999
Proceedings of ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA'99), 1999
1997Type-based Analysis of Communication for Concurrent Programming Languages
Proceedings of the Fourth International Static Analysis Symposium, 1997
Type-based Analysis of Communication for Concurrent Programming Languages
Proceedings of the Fourth International Static Analysis Symposium, 1997
Proceedings of the Fourth International Static Analysis Symposium, 1997