Write a Blog >>
ICFP 2016
Sun 18 - Sat 24 September 2016 Nara, Japan
Tue 20 Sep 2016 16:50 - 17:15 at Noh Theater - Session 8 Chair(s): Scott Owens

Galois connections are a foundational tool for structuring abstraction in
semantics and their use lies at the heart of the theory of abstract
interpretation. Yet, mechanization of Galois connections remains limited to
restricted modes of use, preventing their general application in mechanized
metatheory and certified programming.

This paper presents constructive Galois connections, a variant of Galois
connections that is effective both on paper and in proof assistants; is
complete with respect to a large subset of classical Galois connections; and
enables more general reasoning principles, including the "calculational" style
advocated by Cousot.

To design constructive Galois connection we identify a restricted mode of use
of classical ones which is both general and amenable to mechanization in
dependently-typed functional programming languages. Crucial to our metatheory
is the addition of monadic structure to Galois connections to control a
"specification effect". Effectful calculations may reason classically, while
pure calculations have extractable computational content. Explicitly moving
between the worlds of specification and implementation is enabled by our

To validate our approach, we provide two case studies in mechanizing existing
proofs from the literature: one uses calculational abstract interpretation to
design a static analyzer, the other forms a semantic basis for gradual typing.
Both mechanized proofs closely follow their original paper-and-pencil
counterparts, employ reasoning principles not captured by previous
mechanization approaches, support the extraction of verified algorithms, and
are novel.

Tue 20 Sep
Times are displayed in time zone: Osaka, Sapporo, Tokyo change

16:50 - 17:40: Session 8Research Papers at Noh Theater
Chair(s): Scott OwensUniversity of Kent, UK
16:50 - 17:15
Constructive Galois Connections: Taming the Galois Connection Framework for Mechanized Metatheory
Research Papers
David DaraisUniversity of Maryland, USA, David Van HornUniversity of Maryland, USA
17:15 - 17:40
An Abstract Memory Functor for Verified C Static Analyzers
Research Papers
Sandrine BlazyUniversity of Rennes 1, France, Vincent LaporteIMDEA Software Institute, Spain, David PichardieENS Rennes, France