A Proof-theoretic Characterization of Independence in Type Theory

Authors Yuting Wang, Kaustuv Chaudhuri



PDF
Thumbnail PDF

File

LIPIcs.TLCA.2015.332.pdf
  • Filesize: 0.58 MB
  • 15 pages

Document Identifiers

Author Details

Yuting Wang
Kaustuv Chaudhuri

Cite AsGet BibTex

Yuting Wang and Kaustuv Chaudhuri. A Proof-theoretic Characterization of Independence in Type Theory. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 332-346, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
https://doi.org/10.4230/LIPIcs.TLCA.2015.332

Abstract

For lambda-terms constructed freely from a type signature in a type theory such as LF, there is a simple inductive subordination relation that is used to control type-formation. There is a related—but not precisely complementary—notion of independence that asserts that the inhabitants of the function space tau_1 --> tau_2 depend vacuously on their arguments. Independence has many practical reasoning applications in logical frameworks, such as pruning variable dependencies or transporting theorems and proofs between type signatures. However, independence is usually not given a formal interpretation. Instead, it is generally implemented in an ad hoc and uncertified fashion. We propose a formal definition of independence and give a proof-theoretic characterization of it by: (1) representing the inference rules of a given type theory and a closed type signature as a theory of intuitionistic predicate logic, (2) showing that typing derivations in this signature are adequately represented by a focused sequent calculus for this logic, and (3) defining independence in terms of strengthening for intuitionistic sequents. This scheme is then formalized in a meta-logic, called G, that can represent the sequent calculus as an inductive definition, so the relevant strengthening lemmas can be given explicit inductive proofs. We present an algorithm for automatically deriving the strengthening lemmas and their proofs in G.
Keywords
  • subordination; independence; sequent calculus; focusing; strengthening

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads

References

  1. David Baelde, Kaustuv Chaudhuri, Andrew Gacek, Dale Miller, Gopalan Nadathur, Alwen Tiu, and Yuting Wang. Abella: A system for reasoning about relational specifications. Journal of Formalized Reasoning, 7(2), 2014. Google Scholar
  2. Amy Felty and Dale Miller. Encoding a dependent-type λ-calculus in a logic programming language. In Conference on Automated Deduction, volume 449 of LNAI, pages 221-235. Springer, 1990. Google Scholar
  3. Andrew Gacek. A Framework for Specifying, Prototyping, and Reasoning about Computational Systems. PhD thesis, University of Minnesota, 2009. Google Scholar
  4. Andrew Gacek, Dale Miller, and Gopalan Nadathur. Nominal abstraction. Information and Computation, 209(1):48-73, 2011. Google Scholar
  5. Andrew Gacek, Dale Miller, and Gopalan Nadathur. A two-level logic approach to reasoning about computations. J. of Automated Reasoning, 49(2):241-273, 2012. Google Scholar
  6. Robert Harper, Furio Honsell, and Gordon Plotkin. A framework for defining logics. Journal of the ACM, 40(1):143-184, 1993. Google Scholar
  7. Robert Harper and Daniel R. Licata. Mechanizing metatheory in a logical framework. Journal of Functional Programming, 17(4-5):613-673, July 2007. Google Scholar
  8. Raymond McDowell and Dale Miller. Cut-elimination for a logic with definitions and induction. Theoretical Computer Science, 232:91-119, 2000. Google Scholar
  9. Dale Miller. Unification under a mixed prefix. J. of Symbolic Comp., 14(4):321-358, 1992. Google Scholar
  10. Dale Miller and Gopalan Nadathur. Programming with Higher-Order Logic. Cambridge University Press, June 2012. Google Scholar
  11. Frank Pfenning and Carsten Schürmann. System description: Twelf - A meta-logical framework for deductive systems. In 16th Conf. on Automated Deduction (CADE), number 1632 in LNAI, pages 202-206. Springer, 1999. Google Scholar
  12. Brigitte Pientka and Joshua Dunfield. Beluga: A framework for programming and reasoning with deductive systems (system description). In Fifth International Joint Conference on Automated Reasoning, number 6173 in LNCS, pages 15-21, 2010. Google Scholar
  13. Zachary Snow, David Baelde, and Gopalan Nadathur. A meta-programming approach to realizing dependently typed logic programming. In ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP), pages 187-198, 2010. Google Scholar
  14. Mary Southern and Kaustuv Chaudhuri. A two-level logic approach to reasoning about typed specification languages. In 34th Int. Conf. on Foundations of Software Technology and Theoretical Computer Science (FSTTCS), volume 29 of Leibniz International Proceedings in Informatics (LIPIcs), pages 557-569, December 2014. Google Scholar
  15. Roberto Virga. Higher-order Rewriting with Dependent Types. PhD thesis, Carnegie Mellon University, 1999. Google Scholar
  16. Yuting Wang, Kaustuv Chaudhuri, Andrew Gacek, and Gopalan Nadathur. Reasoning about higher-order relational specifications. In 15th International Symposium on Princples and Practice of Declarative Programming (PPDP), pages 157-168, September 2013. Google Scholar
  17. Kevin Watkins, Iliano Cervesato, Frank Pfenning, and David Walker. A concurrent logical framework I: Judgments and properties. Technical Report CMU-CS-02-101, Carnegie Mellon University, 2003. Revised, May 2003. Google Scholar
  18. The Abella web-site. http://abella-prover.org/, 2015.