Proving Properties of Lazy Functional Programs with SPARKLE

被引：0
|
作者：
de Mol, Maarten [1 ]
van Eekelen, Marko [1 ]
Plasmeijer, Rinus [1 ]
机构：
[1] Radboud Univ Nijmegen, Inst Comp & Informat Sci, Nijmegen, Netherlands
来源：
CENTRAL EUROPEAN FUNCTIONAL PROGRAMMING SCHOOL | 2008年 / 5161卷
关键词：
D O I：
暂无
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
This tutorial paper aims to provide the necessary expertise for working with the proof assistant SPARKLE, which is dedicated to the lazy functional programming language CLEAN. The purpose of a proof assistant is to use formal reasoning to verify the correctness of a computer program. Formal reasoning is very powerful, but is unfortunately also difficult to carry out. Due to their mathematical nature, functional programming languages are well suited for formal reasoning. Moreover, SPARKLE offers specialized support for reasoning about CLEAN, and is integrated into its official development environment. These factors make SPARKLE a proof assistant that is relatively easy to use. This paper provides both theoretical background for formal reasoning, and detailed information about using SPARKLE in practice. Special attention will be given to specific aspects that arise due to lazy evaluation and due to the existence of strictness annotations. Several assignments are included in the text, which provide hands-on experience with SPARKLE.
引用
收藏
页码：41 / 86
页数：46
相关论文
共 50 条
  • [1] Theorem proving for functional programmers - SPARKLE: A functional theorem prover
    de Mol, M
    van Eekelen, M
    Plasmeijer, R
    IMPLEMENTATION OF FUNCTIONAL LANGUAGES, 2002, 2312 : 55 - 71
  • [2] LAZY DEBUGGING OF LAZY FUNCTIONAL PROGRAMS
    SNYDER, RM
    NEW GENERATION COMPUTING, 1990, 8 (02) : 139 - 161
  • [3] Proving properties of functional programs by equality saturation
    S. A. Grechanik
    Programming and Computer Software, 2015, 41 : 149 - 161
  • [4] Proving properties of functional programs by equality saturation
    Grechanik, S. A.
    PROGRAMMING AND COMPUTER SOFTWARE, 2015, 41 (03) : 149 - 161
  • [5] Specialization of lazy functional logic programs
    Alpuente, M
    Falaschi, M
    Julian, P
    Vidal, G
    ACM SIGPLAN NOTICES, 1997, 32 (12) : 151 - 162
  • [6] Axioms for strict and lazy functional programs
    Stärk, RE
    ANNALS OF PURE AND APPLIED LOGIC, 2005, 133 (1-3) : 293 - 318
  • [7] AUTOMATIC PARALLELIZATION OF LAZY FUNCTIONAL PROGRAMS
    HOGEN, G
    KINDLER, A
    LOOGEN, R
    LECTURE NOTES IN COMPUTER SCIENCE, 1992, 582 : 254 - 268
  • [8] Lazy functional programs in a concurrent environment
    Feijs, LMG
    Reniers, MA
    COMPUTER JOURNAL, 1997, 40 (09): : 572 - 584
  • [9] Proving failure in functional logic programs
    López-Fraguas, FJ
    Sánchez-Hernández, J
    COMPUTATIONAL LOGIC - CL 2000, 2000, 1861 : 179 - 193
  • [10] A slicing tool for lazy functional logic programs
    Ochoa, Claudio
    Silva, Josep
    Vidal, German
    LOGICS IN ARTIFICIAL INTELLIGENCE, PROCEEDINGS, 2006, 4160 : 498 - 501
12345