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
 B. E. Aydemir, A. Bohannon, M. Fairbairn, J. N. Foster, B. C. Pierce, P. Sewell, D. Vytiniotis, G. Washburn, S. Weirich, and S. Zdancewic. Mechanized metatheory for the masses: The POPLmark challenge. In Theorem Proving in Higher Order Logics: 18th International Conference, number 3603 in LNCS, pages 50-65. Springer, 2005.
 A. Church. A formulation of the simple theory of types. J. of Symbolic Logic, 5:56-68, 1940.
 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.
 A. Gacek. The Abella interactive theorem prover (system description). In A. Armando, P. Baumgartner, and G. Dowek, editors, Fourth International Joint Conference on Automated Reasoning, volume 5195 of LNCS, pages 154-161. Springer, 2008.
 A. Gacek et al. The Abella system and homepage. http://abella-prover.org/, 2013.
 A. Gacek, D. Miller, and G. Nadathur. Nominal abstraction. Information and Computation, 209(1):48- 73, 2011.
 A. Gacek, D. Miller, and G. Nadathur. A two-level logic approach to reasoning about computations. J. of Automated Reasoning, 49(2):241-273, 2012.
 C. Liang and D. Miller. Focusing and polarization in linear, intuitionistic, and classical logics. Theoretical Computer Science, 410(46):4747-4768, 2009.
6See the theorem same_paths_joinable in the Abella development in Appendix D.
 R. McDowell and D. Miller. Cut-elimination for a logic with definitions and induction. Theoretical Computer Science, 232:91-119, 2000.