Types with semantics: soundness proof assistant

10 years 11 months ago
Types with semantics: soundness proof assistant
We present a parametric Hoare-like logic for computer-aided reasoning about typeable properties of functional programs. The logic is based on the concept of a specialised assertion, which is a predicate expressing the semantics of a typing judgment in a logical framework (here higher-order logic). Replacing in a type inference rule the judgments by the appropriate specialised assertions, one obtains a specialised rule. Specialised assertions have a uniform format, and soundness proofs of specialised rules employ uniform sequences of steps for a variety of type systems. This allows to from the type system and define parametric specialised assertion and rules. Moreover, we define a parametric soundness condition for each program construct which ensures soundness of the corresponding rule. To prove soundness of the specialised rule for the concrete type system one checks the condition and instantiates the parametric rule. We consider specialised logics for "nonpure" type system...
Olha Shkaravska
Added 13 Dec 2009
Updated 13 Dec 2009
Type Conference
Year 2005
Where ICFP
Authors Olha Shkaravska
Comments (0)