This paper presents a translation from Gospel-annotated OCaml programs into Viper, an intermediate verification language featuring Separation Logic. The practical goal is to extend Cameleer with a new back-end to prove heap-dependent OCaml programs. The logical specification of such OCaml programs is described using an extension of Gospel to support Separation Logic features, which we describe in the paper.

翻译：本文提出了一种将Gospel注解的OCaml程序转换为Viper（一种支持分离逻辑的中间验证语言）的方法。其实际目标是通过为Cameleer工具添加新的后端来验证堆依赖型OCaml程序。此类OCaml程序的逻辑规范采用扩展版Gospel进行描述，该扩展支持分离逻辑特性，相关技术细节将在本文中阐述。