"Logic and Computation: Interactive Proof with Cambridge LCF (Cambridge Tracts in Theoretical Computer Science)" - читать интересную книгу автора (Lawrence C. Paulson)