Proving Theorems about LISP Functions

Cited in

(26)

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

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4105761)