Welcome to the DECLARE home page.  DECLARE was a theorem proving shell for higher order logic, based around a simple proof outlining language.  It is best documented in my thesis.  You may see some historical background on the TkHOL home page. You may like to read a presentation outlining the basic idea of declarative theorem proving, entitled Three Tactic Theorem Proving. presented at TPHOLs 99 in Nice, France. There is an extensive description of some proofs I did about the Java Language using DECLARE, also documented in the University of Cambridge Technical Report Proving Java Type Soundness.

See Also

• John Harrison's 1997 Technical Report on Proof Style
• Here are the slides from a talk I gave to the Automated Reasoning Group here entitled "DECLARE: A Prototype Declarative Proof System".