Tatsuya Abe, Ph.D.

Contact Information

Name in Japanese:

Office:

STAIR Lab, Chiba Institute of Technology, 275-0016, Japan.

E-mail:

(λX.(abe.XaXsuya@chibaXech.ac.jp))t

(λX.(Xbe.tXtsuyX@it-chibX.Xc.jp))a

(λX.(abXt@rikXn.jp))e

(λX.(Xbet@mediX.kyoto-u.Xc.jp))a

(λX.(abe.X@aisX.go.jp))t

(λX.(abeX@is.u-Xokyo.ac.jp))t

(λX.(Xbet@kXbX.or.jp))a

Photos:

Research Interests

• Design of programming languages,
• lambda-calculus, type theory, structural proof theory,
• recursion, loop, continuation,
• concurrency, shared memory, data race detection, memory consistency model,
• message-passing, distributed system, extensional equivalence,
• program verification, theorem proving, model checking,
• soundness, completeness, termination, confluence, and congruence of bisimilarity

Papers

1. • Tatsuya Abe and Daisuke Kimura
   • Extending a Call-by-Value Calculus Based on Bilateralism with Dynamic Binding
   • Journal of Applied Logics, 10(4):511--530, 2023.
   • url: [pdf]
2. • Tatsuya Abe and Daisuke Kimura
   • A Typed Lambda-Calculus with First-Class Configurations
   • Journal of Logic and Computation, 33(7):1527--1565, 2023.
   • doi: 10.1093/logcom/exac062
3. • Tatsuya Abe and Tasuku Hiraishi
   • An Extensionally Equivalence-Ensured Language for Task Parallel Processing with Backtracking-Based Load Balancing
   • Journal of Information Processing, 29:434--448, 2021.
   • doi: 10.2197/ipsjjip.29.434
4. • Makoto Hamana, Tatsuya Abe, and Kentaro Kikuchi
   • Polymorphic Computation Systems: Theory and Practice of Confluence with Call-by-Value
   • Science of Computer Programming, 187(102322), 2020.
   • doi: 10.1016/j.scico.2019.102322
5. • Tatsuya Abe
   • A Type System for Data Independence of Loop Iterations in a Directive-Based PGAS Language
   • In Proceedings of the 16th International Conference on Managed Programming Languages and Runtimes (MPLR), pages 50--62, 2019.
   • doi: 10.1145/3357390.3361021
6. • Tatsuya Abe
   • Local Data Race Freedom with Non-Multi-Copy Atomicity
   • In Proceedings of the 25th International Symposium on Model Checking of Software (SPIN), LNCS 10869, pages 196--215, 2018.
   • doi: 10.1007/978-3-319-94111-0_12
7. • Kosuke Matsumoto, Tomoharu Ugawa, and Tatsuya Abe
   • Improvement of a Library for Model Checking under Weakly Ordered Memory Model with SPIN
   • Journal of Information Processing, 26:314--326, 2018.
   • doi: 10.2197/ipsjjip.26.314
8. • Tatsuya Abe
   • A Verifier of Directed Acyclic Graphs for Model Checking with Memory Consistency Models
   • In Proceedings of the 13th Haifa Verification Conference (HVC), LNCS 10629, pages 51--66, 2017.
   • doi: 10.1007/978-3-319-70389-3_4
9. • Tomoharu Ugawa, Tatsuya Abe, and Toshiyuki Maeda
   • Model Checking Copy Phases of Concurrent Copying Garbage Collection with Various Memory Models
   • Proceedings of the ACM on Programming Languages, 1(OOPSLA:53):1--26, 2017.
   • doi: 10.1145/3133877
10. • Tatsuya Abe, Tomoharu Ugawa, and Toshiyuki Maeda
    • Reordering Control Approaches to State Explosion in Model Checking with Memory Consistency Models
    • In Proceedings of the 9th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE), LNCS 10712, pages 170--190, 2017.
    • doi: 10.1007/978-3-319-72308-2_11
11. • Tatsuya Abe and Toshiyuki Maeda
    • A General Model Checking Framework for Various Memory Consistency Models
    • International Journal on Software Tools for Technology Transfer, 19(5):623--647, 2017.
    • doi: 10.1007/s10009-016-0429-y
12. • Tatsuya Abe and Toshiyuki Maeda
    • Concurrent Program Logic for Relaxed Memory Consistency Models with Dependencies across Loop Iterations
    • Journal of Information Processing, 25:244--255, 2017.
    • doi: 10.2197/ipsjjip.25.244
13. • Tatsuya Abe and Toshiyuki Maeda
    • Observation-Based Concurrent Program Logic for Relaxed Memory Consistency Models
    • In Proceedings of the 14th Asian Symposium on Programming Languages and Systems (APLAS), LNCS 10017, pages 63--84, 2016.
    • doi: 10.1007/978-3-319-47958-3_4
14. • Tatsuya Abe, Tomoharu Ugawa, Toshiyuki Maeda, and Kousuke Matsumoto
    • Reducing State Explosion for Software Model Checking with Relaxed Memory Consistency Models
    • In Proceedings of the 2nd Symposium on Dependable Software Engineering: Theories, Tools and Applications (SETTA), LNCS 9984, pages 118--135, 2016.
    • doi: 10.1007/978-3-319-47677-3_8
15. • Tatsuya Abe and Toshiyuki Maeda
    • Optimization of a General Model Checking Framework for Various Memory Consistency Models
    • In Proceedings of the 8th International Conference on Partitioned Global Address Space Programming Models (PGAS), pages 1--10 (online) Number 14, 2014.
    • doi: 10.1145/2676870.2676878
16. • Tatsuya Abe and Toshiyuki Maeda
    • A General Model Checking Framework for Various Memory Consistency Models
    • In Proceedings of the 19th International Workshop on High-Level Parallel Programming Models and Supportive Environments (HIPS), pages 332--341, 2014.
    • doi: 10.1109/IPDPSW.2014.47
17. • Tatsuya Abe, Toshiyuki Maeda, and Mitsuhisa Sato
    • Model Checking Stencil Computations Written in a Partitioned Global Address Space Language
    • In Proceedings of the 18th International Workshop on High-Level Parallel Programming Models and Supportive Environments (HIPS), pages 365--374, 2013.
    • doi: 10.1109/IPDPSW.2013.90
18. • Tasuku Hiraishi, Masaru Ueno, Tatsuya Abe, Motoharu Hibino, Takeshi Iwashita, and Hiroshi Nakashima
    • Xcrypt on Lisp: a Scripting System for Job Level Parallel Programming in Lisp
    • In Proceedings of International Lisp Conference (ILC), pages 107--114, 2012.
    • url: [pdf]
19. • Tatsuya Abe, Toshiyuki Maeda, and Mitsuhisa Sato
    • Model Checking with User-Definable Abstraction for Partitioned Global Address Space Languages
    • In Proceedings of the 6th International Conference on Partitioned Global Address Space Programming Models (PGAS), pages 1--10 (online), 2012.
20. • Tatsuya Abe and Mitsuhisa Sato
    • On-the-Fly Synchronization Checking for Interactive Programming in XcalableMP
    • In Proceedings of the 5th International Workshop on Parallel Programming Models and Systems Software for High-End Computing (P2S2), pages 29--37, 2012.
    • doi: 10.1109/ICPPW.2012.8
21. • Tatsuya Abe and Mitsuhisa Sato
    • Auto-Tuning of Numerical Programs by Block Multi-Color Ordering Code Generation and Job-Level Parallel Execution
    • In Proceedings of the 7th International Workshop on Automatic Performance Tuning (iWAPT), LNCS 7851, pages 404--419, 2012.
    • doi: 10.1007/978-3-642-38718-0_37
22. • Tasuku Hiraishi, Tatsuya Abe, Takeshi Iwashita, and Hiroshi Nakashima
    • Xcrypt: a Perl Extension for Job Level Parallel Programming
    • In Proceedings of the 2nd International Workshop on High-Performance Infrastructure for Scalable Tools (WHIST), pages 1--9 (online), 2012.
    • url: [pdf]
23. • Tatsuya Abe
    • Completeness of Modal Proofs in First-Order Predicate Logic
    • JSSST Computer Software, 24(4):165--177, 2007.
    • doi: 10.11309/jssst.24.4_165
24. • Tatsuya Abe
    • A Concurrent System of Multi-Ported Processes with Causal Dependency
    • In Proceedings of the 2nd Asian Symposium on Programming Languages and Systems (APLAS), LNCS 3302, pages 146--162, 2004.
    • doi: 10.1007/978-3-540-30477-7_10
    • url: [pdf]

Awards, Educations, Projects, and Services

[researchmap]

Manuscripts

1. Owicki--Gries Logic for Timestamp Semantics [pdf]
2. Introduction to Software Model Checking for Lazy Programmers (in Japanese) [pdf]
3. Split of Classical Logic [pdf]
4. Kripke and Meta-Logical Completeness via Curry--Howard Isomorphism [pdf]

Links

• sc-tascell: compiles Tascell programs.
• mmott: provides user-defined timetables for broadcasting listening (BCL) to shortwave bands.
• Hassign: assigns persons to rooms by using an external constraint solver.
• SOL: checks confluence and termination of higher order rewriting systems.
• VeriDAG: modelchecks program graphs with memory consistency models.
• McSPIN: uses SPIN to modelcheck concurrent programs under various memory consistency models.
• Omni Compiler: compiles XcalableMP programs.
• XMP-mode: an Emacs major mode for editing XcalableMP programs.
• Calfwoid: an Android interface of diary in Emacs toward Calfw.
• Xtract: enables us to extract strings by designating columns, ranges, Perl's statements and scripts.
• Xcrypt: a job-level parallel scripting language that helps automating Plan-Do-Check-Act (PDCA) cycles.