Title: The birth of linear logic
Abstract:
Historically, linear logic has arisen as an outcome of
deep semantic analysis of computation
under the proofs-as-programs (Curry-Howard) paradigm.
Although its syntax is frequently referred to in the
substructural logic community,
its original motivations are rarely discussed.
To bridge a gap between the two communities, linear and substructural,
I will give an informal and personal account
to the birth of linear logic, not from a historical, but from
a conceptual point of view. In particular,
I will stress how
the key concepts of linear logic, such as
control of structural rules, decomposition of intuitionistic implication
and involutivity of negation, naturally arise in the context of
denotational semantics;
although linear logic looks rather artificial as a formalization of
reasoning, it is extremely natural in
the semantic understanding of computation.