Proof Pearl: Looping Around the Orbit

Steven Obua

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

Abstract / Description of output

We reexamine the While combinator of higher-order logic (HOL) and introduce the For combinator. We argue that both combinators should be part of the toolbox of any HOL practitioner, not only because they make efficient computations within HOL possible, but also because they facilitate elegant inductive reasoning about loops. We present two examples that support this argument.
Original languageEnglish
Title of host publicationTheorem Proving in Higher Order Logics
Subtitle of host publication20th International Conference, TPHOLs 2007, Kaiserslautern, Germany, September 10-13, 2007. Proceedings
EditorsKlaus Schneider, Jens Brandt
PublisherSpringer Berlin Heidelberg
Number of pages9
ISBN (Electronic)978-3-540-74591-4
ISBN (Print)978-3-540-74590-7
Publication statusPublished - 2007

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg
ISSN (Print)0302-9743


Dive into the research topics of 'Proof Pearl: Looping Around the Orbit'. Together they form a unique fingerprint.

Cite this