Premium
THE JUDGEMENT CALCULUS FOR INTUITIONISTIC LINEAR LOGIC: PROOF THEORY AND SEMANTICS
Author(s) -
Valentini Silvio
Publication year - 1992
Publication title -
mathematical logic quarterly
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.473
H-Index - 28
eISSN - 1521-3870
pISSN - 0942-5616
DOI - 10.1002/malq.19920380105
Subject(s) - linear logic , calculus (dental) , normalisation by evaluation , simply typed lambda calculus , proof theory , gödel's completeness theorem , mathematics , typed lambda calculus , intuitionistic logic , proof calculus , algebra over a field , semantics (computer science) , completeness (order theory) , natural deduction , structural proof theory , curry–howard correspondence , discrete mathematics , operational semantics , lambda calculus , computer science , denotational semantics , programming language , mathematical proof , pure mathematics , medicine , mathematical analysis , geometry , dentistry
In this paper we propose a new set of rules for a judgement calculus, i.e. a typed lambda calculus, based on 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. 1991 MSC: 03B20, 03B40.