Theory and Practice of Second-Order Rewriting: Foundation, Evolution, and SOL

1. Aczel, P.: A general Church-Rosser theorem. Technical report, University of Manchester (1978)

   Google Scholar 

2. Arkor, N., Fiore, M.: Algebraic models of simple type theories: a polynomial approach. In: Proceedings of LICS 2020, pp. 88–101. ACM (2020)

   Google Scholar 

3. Blanqui, F.: Termination and confluence of higher-order rewrite systems. In: Bachmair, L. (ed.) RTA 2000. LNCS, vol. 1833, pp. 47–61. Springer, Heidelberg (2000). https://doi.org/10.1007/10721975_4

   Chapter  MATH  Google Scholar 

4. Blanqui, F.: Termination of rewrite relations on \(\lambda \)-terms based on Girard’s notion of reducibility. Theor. Comput. Sci. 611, 50–86 (2016)

   Article  MathSciNet  Google Scholar 

5. Fiore, M., Hur, C.-K.: Second-order equational logic (extended abstract). In: Dawar, A., Veith, H. (eds.) CSL 2010. LNCS, vol. 6247, pp. 320–335. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-15205-4_26

   Chapter  MATH  Google Scholar 

6. Fiore, M., Hamana, M.: Multiversal polymorphic algebraic theories: syntax, semantics, translations, and equational logic. In: 28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013, pp. 520–529 (2013)

   Google Scholar 

7. Fiore, M.: Semantic analysis of normalisation by evaluation for typed lambda calculus. In: Proceedings of PPDP 2002, pp. 26–37. ACM Press (2002)

   Google Scholar 

8. Fiore, M.: Second-order and dependently-sorted abstract syntax. In: Proceedings of LICS 2008, pp. 57–68 (2008)

   Google Scholar 

9. Fiore, M., Mahmoud, O.: Second-order algebraic theories. In: Hliněný, P., Kučera, A. (eds.) MFCS 2010. LNCS, vol. 6281, pp. 368–380. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-15155-2_33

   Chapter  Google Scholar 

10. Fiore, M., Plotkin, G., Turi, D.: Abstract syntax and variable binding. In: Proceedings of LICS 1999, pp. 193–202 (1999)

    Google Scholar 

11. Fiore, M., Staton, S.: Substitution, jumps, and algebraic effects. In: Proceedings of the CSL-LICS 2014, pp. 41:1–41:10 (2014)

    Google Scholar 

12. Hamana, M., Abe, T., Kikuchi, K.: Polymorphic computation systems: theory and practice of confluence with call-by-value. Sci. Comput. Program. 187(102322) (2020)

    Google Scholar 

13. Hamana, M.: Free \(\Sigma \)-monoids: a higher-order syntax with metavariables. In: Chin, W.-N. (ed.) APLAS 2004. LNCS, vol. 3302, pp. 348–363. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30477-7_23

    Chapter  Google Scholar 

14. Hamana, M.: Universal algebra for termination of higher-order rewriting. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 135–149. Springer, Heidelberg (2005). https://doi.org/10.1007/978-3-540-32033-3_11

    Chapter  MATH  Google Scholar 

15. Hamana, M.: Higher-order semantic labelling for inductive datatype systems. In: Proceedings of PPDP 2007, pp. 97–108. ACM Press (2007)

    Google Scholar 

16. Hamana, M.: Initial algebra semantics for cyclic sharing tree structures. Log. Methods Comput. Sci. 6(3(15)), 1–1–23 (2010)

    Google Scholar 

17. Hamana, M.: Semantic labelling for proving termination of combinatory reduction systems. In: Escobar, S. (ed.) WFLP 2009. LNCS, vol. 5979, pp. 62–78. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-11999-6_5

    Chapter  Google Scholar 

18. Hamana, M.: Polymorphic abstract syntax via Grothendieck construction. In: Hofmann, M. (ed.) FoSSaCS 2011. LNCS, vol. 6604, pp. 381–395. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-19805-2_26

    Chapter  Google Scholar 

19. Hamana, M.: Cyclic datatypes modulo bisimulation based on second-order algebraic theories. Log. Methods Comput. Sci. 13, 1–38 (2017)

    MathSciNet  MATH  Google Scholar 

20. Hamana, M.: How to prove your calculus is decidable: practical applications of second-order algebraic theories and computation. Proc. ACM Program. Lang. 1(22), 1–28 (2017)

    Article  Google Scholar 

21. Hamana, M.: Polymorphic rewrite rules: confluence, type inference, and instance validation. In: Gallagher, J.P., Sulzmann, M. (eds.) FLOPS 2018. LNCS, vol. 10818, pp. 99–115. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-90686-7_7

    Chapter  MATH  Google Scholar 

22. Hamana, M.: How to prove decidability of equational theories with second-order computation analyser SOL. J. Funct. Program. 29(e20) (2019)

    Google Scholar 

23. Hamana, M.: Modular termination for second-order computation rules and application to algebraic effect handlers. arXiv:1912.03434 (2020)

24. Klop, J.W.: Combinatory reduction systems. Ph.D. thesis, CWI. Mathematical Centre Tracts, vol. 127, Amsterdam (1980)

    Google Scholar 

25. Staton, S.: An algebraic presentation of predicate logic. In: Proceedings of FOSSACS 201, pp. 401–417 (2013)

    Google Scholar 

26. Staton, S.: Instances of computational effects: an algebraic perspective. In: Proceedings of LICS 2013, p. 519 (2013)

    Google Scholar 

27. Staton, S.: Algebraic effects, linearity, and quantum programming languages. In: Proceedings of POPL 2015, pp. 395–406 (2015)

    Google Scholar 

28. Yokoyama, T., Hu, Z., Takeichi, M.: Deterministic second-order patterns. Inf. Process. Lett. 89(6), 309–314 (2004)

    Article  MathSciNet  Google Scholar 

Download references