Pages that link to "Item:Q4105761"

The following pages link to Proving Theorems about LISP Functions (Q4105761):

Displaying 26 items.

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