48 citations · 122 across the 17 of their papers we have counts for
Showing 2015Show all
2 papers · 1 filter
cs.PL2015
Constructive Galois Connections: Taming the Galois Connection Framework for Mechanized Metatheory
David Darais, David Van Horn
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…
cs.PL2015
Mechanically Verified Calculational Abstract Interpretation
David Darais, David Van Horn
Calculational abstract interpretation, long advocated by Cousot, is a technique for deriving correct-by-construction abstract interpreters from the formal semantics of programming…