Constructive Galois connections: taming the Galois connection framework for mechanized metatheory
Abstract
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.
Document Details
- Document Type
- Pub Defense Publication
- Publication Date
- Sep 04, 2016
- Source ID
- 10.1145/3022670.2951934
Entities
People
- David Darais
- David Van Horn
Organizations
- Defense Advanced Research Projects Agency
- University of Maryland