From 3 February to 8 February 2008, the Dagstuhl Seminar 08061 State" Conference and Research Center (IBFI), Schloss Dagstuhl. 45 researchers, with interests and expertise in ...
Amal Ahmed, Nick Benton, Martin Hofmann, Greg Morr...
Higher-order logic with shallow type class polymorphism is widely used as a specification formalism. Its polymorphic entities (types, operators, axioms) can easily be equipped wit...
This work presents a framework for fusing flow analysis and theorem proving called logic-flow analysis (LFA). The framework itthe reduced product of two abstract interpretations: ...
This paper describes a type system that is capable of expressing and enforcing immutability constraints. The specific constraint exis that the abstract state of the object to whi...