Reasoning About Higher-Order Relational Specifications

Conference object, Preprint English OPEN
Wang, Yuting; Chaudhuri, Kaustuv; Gacek, Andrew; Nadathur, Gopalan;
(2013)
  • Publisher: ACM
  • Identifiers: doi: 10.1145/2505879.2505889
  • Subject: [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] | Computer Science - Logic in Computer Science | ACM: F.: Theory of Computation/F.4: MATHEMATICAL LOGIC AND FORMAL LANGUAGES/F.4.1: Mathematical Logic/F.4.1.7: Proof theory | ACM: F.: Theory of Computation/F.3: LOGICS AND MEANINGS OF PROGRAMS/F.3.1: Specifying and Verifying and Reasoning about Programs/F.3.1.5: Specification techniques

International audience; The logic of hereditary Harrop formulas (HH) has proven useful for specifying a wide range of formal systems. This logic includes a form of hypothetical judgment that leads to dynamically changing sets of assumptions and that is key to encoding s... View more
Share - Bookmark