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...

• Type: Conference
• Year: 2005
• Where: ICFP
• Authors: Olha Shkaravska
• Keywords: ICFP 2005, Parametric Soundness Condition, Parametric Specialised Assertion, Programming Languages, Specialised Rule