40. Kobayashi, N., Sato, R., Unno, H.: Predicate abstraction and CEGAR for higher-order model checking. SIGPLAN Not. 46(6), 222–233 (2011). https://doi.org/10.1145/1993316.1993525, https://doi.org/10.1145/1993316.1993525

41. Kobayashi, N., Tabuchi, N., Unno, H.: Higher-Order Multi-Parameter Tree Transducers and Recursion Schemes for Program Verification. In: POPL '10: Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages. pp. 495–508. Association for Computing Machinery, New York, NY, USA (2010). https://doi.org/10.1145/1707801.1706355, https://doi.org/10.1145/1707801.1706355

42. Koskinen, E., Terauchi, T.: Local Temporal Reasoning. In: Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). CSL-LICS'14, Association for Computing Machinery, New York, NY, USA (2014). https://doi.org/10.1145/2603088.2603138, https://doi.org/10.1145/2603088.2603138

43. Kozen, D.: Results on the propositional $\mu$-calculus. Theoretical Computer Science 27(3), 333–354 (1983), special Issue Ninth International Colloquium on Automata, Languages and Programming (ICALP) Aarhus, Summer 1982

44. Krishnaswami, N.R.: Higher-order functional reactive programming without space-time leaks. In: Proceedings of ICFP'13. pp. 221–232. ACM, New York, NY, USA (2013)

45. Krishnaswami, N.R., Benton, N.: Ultrametric Semantics of Reactive Programs. In: 2011 IEEE 26th Annual Symposium on Logic in Computer Science. pp. 257–266 (2011). https://doi.org/10.1109/LICS.2011.38

46. Kuwahara, T., Terauchi, T., Unno, H., Kobayashi, N.: Automatic Termination Verification for Higher-Order Functional Programs. In: Shao, Z. (ed.) Programming Languages and Systems. pp. 392–411. ESOP'14, Springer Berlin Heidelberg, Berlin, Heidelberg (2014)

47. Mac Lane, S., Moerdijk, I.: Sheaves in geometry and logic: A first introduction to topos theory. Springer (1992)

48. Marin, S.: Modal proof theory through a focused telescope. PhD thesis, Université Paris Saclay (Jan 2018), https://hal.archives-ouvertes.fr/tel-01951291

49. McBride, C., Paterson, R.: Applicative programming with effects. Journal of Functional Programming 18(1) (2008). https://doi.org/10.1017/S0956796807006326

50. Møgelberg, R.E.: A type theory for productive coprogramming via guarded recursion. In: Proceedings of CSL-LICS 2014. CSL-LICS '14, ACM (2014)

51. Murase, A., Terauchi, T., Kobayashi, N., Sato, R., Unno, H.: Temporal Verification of Higher-Order Functional Programs. In: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. pp. 57–68. POPL'16, Association for Computing Machinery, New York, NY, USA (2016). https://doi.org/10.1145/2837614.2837667, https://doi.org/10.1145/2837614.2837667

52. Nakano, H.: A Modality for Recursion. In: Proceedings of LICS'00. pp. 255–266. IEEE Computer Society (2000)

53. Nanjo, Y., Unno, H., Koskinen, E., Terauchi, T.: A Fixpoint Logic and Dependent Effects for Temporal Property Verification. In: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science. pp. 759–768. LICS'18, Association for Computing Machinery, New York, NY, USA (2018). https://doi.org/10.1145/3209108.3209204, https://doi.org/10.1145/3209108.3209204
54. Ong, C.H.L.: On Model-Checking Trees Generated by Higher-Order Recursion Schemes. In: Proceedings of LICS 2006. pp. 81–90. IEEE Computer Society (2006)

55. Piróg, M., Gibbons, J.: The coinductive resumption monad. Electronic Notes in Theoretical Computer Science **308**, 273–288 (2014)

56. Plotkin, G., Stirling, C.: A Framework for Intuitionistic Modal Logics: Extended Abstract. In: Proceedings of the 1986 Conference on Theoretical Aspects of Reasoning About Knowledge. pp. 399–406. TARK '86, Morgan Kaufmann Publishers Inc., San Francisco, CA, USA (1986)

57. Rondon, P.M., Kawaguci, M., Jhala, R.: Liquid Types. In: Proceedings of the 29th ACM SIGPLAN Conference on Programming Language Design and Implementation. pp. 159–169. PLDI'08, Association for Computing Machinery, New York, NY, USA (2008). https://doi.org/10.1145/1375581.1375602, https://doi.org/10.1145/1375581.1375602

58. Santocanale, L., Venema, Y.: Completeness for flat modal fixpoint logics. Ann. Pure Appl. Logic **162**(1), 55–82 (2010)

59. Sato, R., Iwayama, N., Kobayashi, N.: Combining higher-order model checking with refinement type inference. In: Hermenegildo, M.V., Igarashi, A. (eds.) Proceedings of the 2019 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, PEPM@POPL 2019, Cascais, Portugal, January 14-15, 2019. pp. 47–53. ACM (2019). https://doi.org/10.1145/3294032.3294081, https://doi.org/10.1145/3294032.3294081

60. Simpson, A.K.: The Proof Theory and Semantics of Intuitionistic Modal Logic. Phd thesis, University of Edinburgh (Jul 1994), https://www.era.lib.ed.ac.uk/handle/1842/407

61. Skalka, C., Smith, S., Van Horn, D.: Types and Trace Effects of Higher Order Programs. J. Funct. Program. **18**(2), 179–249 (Mar 2008). https://doi.org/10.1017/S0956796807006466, https://doi.org/10.1017/S0956796807006466

62. Spies, S., Krishnaswami, N., Dreyer, D.: Transfinite Step-Indexing for Termination. Proc. ACM Program. Lang. **5**(POPL) (Jan 2021). https://doi.org/10.1145/3434294, https://doi.org/10.1145/3434294

63. Sprenger, C., Dam, M.: On the Structure of Inductive Reasoning: Circular and Tree-Shaped Proofs in the $\mu$-Calculus. In: Gordon, A.D. (ed.) Foundations of Software Science and Computational Structures, 6th International Conference, FOSSACS 2003 Held as Part of the Joint European Conference on Theory and Practice of Software, ETAPS 2003, Warsaw, Poland, April 7-11, 2003, Proceedings. Lecture Notes in Computer Science, vol. 2620, pp. 425–440. Springer (2003). https://doi.org/10.1007/3-540-36576-1-27, https://doi.org/10.1007/3-540-36576-1-27

64. Unno, H., Satake, Y., Terauchi, T.: Relatively complete refinement type system for verification of higher-order non-deterministic programs. Proc. ACM Program. Lang. **2**(POPL), 12:1–12:29 (2018). https://doi.org/10.1145/3158100, https://doi.org/10.1145/3158100

65. Vazou, N.: Liquid Haskell: Haskell as a theorem prover. Ph.D. thesis, UC San Diego (2016)

66. Vazou, N., Seidel, E.L., Jhala, R., Vytiniotis, D., Peyton-Jones, S.: Refinement Types for Haskell. In: Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming. pp. 269–282. ICFP'14, Association for Computing Machinery, New York, NY, USA (2014). https://doi.org/10.1145/2628136.2628161, https://doi.org/10.1145/2628136.2628161
54. Ong, C.H.L.: On Model-Checking Trees Generated by Higher-Order Recursion Schemes. In: Proceedings of LICS 2006. pp. 81–90. IEEE Computer Society (2006)

55. Piróg, M., Gibbons, J.: The coinductive resumption monad. Electronic Notes in Theoretical Computer Science **308**, 273–288 (2014)

56. Plotkin, G., Stirling, C.: A Framework for Intuitionistic Modal Logics: Extended Abstract. In: Proceedings of the 1986 Conference on Theoretical Aspects of Reasoning About Knowledge. pp. 399–406. TARK '86, Morgan Kaufmann Publishers Inc., San Francisco, CA, USA (1986)

57. Rondon, P.M., Kawaguci, M., Jhala, R.: Liquid Types. In: Proceedings of the 29th ACM SIGPLAN Conference on Programming Language Design and Implementation. pp. 159–169. PLDI'08, Association for Computing Machinery, New York, NY, USA (2008). https://doi.org/10.1145/1375581.1375602, https://doi.org/10.1145/1375581.1375602

58. Santocanale, L., Venema, Y.: Completeness for flat modal fixpoint logics. Ann. Pure Appl. Logic **162**(1), 55–82 (2010)

59. Sato, R., Iwayama, N., Kobayashi, N.: Combining higher-order model checking with refinement type inference. In: Hermenegildo, M.V., Igarashi, A. (eds.) Proceedings of the 2019 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, PEPM@POPL 2019, Cascais, Portugal, January 14-15, 2019. pp. 47–53. ACM (2019). https://doi.org/10.1145/3294032.3294081, https://doi.org/10.1145/3294032.3294081

60. Simpson, A.K.: The Proof Theory and Semantics of Intuitionistic Modal Logic. Phd thesis, University of Edinburgh (Jul 1994), https://www.era.lib.ed.ac.uk/handle/1842/407

61. Skalka, C., Smith, S., Van Horn, D.: Types and Trace Effects of Higher Order Programs. J. Funct. Program. **18**(2), 179–249 (Mar 2008). https://doi.org/10.1017/S0956796807006466, https://doi.org/10.1017/S0956796807006466

62. Spies, S., Krishnaswami, N., Dreyer, D.: Transfinite Step-Indexing for Termination. Proc. ACM Program. Lang. **5**(POPL) (Jan 2021). https://doi.org/10.1145/3434294, https://doi.org/10.1145/3434294

63. Sprenger, C., Dam, M.: On the Structure of Inductive Reasoning: Circular and Tree-Shaped Proofs in the $\mu$-Calculus. In: Gordon, A.D. (ed.) Foundations of Software Science and Computational Structures, 6th International Conference, FOSSACS 2003 Held as Part of the Joint European Conference on Theory and Practice of Software, ETAPS 2003, Warsaw, Poland, April 7-11, 2003, Proceedings. Lecture Notes in Computer Science, vol. 2620, pp. 425–440. Springer (2003). https://doi.org/10.1007/3-540-36576-1-27, https://doi.org/10.1007/3-540-36576-1-27

64. Unno, H., Satake, Y., Terauchi, T.: Relatively complete refinement type system for verification of higher-order non-deterministic programs. Proc. ACM Program. Lang. **2**(POPL), 12:1–12:29 (2018). https://doi.org/10.1145/3158100, https://doi.org/10.1145/3158100

65. Vazou, N.: Liquid Haskell: Haskell as a theorem prover. Ph.D. thesis, UC San Diego (2016)

66. Vazou, N., Seidel, E.L., Jhala, R., Vytiniotis, D., Peyton-Jones, S.: Refinement Types for Haskell. In: Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming. pp. 269–282. ICFP'14, Association for Computing Machinery, New York, NY, USA (2014). https://doi.org/10.1145/2628136.2628161, https://doi.org/10.1145/2628136.2628161
67. Veltri, N., van der Weide, N.: Guarded Recursion in Agda via Sized Types. In: Geuvers, H. (ed.) 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), vol. 131, pp. 32:1–32:19. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany (2019). https://doi.org/10.4230/LIPIcs.FSCD.2019.32, http://drops.dagstuhl.de/opus/volltexte/2019/10539

68. Walukiewicz, I.: Completeness of Kozen's Axiomatisation of the Propositional μ-Calculus. Information and Computation 157(1-2), 142–182 (2000)

69. Watanabe, K., Tsukada, T., Oshikawa, H., Kobayashi, N.: Reduction from Branching-Time Property Verification of Higher-Order Programs to HFL Validity Checking. In: Proceedings of the 2019 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation. pp. 22–34. PEPM 2019, Association for Computing Machinery, New York, NY, USA (2019). https://doi.org/10.1145/3294032.3294077, https://doi.org/10.1145/3294032.3294077

70. Xia, L.Y., Zakowski, Y., He, P., Hur, C.K., Malecha, G., Pierce, B.C., Zdancewic, S.: Interaction Trees: Representing Recursive and Impure Programs in Coq. Proc. ACM Program. Lang. 4(POPL) (2019). https://doi.org/10.1145/3371119, https://doi.org/10.1145/3371119

**Open Access** This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
67. Veltri, N., van der Weide, N.: Guarded Recursion in Agda via Sized Types. In: Geuvers, H. (ed.) 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), vol. 131, pp. 32:1–32:19. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany (2019). https://doi.org/10.4230/LIPIcs.FSCD.2019.32, http://drops.dagstuhl.de/opus/volltexte/2019/10539

68. Walukiewicz, I.: Completeness of Kozen's Axiomatisation of the Propositional μ-Calculus. Information and Computation 157(1-2), 142–182 (2000)

69. Watanabe, K., Tsukada, T., Oshikawa, H., Kobayashi, N.: Reduction from Branching-Time Property Verification of Higher-Order Programs to HFL Validity Checking. In: Proceedings of the 2019 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation. pp. 22–34. PEPM 2019, Association for Computing Machinery, New York, NY, USA (2019). https://doi.org/10.1145/3294032.3294077, https://doi.org/10.1145/3294032.3294077

70. Xia, L.Y., Zakowski, Y., He, P., Hur, C.K., Malecha, G., Pierce, B.C., Zdancewic, S.: Interaction Trees: Representing Recursive and Impure Programs in Coq. Proc. ACM Program. Lang. 4(POPL) (2019). https://doi.org/10.1145/3371119, https://doi.org/10.1145/3371119

**Open Access** This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.