Technical reports

Tool support for logics of programs

Lawrence C. Paulson

November 1996, 31 pages

DOI: 10.48456/tr-406

Abstract

Proof tools must be well designed if they are to be more effective than pen and paper. Isabelle supports a range of formalisms, two of which are described (higher-order logic and set theory). Isabelle’s representation of logic is influenced by logic programming: its “logical variables” can be used to implement step-wise refinement. Its automatic proof procedures are based on search primitives that are directly available to users. While emphasizing basic concepts, the article also discusses applications such as an approach to the analysis of security protocols.

Full text

PDF (0.3 MB)
PS (0.2 MB)

BibTeX record

@TechReport{UCAM-CL-TR-406,
  author =	 {Paulson, Lawrence C.},
  title = 	 {{Tool support for logics of programs}},
  year = 	 1996,
  month = 	 nov,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-406.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-406},
  number = 	 {UCAM-CL-TR-406}
}