Top

Published in:

2020 | OriginalPaper | Chapter

Galois Connections for Recursive Types

Authors : Ahmad Salim Al-Sibahi, Thomas Jensen, Rasmus Ejlers Møgelberg, Andrzej Wąsowski

Published in: From Lambda Calculus to Cybersecurity Through Program Analysis

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

Building a static analyser for a real language involves modeling of large domains capturing the many available data types. To scale domain design and support efficient development of project-specific analyzers, it is desirable to be able to build, extend, and change abstractions in a systematic and modular fashion. We present a framework for modular design of abstract domains for recursive types and higher-order functions, based on the theory of solving recursive domain equations. We show how to relate computable abstract domains to our framework, and illustrate the potential of the construction by modularizing a monolithic domain for regular tree grammars. A prototype implementation in the dependently typed functional language Agda shows how the theoretical solution can be used in practice to construct static analysers.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

previous chapter A Type Theory for Probabilistic –calculus

next chapter Incremental Abstract Interpretation

Available only for authorised users

The construction would not work if we used final coalgebras.

We have flattened the tuple in the first argument, to improve presentation.

https://github.com/ahmadsalim/agda-moddom.

https://static-content.springer.com/image/chp%3A10.1007%2F978-3-030-41103-9_4/MediaObjects/495073_1_En_4_Figk_HTML.gif

and

https://static-content.springer.com/image/chp%3A10.1007%2F978-3-030-41103-9_4/MediaObjects/495073_1_En_4_Figl_HTML.gif

modules.

https://static-content.springer.com/image/chp%3A10.1007%2F978-3-030-41103-9_4/MediaObjects/495073_1_En_4_Fign_HTML.gif

and

https://static-content.springer.com/image/chp%3A10.1007%2F978-3-030-41103-9_4/MediaObjects/495073_1_En_4_Figo_HTML.gif

modules respectively.

Abbott, M.G., Altenkirch, T., Ghani, N.: Containers: constructing strictly positive types. Theoret. Comput. Sci. 342(1), 3–27 (2005)MathSciNetCrossRef

Abramsky, S., Jung, A.: Domain theory. In: Abramsky, S., Gabbay, D.M., Maibaum, T.S.E. (eds.) Handbook of Logic in Computer Science, vol. 3, pp. 1–168. Clarendon Press, Oxford (1994)

Aiken, A., Murphy, B.R.: Implementing regular tree expressions. In: Hughes, J. (ed.) FPCA 1991. LNCS, vol. 523, pp. 427–447. Springer, Heidelberg (1991). https://doi.org/10.1007/3540543961_21CrossRef

Awodey, S.: Category Theory. Oxford University Press, Oxford (2011)MATH

Benton, P.N.: Strictness properties of lazy algebraic datatypes. In: Cousot, P., Falaschi, M., Filé, G., Rauzy, A. (eds.) WSA 1993. LNCS, vol. 724, pp. 206–217. Springer, Heidelberg (1993). https://doi.org/10.1007/3-540-57264-3_42CrossRef

Bodin, M., Gardner, P., Jensen, T., Schmitt, A.: Skeletal semantics and their interpretations. PACMPL 3(POPL), 44:1–44:31 (2019)

Chang, B.E., Rival, X.: Relational inductive shape analysis. In: Necula, G.C., Wadler, P. (eds.) POPL 2008, pp. 247–260. ACM (2008)

Chang, B.-Y.E., Rival, X., Necula, G.C.: Shape analysis with structural invariant checkers. In: Nielson, H.R., Filé, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 384–401. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-74061-2_24 CrossRef

Cousot, P.: The calculational design of a generic abstract interpreter. In: Broy, M., Steinbrüggen, R. (eds.) Calculational System Design. NATO ASI Series F. IOS Press, Amsterdam (1999)

10.

Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Graham, R.M., Harrison, M.A., Sethi, R. (eds.) POPL 1977, pp. 238–252. ACM (1977)

11.

Cousot, P., Cousot, R.: Invited talk: higher order abstract interpretation (and application to comportment analysis generalizing strictness, termination, projection, and PER analysis. In: Bal, H.E. (ed.) Proceedings of the IEEE Computer Society 1994 International Conference on Computer Languages, Toulouse, France, 16–19 May 1994, pp. 95–112. IEEE Computer Society (1994)

12.

Cousot, P., Cousot, R.: Formal language, grammar and set-constraint-based program analysis by abstract interpretation. In: FPCA 1995, pp. 170–181. ACM (1995)

13.

Cousot, P., Cousot, R.: Modular static program analysis. In: Horspool, R.N. (ed.) CC 2002. LNCS, vol. 2304, pp. 159–179. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45937-5_13CrossRef

14.

Darais, D., Labich, N., Nguyen, P.C., Horn, D.V.: Abstracting definitional interpreters (functional pearl). PACMPL 1(ICFP), 12:1–12:25 (2017)

15.

Jensen, T.P.: Disjunctive program analysis for algebraic data types. ACM Trans. Program. Lang. Syst. 19(5), 751–803 (1997)CrossRef

16.

Journault, M., Miné, A., Ouadjaout, A.: Modular static analysis of string manipulations in C programs. In: Podelski, A. (ed.) SAS 2018. LNCS, vol. 11002, pp. 243–262. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-99725-4_16CrossRef

17.

Keidel, S., Poulsen, C.B., Erdweg, S.: Compositional soundness proofs of abstract interpreters. PACMPL 2(ICFP), 72:1–72:26 (2018)

18.

Midtgaard, J., Jensen, T.: A calculational approach to control-flow analysis by abstract interpretation. In: Alpuente, M., Vidal, G. (eds.) SAS 2008. LNCS, vol. 5079, pp. 347–362. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-69166-2_23CrossRefMATH

19.

Nielson, F., Nielson, H.R.: The tensor product in wadler’s analysis of lists. Sci. Comput. Program. 22(3), 327–354 (1994)MathSciNetCrossRef

20.

Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer, Heidelberg (1999). https://doi.org/10.1007/978-3-662-03811-6CrossRefMATH

21.

Norell, U.: Dependently typed programming in agda. In: Koopman, P., Plasmeijer, R., Swierstra, D. (eds.) AFP 2008. LNCS, vol. 5832, pp. 230–266. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-04652-0_5CrossRefMATH

22.

Rival, X., Toubhans, A., Chang, B.-Y.E.: Construction of abstract domains for heterogeneous properties (position paper). In: Margaria, T., Steffen, B. (eds.) ISoLA 2014. LNCS, vol. 8803, pp. 489–492. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-662-45231-8_40CrossRef

23.

Streicher, T.: Domain-Theoretic Foundations of Functional Programming. World Scientific Publishing Company, Singapore (2006)CrossRef

24.

Tarski, A.: A lattice-theoretical fixpoint theorem and its applications. Pac. J. Math. 5(2), 285–309 (1955)MathSciNetCrossRef

25.

Toubhans, A., Chang, B.-Y.E., Rival, X.: Reduced product combination of abstract domains for shapes. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 375–395. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-35873-9_23CrossRefMATH

Title: Galois Connections for Recursive Types
Authors: Ahmad Salim Al-Sibahi
Thomas Jensen
Rasmus Ejlers Møgelberg
Andrzej Wąsowski
Publisher: Springer International Publishing
Book: From Lambda Calculus to Cybersecurity Through Program Analysis
Print ISBN: 978-3-030-41102-2

Electronic ISBN: 978-3-030-41103-9

Copyright Year: 2020
DOI: https://doi.org/10.1007/978-3-030-41103-9_4

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"