Standard
Galois Connections for Recursive Types. / Al-Sibahi, Ahmad Salim; Jensen, Thomas; Møgelberg, Rasmus Ejlers; Wąsowski, Andrzej.
sFrom Lambda Calculus to Cybersecurity Through Program Analysis: Essays Dedicated to Chris Hankin on the Occasion of His Retirement. Springer VS, 2020. p. 105-131 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 12065 LNCS).
Research output: Chapter in Book/Report/Conference proceeding › Book chapter › Research › peer-review
Harvard
Al-Sibahi, AS
, Jensen, T, Møgelberg, RE & Wąsowski, A 2020,
Galois Connections for Recursive Types. in
sFrom Lambda Calculus to Cybersecurity Through Program Analysis: Essays Dedicated to Chris Hankin on the Occasion of His Retirement. Springer VS, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 12065 LNCS, pp. 105-131.
https://doi.org/10.1007/978-3-030-41103-9_4APA
Al-Sibahi, A. S.
, Jensen, T., Møgelberg, R. E., & Wąsowski, A. (2020).
Galois Connections for Recursive Types. In
sFrom Lambda Calculus to Cybersecurity Through Program Analysis: Essays Dedicated to Chris Hankin on the Occasion of His Retirement (pp. 105-131). Springer VS. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) Vol. 12065 LNCS
https://doi.org/10.1007/978-3-030-41103-9_4Vancouver
Al-Sibahi AS
, Jensen T, Møgelberg RE, Wąsowski A.
Galois Connections for Recursive Types. In sFrom Lambda Calculus to Cybersecurity Through Program Analysis: Essays Dedicated to Chris Hankin on the Occasion of His Retirement. Springer VS. 2020. p. 105-131. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 12065 LNCS).
https://doi.org/10.1007/978-3-030-41103-9_4Author
Al-Sibahi, Ahmad Salim ; Jensen, Thomas ; Møgelberg, Rasmus Ejlers ; Wąsowski, Andrzej. / Galois Connections for Recursive Types. sFrom Lambda Calculus to Cybersecurity Through Program Analysis: Essays Dedicated to Chris Hankin on the Occasion of His Retirement. Springer VS, 2020. pp. 105-131 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 12065 LNCS).
Bibtex
@inbook{ace27b3b769948b38024b7dcb1899847,
title = "Galois Connections for Recursive Types",
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.",
author = "Al-Sibahi, {Ahmad Salim} and Thomas Jensen and M{\o}gelberg, {Rasmus Ejlers} and Andrzej W{\c a}sowski",
year = "2020",
doi = "10.1007/978-3-030-41103-9_4",
language = "English",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer VS",
pages = "105--131",
booktitle = "sFrom Lambda Calculus to Cybersecurity Through Program Analysis",
}
RIS
TY - CHAP
T1 - Galois Connections for Recursive Types
AU - Al-Sibahi, Ahmad Salim
AU - Jensen, Thomas
AU - Møgelberg, Rasmus Ejlers
AU - Wąsowski, Andrzej
PY - 2020
Y1 - 2020
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=85079614059&partnerID=8YFLogxK
U2 - 10.1007/978-3-030-41103-9_4
DO - 10.1007/978-3-030-41103-9_4
M3 - Book chapter
AN - SCOPUS:85079614059
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 105
EP - 131
BT - sFrom Lambda Calculus to Cybersecurity Through Program Analysis
PB - Springer VS
ER -
