Proving Theorems about LISP Functions

DOI10.1145/321864.321875zbMath0338.68014OpenAlexW1988651604MaRDI QIDQ4105761

Robert S. Boyer, J. Strother Moore

Publication date: 1975

Published in: Journal of the ACM (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/321864.321875

Mathematics Subject Classification ID

Related Items (25)

A two-valued logic for properties of strict functional programs allowing partial functions ⋮ The McCarthy's recursion induction principle: oldy but goody ⋮ Unnamed Item ⋮ Trends in trends in functional programming 1999/2000 versus 2007/2008 ⋮ Mechanizing structural induction. I: Formal system ⋮ Mechanizing structural induction. II: Strategies ⋮ Tactics for mechanized reasoning: a commentary on Milner (1984) ‘The use of machines to assist in rigorous proof’ ⋮ Function extraction ⋮ Unnamed Item ⋮ An ACL2 Tutorial ⋮ Unnamed Item ⋮ Manipulating accumulative functions by swapping call-time and return-time computations ⋮ Unfolding--definition--folding, in this order, for avoiding unnecessary variables in logic programs ⋮ A class of functions synthesized from a finite number of examples and a lisp program scheme ⋮ A partial evaluator, and its use as a programming tool ⋮ Non-resolution theorem proving ⋮ Milestones from the Pure Lisp Theorem Prover to ACL2 ⋮ A pragmatic approach to resolution-based theorem proving ⋮ Towards the automation of set theory and its logic ⋮ Current methods for proving program correctness ⋮ Informational logic for automated reasoning ⋮ Proofs by induction in equational theories with constructors ⋮ Some fundamental algebraic tools for the semantics of computation. I. Comma categories, colimits, signatures and theories ⋮ Proof-producing translation of higher-order logic into pure and stateful ML ⋮ A selected bibliography on constructive mathematics, intuitionistic type theory and higher order deduction

This page was built for publication: Proving Theorems about LISP Functions