Formal methods within a totally functional approach to programming

Bailes, P. A. and Kemp, C. J. M. (2003). Formal methods within a totally functional approach to programming. In: B. Aichernig and T. Maibaum, Lecture Notes in Computer Science: Formal Methods at the Crossroads: From Panacea to Foundational Support. The Tenth Anniversary Colloquium of UNU/IIST, Lisbon, Portugal, (287-307). 18-20 March, 2002.

Attached Files (Some files may be inaccessible until you login with your UQ eSpace credentials)
Name Description MIMEType Size Downloads
Formal_methods_within_a_totally.pdf Formal_methods_within_a_totally.pdf application/pdf 214.95KB 0

Author Bailes, P. A.
Kemp, C. J. M.
Title of paper Formal methods within a totally functional approach to programming
Conference name The Tenth Anniversary Colloquium of UNU/IIST
Conference location Lisbon, Portugal
Conference dates 18-20 March, 2002
Proceedings title Lecture Notes in Computer Science: Formal Methods at the Crossroads: From Panacea to Foundational Support   Check publisher's open access policy
Journal name Formal Methods At the Crossroads: From Panacea to Foundational Support   Check publisher's open access policy
Place of Publication Berlin
Publisher Springer
Publication Year 2003
Sub-type Fully published paper
Open Access Status File (Author Post-print)
ISBN 978-3-540-20527-2
ISSN 0302-9743
Editor B. Aichernig
T. Maibaum
Volume 2757
Start page 287
End page 307
Total pages 11
Language eng
Abstract/Summary Taking functional programming to its extremities in search of simplicity still requires integration with other development (e.g. formal) methods. Induction is the key to deriving and verifying functional programs, but can be simplified through packaging proofs with functions, particularly folds, on data (structures). Totally Functional Programming avoids the complexities of interpretation by directly representing data (structures) as platonic combinators - the functions characteristic to the data. The link between the two simplifications is that platonic combinators are a kind of partially-applied fold, which means that platonic combinators inherit fold-theoretic properties, but with some apparent simplifications due to the platonic combinator representation. However, despite observable behaviour within functional programming that suggests that TFP is widely-applicable, significant work remains before TFP as such could be widely adopted.
Subjects 080308 Programming Languages
Keyword Computer Science, Theory & Methods
Q-Index Code E1
Q-Index Status Provisional Code
Institutional Status Unknown

 
Versions
Version Filter Type
Citation counts: TR Web of Science Citation Count  Cited 1 times in Thomson Reuters Web of Science Article | Citations
Scopus Citation Count Cited 1 times in Scopus Article | Citations
Google Scholar Search Google Scholar
Created: Tue, 14 Aug 2007, 00:08:53 EST