In this paper we propose a new set of rules for a judgement calculus, i.e. a typed lambda calculus, based In Intuitionistic Linear Logic; these rules ease the problem of defining a suitable mathematical semantics. A proof of the canonical form theorem for this new system is given: it assures, beside the consistency of the calculus, the termination of the evaluation process of every well-typed element. The definition of the mathematical semantics and a completeness theorem, that turns out to be a representation theorem, follow. This semantics is the basis to obtain a semantics for the evaluation process of every well-typed program.

The judgement calculus for Intuitionistic Linear Logic: proof theory and semantics

VALENTINI, SILVIO
1992

Abstract

In this paper we propose a new set of rules for a judgement calculus, i.e. a typed lambda calculus, based In Intuitionistic Linear Logic; these rules ease the problem of defining a suitable mathematical semantics. A proof of the canonical form theorem for this new system is given: it assures, beside the consistency of the calculus, the termination of the evaluation process of every well-typed element. The definition of the mathematical semantics and a completeness theorem, that turns out to be a representation theorem, follow. This semantics is the basis to obtain a semantics for the evaluation process of every well-typed program.
File in questo prodotto:
Non ci sono file associati a questo prodotto.
Pubblicazioni consigliate

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: https://hdl.handle.net/11577/136813
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 6
  • ???jsp.display-item.citation.isi??? 2
social impact