Galois Connections for Recursive Types

Ahmad Salim Al-Sibahi, Thomas P. Jensen, Rasmus Ejlers Møgelberg, Andrzej Wasowski

Research output: Conference Article in Proceeding or Book/Report chapterBook chapterResearchpeer-review


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.
Original languageEnglish
Title of host publicationFrom Lambda Calculus to Cybersecurity Through Program Analysis
Publication date2020
ISBN (Print)978-3-030-41102-2
ISBN (Electronic)978-3-030-41103-9
Publication statusPublished - 2020
SeriesLecture Notes in Computer Science


  • Static Analysis
  • Abstract Domains
  • Recursive Types
  • Higher-Order Functions
  • Modular Design


Dive into the research topics of 'Galois Connections for Recursive Types'. Together they form a unique fingerprint.

Cite this