37. Leroy, X., Pessaux, F.: Type-based analysis of uncaught exceptions. ACM Transactions on Programming Languages and Systems 22(2), 340–377 (2000). https://doi.org/10.1145/349214.349230

38. Li, H., Berenger, F., Chang, B.E., Rival, X.: Semantic-directed clumping of disjunctive abstract states. In: Castagna, G., Gordon, A.D. (eds.) Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017. pp. 32–45. ACM (2017). https://doi.org/10.1145/3009837.3009881

39. Maranget, L.: Warnings for pattern matching. Journal of Functional Programming 17(3), 387–421 (2007). https://doi.org/10.1017/S0956796807006223

40. Mauborgne, L.: Representation of Sets of Trees for Abstract Interpretation. phdthesis, École Polytechnique (Nov 1999), https://www.di.ens.fr/~mauborgn/publi/t.pdf

41. Mauborgne, L.: An Incremental Unique Representation for Regular Trees. Nordic Journal of Computing 7(4), 290–311 (Dec 2000), https://software.imdea.org/~mauborgn/publi/njc7.pdf

42. Mauborgne, L.: Improving the representation of infinite trees to deal with sets of trees. In: Smolka, G. (ed.) Programming Languages and Systems, 9th European Symposium on Programming, ESOP 2000, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS 2000, Berlin, Germany, March 25 - April 2, 2000, Proceedings. Lecture Notes in Computer Science, vol. 1782, pp. 275–289. Springer (2000). https://doi.org/10.1007/3-540-46425-5_18

43. Midtgaard, J.: Control-flow analysis of functional programs. ACM Computing Surveys 44(3), 10:1–10:33 (2012). https://doi.org/10.1145/2187671.2187672

44. Midtgaard, J., Jensen, T.: A Calculational Approach to Control-Flow Analysis by Abstract Interpretation. In: Static Analysis, pp. 347–362. Springer Berlin Heidelberg (2008). https://doi.org/10.1007/978-3-540-69166-2_23

45. Midtgaard, J., Jensen, T.P.: Control-Flow Analysis of Function Calls and Returns by Abstract Interpretation. In: Proceedings of the 14th ACM SIGPLAN international conference on Functional programming - ICFP '09. ACM Press (2009). https://doi.org/10.1145/1596550.1596592

46. Midtgaard, J., Jensen, T.P.: Control-Flow Analysis of Function Calls and Returns by Abstract Interpretation. Information and Computation 211, 49–76 (Feb 2012). https://doi.org/10.1016/j.ic.2011.11.005

47. Milner, R.: A Theory of Type Polymorphism in Programming. Journal of Computer and System Sciences 17(3), 348–375 (dec 1978). https://doi.org/10.1016/0022-0000(78)90014-4

48. Montagu, B., Jensen, T.P.: Stable Relations and Abstract Interpretation of Higher-order Programs. Proc. ACM Program. Lang. 4(ICFP), 119:1–119:30 (2020). https://doi.org/10.1145/3409001

49. Montagu, B., Jensen, T.P.: Trace-Based Control-Flow Analysis. In: Freund, S.N., Yahav, E. (eds.) PLDI '21: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, Virtual Event, Canada, June 20-25, 2021. pp. 482–496. ACM (2021). https://doi.org/10.1145/3453483.3454057

50. Nielson, F., Nielson, H.R.: Interprocedural Control Flow Analysis. In: Programming Languages and Systems, pp. 20–39. Springer Berlin Heidelberg (1999). https://doi.org/10.1007/3-540-49099-x_3

51. Okasaki, C.: Red-Black Trees in a Functional Setting. J. Funct. Program. 9(4), 471–477 (1999), http://journals.cambridge.org/action/displayAbstract?aid=44273

52. Okasaki, C., Gill, A.: Fast Mergeable Integer Maps. In: Morriset, G. (ed.) Proceedings of the 1998 ACM SIGPLAN workshop on ML. pp. 77–86 (Sep 1998)
37. Leroy, X., Pessaux, F.: Type-based analysis of uncaught exceptions. ACM Transactions on Programming Languages and Systems 22(2), 340–377 (2000). https://doi.org/10.1145/349214.349230

38. Li, H., Berenger, F., Chang, B.E., Rival, X.: Semantic-directed clumping of disjunctive abstract states. In: Castagna, G., Gordon, A.D. (eds.) Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017. pp. 32–45. ACM (2017). https://doi.org/10.1145/3009837.3009881

39. Maranget, L.: Warnings for pattern matching. Journal of Functional Programming 17(3), 387–421 (2007). https://doi.org/10.1017/S0956796807006223

40. Mauborgne, L.: Representation of Sets of Trees for Abstract Interpretation. phdthesis, École Polytechnique (Nov 1999), https://www.di.ens.fr/~mauborgn/publi/t.pdf

41. Mauborgne, L.: An Incremental Unique Representation for Regular Trees. Nordic Journal of Computing 7(4), 290–311 (Dec 2000), https://software.imdea.org/~mauborgn/publi/njc7.pdf

42. Mauborgne, L.: Improving the representation of infinite trees to deal with sets of trees. In: Smolka, G. (ed.) Programming Languages and Systems, 9th European Symposium on Programming, ESOP 2000, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS 2000, Berlin, Germany, March 25 - April 2, 2000, Proceedings. Lecture Notes in Computer Science, vol. 1782, pp. 275–289. Springer (2000). https://doi.org/10.1007/3-540-46425-5_18

43. Midtgaard, J.: Control-flow analysis of functional programs. ACM Computing Surveys 44(3), 10:1–10:33 (2012). https://doi.org/10.1145/2187671.2187672

44. Midtgaard, J., Jensen, T.: A Calculational Approach to Control-Flow Analysis by Abstract Interpretation. In: Static Analysis, pp. 347–362. Springer Berlin Heidelberg (2008). https://doi.org/10.1007/978-3-540-69166-2_23

45. Midtgaard, J., Jensen, T.P.: Control-Flow Analysis of Function Calls and Returns by Abstract Interpretation. In: Proceedings of the 14th ACM SIGPLAN international conference on Functional programming - ICFP '09. ACM Press (2009). https://doi.org/10.1145/1596550.1596592

46. Midtgaard, J., Jensen, T.P.: Control-Flow Analysis of Function Calls and Returns by Abstract Interpretation. Information and Computation 211, 49–76 (Feb 2012). https://doi.org/10.1016/j.ic.2011.11.005

47. Milner, R.: A Theory of Type Polymorphism in Programming. Journal of Computer and System Sciences 17(3), 348–375 (dec 1978). https://doi.org/10.1016/0022-0000(78)90014-4

48. Montagu, B., Jensen, T.P.: Stable Relations and Abstract Interpretation of Higher-order Programs. Proc. ACM Program. Lang. 4(ICFP), 119:1–119:30 (2020). https://doi.org/10.1145/3409001

49. Montagu, B., Jensen, T.P.: Trace-Based Control-Flow Analysis. In: Freund, S.N., Yahav, E. (eds.) PLDI '21: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, Virtual Event, Canada, June 20-25, 2021. pp. 482–496. ACM (2021). https://doi.org/10.1145/3453483.3454057

50. Nielson, F., Nielson, H.R.: Interprocedural Control Flow Analysis. In: Programming Languages and Systems, pp. 20–39. Springer Berlin Heidelberg (1999). https://doi.org/10.1007/3-540-49099-x_3

51. Okasaki, C.: Red-Black Trees in a Functional Setting. J. Funct. Program. 9(4), 471–477 (1999), http://journals.cambridge.org/action/displayAbstract?aid=44273

52. Okasaki, C., Gill, A.: Fast Mergeable Integer Maps. In: Morriset, G. (ed.) Proceedings of the 1998 ACM SIGPLAN workshop on ML. pp. 77–86 (Sep 1998)
53. Pessaux, F., Leroy, X.: Type-based analysis of uncaught exceptions. In: Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. ACM (jan 1999). https://doi.org/10.1145/292540.292565

54. Pessaux, F.: Détection statique d'exceptions non rattrapées en Objective Caml. Ph.D. thesis, Université Paris 6 (1999), http://www.theses.fr/1999PA066398

55. Pierce, B.C.: Types and Programming Languages. MIT Press, Cambridge, Mass (2002)

56. Rémy, D.: Type checking records and variants in a natural extension of ML. In: Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages - POPL '89. ACM Press (1989). https://doi.org/10.1145/75277.75284

57. Reynolds, J.C.: Automatic Computation of Data Set Definitions. Information Processing **68**, 456–461 (1969)

58. Seidl, H., Vogler, R.: Three Improvements to the Top-Down Solver. In: Sabel, D., Thiemann, P. (eds.) Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming, PPDP 2018, Frankfurt am Main, Germany, September 03-05, 2018. pp. 21:1–21:14. ACM (2018). https://doi.org/10.1145/3236950.3236967

59. Shivers, O.: The Semantics of Scheme Control-Flow Analysis. In: Proceedings of the 1991 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation. pp. 190–198. PEPM '91, Association for Computing Machinery, New York, NY, USA (1991). https://doi.org/10.1145/115865.115884

60. Valnet, M., Monat, R., Miné, A.: Analyse statique de valeurs par interprétation abstraite de programmes fonctionnels manipulant des types algébriques récursifs. In: JFLA 2023-34èmes Journées Francophones des Langages Applicatifs. pp. 210–241 (2023)

61. de Vilhena, P.E., Pottier, F.: A Type System for Effect Handlers and Dynamic Labels. In: Programming Languages and Systems, pp. 225–252. Springer Nature Switzerland (2023). https://doi.org/10.1007/978-3-031-30044-8_9

62. de Vilhena, P.E., Pottier, F., Jourdan, J.: Spy game: verifying a local generic solver in Iris. Proc. ACM Program. Lang. **4***(POPL), 33:1–33:28 (2020). https://doi.org/10.1145/3371101

63. Vojdani, V., Apinis, K., Rōtov, V., Seidl, H., Vene, V., Vogler, R.: Static race detection for device drivers: the goblint approach. In: Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering, ASE 2016. pp. 391–402. ACM (2016). https://doi.org/10.1145/2970276.2970337

64. Wright, A.K., Jagannathan, S.: Polymorphic Splitting: An Effective Polyvariant Flow Analysis. ACM Trans. Program. Lang. Syst. **20**(1), 166–207 (1998). https://doi.org/10.1145/271510.271523

65. Yi, K.: Compile-time Detection of Uncaught Exceptions in Standard ML Programs. In: Charlier, B.L. (ed.) Static Analysis, First International Static Analysis Symposium, SAS'94, Namur, Belgium, September 28-30, 1994, Proceedings. Lecture Notes in Computer Science, vol. 864, pp. 238–254. Springer (1994). https://doi.org/10.1007/3-540-58485-4_4

66. Yi, K.: An Abstract Interpretation for Estimating Uncaught Exceptions in Standard ML Programs. Sci. Comput. Program. **31**(1), 147–173 (1998). https://doi.org/10.1016/S0167-6423(96)00044-5

67. Yi, K., Ryu, S.: A cost-effective estimation of uncaught exceptions in Standard ML programs. Theoretical Computer Science **277**(1-2), 185–217 (2002). https://doi.org/10.1016/S0304-3975(00)00317-0
53. Pessaux, F., Leroy, X.: Type-based analysis of uncaught exceptions. In: Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. ACM (jan 1999). https://doi.org/10.1145/292540.292565

54. Pessaux, F.: Détection statique d'exceptions non rattrapées en Objective Caml. Ph.D. thesis, Université Paris 6 (1999), http://www.theses.fr/1999PA066398

55. Pierce, B.C.: Types and Programming Languages. MIT Press, Cambridge, Mass (2002)

56. Rémy, D.: Type checking records and variants in a natural extension of ML. In: Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages - POPL '89. ACM Press (1989). https://doi.org/10.1145/75277.75284

57. Reynolds, J.C.: Automatic Computation of Data Set Definitions. Information Processing **68**, 456–461 (1969)

58. Seidl, H., Vogler, R.: Three Improvements to the Top-Down Solver. In: Sabel, D., Thiemann, P. (eds.) Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming, PPDP 2018, Frankfurt am Main, Germany, September 03-05, 2018. pp. 21:1–21:14. ACM (2018). https://doi.org/10.1145/3236950.3236967

59. Shivers, O.: The Semantics of Scheme Control-Flow Analysis. In: Proceedings of the 1991 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation. pp. 190–198. PEPM '91, Association for Computing Machinery, New York, NY, USA (1991). https://doi.org/10.1145/115865.115884

60. Valnet, M., Monat, R., Miné, A.: Analyse statique de valeurs par interprétation abstraite de programmes fonctionnels manipulant des types algébriques récursifs. In: JFLA 2023-34èmes Journées Francophones des Langages Applicatifs. pp. 210–241 (2023)

61. de Vilhena, P.E., Pottier, F.: A Type System for Effect Handlers and Dynamic Labels. In: Programming Languages and Systems, pp. 225–252. Springer Nature Switzerland (2023). https://doi.org/10.1007/978-3-031-30044-8_9

62. de Vilhena, P.E., Pottier, F., Jourdan, J.: Spy game: verifying a local generic solver in Iris. Proc. ACM Program. Lang. **4** (POPL), 33:1–33:28 (2020). https://doi.org/10.1145/3371101

63. Vojdani, V., Apinis, K., Rōtov, V., Seidl, H., Vene, V., Vogler, R.: Static race detection for device drivers: the goblint approach. In: Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering, ASE 2016. pp. 391–402. ACM (2016). https://doi.org/10.1145/2970276.2970337

64. Wright, A.K., Jagannathan, S.: Polymorphic Splitting: An Effective Polyvariant Flow Analysis. ACM Trans. Program. Lang. Syst. **20**(1), 166–207 (1998). https://doi.org/10.1145/271510.271523

65. Yi, K.: Compile-time Detection of Uncaught Exceptions in Standard ML Programs. In: Charlier, B.L. (ed.) Static Analysis, First International Static Analysis Symposium, SAS'94, Namur, Belgium, September 28-30, 1994, Proceedings. Lecture Notes in Computer Science, vol. 864, pp. 238–254. Springer (1994). https://doi.org/10.1007/3-540-58485-4_4

66. Yi, K.: An Abstract Interpretation for Estimating Uncaught Exceptions in Standard ML Programs. Sci. Comput. Program. **31**(1), 147–173 (1998). https://doi.org/10.1016/S0167-6423(96)00044-5

67. Yi, K., Ryu, S.: A cost-effective estimation of uncaught exceptions in Standard ML programs. Theoretical Computer Science **277**(1-2), 185–217 (2002). https://doi.org/10.1016/S0304-3975(00)00317-0
# A Abstract Domain

The concretisation function on abstract values enjoys the standard weakening and substitution properties.

**Lemma 7 (Weakening).** Let $\Gamma$ and $\Gamma'$ be environments, such that $\text{dom } \Gamma \cap \text{dom } \Gamma' = \emptyset$. Then, we have $\gamma_{\Gamma}A = \gamma_{\Gamma, \Gamma'}A$.

*Proof.* By induction on $A$, generalising $\Gamma'$.

**Lemma 8 (Substitution).** Let $\Gamma$ and $\Gamma'$ be environments, such that $\text{dom } \Gamma \cap \text{dom } \Gamma' = \emptyset$ and $\alpha \notin \text{dom } \Gamma \cup \text{dom } \Gamma'$. Then, $\gamma_{\Gamma, \alpha; \gamma_{\Gamma}(A'), \Gamma'}(A) = \gamma_{\Gamma, \Gamma'}(A[\alpha \leftarrow A'])$.

*Proof.* By induction on $A$, generalising $\Gamma'$, and applying Lemma 7 in the case of variables.

*Proof (Lemma 2).* We want to show that $\gamma(\mu\alpha.A) = \gamma(A[\alpha \leftarrow \mu\alpha.A])$. The proof proceeds as follows:

$$ 
\begin{align*}
\gamma(\mu\alpha.A) &= \text{lfp}_{\subseteq}(\lambda S.\gamma_{\alpha:S}(A)) && (\text{by definition}) \\
&= \gamma_{\alpha:\gamma(\mu\alpha.A)}(A) && (\text{by the fixed point property}) \\
&= \gamma(A[\alpha \leftarrow \mu\alpha.A]) && (\text{by Lemma 8})
\end{align*}
$$

**Lemma 9.** If $A_1$ and $A_2$ are well-formed and $A_1$ is $\alpha$-contractive, then $A_1[\alpha \leftarrow A_2]$ is well-formed.

**Definition 9 (Projection on constructors).** The projection on constructors of a well-formed abstract value $A$, written $A.constructs$, is defined as follows:

$$ 
\begin{align*}
\{\text{ints} : I; \text{constructs} : C; \text{fun}s : F\}.\text{constructs} &= C \\
(\mu\alpha.A).\text{constructs} &= (A[\alpha \leftarrow \mu\alpha.A]).\text{constructs}
\end{align*}
$$

**Lemma 10 (Soundness of projection on constructors).** The following inclusion is satisfied: $\gamma(A) \cap \{c(v_1, \dots, v_n) \mid c \in C, \forall 1 \le i \le n, v_i \in V\} \subseteq \gamma(A.constructs)$

**Definition 10 (Projection on closures).** The projection on function closures of a well-formed abstract value $A$, written $A.fun$s, is defined as follows:

$$ 
\begin{align*}
\{\text{ints} : I; \text{constructs} : C; \text{fun}s : F\}.\text{fun}s &= F \\
(\mu\alpha.A).\text{fun}s &= (A[\alpha \leftarrow \mu\alpha.A]).\text{fun}s
\end{align*}
$$

**Lemma 11 (Soundness of projection on closures).** The following inclusion is satisfied: $\gamma(A) \cap \{\langle E, \mu f. \lambda x.t \rangle \mid E \in \mathbb{E}\} \subseteq \gamma(A.fun}s$

**Definition 11 (Abstract union).** The union of abstract values, written $A_1 \sqcup A_2 = A_3$ is specified as a co-inductive relation by the rules of Fig. 5. In this definition, the function $\sqcup_I$ is given by the user-provided abstract domain on integers.
# A Abstract Domain

The concretisation function on abstract values enjoys the standard weakening and substitution properties.

**Lemma 7 (Weakening).** Let $\Gamma$ and $\Gamma'$ be environments, such that $\text{dom } \Gamma \cap \text{dom } \Gamma' = \emptyset$. Then, we have $\gamma_{\Gamma}A = \gamma_{\Gamma, \Gamma'}A$.

*Proof.* By induction on $A$, generalising $\Gamma'$.

**Lemma 8 (Substitution).** Let $\Gamma$ and $\Gamma'$ be environments, such that $\text{dom } \Gamma \cap \text{dom } \Gamma' = \emptyset$ and $\alpha \notin \text{dom } \Gamma \cup \text{dom } \Gamma'$. Then, $\gamma_{\Gamma, \alpha; \gamma_{\Gamma}(A'), \Gamma'}(A) = \gamma_{\Gamma, \Gamma'}(A[\alpha \leftarrow A'])$.

*Proof.* By induction on $A$, generalising $\Gamma'$, and applying Lemma 7 in the case of variables.

*Proof (Lemma 2).* We want to show that $\gamma(\mu\alpha.A) = \gamma(A[\alpha \leftarrow \mu\alpha.A])$. The proof proceeds as follows:

$$ 
\begin{align*}
\gamma(\mu\alpha.A) &= \text{lfp}_{\subseteq}(\lambda S.\gamma_{\alpha:S}(A)) && (\text{by definition}) \\
&= \gamma_{\alpha:\gamma(\mu\alpha.A)}(A) && (\text{by the fixed point property}) \\
&= \gamma(A[\alpha \leftarrow \mu\alpha.A]) && (\text{by Lemma 8})
\end{align*}
$$

**Lemma 9.** If $A_1$ and $A_2$ are well-formed and $A_1$ is $\alpha$-contractive, then $A_1[\alpha \leftarrow A_2]$ is well-formed.

**Definition 9 (Projection on constructors).** The projection on constructors of a well-formed abstract value $A$, written $A.constructs$, is defined as follows:

$$ 
\begin{align*}
\{\text{ints} : \text{l}; \text{constructs} : \text{C}; \text{fun}s : \text{F}\}.\text{constructs} &= \text{C} \\
(\mu\alpha.A).\text{constructs} &= (A[\alpha \leftarrow \mu\alpha.A]).\text{constructs}
\end{align*}
$$

**Lemma 10 (Soundness of projection on constructors).** The following inclusion is satisfied: $\gamma(A) \cap \{c(v_1, \dots, v_n) \mid c \in \mathcal{C}, \forall 1 \le i \le n, v_i \in \mathbb{V}\} \subseteq \gamma(A.constructs)$

**Definition 10 (Projection on closures).** The projection on function closures of a well-formed abstract value $A$, written $A.fun$s, is defined as follows:

$$ 
\begin{align*}
\{\text{ints} : \text{l}; \text{constructs} : \text{C}; \text{fun}s : \text{F}\}.\text{fun}s &= \text{F} \\
(\mu\alpha.A).\text{fun}s &= (A[\alpha \leftarrow \mu\alpha.A]).\text{fun}s
\end{align*}
$$

**Lemma 11 (Soundness of projection on closures).** The following inclusion is satisfied: $\gamma(A) \cap \{\langle E, \mu f. \lambda x.t \rangle \mid E \in \mathbb{E}\} \subseteq \gamma(A.fun}s$

**Definition 11 (Abstract union).** The union of abstract values, written $A_1 \sqcup A_2 = A_3$ is specified as a co-inductive relation by the rules of Fig. 5. In this definition, the function $\sqcup_I$ is given by the user-provided abstract domain on integers.
$$ \frac{A_1[\alpha \leftarrow \mu\alpha.A_1] \sqcup A_2 = A_3}{\mu\alpha.A_1 \sqcup A_2 = A_3} \qquad \frac{A_1 \neq \mu\beta.A'_1}{A_1 \sqcup A_2[\alpha \leftarrow \mu\alpha.A_2] = A_3} \qquad \frac{A_1 \neq \mu\beta.A'_1 \quad A_2 \neq \mu\beta.A'_2}{A_1 \sqcup A_2 = A_3[\alpha \leftarrow \mu\alpha.A_3]} $$

$$ \frac{\text{I}_1 \sqcup \text{I}_2 = \text{I}_3}{C_1 \sqcup C_2 = C_3 \quad F_1 \sqcup F_2 = F_3 \quad A_3 = \{\text{ints} : \text{I}_3; \text{constructs} : C_3; \text{fun}s : F_3\}} \\ \{\text{ints} : \text{I}_1; \text{constructs} : C_1; \text{fun}s : F_1\} \sqcup \{\text{ints} : \text{I}_2; \text{constructs} : C_2; \text{fun}s : F_2\} = A_3 $$

$$ C_1 \sqcup C \bar{=} \bar{T} \qquad \bar{T} \sqcup C_2 = \bar{T} $$

$$ \frac{C_3 = C_1 \setminus \text{dom } C_2 \cup C_2 \setminus \text{dom } C_1 \cup \{c \mapsto (A_{3,1}^c, \dots, A_{3,n}^c) \mid c \in \text{dom } C_1 \cap \text{dom } C_2\} \\ \forall (c \mapsto (A_{1,1}^c, \dots, A_{1,n}^c)) \in C_1, \forall (c \mapsto (A_{2,1}^c, \dots, A_{2,n}^c)) \in C_2, \forall 1 \le i \le n, A_{1,i}^c \sqcup A_{2,i}^c = A_{3,i}^c}{C_1 \sqcup C_2 = C_3} $$

$$ F_1 \sqcup F \bar{=} \bar{T} \qquad \bar{T} \sqcup F_2 = \bar{T} $$

$$ \frac{F_3 = F_1 \setminus \text{dom } F_2 \cup F_2 \setminus \text{dom } F_1 \cup \{\mu f. \lambda x. t \mapsto E_3^l \mid (\mu f. \lambda x. t) \in \text{dom } F_1 \cap \text{dom } F_2\} \\ \forall (\mu f. \lambda x. t \mapsto E_1^l) \in F_1, \forall (\mu f. \lambda x. t \mapsto E_2^l) \in F_2, \forall x \in \text{dom } E_1^l, E_1^l(x) \sqcup E_2^l(x) = E_3^l(x)}{F_1 \sqcup F_2 = F_3} $$

<caption>**Fig. 5.** Union of abstract values: the rules define a co-inductive relation.</caption>

Although the specification of abstract union is non-deterministic, it is easy to show that two possible outputs of the abstract union are necessarily included in each other.

**Definition 12 (Abstract intersection).** The intersection of abstract values, written $A_1 \sqcap A_2 = A_3$ is specified as a co-inductive relation by the rules of Figure 6. In this definition, the function $\sqcap_I$ is given by the user-provided abstract domain on integers.
$$ \frac{A_1[\alpha \leftarrow \mu\alpha.A_1] \sqcup A_2 = A_3}{\mu\alpha.A_1 \sqcup A_2 = A_3} \qquad \frac{A_1 \neq \mu\beta.A'_1}{A_1 \sqcup A_2[\alpha \leftarrow \mu\alpha.A_2] = A_3} \qquad \frac{A_1 \neq \mu\beta.A'_1 \quad A_2 \neq \mu\beta.A'_2}{A_1 \sqcup A_2 = A_3[\alpha \leftarrow \mu\alpha.A_3]} $$

$$ \frac{\text{I}_1 \sqcup \text{I}_2 = \text{I}_3}{C_1 \sqcup C_2 = C_3 \quad F_1 \sqcup F_2 = F_3 \quad A_3 = \{\text{ints} : \text{I}_3; \text{constructs} : C_3; \text{fun}s : F_3\}} \\ \{\text{ints} : \text{I}_1; \text{constructs} : C_1; \text{fun}s : F_1\} \sqcup \{\text{ints} : \text{I}_2; \text{constructs} : C_2; \text{fun}s : F_2\} = A_3 $$

$$ C_1 \sqcup C \bar{=} \bar{T} \qquad \bar{T} \sqcup C_2 = \bar{T} $$

$$ C_3 = C_1 \setminus \text{dom } C_2 \cup C_2 \setminus \text{dom } C_1 \cup \{c \mapsto (A_{3,1}^c, \dots, A_{3,n}^c) \mid c \in \text{dom } C_1 \cap \text{dom } C_2\} \\ \forall (c \mapsto (A_{1,1}^c, \dots, A_{1,n}^c)) \in C_1, \forall (c \mapsto (A_{2,1}^c, \dots, A_{2,n}^c)) \in C_2, \forall 1 \le i \le n, A_{1,i}^c \sqcup A_{2,i}^c = A_{3,i}^c $$

$$ F_1 \sqcup F \bar{=} \bar{T} \qquad \bar{T} \sqcup F_2 = \bar{T} $$

$$ F_3 = F_1 \setminus \text{dom } F_2 \cup F_2 \setminus \text{dom } F_1 \cup \{\mu f. \lambda x. t \mapsto E_3^\ell \mid (\mu f. \lambda x. t) \in \text{dom } F_1 \cap \text{dom } F_2\} \\ \forall (\mu f. \lambda x. t \mapsto E_1^\ell) \in F_1, \forall (\mu f. \lambda x. t \mapsto E_2^\ell) \in F_2, \forall x \in \text{dom } E_1^\ell, E_1^\ell(x) \sqcup E_2^\ell(x) = E_3^\ell(x) $$

**Fig. 5.** Union of abstract values: the rules define a co-inductive relation.

Although the specification of abstract union is non-deterministic, it is easy to show that two possible outputs of the abstract union are necessarily included in each other.

**Definition 12 (Abstract intersection).** The intersection of abstract values, written $A_1 \sqcap A_2 = A_3$ is specified as a co-inductive relation by the rules of Figure 6. In this definition, the function $\sqcap_I$ is given by the user-provided abstract domain on integers.
$$ \frac{A_1[\alpha \leftarrow \mu\alpha.A_1] \sqcap A_2 = A_3}{\mu\alpha.A_1 \sqcap A_2 = A_3} \qquad \frac{A_1 \neq \mu\beta.A_1' \qquad A_2 \neq \mu\beta.A_2'}{A_1 \sqcap A_2[\alpha \leftarrow \mu\alpha.A_2] = A_3 \qquad A_1 \sqcap A_2 = A_3[\alpha \leftarrow \mu\alpha.A_3]} \qquad \frac{A_1 \sqcap A_2 = \mu\alpha.A_3}{A_1 \sqcap A_2 = A_3} $$

$$ \frac{\text{l}_1 \sqcap \text{l}_2 = \text{l}_3}{C_1 \sqcap C_2 = C_3 \qquad F_1 \sqcap F_2 = F_3 \qquad A_3 = \{\text{ints} : \text{l}_3; \text{constructs} : C_3; \text{fun}s : F_3\}} $$

$$ \{\text{ints} : \text{l}_1; \text{constructs} : C_1; \text{fun}s : F_1\} \sqcap \{\text{ints} : \text{l}_2; \text{constructs} : C_2; \text{fun}s : F_2\} = A_3 $$

$$ \overline{C_1 \sqcap C_2} = \overline{C_1} \qquad \overline{\top \sqcap C_2} = \overline{C_2} $$

$$ \frac{C_3 = \{c \mapsto (A_{3,1}^c, \dots, A_{3,n}^c) \mid c \in \text{dom } C_1 \cap \text{dom } C_2 \wedge \forall 1 \le i \le n, A_{3,i}^c \neq \top\} \quad \forall (c \mapsto (A_{1,1}^c, \dots, A_{1,n}^c)) \in C_1, \forall (c \mapsto (A_{2,1}^c, \dots, A_{2,n}^c)) \in C_2, \forall 1 \le i \le n, A_{1,i}^c \sqcap A_{2,i}^c = A_{3,i}^c}{C_1 \sqcap C_2 = C_3} $$

$$ \overline{F_1 \sqcap F_2} = \overline{F_1} \qquad \overline{\top \sqcap F_2} = \overline{F_2} $$

$$ \frac{F_3 = \{\mu f. \lambda x. t \mapsto E_3^\ell \mid (\mu f. \lambda x. t) \in \text{dom } F_1 \cap \text{dom } F_2 \wedge \forall x, E_3^\ell(x) \neq \top\} \quad \forall (\mu f. \lambda x. t \mapsto E_1^\ell) \in F_1, \forall (\mu f. \lambda x. t \mapsto E_2^\ell) \in F_2, \forall x \in \text{dom } E_1^\ell, E_1^\ell(x) \sqcap E_2^\ell(x) = E_3^\ell(x)}{F_1 \sqcap F_2 = F_3} $$

<caption>**Fig. 6.** Intersection of abstract values: the rules define a co-inductive relation.</caption>
$$ \frac{A_1[\alpha \leftarrow \mu\alpha.A_1] \sqcap A_2 = A_3}{\mu\alpha.A_1 \sqcap A_2 = A_3} \qquad \frac{A_1 \neq \mu\beta.A_1' \qquad A_2 \neq \mu\beta.A_2'}{A_1 \sqcap A_2[\alpha \leftarrow \mu\alpha.A_2] = A_3 \qquad A_1 \sqcap A_2 = A_3[\alpha \leftarrow \mu\alpha.A_3]} \qquad \frac{A_1 \sqcap A_2 = \mu\alpha.A_3}{A_1 \sqcap A_2 = A_3} $$

$$ C_1 \sqcap C_2 = C_3 \qquad F_1 \sqcap F_2 = F_3 \qquad A_3 = \{\text{ints} : I_3; \text{constructs} : C_3; \text{fun}s : F_3\} $$

$$ \{\text{ints} : I_1; \text{constructs} : C_1; \text{fun}s : F_1\} \sqcap \{\text{ints} : I_2; \text{constructs} : C_2; \text{fun}s : F_2\} = A_3 $$

$$ \overline{C_1 \sqcap C_2} = \overline{C_1} \qquad \overline{\top \sqcap C_2} = \overline{C_2} $$

$$ C_3 = \{c \mapsto (A_{3,1}^c, \dots, A_{3,n}^c) \mid c \in \text{dom } C_1 \cap \text{dom } C_2 \wedge \forall 1 \le i \le n, A_{3,i}^c \ne \perp\} \\ \forall (c \mapsto (A_{1,1}^c, \dots, A_{1,n}^c)) \in C_1, \forall (c \mapsto (A_{2,1}^c, \dots, A_{2,n}^c)) \in C_2, \forall 1 \le i \le n, A_{1,i}^c \sqcap A_{2,i}^c = A_{3,i}^c \\ \frac{C_1 \sqcap C_2 = C_3}{C_1 \sqcap C_2 = C_3} $$

$$ \overline{F_1 \sqcap F_2} = \overline{F_1} \qquad \overline{\top \sqcap F_2} = \overline{F_2} $$

$$ F_3 = \{\mu f. \lambda x. t \mapsto E_3^\ell | (\mu f. \lambda x. t) \in \text{dom } F_1 \cap \text{dom } F_2 \wedge \forall x, E_3^\ell(x) \neq \perp\} \\ \forall (\mu f. \lambda x. t \mapsto E_1^\ell) \in F_1, \forall (\mu f. \lambda x. t \mapsto E_2^\ell) \in F_2, \forall x \in \text{dom } E_1^\ell, E_1^\ell(x) \sqcap E_2^\ell(x) = E_3^\ell(x) \\ \frac{F_1 \sqcap F_2 = F_3}{F_1 \sqcap F_2 = F_3} $$

<caption>**Fig. 6.** Intersection of abstract values: the rules define a co-inductive relation.</caption>
# B Transfer Functions

**Definition 13 (Abstract constructor removal).**

$$ \{\text{ints} : \mathbf{l}; \text{constructs} : \mathbf{C}; \text{funns} : \mathbf{F}\} \setminus c = \begin{cases} \{\text{constructs} : \mathbf{C}\} & \text{if } C = \mathbf{T} \\ \{\text{constructs} : \mathbf{C} \setminus c\} & \text{otherwise} \end{cases} \\ (\mu\alpha.A) \setminus c = (A[\alpha \leftarrow \mu\alpha.A]) \setminus c $$

where $C \setminus c$ is the map $C$ from which the key $c$ is removed.

**Definition 14 (Abstract complement).**

$$ \begin{array}{l} \mathcal{L}^{\#} :: \mathbb{T} \to \mathcal{A} \to \mathcal{A} \\ x \mathcal{L}^{\#} \mathcal{A} = \bot \\ c(p_1, \dots, p_n) \mathcal{L}^{\#} \mathcal{A} = \mathcal{A} \setminus c \sqcup \\ \qquad \bigcup_{1 \le i \le n} \left\{ \text{constructs} : \left\{ \begin{array}{l} c \mapsto (A_1, \dots, A_{i-1}, \\ \qquad p_i \mathcal{L}^{\#} A_i, \\ \qquad A_{i+1}, \dots, A_n) \end{array} \right\} \right\} \\ \text{where } (A_1, \dots, A_n) = \mathcal{A}.\text{constructs}(c) \\ p + q \mathcal{L}^{\#} \mathcal{A} = (p \mathcal{L}^{\#} \mathcal{A}) \sqcap (q \mathcal{L}^{\#} \mathcal{A}) \\ p \setminus q \mathcal{L}^{\#} \mathcal{A} = p \mathcal{L}^{\#} \mathcal{A} \end{array} $$

**Definition 15 (Abstract matching).**

$$ \begin{array}{l} \mathcal{L}^{\#} :: \mathbb{P} \to \mathcal{A} \to \mathbb{E}_{\perp} \\ x \mathcal{L}^{\#} \mathcal{A} = \begin{cases} \bot & \text{if } \mathcal{A} = \bot \\ \{x \mapsto \mathcal{A}\} & \text{otherwise} \end{cases} \\ c(p_1, \dots, p_n) \mathcal{L}^{\#} \mathcal{A} = \begin{cases} \bot & \text{if } c \notin \text{dom } \mathcal{A}.\text{constructs} \\ \{\} & \text{if } n = 0 \text{ and } c \in \text{dom } \mathcal{A}.\text{constructs} \\ \bigcap_{1 \le i \le n} p_i \mathcal{L}^{\#} A_i & \text{if } n \ge 1 \text{ and } \mathcal{A}.\text{constructs}(c) = (A_1, \dots, A_n) \end{cases} \\ p + q \mathcal{L}^{\#} \mathcal{A} = (p \mathcal{L}^{\#} \mathcal{A}) \sqcup (q \mathcal{L}^{\#} \mathcal{A}) \\ p \setminus q \mathcal{L}^{\#} \mathcal{A} = p \mathcal{L}^{\#} (q \mathcal{L}^{\#} \mathcal{A}) \end{array} $$
# B Transfer Functions

**Definition 13 (Abstract constructor removal).**

$$ \{\text{ints} : \mathbb{I}; \text{constructs} : \mathcal{C}; \text{funns} : \mathcal{F}\} \setminus c = \begin{cases} \{\text{constructs} : \mathcal{C}\} & \text{if } C = \top \\ \{\text{constructs} : \mathcal{C} \setminus c\} & \text{otherwise} \end{cases} \\ (\mu\alpha.A) \setminus c = (\mathcal{A}[\alpha \leftarrow \mu\alpha.A]) \setminus c $$

where $C \setminus c$ is the map $C$ from which the key $c$ is removed.

**Definition 14 (Abstract complement).**

$$ \begin{array}{l} \llcorner^{\#} :: \mathbb{T} \to \mathcal{A} \to \mathcal{A} \\ x \llcorner^{\#} \mathcal{A} = \bot \\ c(p_1, \dots, p_n) \llcorner^{\#} \mathcal{A} = \mathcal{A} \setminus c \sqcup \\ \qquad \bigcup_{1 \le i \le n} \left\{ \text{constructs} : \left\{ \begin{array}{l} c \mapsto (A_1, \dots, A_{i-1}, \\ \qquad p_i \llcorner^{\#} A_i, \\ \qquad A_{i+1}, \dots, A_n) \end{array} \right\} \right\} \\ \text{where } (A_1, \dots, A_n) = \mathcal{A}.\text{constructs}(c) \\ p + q \llcorner^{\#} \mathcal{A} = (p \llcorner^{\#} \mathcal{A}) \sqcap (q \llcorner^{\#} \mathcal{A}) \\ p \setminus q \llcorner^{\#} \mathcal{A} = p \llcorner^{\#} \mathcal{A} \end{array} $$

**Definition 15 (Abstract matching).**

$$ \begin{array}{l} \llcorner^{\#} :: \mathbb{P} \to \mathcal{A} \to \mathbb{E}_{\perp} \\ x \llcorner^{\#} \mathcal{A} = \begin{cases} \bot & \text{if } \mathcal{A} = \bot \\ \{x \mapsto \mathcal{A}\} & \text{otherwise} \end{cases} \\ c(p_1, \dots, p_n) \llcorner^{\#} \mathcal{A} = \begin{cases} \bot & \text{if } c \notin \text{dom } \mathcal{A}.\text{constructs} \\ \{\} & \text{if } n = 0 \text{ and } c \in \text{dom } \mathcal{A}.\text{constructs} \\ \bigcap_{1 \le i \le n} p_i \llcorner^{\#} A_i & \text{if } n \ge 1 \text{ and } \mathcal{A}.\text{constructs}(c) = (A_1, \dots, A_n) \end{cases} \\ p + q \llcorner^{\#} \mathcal{A} = (p \llcorner^{\#} \mathcal{A}) \sqcup (q \llcorner^{\#} \mathcal{A}) \\ p \setminus q \llcorner^{\#} \mathcal{A} = p \llcorner^{\#} (q \llcorner^{\#} \mathcal{A}) \end{array} $$
<figure><img src="image_6.png" /></figure>

RESEARCH CENTRE
RENNES - BRETAGNE ATLANTIQUE

Campus universitaire de Beaulieu
35042 Rennes Cedex

Publisher
Inria
Domaine de Voluceau - Rocquencourt
BP 105 - 78153 Le Chesnay Cedex
inria.fr

ISSN 0249-6399
<figure><img src="image_7.png" /></figure>

RESEARCH CENTRE
RENNES - BRETAGNE ATLANTIQUE

Campus universitaire de Beaulieu
35042 Rennes Cedex

Publisher
Inria
Domaine de Voluceau - Rocquencourt
BP 105 - 78153 Le Chesnay Cedex
inria.fr

ISSN 0249-6399