Ichiro Hasuo

• National Institute of Informatics
• ichiro [at] is.s.u-tokyo.ac.jp

• English
• Japanese
• Dutch
• Chinese

• Home
• Contact
• Research
• Cv
• Papers
• Talks
• Teaching
• Group

For articles in Japanese, see also here.

Latest Papers

Please refer to my dblp entry.

2017

• Ichiro Hasuo.
  Metamathematics for Systems Design: Comprehensive Transfer of Formal Methods Techniques to Cyber-Physical Systems.
  A position paper for the ERATO MMSD project. Position Paper, New Generation Computing, Ohmsha/Springer. 2017.
  [Springer|pdf]
• Corina Cirstea, Shunsuke Shimizu, and Ichiro Hasuo.
  Parity Automata for Quantitative Linear Time Logics.
  To appear in Proc. CALCO 2017.
• Ichiro Hasuo, Toshiki Kataoka, and Kenta Cho.
  Coinductive Predicates and Final Sequences in a Fibration.
  Extended version of [Hasuo, Cho, Kataoka & Jacobs, MFPS 2013]. Mathematical Structures in Computer Science, 2017.
  [doi]
• Natsuki Urabe, Masaki Hara and Ichiro Hasuo.
  Categorical Liveness Checking by Corecursive Algebras.
  To appear in Proc. LICS 2017.

2016

• Natsuki Urabe and Ichiro Hasuo.
  Coalgebraic Infinite Traces and Kleisli Simulations.
  Extended version of [Urabe & Hasuo, CALCO 2015]. Submitted.
• Takumi Akazaki and Ichiro Hasuo.
  Time Robustness in MTL and Expressivity in Hybrid System Falsification.
  Extended version of [Akazaki & Hasuo, CAV 2015]. Submitted.
• Masaki Waga, Takumi Akazaki and Ichiro Hasuo.
  A Boyer-Moore Type Algorithm for Timed Pattern Matching.
  Proc. FORMATS 2016, LNCS 9884, p. 121-139.
  [lncs | extended version at arXiv]
• Natsuki Urabe, Shunsuke Shimizu, and Ichiro Hasuo.
  Fair Simulation for Nondeterministic and Probabilistic Büchi Automata: a Coalgebraic Perspective.
  Preprint.
  [arXiv]
• Natsuki Urabe, Shunsuke Shimizu, and Ichiro Hasuo.
  Coalgebraic Trace Semantics for Büchi and Parity Automata.
  To appear in Proc. CONCUR 2016.
  [preprint version at arXiv]
• Ichiro Hasuo and Naohiko Hoshino.
  Semantics of Higher-Order Quantum Computation via Geometry of Interaction.
  Extended version of [Hasuo & Hoshino, LICS 2011]. To appear in Annals of Pure and Applied Logic.
  [preprint version at arXiv]
• Wataru Hino, Hiroki Kobayashi, Ichiro Hasuo and Bart Jacobs.
  Healthiness from Duality.
  To appear in Proc. LICS 2016.
  [acm | preprint version with appendices at arXiv]
• Ichiro Hasuo and Prakash Panangaden, editors.
  Special Issue on Quantum Physics and Logic (QPL 2014).
  New Generation Comput. 34(1-2): 1-2, 2016.
• Natsuki Urabe and Ichiro Hasuo.
  Quantitative Simulations by Matrices.
  Extended version of [Urabe & Hasuo, CONCUR 2014].
  To appear in Information and Computation.
  [elsevier | preprint pdf]
• Ichiro Hasuo, editor.
  Coalgebraic Methods in Computer Science, the 13th International Workshop (CMCS 2016), Proceedings.
  LNCS 9608.
  [lncs]
• Ichiro Hasuo, Shunsuke Shimizu, and Corina Cirstea.
  Lattice-theoretic progress measures and coalgebraic model checking.
  Proc. POPL 2016, p. 718-732.
  [acm | extended version at arXiv]
• Koko Muroya, Naohiko Hoshino and Ichiro Hasuo.
  Memoryful Geometry of Interaction II: Recursion and Adequacy.
  Proc. POPL 2016, p. 748-760.
  [acm | pdf]
• Kengo Kido, Swarat Chaudhuri and Ichiro Hasuo.
  Abstract Interpretation with Infinitesimals: Towards Scalability in Nonstandard Static Analysis.
  Proc. VMCAI 2016, LNCS 9583, p. 229-249.
  [lncs | extended version at arXiv]

2015

• Koko Muroya, Naohiko Hoshino and Ichiro Hasuo.
  Memoryful GoI with Recursion.
  Short abstract presented at LOLA 2015.
  [pdf]
• Shota Nakagawa and Ichiro Hasuo.
  Near-Optimal Scheduling for LTL with Future Discounting.
  Proc. TGC 2015, LNCS 9533, p. 112-130.
  [lncs | preliminary version in the pre-proceedings]
• Natsuki Urabe and Ichiro Hasuo.
  Coalgebraic Infinite Traces and Kleisli Simulations.
  Proc. CALCO 2015, p. 320-335.
  [extended version at arXiv]
• Koko Muroya, Toshiki Kataoka, Ichiro Hasuo and Naohiko Hoshino.
  Compiling Effectful Terms to Transducers: Prototype Implementation of Memoryful Geometry of Interaction.
  Preprint.
• Ichiro Hasuo.
  Generic Weakest Precondition Semantics from Monads Enriched with Order.
  Theoretical Computer Science, 604:2-29, 2015.
  [doi | pdf]
• Kengo Kido, Swarat Chaudhuri and Ichiro Hasuo.
  Abstract Interpretation with Infinitesimals: Towards Scalability in Nonstandard Static Analysis (Preliminary Report).
  Proc. SNR 2015.
  
• Takumi Akazaki and Ichiro Hasuo.
  Time Robustness in MTL and Expressivity in Hybrid System Falsification.
  Proc. CAV 2015.
  LNCS 9207, p. 356-374. Springer-Verlag.
  [doi | extended version at arXiv]

2014

• Takumi Akazaki, Ichiro Hasuo, and Kohei Suenaga.
  Input Synthesis for Sampled Data Systems by Program Logic.
  Proc. HAS 2014.
  EPTCS 174, p. 22-39. Published on 22 Jan 2015.
  [eptcs | local pdf]
• Bob Coecke, Ichiro Hasuo and Prakash Panangaden, editors.
  Quantum Physics and Logic, the 11th International Workshop (QPL 2014), Proceedings.
  EPTCS 172.
  [eptcs]
• Koko Muroya, Toshiki Kataoka, Ichiro Hasuo and Naohiko Hoshino.
  Compiling Effectful Terms to Transducers: Prototype Implementation of Memoryful Geometry of Interaction (Preliminary Report).
  Short abstract presented at LOLA 2014.
  [pdf]
• Natsuki Urabe and Ichiro Hasuo.
  Generic Forward and Backward Simulations III: Quantitative Simulations by Matrices.
  Proc. CONCUR 2014.
  LNCS 8704, p. 451-466. Springer-Verlag. (Best Paper Award)
  [lncs | pdf (extended version with appendices)]
• Naohiko Hoshino, Koko Muroya and Ichiro Hasuo.
  Memoryful Geometry of Interaction: From Coalgebraic Components to Algebraic Effects.
  Proc. CSL-LICS 2014, paper 52.
  [acm | preprint pdf]
• Ugo Dal Lago, Claudia Faggian, Ichiro Hasuo and Akira Yoshimizu.
  The Geometry of Synchronization.
  Proc. CSL-LICS 2014, paper 35.
  [acm | extended version, arXiv]
• Ichiro Hasuo.
  Generic Weakest Precondition Semantics from Monads Enriched with Order.
  Proc. CMCS 2014 (an invited paper).
  LNCS 8446, p. 10-32. Springer-Verlag.
  [lncs | preprint pdf]
• Akira Yoshimizu, Ichiro Hasuo, Claudia Faggian, and Ugo Dal Lago.
  Measurements in Proof Nets as Higher-Order Quantum Circuits.
  Proc. ESOP 2014.
  LNCS 8410, p. 371-391. Springer-Verlag.
  [doi | preprint pdf, with an appendix]

2013

• Ichiro Hasuo, Kenta Cho, Toshiki Kataoka, and Bart Jacobs.
  Coinductive Predicates and Final Sequences in a Fibration.
  Proc. MFPS XXIX, Electr. Notes Comp. Sci. 298:197-214, 2013.
  [doi | preprint pdf, with an appendix]
• Kohei Suenaga, Hiroyoshi Sekine, and Ichiro Hasuo.
  Hyperstream Processing Systems: Nonstandard Modeling of Continuous-Time Signals.
  Proc. POPL 2013, p. 417-430. ACM.
  [acm | local copy with appendices]

2012

• Hiroyoshi Sekine, Kohei Suenaga and Ichiro Hasuo.
  Simulink Blocks as Stream Processing --- An Approach from Nonstandard Analysis (Preliminary Report).
  Proc. NSV 2012.
  
• Ichiro Hasuo and Kohei Suenaga.
  Exercises in Nonstandard Static Analysis of Hybrid Systems.
  Proc. CAV 2012.
  LNCS 7358, p. 462-478. Springer-Verlag.
  [LNCS | Extended ver. with proofs]

2011

• Ichiro Hasuo and Bart Jacobs.
  Traces for Coalgebraic Components.
  Mathematical Structures in Computer Science, 21:267-320, 2011.
  [CUP | preprint pdf]
• Ichiro Hasuo.
  The Microcosm Principle and Compositionality of GSOS-Based Component Calculi.
  
  • Proc. CALCO 2011.
    LNCS 6859, p. 222-236. Springer-Verlag.
    [LNCS | preprint pdf]
  • Extended version with proofs:
    [pdf]
• Kohei Suenaga and Ichiro Hasuo.
  Programming with Infinitesimals: A While-Language for Hybrid System Modeling.
  
  • Proc. ICALP 2011, Track B.
    LNCS 6756, p. 392-403. Springer-Verlag.
    [LNCS | preprint pdf]
  • Extended version with proofs:
    [pdf]
• Ichiro Hasuo and Naohiko Hoshino.
  Semantics of Higher-Order Quantum Computation via Geometry of Interaction.
  
  • Proc. LICS 2011.
    p. 237-246. IEEE Computer Society.
    [IEEE | preprint pdf]
  • Extended version with proofs: to appear in RIMS Preprints.
    [pdf]

2010

• Ichiro Hasuo and Kazuyuki Asada.
  Categorifying Computations into Components via Arrows as Profunctors.
  An extended version of [Asada-Hasuo, CMCS 2010]. Preprint.
  [pdf]
• Ichiro Hasuo.
  Generic Forward and Backward Simulations II: Probabilistic Simulation.
  
  • Proc. CONCUR 2010 - Concurrency Theory.
    LNCS 6269, p. 447-461. Springer-Verlag.
    [LNCS | preprint pdf]
  • Extended version with additional proofs and examples: RIMS Preprints 1698, June 2010.
    [pdf | RIMS]
• Ichiro Hasuo, Bart Jacobs, and Milad Niqui.
  Coalgebraic Representation Theory of Fractals (Extended Abstract).
  Proc. Mathematical Foundations of Programming Semantics (MFPS XXVI), Electr. Notes Comp. Sci. 265:351-368, 2010.
  [doi | preprint pdf, with an appendix]
• Ichiro Hasuo, Yoshinobu Kawabe and Hideki Sakurada.
  Probabilistic Anonymity via Coalgebraic Simulations.
  Theoretical Computer Science, 411(22-24):2239-2259, 2010.
  [doi | preprint pdf]
• Kazuyuki Asada and Ichiro Hasuo.
  Categorifying Computations into Components via Arrows as Profunctors.
  Proc. Coalgebraic Methods Comp. Sci. (CMCS 2010), Electr. Notes Comp. Sci. 264(2):25-45, 2010.
  [doi | preprint pdf]

2009

• Bart Jacobs and Ichiro Hasuo.
  Semantics and Logic for Security Protocols.
  Journal of Computer Security, 17(6):909-944, 2009.
  [gzipped ps | pdf | accompanying PVS sources]
• Bart Jacobs, Chris Heunen and Ichiro Hasuo.
  Categorical Semantics for Arrows.
  Journal of Functional Programming, 19(3-4):403-438, 2009.
  [ps | pdf]
• Ichiro Hasuo.
  Pseudo Functorial Semantics.
  Preprint.
  [ps | pdf]
• Ichiro Hasuo, Chris Heunen, Bart Jacobs, and Ana Sokolova.
  Coalgebraic Components in a Many-Sorted Microcosm.
  Conference on Algebra and Coalgebra in Computer Science (CALCO 2009).
  LNCS 5728, p. 64-80. Springer-Verlag.
  [ps | pdf]

2008

• Ichiro Hasuo.
  Tracing Anonymity with Coalgebras.
  PhD thesis, Radboud University Nijmegen.
  Defended on March 10, 2008.
  Hard copies available on request!
  [ps | pdf]
• Ichiro Hasuo, Bart Jacobs and Ana Sokolova.
  The Microcosm Principle and Concurrency in Coalgebra.
  Foundations of Software Science and Computation Structures (FoSSaCS 2008).
  LNCS 4962, p. 246-260. Springer-Verlag.
  [lncs | ps | pdf]

2007

• Ichiro Hasuo, Bart Jacobs and Ana Sokolova.
  Generic Trace Semantics via Coinduction.
  Extended version of [2006,CMCS] and [2005,CALCO].
  Logical Methods in Computer Science, 3(4:11), 2007.
  [lmcs | ps | pdf]
• Ichiro Hasuo, Bart Jacobs and Tarmo Uustalu.
  Categorical Views on Computations on Trees (Extended Abstract).
  International Colloquium on Automata, Languages and Programming (ICALP 2007), Track B.
  LNCS 4596, p. 619-630. Springer-Verlag.
  [lncs | ps | pdf]
• Ichiro Hasuo and Yoshinobu Kawabe.
  Probabilistic Anonymity via Coalgebraic Simulations.
  European Symposium on Programming (ESOP '07).
  LNCS 4421, p. 379-394. Springer-Verlag.
  [lncs | gzipped ps | pdf | bib]

2006

• Bart Jacobs and Ichiro Hasuo.
  Freyd is Kleisli, for Arrows.
  Workshop on Mathematically Structured Functional Programming (MSFP '06).
  The proceedings are in eWiC.
  [eWiC | gzipped ps | pdf | bib]
• Ichiro Hasuo.
  Generic Forward and Backward Simulations.
  • International Conference on Concurrency Theory (CONCUR 2006).
    LNCS 4137, p.406-420. Springer-Verlag.
    [lncs | gzipped ps | pdf | bib]
  • Extended version: Technical report, Research Center for Verification and Semantics,
    National Institute of Advanced Industrial Science and Technology (CVS, AIST), Japan.
    [gzipped ps | pdf]
• Ichiro Hasuo, Bart Jacobs and Ana Sokolova.
  Generic Trace Theory.
  International Workshop on Coalgebraic Methods in Computer Science (CMCS 2006).
  ENTCS 164, p.47-65. Elsevier B.V.
  [entcs | gzipped ps | pdf | bib]
• Nuttapong Attrapadung, Yang Cui, David Galindo, Goichiro Hanaoka,
  Ichiro Hasuo, Hideki Imai, Kanta Matsuura, Peng Yang and Rui Zhang.
  Relations among notions of security for identity based encryption schemes.
  Latin American Theoretical Informatics Symposium (LATIN '06).
  LNCS 3887, p.130-141. Springer-Verlag.
  [lncs | bib]

2005

• David Galindo and Ichiro Hasuo.
  Security Notions for Identity Based Encryption.
  Cryptology ePrint Archive, Report 2005/253.
  [copy]
• Flavio D. Garcia, Ichiro Hasuo, Wolter Pieters and Peter van Rossum.
  Provable Anonymity.
  ACM Workshop on Formal Methods in Security Engineering (FMSE '05).
  p.63-72, ACM press.
  [gzipped ps | pdf | bib]
• Ichiro Hasuo and Bart Jacobs.
  Coalgebraic Trace Semantics for Probabilistic Systems (Abstract).
  CALCO-jnr workshop, 2005.
  [gzipped ps | pdf]
• Ichiro Hasuo and Bart Jacobs.
  Context-free Languages via Coalgebraic Trace Semantics.
  Conference on Algebra and Coalgebra in Computer Science (CALCO 2005).
  LNCS 3629, p.204-233. Springer-Verlag.
  Revised June 2005.
  [lncs | gzipped ps | pdf | bib]

2003

• Ichiro Hasuo and Ryo Kashima.
  Kripke Completeness of First-Order Constructive Logics with Strong Negation.
  Logic Journal of the IGPL, 11(6): 615-646, 2003.
  [gzipped ps | pdf | bib]