Reasoning About CBV Functional Programs in Isabelle/HOL

John Longley, Randy Pollack

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

We consider the old problem of proving that a computer program meets some specification. By proving, we mean machine checked proof in some formal logic. The programming language we choose to work with is a call by value functional language, essentially the functional core of Standard ML (SML). In future work we hope to add exceptions, then references and I/O to the language.
Original languageEnglish
Title of host publicationTheorem Proving in Higher Order Logics
Subtitle of host publication17th International Conference, TPHOLs 2004, Park City, Utah, USA, September 14-17, 2004. Proceedings
EditorsKonrad Slind, Annette Bunker, Ganesh Gopalakrishnan
PublisherSpringer
Pages201-216
Number of pages16
ISBN (Electronic)978-3-540-30142-4
ISBN (Print)978-3-540-23017-5
DOIs
Publication statusPublished - 2004

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg
Volume3223
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Fingerprint

Dive into the research topics of 'Reasoning About CBV Functional Programs in Isabelle/HOL'. Together they form a unique fingerprint.

Cite this