What term assignments can do for focusing

Guillaume Munch-Maccagnoni 1, 2
1 GALLINETTE - Gallinette : vers une nouvelle génération d'assistant à la preuve
Inria Rennes – Bretagne Atlantique , LS2N - Laboratoire des Sciences du Numérique de Nantes
Abstract : Describing proof systems as type systems for term calculi has a crucial consequence for their study: because terms bear the burden of reflecting the structure of the proofs, traditional restrictions on the shape of the derivations meant to make this structure appear are no longer useful. Concretely, the structure of terms need not match that of derivations. Instead, one proves that terms provide a quotient of equivalent derivations, and that one can reason about proofs by induction on the term. As a consequence, translations between various proof systems are avoided: usual proof systems are expressible, and proof transformations can be performed internally. This asks for a rephrasing of standard focusing results. In the traditional termless approach to focusing inspired by Andreoli, the proof system is reduced to an algorithmic description of canonical forms, itself treated as a proof system. In our approach, focusing is stated internally, as properties providing a canonical description of normal forms. This approach is modular and self-contained, and allows us to state clearly and in full generality aspects that are sometimes omitted, such as the freedom in choosing the order of inversion, or the preservation of the interpretation in any model. The range of models is also relaxed. This talk is based on Section 6.4 to 7 of https://hal.inria.fr/hal-01528857.
Complete list of metadatas

https://hal.inria.fr/hal-01991571
Contributor : Guillaume Munch-Maccagnoni <>
Submitted on : Thursday, January 24, 2019 - 12:53:39 PM
Last modification on : Tuesday, March 26, 2019 - 9:25:22 AM

Identifiers

  • HAL Id : hal-01991571, version 1

Citation

Guillaume Munch-Maccagnoni. What term assignments can do for focusing. 4th International Workshop on Structures and Deduction (SD 2017), Sep 2017, Oxford, United Kingdom. ⟨hal-01991571⟩

Share

Metrics

Record views

35