ITU

Galois Connections for Recursive Types

Research output: Conference Article in Proceeding or Book/Report chapter › Book chapter › Research › peer-review

Standard

Galois Connections for Recursive Types. / Al-Sibahi, Ahmad Salim; Jensen, Thomas P.; Møgelberg, Rasmus Ejlers; Wasowski, Andrzej.

From Lambda Calculus to Cybersecurity Through Program Analysis. Springer, 2020. p. 105-131 (Lecture Notes in Computer Science, Vol. 12065).

Research output: Conference Article in Proceeding or Book/Report chapter › Book chapter › Research › peer-review

Harvard

Al-Sibahi, AS, Jensen, TP, Møgelberg, RE & Wasowski, A 2020, Galois Connections for Recursive Types. in From Lambda Calculus to Cybersecurity Through Program Analysis. Springer, Lecture Notes in Computer Science, vol. 12065, pp. 105-131. https://doi.org/10.1007/978-3-030-41103-9_4

APA

Al-Sibahi, A. S., Jensen, T. P., Møgelberg, R. E., & Wasowski, A. (2020). Galois Connections for Recursive Types. In From Lambda Calculus to Cybersecurity Through Program Analysis (pp. 105-131). Springer. Lecture Notes in Computer Science Vol. 12065 https://doi.org/10.1007/978-3-030-41103-9_4

Vancouver

Al-Sibahi AS, Jensen TP, Møgelberg RE, Wasowski A. Galois Connections for Recursive Types. In From Lambda Calculus to Cybersecurity Through Program Analysis. Springer. 2020. p. 105-131. (Lecture Notes in Computer Science, Vol. 12065). https://doi.org/10.1007/978-3-030-41103-9_4

Author

Al-Sibahi, Ahmad Salim ; Jensen, Thomas P. ; Møgelberg, Rasmus Ejlers ; Wasowski, Andrzej. / Galois Connections for Recursive Types. From Lambda Calculus to Cybersecurity Through Program Analysis. Springer, 2020. pp. 105-131 (Lecture Notes in Computer Science, Vol. 12065).

Bibtex

@inbook{404d2e4bd22c43e7b0ea8839802df00c,
title = "Galois Connections for Recursive Types",
abstract = "Building a static analyses 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.",
author = "Al-Sibahi, {Ahmad Salim} and Jensen, {Thomas P.} and M{\o}gelberg, {Rasmus Ejlers} and Andrzej Wasowski",
year = "2020",
doi = "10.1007/978-3-030-41103-9_4",
language = "English",
isbn = "978-3-030-41102-2",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "105--131",
booktitle = "From Lambda Calculus to Cybersecurity Through Program Analysis",
address = "Germany",

}

RIS

TY - CHAP

T1 - Galois Connections for Recursive Types

AU - Al-Sibahi, Ahmad Salim

AU - Jensen, Thomas P.

AU - Møgelberg, Rasmus Ejlers

AU - Wasowski, Andrzej

PY - 2020

Y1 - 2020

N2 - Building a static analyses 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.

AB - Building a static analyses 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.

U2 - 10.1007/978-3-030-41103-9_4

DO - 10.1007/978-3-030-41103-9_4

M3 - Book chapter

SN - 978-3-030-41102-2

T3 - Lecture Notes in Computer Science

SP - 105

EP - 131

BT - From Lambda Calculus to Cybersecurity Through Program Analysis

PB - Springer

ER -

ID: 85385935