Reasoning About Higher-Order Relational Specifications

Conference object, Preprint English OPEN
Wang, Yuting ; Chaudhuri, Kaustuv ; Gacek, Andrew ; Nadathur, Gopalan (2013)
  • Publisher: ACM
  • Related identifiers: doi: 10.1145/2505879.2505889
  • Subject: [ 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... View more
  • References (23)
    23 references, page 1 of 3

    [1] The Abella prover, 2013. Available at

    [2] B. Accattoli. Proof pearl: Abella formalization of lambda calculus cube property. In C. Hawblitzel and D. Miller, editors, Second International Conference on Certified Programs and Proofs, volume 7679 of LNCS, pages 173-187. Springer, 2012.

    [3] J. Cheney and C. Urban. Alpha-Prolog: A logic programming language with names, binding, and alpha-equivalence. In B. Demoen and V. Lifschitz, editors, Logic Programming, 20th International Conference, volume 3132 of LNCS, pages 269-283. Springer, 2004.

    [4] J. Cheney and C. Urban. Nominal logic programming. ACM Trans. Program. Lang. Syst., 30(5):1-47, 2008.

    [5] A. Church. A formulation of the simple theory of types. J. of Symbolic Logic, 5:56-68, 1940.

    [6] N. G. de Bruijn. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser Theorem. Indagationes Mathematicae, 34(5):381-392, 1972.

    [7] A. Felty and D. Miller. Encoding a dependent-type λ-calculus in a logic programming language. In M. Stickel, editor, Proceedings of the 1990 Conference on Automated Deduction, volume 449 of LNAI, pages 221-235. Springer, 1990.

    [8] A. Felty and A. Momigliano. Hybrid: A definitional two-level approach to reasoning with higher-order abstract syntax. J. of Automated Reasoning, 48:43-105, 2012.

    [9] A. Gacek. A Framework for Specifying, Prototyping, and Reasoning about Computational Systems. PhD thesis, University of Minnesota, 2009.

    [10] A. Gacek, D. Miller, and G. Nadathur. Nominal abstraction. Information and Computation, 209(1):48-73, 2011.

  • Metrics
    No metrics available
Share - Bookmark