A Proof-theoretic Characterization of Independence in Type Theory

Yuting Wang 1 Kaustuv Chaudhuri 2
2 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France, X - École polytechnique, CNRS - Centre National de la Recherche Scientifique : UMR7161
Abstract : For λ-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 τ 1 → τ 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.
Type de document :
Communication dans un congrès
Thorsten Altenkirch. 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015), Jul 2015, Warsaw, Poland. Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 38, pp.332--346, Leibniz International Proceedings in Informatics (LIPIcs). 〈http://rdp15.mimuw.edu.pl/index.php?site=tlca〉. 〈10.4230/LIPIcs.TLCA.2015.332〉
Liste complète des métadonnées

Littérature citée [16 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01222743
Contributeur : Kaustuv Chaudhuri <>
Soumis le : lundi 2 novembre 2015 - 14:16:30
Dernière modification le : jeudi 10 mai 2018 - 02:06:28
Document(s) archivé(s) le : mercredi 3 février 2016 - 10:26:19

Fichier

p00-wang.pdf
Fichiers éditeurs autorisés sur une archive ouverte

Licence


Distributed under a Creative Commons Paternité - Pas de modifications 4.0 International License

Identifiants

Citation

Yuting Wang, Kaustuv Chaudhuri. A Proof-theoretic Characterization of Independence in Type Theory. Thorsten Altenkirch. 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015), Jul 2015, Warsaw, Poland. Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 38, pp.332--346, Leibniz International Proceedings in Informatics (LIPIcs). 〈http://rdp15.mimuw.edu.pl/index.php?site=tlca〉. 〈10.4230/LIPIcs.TLCA.2015.332〉. 〈hal-01222743〉

Partager

Métriques

Consultations de la notice

322

Téléchargements de fichiers

56