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 条

[31] The cache behaviour of large lazy functional programs on stock hardware
Nethercote, N
Mycroft, A
ACM SIGPLAN NOTICES, 2003, 38 (02) : 44 - 55
[32] The results of: Profiling large-scale lazy functional programs
Jarvis, SA
Morgan, RG
IMPLEMENTATION OF FUNCTIONAL LANGUAGES, 1997, 1268 : 200 - 221
[33] Dynamic slicing of lazy functional programs based on redex trails
DIA, Technical University of Madrid, Campus de Montegancedo s/n, 28660 Boadilla del Monte, Spain
不详
High Order Symbol Comput, 2008, 1-2 (147-192):
[34] Testing and tracing lazy functional programs using QuickCheck and Hat
Claessen, K
Runciman, C
Chitil, O
Hughes, J
Wallace, M
ADVANCED FUNCTIONAL PROGRAMMING, 2003, 2638 : 59 - 99
[35] How to do Proofs Practically Proving Properties about Effectful Programs' Results (Functional Pearl)
Jacobs, Koen
Nuyts, Andreas
Devriese, Dominique
TYDE '19: PROCEEDINGS OF THE 4TH ACM SIGPLAN INTERNATIONAL WORKSHOP ON TYPE-DRIVEN DEVELOPMENT, 2019, : 1 - 13
[36] Theorem proving using lazy proof explication
Flanagan, C
Joshi, R
Ou, XM
Saxe, JB
COMPUTER AIDED VERIFICATION, 2003, 2725 : 355 - 367
[37] PROVING TERMINATION PROPERTIES OF PROLOG PROGRAMS - A SEMANTIC APPROACH
BAUDINET, M
JOURNAL OF LOGIC PROGRAMMING, 1992, 14 (1-2): : 1 - 29
[38] Proving LTL Properties of Bitvector Programs and Decompiled Binaries
Liu, Yuandong Cyrus
Pang, Chengbin
Dietsch, Daniel
Koskinen, Eric
Le, Ton-Chanh
Portokalidis, Georgios
Xu, Jun
PROGRAMMING LANGUAGES AND SYSTEMS, APLAS 2021, 2021, 13008 : 285 - 304
[39] PROVING PROPERTIES OF PASCAL PROGRAMS IN MIZAR-2
RUDNICKI, P
DRABENT, W
ACTA INFORMATICA, 1985, 22 (03) : 311 - 331
[40] The correctness of a higher-order lazy functional language implementation: An exercise in mechanical theorem proving
Mintchev, S
Lester, D
HIGHER-ORDER ALGEBRA, LOGIC, AND TERM REWRITING, 1996, 1074 : 144 - 162

← 1 2 3 4 5 →