Linear Logic, we concisely write LL, has been introduced recently by Jean Yves Girard in Theoretical Computer Science 50 (1987). Born from the semantics of second order lambda calculus, LL is more expressive than traditional logic (both classical and intuiti0nistic), Due to the absence of structural rules and to a particular treatment of negation, which is denoted here by ±, proofs in LL do not have a "directional character". The constructive meaning of a proof of A--> B is a function mapping all proofs of A into proofs of B; in LL A---oB has a similar meaning, but B±---oA± represents the same formula and has the same proofs: so one of such proofs can map a proof of A into one of B as well as a proof of B± into one of A±. In this paper we are interested in the multiplicative second order subsystem LL* of linear logic; we introduce a calculus whose terms are canonical representations of proofs. The aim of the calculus is to give a better comprehension of the computational aspects of the process of cut-elimination. We prove that the calculus obeys strong normalization and the Church-Rosser properties.

A typed calculus based on a fragment of linear logic

SOLITRO, Ugo
1989

Abstract

Linear Logic, we concisely write LL, has been introduced recently by Jean Yves Girard in Theoretical Computer Science 50 (1987). Born from the semantics of second order lambda calculus, LL is more expressive than traditional logic (both classical and intuiti0nistic), Due to the absence of structural rules and to a particular treatment of negation, which is denoted here by ±, proofs in LL do not have a "directional character". The constructive meaning of a proof of A--> B is a function mapping all proofs of A into proofs of B; in LL A---oB has a similar meaning, but B±---oA± represents the same formula and has the same proofs: so one of such proofs can map a proof of A into one of B as well as a proof of B± into one of A±. In this paper we are interested in the multiplicative second order subsystem LL* of linear logic; we introduce a calculus whose terms are canonical representations of proofs. The aim of the calculus is to give a better comprehension of the computational aspects of the process of cut-elimination. We prove that the calculus obeys strong normalization and the Church-Rosser properties.
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/11562/17914
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? 4
social impact