Sciweavers

Free Online Productivity Tools i2Speak i2Symbol i2OCR iTex2Img iWeb2Print iWeb2Shot i2Type iPdf2Split iPdf2Merge i2Bopomofo i2Arabic i2Style i2Image i2PDF iLatex2Rtf Sci2ools

10

TPHOL
2005
IEEE

favoriteEmaildiscussreport

93views Automated Reasoning» more TPHOL 2005»

Proof Pearl: Using Combinators to Manipulate let-Expressions in Proof

13 years 10 months ago

Proof Pearl: Using Combinators to Manipulate let-Expressions in Proof

Download nicta.com.au

We discuss methods for dealing eﬀectively with let-bindings in proofs. Our contribution is a small set of unconditional rewrite rules, found by the bracket abstraction translation from the λ-calculus to combinators. This approach copes with the usual HOL encodings of paired ion, ensures that bound variable names are preserved, and uses only conventional simpliﬁcation technology.

Michael Norrish, Konrad Slind

Real-time Traffic

Artificial Intelligence | Bracket Abstraction Translation | TPHOL 2005 | Unconditional Rewrite Rules | Usual Hol Encodings |

claim paper

Related Content

» Leveraging Interpolant Strength in Model Checking

» Towards performing everyday manipulation activities

» Building Certified Static Analysers by Modular Construction of Wellfounded Lattices

» Engineering formal metatheory

» Remote Collaboration Using Augmented Reality Videoconferencing

» Teaching Binary Tree Algorithms through Visual Programming

» Fable A Language for Enforcing Userdefined Security Policies

» A Resource Framework for Quantum Shannon Theory

Post Info
More Details (n/a)

Added	25 Jun 2010
Updated	25 Jun 2010
Type	Conference
Year	2005
Where	TPHOL
Authors	Michael Norrish, Konrad Slind

Comments (0)