Polymorphism and separation in hoare type theory

In previous work, we proposed a Hoare Type Theory (HTT) which combines effectful higher-order functions, dependent types and Hoare Logic specifications into a unified framework. However, the framework did not support polymorphism, and failed to provide a modular treatment of state in specifications. In this paper, we address these shortcomings by showing that the addition of polymorphism alone is sufficient for capturing modular state specifications in the style of Separation Logic. Furthermore, we argue that polymorphism is an essential ingredient of the extension, as the treatment of higher-order functions requires operations not encodable via the spatial connectives of Separation Logic. Categories and Subject Descriptors F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs General Terms Languages, Verification Keywords Type Theory, Hoare Logic, Separation Logic

• Type: Conference
• Year: 2006
• Where: ICFP
• Authors: Aleksandar Nanevski, Greg Morrisett, Lars Birkedal
• Keywords: Hoare Logic, Hoare Type Theory, ICFP 2006, Programming Languages, Separation Logic