Reasoning About Higher-Order Relational Specifications
Conference object, Preprint
- Publisher: ACM
[ INFO.INFO-LO ] Computer Science [cs]/Logic in Computer Science [cs.LO] | ACM : F.: Theory of Computation/F.4: MATHEMATICAL LOGIC AND FORMAL LANGUAGES/F.4.1: Mathematical Logic/F.4.1.7: Proof theory | Computer Science - Logic in Computer Science | 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...